Skip to main content
MathOverflow

Return to Answer

typo fixes, + made references to PA vs. HA more consistent
Source Link
Peter LeFanu Lumsdaine
Peter LeFanu Lumsdaine
  • 21.3k
  • 2
  • 75
  • 128

Fortunately, though, we don't need to posit a Set0 for this and end up with the same problem one turtle lower down. To formalise the fundamentals of proof theory, we just need to be able to talk about manipulating strings of symbols, so a theory of the natural numbers (eg PA or even HA) is more than enough. On the other hand, we do have to presume some given meta-theory (as most traditional logicians would call it) or logical framework (as many computer scientists would) to get off the ground, and for that we really do have the problem that we can't talk about it as an object itself without passing to a meta-meta-theory. This is a real problem, but more a philosophical than a mathematical one: we just have to either accept a potential infinite regress, or make a leap of faith that facts proven within our meta-theory, about some internal version of it, will apply to the meta-theory itself (whether this is a platonic object, a physical computer system, or whatever else).

The second issue is one of reflection, and has a more satisfying resolution. (I'll keep the meta-theory informal, but PA or even HA would be more than enough to formalise this, I think.) Say we have some axioms for Set1, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define Set2 as the "internal version" of the same theory in Set1, and so on. Now we can prove:

Suppose Set1 proves Con(Set2). By the above proposition, Set1 also proves "Set2 proves Con(Set3)". Now, by G&oumldel'sGödel's theorem for Set2, we can deduce (still in Set1) the theorem "Set2 is inconsistent**"inconsistent". But now we have proofs in Set1 of both Con(Set2) and its negation; so Set1 is inconsistent. QED

Fortunately, though, we don't need to posit a Set0 for this and end up with the same problem one turtle lower down. To formalise the fundamentals of proof theory, we just need to be able to talk about manipulating strings of symbols, so a theory of the natural numbers (eg PA) is more than enough. On the other hand, we do have to presume some given meta-theory (as most traditional logicians would call it) or logical framework (as many computer scientists would) to get off the ground, and for that we really do have the problem that we can't talk about it as an object itself without passing to a meta-meta-theory. This is a real problem, but more a philosophical than a mathematical one: we just have to either accept a potential infinite regress, or make a leap of faith that facts proven within our meta-theory, about some internal version of it, will apply to the meta-theory itself (whether this is a platonic object, a physical computer system, or whatever else).

The second issue is one of reflection, and has a more satisfying resolution. (I'll keep the meta-theory informal, but PA or even HA would be more than enough to formalise this.) Say we have some axioms for Set1, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define Set2 as the "internal version" of the same theory in Set1, and so on. Now we can prove:

Suppose Set1 proves Con(Set2). By the above proposition, Set1 also proves "Set2 proves Con(Set3)". Now, by G&oumldel's theorem for Set2, we can deduce (still in Set1) the theorem "Set2 is inconsistent**". But now we have proofs in Set1 of both Con(Set2) and its negation; so Set1 is inconsistent. QED

Fortunately, though, we don't need to posit a Set0 for this and end up with the same problem one turtle lower down. To formalise the fundamentals of proof theory, we just need to be able to talk about manipulating strings of symbols, so a theory of the natural numbers (eg PA or even HA) is more than enough. On the other hand, we do have to presume some given meta-theory (as most traditional logicians would call it) or logical framework (as many computer scientists would) to get off the ground, and for that we really do have the problem that we can't talk about it as an object itself without passing to a meta-meta-theory. This is a real problem, but more a philosophical than a mathematical one: we just have to either accept a potential infinite regress, or make a leap of faith that facts proven within our meta-theory, about some internal version of it, will apply to the meta-theory itself (whether this is a platonic object, a physical computer system, or whatever else).

The second issue is one of reflection, and has a more satisfying resolution. (I'll keep the meta-theory informal, but HA would be more than enough to formalise this, I think.) Say we have some axioms for Set1, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define Set2 as the "internal version" of the same theory in Set1, and so on. Now we can prove:

Suppose Set1 proves Con(Set2). By the above proposition, Set1 also proves "Set2 proves Con(Set3)". Now, by Gödel's theorem for Set2, we can deduce (still in Set1) the theorem "Set2 is inconsistent". But now we have proofs in Set1 of both Con(Set2) and its negation; so Set1 is inconsistent. QED

Source Link
Peter LeFanu Lumsdaine
Peter LeFanu Lumsdaine
  • 21.3k
  • 2
  • 75
  • 128

Your question raises two interesting issues: one of formalisation, one of externalisation/reflection. The former contains a real problem, but more philosophical than mathematical; the latter is I think where the mathematical content of your question lies, and it has a positive answer.

You hit the first one on the head when you point out: "of course one could just argue that Set1, not being formalized, is not amenable to mathematical investigation," and I don't think your next point quite answers that question: you discuss the externalisation issues of Gödel's theorem, but that's separate from the formalisation question. You ask for a reason to believe Set1 doesn't prove something — how could one hope to give that without discussing Set1 as a precise object in some meta-theory?

Fortunately, though, we don't need to posit a Set0 for this and end up with the same problem one turtle lower down. To formalise the fundamentals of proof theory, we just need to be able to talk about manipulating strings of symbols, so a theory of the natural numbers (eg PA) is more than enough. On the other hand, we do have to presume some given meta-theory (as most traditional logicians would call it) or logical framework (as many computer scientists would) to get off the ground, and for that we really do have the problem that we can't talk about it as an object itself without passing to a meta-meta-theory. This is a real problem, but more a philosophical than a mathematical one: we just have to either accept a potential infinite regress, or make a leap of faith that facts proven within our meta-theory, about some internal version of it, will apply to the meta-theory itself (whether this is a platonic object, a physical computer system, or whatever else).

The second issue is one of reflection, and has a more satisfying resolution. (I'll keep the meta-theory informal, but PA or even HA would be more than enough to formalise this.) Say we have some axioms for Set1, strong enough that it contains an "internal copy" of the natural numbers and hence can talk about basic proof theory; then define Set2 as the "internal version" of the same theory in Set1, and so on. Now we can prove:

Lemma. (An instance of a reflection principle for provability.) If Set1 proves "Set2 is consistent", then it also proves "Set2 proves 'Set3 is consistent' ".

(This is a good exercise in internalisation; it essentially comes from the fact that "being a proof" is a very straightforward property, and hence robust under internalisation.)

Now, if Set1 is able to prove Gödel's theorem for Set2 (in the form you state it, i.e. "if Set2 proves consistency of Set3, then Set2 is inconsistent"), we can deduce Gödel's theorem for Set1 as follows:

Suppose Set1 proves Con(Set2). By the above proposition, Set1 also proves "Set2 proves Con(Set3)". Now, by G&oumldel's theorem for Set2, we can deduce (still in Set1) the theorem "Set2 is inconsistent**". But now we have proofs in Set1 of both Con(Set2) and its negation; so Set1 is inconsistent. QED

So your question has a positive answer: if we're allowed to reason mathematically about Set1 at all, then yes, we have reason to believe it doesn't prove the consistency of Set2.