An infinitely long proof is not a proof, since proofs are finite by definition.
The truth value of a statement does not depend on the existence of a proof anyways, the definition of truth is that it holds in any model. It is just a corollary of Goedel’s completeness theorem that syntactic truth (existence of a (finite) proof) coincides with semantic truth if the axiom system satisfies certain assumptions.
With that definition of truth, a Goedel sentence is not “true”, because there are models in which it fails to hold; neither is its negation “true”, because there are models in which it does. But that’s not the only way in which the word “true” is used about mathematical statements (though perhaps it should be); many people are quite sure that (e.g.) a Goedel sentence for their favourite formalization of arithmetic is either true or false (and by the latter they mean not-true). There’s plenty of reason to be skeptical about the sort of Platonism that would guarantee that every statement in the language of (say) Principia Mathematica or ZF is “really” true or false, but it hardly seems reasonable to declare it wrong by definition as you’re doing here.
many people are quite sure that (e.g.) a Goedel sentence for their favourite formalization of arithmetic is either true or false (and by the latter they mean not-true).
Those people seem a bit silly, then. If you say “The Godel sentence (G) is true of the smallest model (i.e. the standard model) of first-order Peano Arithmetic (PA)” then this truth follows from G being unprovable: if there were a proof of G in the smallest model, there would be a proof of G in all models, and if there were a proof of G in all models, then by Godel’s completeness theorem G would be provable in PA. To insist that the Godel sentence is true in PA—that it is true wherever the axioms of PA are true—rather than being only “true in the smallest model of PA”—is just factually wrong, flat wrong as math.
The people I’m thinking of—I was one of them, once—would not say either “G is true in PA” or “G is true in such-and-such a model of PA”. They would say, simply, “G is true”, and by that they would mean that what G says about the natural numbers is true about the natural numbers—you know, the actual, real, natural numbers. And they would react with some impatience to the idea that “the actual, real, natural numbers” might not be a clearly defined notion, or that statements about them might not have a well-defined truth value in the real world.
I think most people who know Goedel’s theorem say “G is true” and are “unreflective platonists,” by which I mean that they act like the natural numbers really exist, etc, but if you pushed them on it, they’d admit the doubt of your last couple of sentences.
Similarly, most people (eg, everyone on this thread), state Goedel’s completeness theorem platonically: a statement is provable if it is true in every model. That doesn’t make sense without models having some platonic existence. (yes, you can talk about internal models, but people don’t.) I suppose you could take the platonic position that all models exist without believing that it is possible to single out the special model. (Eliezer referred to “the minimal model”; does that work?)
You are right: you may come up with another consistent way of defining truth.
However, my comment was a reaction to silas’s comment, in which he seemed to confuse the notion syntactic and semantic truth, taking provability as the primary criterion. I just pointed out that even undergraduate logic courses treat semantic truth as basis and syntactic truth enters the picture as a consequence.
An infinitely long proof is not a proof, since proofs are finite by definition.
The truth value of a statement does not depend on the existence of a proof anyways, the definition of truth is that it holds in any model. It is just a corollary of Goedel’s completeness theorem that syntactic truth (existence of a (finite) proof) coincides with semantic truth if the axiom system satisfies certain assumptions.
With that definition of truth, a Goedel sentence is not “true”, because there are models in which it fails to hold; neither is its negation “true”, because there are models in which it does. But that’s not the only way in which the word “true” is used about mathematical statements (though perhaps it should be); many people are quite sure that (e.g.) a Goedel sentence for their favourite formalization of arithmetic is either true or false (and by the latter they mean not-true). There’s plenty of reason to be skeptical about the sort of Platonism that would guarantee that every statement in the language of (say) Principia Mathematica or ZF is “really” true or false, but it hardly seems reasonable to declare it wrong by definition as you’re doing here.
Those people seem a bit silly, then. If you say “The Godel sentence (G) is true of the smallest model (i.e. the standard model) of first-order Peano Arithmetic (PA)” then this truth follows from G being unprovable: if there were a proof of G in the smallest model, there would be a proof of G in all models, and if there were a proof of G in all models, then by Godel’s completeness theorem G would be provable in PA. To insist that the Godel sentence is true in PA—that it is true wherever the axioms of PA are true—rather than being only “true in the smallest model of PA”—is just factually wrong, flat wrong as math.
This thread needs a link to Tarski’s undefinability theorem.
Also, you’re assuming the consistency of PA.
The people I’m thinking of—I was one of them, once—would not say either “G is true in PA” or “G is true in such-and-such a model of PA”. They would say, simply, “G is true”, and by that they would mean that what G says about the natural numbers is true about the natural numbers—you know, the actual, real, natural numbers. And they would react with some impatience to the idea that “the actual, real, natural numbers” might not be a clearly defined notion, or that statements about them might not have a well-defined truth value in the real world.
In other words, Platonists.
I think most people who know Goedel’s theorem say “G is true” and are “unreflective platonists,” by which I mean that they act like the natural numbers really exist, etc, but if you pushed them on it, they’d admit the doubt of your last couple of sentences.
Similarly, most people (eg, everyone on this thread), state Goedel’s completeness theorem platonically: a statement is provable if it is true in every model. That doesn’t make sense without models having some platonic existence. (yes, you can talk about internal models, but people don’t.) I suppose you could take the platonic position that all models exist without believing that it is possible to single out the special model. (Eliezer referred to “the minimal model”; does that work?)
You are right: you may come up with another consistent way of defining truth.
However, my comment was a reaction to silas’s comment, in which he seemed to confuse the notion syntactic and semantic truth, taking provability as the primary criterion. I just pointed out that even undergraduate logic courses treat semantic truth as basis and syntactic truth enters the picture as a consequence.