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: learning: questions

Topic: Right way to prove 'correctness' of encodings in logic..

Suraaj K S (Jun 20 2024 at 13:52):

This question is not strictly category theory, but I think there are a lot of people here who might have answers..

Let us assume that I am using ZFC set theory as my metalogic.

Within my metalogic, I think it is possible to encode ZFC. So, I could have (meta)logical statements like IsZFCProvable(phi) == ∃proof: IsZFCProof(phi, proof). (IsZFCProof should also be computable, but I don't know how to express that...)

In the same vein, I think that it is possible to encode another logic, maybe Martin-Löf type theory.

Moreover, I think I can define an operator encode(zfc_phi), which takes in a sentence of my encoded ZFC set theory, and gives a sentence of my encoded Martin-Löf type theory.

For correctness, I think what I'd want is something like: ∀ zfc_phi: ( ∃mltt_proof : IsMLTTProof(encode(zfc_phi),mltt_proof) ⇒ IsZFCProvable(zfc_phi))

I think that this says that I can 'do ZFC' in MLTT. However, it doesn't really say what happens when I prove an arbitrary theorem in MLTT (only theorems of the 'shape' encode(zfc_phi)).

• So do I need another statement about decode(mltt_phi)?
• Should encode and decode be inverses of each other? This means that the two sentences in the two logics are isomorphic, which I don't think should happen?
• Is this the way one traditionally reasons about different foundational systems? I don't think this is what people mean when they say 'constructing a model'. Is there a well-known name for this idea?
• I think that you could even encode zfc in Peano arithmetic. In this case, can one say that PA is all you need? (I would like to think not...)
• Finally, I was wondering if the statements I mentioned can even be proved? Or does some impossibility theorem like Godel incompleteness come into the picture?

Note: The same question is here - https://math.stackexchange.com/questions/4935072/right-way-to-prove-correctness-of-encoding-in-another-logic

John Baez (Jun 20 2024 at 14:58):

There are a lot of parts to your question, and I don't have the energy to think about all of them, but it sounds like you're interested in the concept of 'interpreting' one theory in another. Wikipedia has an article on this:

• Wikipedia, Interpretability.

but unfortunately it's rather sketchy. You can see an example on Math Stackexchange.

John Baez (Jun 20 2024 at 14:58):

I hope someone else engages with your questions more deeply!

Patrick Nicodemus (Jun 20 2024 at 20:25):

Suraaj what you're saying makes sense. Some comments:

• ZFC as metalogic is probably much much stronger than what you need to talk about ZFC and MLTT and talk about translating one into another. I would hazard a guess that this can be done in primitive recursive arithmetic which is a very weak logic.
• computability can be expressed using the Herbrand-Godel general recursive functions on the natural numbers or the Delta_0 functions on the hereditarily finite sets
• I agree with John that the concept you're looking for is bi-interpretability
• this shouldn't violate Godels incompleteness theorem as stated but I strongly doubt the arrow goes the other way

Patrick Nicodemus (Jun 20 2024 at 20:26):

(that is, the theorem being provable in ZFC doesn't imply it's provable in MLTT - MLTT is a much weaker theory )

Suraaj K S (Jun 20 2024 at 21:01):

@Patrick Nicodemus, thanks for your response!

It is good to know that ZFC is probably too strong of a metalogic..
I'm a little bit confused about the 'weaker theory' statement. For example:
Let's use Peano Arithmetic as a formal system. I think I could do some fancy encoding (maybe Godel numbering) to encode ZFC set theory fully into PA.
This means that I could have PA predicates such as IsZFCProvable == ∃ proofnum: IsZFCProof(zfc_phi_num , proofnum).

Effectively, I could do all of ZFC in PA?

Of course, I could do all of PA in ZFC too..

We still call ZFC a stronger theory than PA. Why is that?

Patrick Nicodemus (Jun 20 2024 at 21:04):

"do" is much too vague a word here (we can "do" ZFC in PA). It very much depends on what you want to do specifically.

Patrick Nicodemus (Jun 20 2024 at 21:05):

If ZFC proves phi, then PA proves "ZFC proves phi".

But PA does not necessarily prove phi.

Suraaj K S (Jun 20 2024 at 21:09):

I see. That makes sense. However, ZFC and PA have different syntax, I'm not sure how I can formalize "PA does not prove phi"

Suraaj K S (Jun 20 2024 at 21:13):

Moreover, I think that we'd need to be careful to use only constructive logic or something?
A classical proof of IsZFCProvable(phi) in PA might not give a proof of phi in ZFC...

Patrick Nicodemus (Jun 20 2024 at 21:15):

Yes that's a good point. I was being somewhat sloppy there.

If one proves that the set of natural numbers as defined in ZFC is a model of the theory PA, then one can translate sentences of PA into ZFC sentences which concern the set of natural numbers. Within the image of this translation we can talk about whether PA or ZFC can prove the sentence.

Patrick Nicodemus (Jun 20 2024 at 21:17):

Suraaj K S said:

Moreover, I think that we'd need to be careful to use only constructive logic or something?
A classical proof of IsZFCProvable(phi) in PA might not give a proof of phi in ZFC...

I see what you're suggesting here. However consider that a computer can search for/recognize a proof of phi in ZFF. If PA proves that there is such a proof, even by non-constructive means then we can turn this into a constructive proof just by searching for the theorem until we find it

Patrick Nicodemus (Jun 20 2024 at 21:18):

A more technical way to say this is that "Is ZFC provable(phi)" belongs to a class of formulas called Sigma_1 which are constructively provable if and if they are classically provable

John Baez (Jun 20 2024 at 22:09):

Suraaj K S said:

I see. That makes sense. However, ZFC and PA have different syntax, I'm not sure how I can formalize "PA does not prove phi"

As Patrick more or less notes, one can prove in ZFC that the ordinal $\omega$ together with the obvious notions of $0 \in \omega, S: \omega \to \omega$ and $+, \cdot: \omega \times \omega \to \omega$ give a model of PA. Using this one can translate all sentences of PA into sentences about $(\omega, 0, S, +, \cdot)$. But then there are a lot of such sentences which are provable in ZFC but not in PA.

Informally speaking: ZFC lets us prove lots of statements about natural numbers that can be stated in PA, but are not provable in PA.

One famous example is Goodstein's theorem. This can be stated in PA, it's not provable in PA, but it's provable using PA + induction up to $\epsilon_0$, which is much less than the full power of ZFC.

Suraaj K S (Jun 20 2024 at 23:59):

Ah I see. I guess I was conflating two things..

• Encoding the proof system of one logic in another
• Finding a model of another logic in another