tea.mathoverflow.net - Discussion Feed (How to prove Con(PA) in ZFC?)

thierryzell comments on "How to prove Con(PA) in ZFC?" (12316)

2011-01-02T06:43:56-08:00

This is really odd! It happens so often on MO that posters have to be sternly reminded to take their meta discussions here on Meta. Now here is an example of a discussion on Meta where most of the content would have been more at home on MO. :)

Kidding aside, it appears to me that beyond the research/non-research level issue, what makes or breaks a MO question (as in: what is likely to elicit interesting answers) is the care in framing a detailed question that goes to the heart of what needs to be clarified. In that respect, David's question is quite fertile, whereas the rather terse question he linked from was not. In that case, I don't think re-opening the original question would have been a good move: it would be much better to post an entirely new question.

David Speyer comments on "How to prove Con(PA) in ZFC?" (12262)

2010-12-28T07:05:35-08:00

Thanks for all the useful responses. The thing this has convinced me is that I should actually learn set theory systematically, rather than picking it up piecemeal in the course of reading webfora. In particular, I now realize that while I have heard people say "ordinary mathematical arguments can all be formalized in ZFC" many times, I haven't actually thought through how to do this in practice.

In particular, it was not clear to me why exhibiting a set which obeys the axioms of PA shows that ZFC proves Con(PA) but exhibiting a class (all sets) which obeys ZFC does not prove that ZFC proves Con(ZFC). You actually have to get into the weeds of how to formalize the "model implies consistent" argument to see why a model has to be a set.

Anyway, I'm spending my winter break looking at Smullyan and Fitting, so I will hopefully ask fewer basic set theory questions in the future.

Timothy Chow comments on "How to prove Con(PA) in ZFC?" (12252)

2010-12-27T21:21:05-08:00

As one of the people who voted to close this question, maybe I should say a bit more about why I judged it to be "too elementary." The answer to the mathematical question boils down to, "to prove that PA is consistent, you do what you always do to prove that some set of axioms is consistent: you exhibit a structure (namely, the natural numbers) and show that it satisfies all the axioms; this is an ordinary mathematical argument, and ordinary mathematical arguments can all be formalized in ZFC." Now, if you think that there's something fishy about this reasoning, because you think there's some illegitimate assumption about the definability of truth buried in there, then asking for clarification about that point is a fine MO question. But the question as posed struck me as demonstrating that the person asking the question hadn't made any attempt to think about it first. I might have been more lenient if I hadn't noticed that the person in question had made other contributions to MO that exhibited what seemed to me to be similar laziness.

Andres Caicedo comments on "How to prove Con(PA) in ZFC?" (12207)

2010-12-23T14:01:46-08:00

Though this has nothing to do with the question at hand, it may be worth pointing out that both ZFC and PA can define (for each n) "partial" truth predicates T_n that can handle all formulas in their language of complexity Sigma_n or lower. The fact that we cannot diagonalize and obtain a full truth predicate is essentially the same problem with recursive definitions Andreas mentions above.

WillieWong comments on "How to prove Con(PA) in ZFC?" (12200)

2010-12-23T09:36:48-08:00

@andrej: the hope is that by answering a few of those questions, you can help raise the general awareness of logic! Just because the bar is lower now doesn't mean the bar need to stay that low. I've always enjoyed reading yours and JDH's (and many others') answers in that direction.

andrejbauer comments on "How to prove Con(PA) in ZFC?" (12199)

2010-12-23T09:18:16-08:00

I agree with Noah, but there's a limit to how basic a question one should be able to ask. The limit is likely to be lower in logic than in algebra and analysis simply because the general level of knowledge in logic is lower than in algebra and analysis. Oh well, I suppose logicians will just have to live with it.

Kevin Walker comments on "How to prove Con(PA) in ZFC?" (12198)

2010-12-23T09:12:00-08:00

I agree with Noah. For me, the most useful thing about MO is the opportunity to ask questions which experts in fields other than my own can answer quickly and easily.

Noah Snyder comments on "How to prove Con(PA) in ZFC?" (12197)

2010-12-23T08:26:03-08:00

