Skip to main content
30 votes

Can proof by contradiction work without the law of excluded middle?

You asked (I am making your question a bit crisper): "What formal guarantee is there that it cannot happen that both $\lnot p$ and $p$ lead to a contradiction?" You seem to worry that if logic is ...
Andrej Bauer's user avatar
  • 30.9k
17 votes
Accepted

Why does soundness imply consistency?

I recommend looking into formal logic beyond vague, hand-wavy descriptions. It's interesting and highly relevant to computer science. Unfortunately, the terminology and narrow focus of even textbooks ...
Derek Elkins left SE's user avatar
12 votes

What are the conditions necessary for a programming language to have no undefined behavior?

First off, let's be clear on what "undefined behaviour" is. In just C alone (and this is the understanding inherited by C++), there are two possible meanings, depending on which version of ...
Pseudonym's user avatar
  • 22.3k
11 votes

Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

No, it doesn't require that. These are two orthogonal issues. You can easily define a new programming language where you provide fully defined semantics for all operations; yet it can be Turing ...
D.W.'s user avatar
  • 162k
8 votes

What are the conditions necessary for a programming language to have no undefined behavior?

The C language may say "if you do X, then whatever the result is, is not a violation of the C Standard". "Whatever the result is" can include the result that you hoped for, some ...
gnasher729's user avatar
  • 30.7k
8 votes

Is Goedel's 1st theorem not algorithmically derivable?

Your reasoning is incorrect. It is true that your hypothetical "proof deriver" cannot derive all true statements. No proof derivation system can, and indeed, it is not even possible to express the ...
cody's user avatar
  • 8,233
7 votes

Can proof by contradiction work without the law of excluded middle?

I think your question boils down to "when doing formal verification with some sort of formal logic, what sort of guarantee do I have that the logic is consistent?". And the answer is: none. That's ...
D.W.'s user avatar
  • 162k
6 votes

Did Wheeler really believe that physics was undecidable?

The inference "the universe would be completely computable, so no undecidable/uncomputable things could exist" is invalid. In the effective topos, where everything is computable, there are many ...
Andrej Bauer's user avatar
  • 30.9k
5 votes
Accepted

What are the conditions necessary for a programming language to have no undefined behavior?

The problem of statically detecting undefined behavior has nothing to do with undefinedness as such. It's just impossible to prove in general that programs in a Turing-complete language will do ...
benrg's user avatar
  • 2,157
5 votes

Analogy between Gödel's incompleteness proof and Richard's argument

Both examples are instances of diagonalization, a technique also used to prove Cantor's theorem ($\kappa < 2^\kappa$ for all cardinals $\kappa$) and Turing's theorem that the halting problem is ...
Yuval Filmus's user avatar
4 votes
Accepted

Does Gödel's first incompleteness theorem apply to quantifier-free arithmetics?

What you are referring to is called Baby Arithmetic ($\mathsf{BA}$) in Peter Smith's book An introduction to Gödel's Theorems. $\mathsf{BA}$'s language [has] one single individual constant $0$, the ...
Pål GD's user avatar
  • 16.7k
4 votes
Accepted

Does godel's incompleteness theorem still hold if we have a TM that can do an infinity amount of computations?

There is some ambiguity in how to define these new machines, essentially based on the question whether we can nest the "bursts of doing infinitely many steps in some finite time" or not. In the ...
Arno's user avatar
  • 3,183
4 votes

Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

Your intuition is incorrect. The analogies you're trying to draw are not there, even though it's understandable you would expect them. Programming languages can be defined as formal systems, but they ...
Andrej Bauer's user avatar
  • 30.9k
4 votes

What are the conditions necessary for a programming language to have no undefined behavior?

So my question now is, what conditions need to be imposed on a Turing complete language in order to guarantee that all possible programs written in the language will have fully defined behavior ...
yeputons's user avatar
  • 256
3 votes

What are the conditions necessary for a programming language to have no undefined behavior?

