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 ...
- 30k
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 ...
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 ...
- 21.6k
10
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.♦
- 156k
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 ...
- 8,089
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 ...
- 28.3k
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.♦
- 156k
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 ...
- 30k
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 ...
- 2,091
5
votes
Accepted
Understanding of Turing's Answer to the Entscheidungsproblem
What Gödel showed is that there is no finite first-order axiomatization of the theory of the natural numbers. What this means is that if you give a finite list of first-order axioms and schemas, then ...
- 275k
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 ...
- 275k
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 ...
- 15.5k
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 ...
- 2,683
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 ...
- 256
3
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 ...
- 30k
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 ...
- 1,409
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 ...
- 131
3
votes
What are the conditions necessary for a programming language to have no undefined behavior?
Lets look at a sample program
...
- 131
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 ...
- 131
2
votes
Is there a decidable problem which has a proof that it cannot be proved to have a particular deciding Turing machine?
Let us examine the following language:
$x\in L \iff ZFC \hspace{1mm} \text{is consistent}$.
Clearly, $L$ is decidable, and is decided by either the constant 1 or 0 machines.
Proofs from ZFC for the ...
- 13.3k
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 ...
- 5,382
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 ...
- 275k
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)$, ...
- 2,091
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.♦
- 156k
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 ...
- 2,713
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 ...
- 530
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. ...
- 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 ...
- 2,713
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 ...
- 2,713
Only top scored, non community-wiki answers of a minimum length are eligible