I don't have a strong opinion on this question, but when it looked like it might get closed I thought about starting a meta thread about whether we're setting the "research level" bar too high. I think it's good for MO to be a place where research mathematicians can ask questions about subjects that aren't in their field. Such questions will typically not be "research level" from the point of view of someone in the field, but I don't think that automatically means we should close them.

Andreas Blass comments on "How to prove Con(PA) in ZFC?" (12196)

2010-12-23T08:00:59-08:00

Just to confirm and slightly amplify Andrej's comments: In ZF, one can define truth in models whose underlying sets are genuinely sets; that includes the standard model of PA. One cannot (in general) define truth in "models" whose underlying "sets" are proper classes; in particular, one cannot define truth in the universe of all sets. (It is a nice exercise to dig into the definition for the set-sized situation and see what goes wrong in the class-sized situation. It has nothing much to do with "truth"; it's a problem with recursive definitions in general.)

Let me also mention, in connection with David's statement that "we would need to choose a Godel encoding of statements and proofs," that such a coding is needed only if we want to formulate Con(PA) as an arithmetical statement. If all we wanted was to prove, in ZF, that PA is consistent, we could just use the standard representations of sequences as sets (of ordered pairs), without any need to code them as numbers. I grant, however, that in the case at hand we might want an arithmetical coding, since the original question begins by mentioning that PA doesn't prove Con(PA), a fact that makes sense only when Con(PA) is an arithmetical statement.

andrejbauer comments on "How to prove Con(PA) in ZFC?" (12191)

2010-12-23T06:41:08-08:00

It is better to just think about the following: Goedel's completeness theorem is proved inside ZFC. In particular, nowhere in the proof do we have to rely on a truth predicate for ZFC. All we need is a predicate which expresses the fact "first-order statement $\phi$ in first-order language $L$ is valid in model $M$", and this is defined by induction on $\phi$.

Then your worries disappear. Since ZFC proves there is a model of PA, ZFC proves that PA is consistent by Goedel's completeness theorem.

andrejbauer comments on "How to prove Con(PA) in ZFC?" (12190)

2010-12-23T06:37:18-08:00

You are right that truth of ZFC statements is not definable in ZFC, but thruth of PA statements in $\omega$ is definable in ZFC.

David Speyer comments on "How to prove Con(PA) in ZFC?" (12189)

2010-12-23T06:06:05-08:00

I am looking at question http://mathoverflow.net/questions/50173 . I am not exactly saying this should be re-opened. However, the answer seems less obvious to me than it does to the closers.

As many people have explained, ZF proves that PA has a model. More precisely, ZF proves that there is a set omega and a function S:omega --> omega such that S obeys the first 4 Peano axioms and such that, if X is a subset of omega containing 0 and closed under S then X=omega. I am fine with how to prove all of this.

We therefore have the following meta-theorem. If phi is any property then ZF proves the statement "If phi(0) and if, for all k in omega, phi(k) implies phi(k+1), then phi(n) holds for all n in omega.".

Now, we would like to establish that ZF proves Con(PA). That means we need to chose a Godel encoding of statements and proofs in PA, and show that the following is a theorem of ZF "For any statement T of PA, and any proof P, if P is a proof of T, then T is not "0 \neq 0.".". The obviously plan of proof is to prove, by induction on the length of P, the more precise statement: "For any statement T of PA, and any proof P, if P is a proof of T, then P is true of omega."

But this seems to run directly into the problem that truth is not definable! http://planetmath.org/encyclopedia/TarskisResultOnTheUndefinabilityOfTruth.html

I even run into a problem dealing with the axioms of PA. For any property phi, I can prove that the following is a theorem of ZF "If phi(0) and if, for k in omega, phi(k) implies phi(Sk), then phi(n) for all n in omega." But I can't even see how to express in ZF the statement: "For every property phi, if phi(0) and if, for k in omega, phi(k) implies phi(Sk), then phi(n) for all n in omega." Again, I seem to need a truth predicate.

I'm sure there is a standard way around this, but what is it? And is that question sophisticated enough to ask on MO?