Lets look at a sample program ...
QuadmasterXLII's user avatar
3 votes

Why does soundness imply consistency?

Soundness and consistency are properties of deductive systems. Soundness can only be defined with respect to some semantics that is assumed to be given independently from the deductive system. In ...
Dima Chubarov's user avatar
3 votes

Is there any concrete relation between Gödel's incompleteness theorem, the halting problem and universal Turing machines?

A slightly weaker form of Gödel's first incompleteness theorem can be derived from the undecidability of the Halting problem with a short proof. The full incompleteness theorems also have a short ...
Julius Kunze's user avatar
3 votes

What are the conditions necessary for a programming language to have no undefined behavior?

Starting from the C/C++ languages, ruling out all undefined behavior would be very hard. But if you're designing a language from scratch, it's not difficult at all to rule out undefined behavior. Many ...
Glenn Willen's user avatar
2 votes

Is Goedel's 1st theorem not algorithmically derivable?

Our proof deriver enumerates all possible axiomatic systems But the set of possible axiomatic systems also include the inconsistent systems. On the other hand, the consistent axiomatic systems are ...
Thomas Klimpel's user avatar
2 votes

Why does soundness imply consistency?

Your proof system is neither sound nor consistent, since $A$ is not a true proposition unless $A \equiv \top$, In which case $\lnot A \equiv \bot$ is not a true proposition. This argument shows that ...
Yuval Filmus's user avatar
2 votes

Caroll's paradox => Rice theorem?

Well, any true statement implies every other true statement, so in that vacuous sense, I suppose one implies the other. But no, I wouldn't say that Carroll's paradox implies Rice's theorem in any ...
D.W.'s user avatar
  • 162k
2 votes

Why does soundness imply consistency?

Often when we come up with logical systems, they are motivated by an attempt to describe a pre-existing phenomenon. For example, Peano arithmetic is an attempt to axiomatize the natural numbers along ...
Ben Millwood's user avatar
2 votes

Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

The incompleteness theorem only applies to formal systems that can express a certain amount of arithmetic. In particular, they have to support statements of the form $\forall n\in\mathbb N. P(n)$, ...
benrg's user avatar
  • 2,157
2 votes
Accepted

Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem

We know from deduction theorem that $(\vdash q\rightarrow\vdash p)\iff (\vdash p\rightarrow q)$ This is false. If $\not\vdash q$ then the clause $(\vdash q)\rightarrow(\vdash p)$ (re-parenthesized ...
Noah Schweber's user avatar
1 vote

Self-referential systems cannot predict their future behaviour? (reference request)

I'm not going to watch or engage with the video but to answer your question, it is possible for a self-referencing program to make statements about its own behaviour. Fix an encoding of programs. ...
Sam Ezeh's user avatar
  • 131
1 vote

Many-one reductions between the set of true sentences and a particular arithmetical set

For any such $X$ we have $X\le_mTh(\mathbb{N})$ but not conversely (and in fact $Th(\mathbb{N})$ is vastly more complicated than $X$). To see that $X\le_mTh(\mathbb{N})$, we want to translate a ...
Noah Schweber's user avatar
1 vote

Relation between "undecidability of arithmetic" and "godel's incompleteness theorem"?

Yes, if we know that $Th(\mathcal{N})$ is undecidable then we know that it is not computably axiomatizable, and in particular we know that no computably axiomatizable theory consisting only of true ...
Noah Schweber's user avatar
1 vote

Can proof by contradiction work without the law of excluded middle?

When used to guarantee the truth of a formal statement, all proofs implicitly assume the consistency of the system that they're based in. This is because if the system is inconsistent, the entirety of ...
Alecto Irene Perez's user avatar
1 vote

Why does soundness imply consistency?

To have a concise (and intuitive) answer I will paraphrase what Scott Aaronson said in his 6.045/18.400 MIT lecture. He said something like this: Soundness means everything provable is true. Since ...
Charlie Parker's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible