Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: general

Topic: Consistency proofs

John Baez (Oct 15 2020 at 21:34):

Fun question raised by my old college pal Bruce Smith:

I read somewhere that PA can prove that ZF can prove that PA is consistent. Do you agree?

I think the answer must be yes.

John Baez (Oct 15 2020 at 22:00):

If so, it's like "Maybe I can't prove that what I'm saying is right, but I can prove that my big brother can prove it."

John Baez (Oct 15 2020 at 22:03):

(Where I'm sloppily translating "consistent" as "right".)

Fawzi Hreiki (Oct 15 2020 at 22:28):

Is this in general true for any two theories one of which contains the other?

Dan Doel (Oct 15 2020 at 22:35):

I think it's a relatively reasonable expectation in a lot of situations. If you can prove by hand that ZF proves PA consistent, PA should be good enough to represent your by hand proof.

Dan Doel (Oct 15 2020 at 22:36):

And I think that's the right analogy.

Dan Doel (Oct 15 2020 at 22:37):

So, probably much weaker systems than PA can prove that ZF proves PA consistent.

John Baez (Oct 15 2020 at 22:50):

Fawzi Hreiki said:

Is this in general true for any two theories one of which contains the other?

No, not in general. For example PA contains itself and we can't get a result like this in that case (as long as PA is consistent).

We are using a couple of things here:

• PA is strong enough that we can use it to formalize and prove things about the concept of "proof given some finite system of axioms" - or more generally, "proof given some system of axioms that a computer program could list".

• ZF is strong enough that it can prove the consistency of PA.

John Baez (Oct 15 2020 at 22:54):

Dan Doel said:

So, probably much weaker systems than PA can prove that ZF proves PA consistent.

Yes, it would be fun to find a fairly weak one. Also much weaker systems than ZF can prove PA consistent.

Dan Doel (Oct 15 2020 at 22:56):

Like PA+Con(PA) :)

John Baez (Oct 15 2020 at 22:56):

Cheater.

Dan Doel (Oct 15 2020 at 22:57):

Of course, that looks a lot simpler than it actually is to write down, I imagine.

John Baez (Oct 15 2020 at 22:57):

Yes, I should have challenged you to write Con(PA) in the language of PA.

Dan Doel (Oct 15 2020 at 22:57):

No thanks.

Fawzi Hreiki (Oct 15 2020 at 23:23):

Ah of course, I should have prefaced that I meant 'properly contains'. To make this more precise, suppose you have two first-order theories $T_1$ and $T_2$ such that:

• $T_1$ is at least as strong as PA.
• $T_2$ proves that a model of $T_1$ exists (or equivalently, $T_2$ proves that $T_1$ is consistent).

Then does $T_1$ prove that $T_2$ proves Con($T_1$)?

Todd Trimble (Oct 16 2020 at 01:53):

John Baez said:

If so, it's like "Maybe I can't prove that what I'm saying is right, but I can prove that my big brother can prove it."

Assuming whatever my big brother says. He's prone to making bolder claims than I make.

André Beuckelmann (Oct 16 2020 at 08:59):

@Fawzi Hreiki Kind of. For this to work properly, you also want to require $T_2$ to be recursively enumerable. Otherwise, $T_1$ might not be able to represent it (for example, if you have uncountably many axioms, PA could not encode that) - it could still represent the proof, though, as it can make use of only finitely many of the axioms, it just wouldn't be able to say that this is a proof in $T_2$.

André Beuckelmann (Oct 16 2020 at 09:12):

Dan Doel said:

Like PA+Con(PA) :)

For a fairer answer, $PA+\varepsilon_0\text{ is well-ordered}$ works, by Gentzen's proof (this also looks quite horrible, if you were to actually write out what $\varepsilon_0$ being well ordered means in $PA$). Similarly, PA, together with Goodstein's theorem or Paris-Harrington, should work.

André Beuckelmann (Oct 16 2020 at 09:28):

Dan Doel said:

So, probably much weaker systems than PA can prove that ZF proves PA consistent.

Robinson's Q is probably one of the the weakest ones that work, here. Of course, you can do something simpler, if you also allow stupid answers (in PA, the prove that ZF proves that PA is consistent requires only finitely many numbers, so we can replace all our function symbols with relations and use the complete theory of those numbers).

Dan Doel (Oct 16 2020 at 13:10):

Well, I was wondering about something like that, although less contrived. Like, can you get away with something extra weak because you only need to represent a particular proof, not arbitrary proofs?

John Baez (Oct 16 2020 at 14:55):

Fawzi Hreiki said:

Ah of course, I should have prefaced that I meant 'properly contains'. To make this more precise, suppose you have two first-order theories $T_1$ and $T_2$ such that:

• $T_1$ is at least as strong as PA.
• $T_2$ proves that a model of $T_1$ exists (or equivalently, $T_2$ proves that $T_1$ is consistent).

Then does $T_1$ prove that $T_2$ proves Con($T_1$)?

John Baez (Oct 16 2020 at 14:59):

That sounds correct if also $T_2$ is finitely axiomatizable, or more generally recursively axiomatizable. You're assuming $T_2$ proves $\mathrm{Con}(T_1)$:

$T_2 \vdash \mathrm{Con}(T_1)$

Since $T_1$ is at least as strong as PA and $T_2$ is recursively axiomatizable we can write down a "provability predicate" $P$ such that any sentence $\phi$ is provable in $T_2$ iff $P(\ulcorner \phi \urcorner)$, where $\ulcorner \phi \urcorner$ is the Goedel number of $\phi$:

$(T_2 \vdash \phi ) \iff (T_1 \vdash P(\ulcorner \phi \urcorner))$

From these facts we conclude

$T_1 \vdash P(\ulcorner \mathrm{Con}(T_1) \urcorner)$

Nikolaj Kuntner (Oct 16 2020 at 15:59):

@André Beuckelmann Regarding the +eps_0 issue, I'm involved in a related question in another forum of intellectuals, and the issue came up about the definition of ordinals. Are ordinals a set theoretical concept? The answer might be formally yes if we go with the definition that ordinal just means well-ordered (well-founded trichotomous transitive) set. But then it seems like we're sloppy to say "Gentzens proof yadda yadda PA+ordinal up to epslon_0", since we actually speak about PRA expressions of some order type. How do we conceptualize order type without ever touching any set theory axiom? Is it just that ordinals (the sets) capture all things that can have the same order type as some other expression? To ask the first question differently, are ordinals morally a set theoretical concept? Would the claim about Gentzens result be better expressed as speaking explicitly about how it involves the structures/tree of PA proofs which happen to have the same order type as the structures/tree of the PRA expressions in question?
I'm a bit confused about "ordinal" in this context.

Oscar Cunningham (Oct 16 2020 at 16:12):

One interesting fact is that most proofs that are seemingly set-theoretic can be reduced to not mention sets at all. For example Gödel/Cohen's proofs that the consistency of ZF implies the consistency of ZFC/ZF¬C. Both proofs work by using the completeness theorem to say that if ZF is consistent then it has a model $V$. Then they manipulate $V$ to produce a model $V^*$ in which choice does/doesn't hold. Then since ZFC/ZF¬C has a model, it is consistent.

The interesting thing is that both these proofs have now been given in PA. That is, $\sf{PA}\vdash\mathrm{Con}(\sf{ZF})\to\mathrm{Con}(\sf{ZFC})$ and $\sf{PA}\vdash\mathrm{Con}(\sf{ZF})\to\mathrm{Con}(\sf{ZF¬C})$. This is the despite the fact that there is absolutely no way to phrase the idea 'model of ZF' in PA!

André Beuckelmann (Oct 16 2020 at 16:26):

@Nikolaj Kuntner Yes, I guess speaking about trees might be more illuminating. If I remember correctly, Gentzen's proof essentially works as follows: he formulates a proof system for proofs in PA and, for most of the steps allowed in proofs, it is quite easy to see that they cannot produce any contradictions. The exception, here, is the cut rule, so he shows that one can get rid of this rule by manipulating the proof (which can be expressed as trees) using some procedure, and $\varepsilon_0$ being well ordered is only used to show that this procedure terminates: we label the trees in some way (by ordinals less than $\varepsilon_0$), such that we get a decreasing sequence of ordinals, which, thus, has to terminate.

As to what $\varepsilon_0$ being well ordered actually means in PA$ The ordinals below $\varepsilon_0$ are all of a particular form, they are the ordinals you can get to in finitely many steps by applying $0, +,$ or $\omega^\bullet$. Thus, we can encode every such ordinal by a natural number (and we can determine whether one code represents a larger ordinal than another). Thus, we can meaningfully ask, whether or not we can do transfinite induction using those codes.
Whilst ordinals themselves are sort of set theoretic, when it comes to those kind of results as "some ordinal implies the consistency of some theory", we are not actually talking about the ordinals themselves, but only such codings: To any nice theory that can interpret PA, we can assign a recursive ordinal (i.e. one whose elements can be coded in a computable way) which is the smallest one, such that the theory cannot prove that transfinite induction holds for those encodings, which we call its proof theoretic ordinal - so, despite ZFC being able to construct huge (recursive) ordinals, it does not actually prove that they, when encoded using natural numbers, are well-ordered.

Nikolaj Kuntner (Oct 16 2020 at 17:02):

The ordinals encoded by natural numbers are all below $\omega_1$, so I don't follow that last sentence. Can you elaborate on it? About which objects, formally, is the statement that the theory ZFC does not have a proof that they are well-ordered?

Dan Doel (Oct 16 2020 at 17:16):

Since the proof theoretic ordinal is defined to be a recursive ordinal, it's below $ω^{CK}_1$ even (the Church-Kleene ordinal, which is below $ω_1$).

Nikolaj Kuntner (Oct 16 2020 at 17:56):

Isn't the encoding of countable ordinals straight forward in ZF and transfinite induction holds on them?

John Baez (Oct 16 2020 at 17:57):

@Nikolaj Kuntner - Andre was talking about Ordinal analysis. Each theory like ZFC or PA has some smallest countable ordinal that it cannot prove well-founded. For ZFC this ordinal is so huge that nobody understands it. For PA it's $\varepsilon_0$. At the link you can see other examples listed.

Nikolaj Kuntner (Oct 16 2020 at 18:01):

I have interpreted the encoded phrase to be about the ordinals themselves, when really it's really (at least) about the order relation for them.

Dan Doel (Oct 16 2020 at 18:03):

I think it might be best to think of ordinals as actually being about the relation. The carrier is incidental.

Nikolaj Kuntner (Oct 16 2020 at 18:05):

