A comprehensive article describing the fundamental notions of computability and truth annotated with opinions on types and proofs.
A comprehensive article describing the fundamental notions of computability and truth annotated with opinions on types and proofs.
This is a conceptual mistake. For starters, the notion of “everything that’s true” isn’t well-defined. Are we talking about truth in a theory, or truth in some specific model?
As furia-krucha said in a comment, Gödel’s completeness theorem says that a statement in a first-order theory is provable (i.e. a theorem) iff it holds in every model of the theory. For example, if a statement in the language of groups is neither provable nor refutable, there exist groups where the statement holds, as well as groups where the statement doesn’t hold.
Gödel’s first incompleteness theorem then says that every effectively axiomatized first-order theory (i.e., whose theorems can be enumerated) contains statements that are neither provable nor refutable. It says nothing about the “actual truth” of said statements. They are true in some models, false in others. Heck, they remain neither provable nor refutable in some models!
I am considering this: a theory is defined to be the set of statements that are provable by the axioms and deduction rules of said theory. So “a first-order theory contains statements that are neither provable nor refutable,” makes no sense to me.
What do you mean by “actual truth”? A theory is merely a language; within it we say things, which we are supposed to believe to be true. If a theory is unsound, then you can say something in the theory that is not “actually true”, and conversely if a theory is sound then every expression that can be proved must be “actually true”. So, a theory says at least something about “actual truth” of statements, namely that if we believe a theory to be sound then we believe every provable statement to be true.
Sometimes you have reasons to believe a theory to be unsound, namely if you can find one counter-example of a statement that is provable, but which you know to be false.
“Heck, they remain neither provable nor refutable in some models!” I don’t understand you here; how can you prove something in a model, if a model is just a way of expressing what is true, viz. a semantics? Models don’t necessarily have an associated proof theory; they are simply constructions which we believe characterize certain real-world elements. Only for sound and complete axiomatizations is it the case that we have that all models correspond to a statement in its (sound and complete) proof theory. But Gödel here argues that no such complete proof theory exists for sufficiently powerful axiomatizations.
Coming back to the original quote: “in essence, either it can’t prove everything that’s true, or it can prove things that aren’t true.”
I believe that this correct. I read “it can’t prove everything that’s true” as simply meaning “there exists something that is true which it cannot prove”, as a counter-example to the universal quantification, and to me that is incompleteness.
As his theorem is a basic diagonalization theorem, I expect this to be of equal value as: “a Turing machine either can’t prove that it halts, or it has incorrect proofs,” which is basically the Halting theorem: it is undecidable by a Turing machine whether some other Turing machine halts on a given input.
Do you agree or is this just nonsense?
Errr, sorry. What I mean is: You have a theory T defined using a language L. If T is both consistent and sufficiently powerful, then L must contain statements that are neither provable nor refutable in T.
I’m not supposed to “believe” anything. I’m supposed to use it to prove things. If I’m given an inconsistent theory, I can prove contradictory statements, and that’s all there is to it.
I disagree with the notion of “actual truth” to begin with, at least as something mathematics should be concerned with. Provability offers a compelling, very concrete alternative, as it can be computably verified, if we are careful about how define our theories. Truth is best left to philosophers.
Whether there exist models of mathematical theories “in the real world” doesn’t really concern me. For me, a model must itself be a mathematical object, for example, a group is a model of the theory of a group, and a category of group objects is a model of the theory of groups (as entities that interact with one another).
Why do you assert that unprovable statements in a theory are true, if there exist models of the theory in which they are false?
I agree with you, in principle. However, I also consider that it is in general undecidable whether a given first-order theory is consistent. Therefore, if you give me a random theory, I have no other choice than to believe.
Very good point; some logicians also prefer provability over truth. But we simply shift our focus here, from “that is true in the real-world” to “that can be computed in the real-world”, both of which are still left to philosophers: simply stated, computability still suffers from the assumption of the Church-Turing thesis.
What you say about verifiability, is also quite subtle: the “carefulness” in the definition of theories probably means that we need a decidable theory. Hence, theories not “sufficiently powerful”.
Sorry for my vague meaning, but with “real-world elements” I, indeed, also mean mathematical constructions. However, it also includes the objects for which mathematics not yet has adequate characterizations.
Not sure. What is a model of a theory? To me that sounds like a proof object. For example, groups are a model of group theory, and groups themselves are proof terms of said theory. If your definition of “truth” is exactly the same as your theory, then, indeed, you are right: in terms of programming it means “all its bugs are its features.”
But to me that feels not right: a theory is true until you encounter a sentence which it proves but to which you not agree. Similarly, Brouwer felt that “the law of excluded middle” is somehow not “actually true,” and started developing Constructive Logic. There are similar reasons for the existence of Linear Logic, which basically amounts to not believing that you can apply a certain term (think: proof of some lemma) indefinitely often.
I think another approach of viewing Gödel’s incompleteness theorem is as follows:
We know that certain languages, say Peano arithmetic, can “realize” certain theories. That means, within the axiomatic system of Peano arithmetic, we can encode a proof theory that expresses certain truths. This “embedding” is also known from constructive first-order logic, where we can perform double negation translation of any classical sentence and find a constructive sentence that is true if and only if the classical sentence is true.
Now consider a system that is self-embeddable, that is: we know that every statement can be encoded into the object-level of the language and we can prove that this is a correct realization. Now, if we analyse the statement something along the lines of a Liar paradox: “I am not provable”. If the statement is true and the system is complete, it means that there exists a proof. We now encode the proof into the object-level, i.e. by realizing the proof into the system itself, call this the number G. Then we construct a new statement: “G is not provable”. Clearly this is not true, since as counter-example we can point to the proof G itself. However, “I am not provable” is true, but “G is not provable” is false: contradiction, hence the system cannot be complete.
And this last paragraph is the “basic diagonalization” which I mentioned last time: feeding the system into itself. It is the same trick that is used by Cantor to show that the Reals are larger than the Rationals. If you think Gödel’s Incompleteness Theorem is false, then you must also believe that the Reals are equally large as the Rationals!
You don’t need to “believe” in a theory to use it.
It isn’t clear to me what you mean by a theory being “true”. For me, all that a theory can aspire to be is “useful”, and that ultimately depends on your purposes. Programming has uses for inconsistent theories (such as most type systems, when viewed as logics), and I wouldn’t be surprised if so did physics.
I’m aware. In fact, in my original comment, I was going to say something along the lines of “Arithmetic is very powerful. If mathematical induction is available to you, you can define more general inductive structures, such as the syntax and (proof-theoretic) semantics of first-order logic…”, but then I forgot how I was going to relate that to the original topic, so I dropped it.
Of course, I don’t think Gödel’s incompleteness theorem is false. I just disagree that you can extract any conclusions about “truth” from it, because “truth” is extra-mathematical.
I see now what you mean, by “conceptual mistake”. By soundness and completeness, a statement is provable if and only if the statement is true in every model. If a statement is unprovable, there exists some model in which the statement is false. So it can not be the case that an unprovable statement is true.
I think both the author of the original post and I have mixed up the two notions of completeness here:
Just reading this topic from a while back. Thank you for this discussion, really wonderful to read back!