| > Question: Can a sentence be provably true in one arithmetic system but not another? The answer is yes! ZFC |- AC
but ZF |/- AC
and both ZFC and ZF can encode arithmetic.But there's an issue here: no-one really talks about the "truth" of the Axiom of Choice as though it's a concrete thing: it's a very controversial axiom, and although most mathematicians accept it, quite a few don't. Constructivist mathematicians don't accept it, and it's provably equivalent to the law of the excluded middle, so it can't be used in intuitionistic logics. Now you might counter and say that AC isn't the Gödel sentence for ZFC, and the Gödel sentence for PA is true in the intended model. But that's a different matter from whether it's provable from an axiomatic foundation. The reason I think this matters is because mathematicians work with proofs! Most mathematicians aren't working in foundations, and rely on proofs to the extent that they don't even consider the truth of statements which cannot be proven. > If so that means there are provably true sentences which exist, but not provably true with the axioms that I have at my disposal right now? The issue is that provability is completely contingent on the set of axioms you use: provability isn't a universal notion. Of course if you add something which is unprovable (such as the Gödel sentence) to PA, you get a new system which can prove more things: but this system has its own unprovable Gödel sentence. I'd also question what you mean by "provably true": a sentence is provable from a theory when there exists a derivation in some proof calculus of the sentence starting from the axioms of the theory. "True" is much harder to pin down, and we wouldn't usually say "provably true". "True" can mean "true in the intended model", "true in all models", or even just "provable from a set of axioms". The Gödel sentence is "true but unprovable" only in the sense that it is true in the intended model: it is not a tautology. I think most people who have had a brief exposure to mathematics would consider "true in all models" (i.e. tautological truth) to be what is meant by "true", so I don't like it being used to mean "true in the intended model" without qualification. |