What's confusing is that if $\omega_1$ is something small for ZFC and at the same time it's the object containing all countable ordinals, then the relation (where for a relation on $X$ I'm thinking of $\subset X\times X$) that encodes how all countable ordinals relate to each other intuitively also seems at least smaller than, say $\omega_1^{\omega_1}$. Which is itself smaller or equal to ${\mathbb R}\to {\mathbb R}$, so not big as far as ZFC is concerned.

John Baez (Oct 16 2020 at 18:07):

I think you should read a bit of the Wikipedia article on ordinal analysis and follow the links that discuss Kleene's O and ordinal notation.

John Baez (Oct 16 2020 at 18:08):

Any axiom system is only able to provide a notation for all ordinals $\lt \alpha$ for some countable $\alpha$.

Nikolaj Kuntner (Oct 16 2020 at 18:24):

Okay, I never dared to look into Kleene's O and notation. Given the recursive nature, the "relation" seems to demand more than just something along the lines of a cartesian product.
This topic always seems vast when I come across it. Maybe I haven't found a finite encoding of grid points of this theory to be able to save it in my head. Same with fixed points of large cardinals btw.

John Baez (Oct 16 2020 at 18:56):

I'm not an expert on this stuff. The details are complicated but we can imagine what it means to have a notation system for countable ordinals $\lt \alpha$. It basically means that we have "names" for these ordinals, written out in some formal language, and a way to prove, for each distinct pair of these names, which ordinal is smaller.

John Baez (Oct 16 2020 at 18:57):

PA can make a system of names for ordinals $\lt \varepsilon_0$, which is not very surprising since this is Cantor normal form.

John Baez (Oct 16 2020 at 19:01):

What's surprising and exciting is that people can sometimes figure out the biggest countable ordinal $\alpha$ such that a given formal system can create a notation system for ordinals $\lt \alpha$.

John Baez (Oct 16 2020 at 19:01):

And this seems to give a fairly objective measure of the "strength" of a system.

Shea Levy (Oct 16 2020 at 19:02):

John Baez said:

And this seems to give a fairly objective measure of the "strength" of a system.

Haven't been following this whole thread, does this respect the usual "strength" partial order?

John Baez (Oct 16 2020 at 19:15):

Since the order I'm talking about now - the order of proof-theoretic ordinals - is a linear order, there's no way it can completely agree with the usual ordering of theories by strength, which is merely a partial order. But I think if one theory is stronger than another its proof-theoretic order is $\ge$ that of the other.

John Baez (Oct 16 2020 at 19:17):

If you look at the list on Wikipedia you'll see lots of theories with different strength have the same proof-theoretic ordinal.

Dan Doel (Oct 16 2020 at 20:38):

I thought I'd recalled hearing that proof theoretic ordinal could actually disagree with other notions of strength, but I don't really know any details.

Dan Doel (Oct 16 2020 at 20:40):

In an opposite order sense, not just a partial vs. total order sense. Maybe it was just the latter, though.

David Michael Roberts (Oct 16 2020 at 23:12):

Tim Chow has a great article that gives one way one might think of the well-foundedness of $\varepsilon_0$ when being super pedantic about consistency of arithmetic: https://arxiv.org/abs/1807.05641 Theorem 2. I guess it has an empirical flavour.

But one should think of trees as somehow being encoded via Cantor normal form via prime factorisation/Gödel numbering.

Pedro Minicz (Oct 29 2020 at 14:42):

This discussion got me thinking, is there any intuitionistic theory $T$ that can prove $\neg \neg \mathrm{Con}(T)$? This is clearly impossible if $\mathrm{Con}(T)$ is a stable proposition, so the next question would be for which intuitionistic theories $T$, $\mathrm{Con}(T)$ is a stable proposition?

Dan Doel (Oct 29 2020 at 15:13):

$\mathsf{Con}(T)$ is usually defined as "not inconsistent", so it is equivalent to $¬¬\mathsf{Con}(T)$ intuitionistically, since the latter is triple negated.

Dan Doel (Oct 29 2020 at 15:15):

And the reason for that is that "inconsistent" is like $∃ n. \mathsf{Proves}(n, \ulcorner ⊥ \urcorner)$.

Nikolaj Kuntner (Nov 01 2020 at 12:46):

Is it clear that the ordinal strength - defined as capability of proving rather constructive consistence of ordinals - is a good indicator for what the theory can prove as a whole? Are there axioms one might e.g. add to second order arithmetic that would enable one to prove "beloved theorems" not provable in the theory before, but those axioms don't contribute whatsoever to the ordinal strength?

Dan Doel (Nov 01 2020 at 15:24):

I don't think second order arithmetic has a known proof theoretic ordinal.

John Baez (Nov 01 2020 at 15:52):

Is it clear that the ordinal strength - defined as capability of proving rather constructive consistence of ordinals - is a good indicator for what the theory can prove as a whole?

There are many very different theories with the same proof-theoretic ordinal, so I'd say the answer is no.

John Baez (Nov 01 2020 at 15:59):

For example $\mathrm{WKL}_0$ is $\mathrm{RCA}_0$ plus the weak Konig's lemma, so $\mathrm{WKL}_0$ is stronger, but they both have the same proof-theoretic ordinal - and they're two of the big five subsystems of second-order arithmetic, so they're not just silly counterexamples.

Nikolaj Kuntner (Nov 01 2020 at 23:20):

Okay makes sense, thanks.