Efficiently modeling Turing machines in Peano Arithmetic

Question

The (undecidable) Peano Arithmetic (PA) is powerful enough to model Turing machines.

Consider a standard first order axiomatization of Peano Arithmetic and a standard Hilbert-style proof system $\mathcal F$.

1. Is it true that every first order informal proposition $P$ about computation and Turing machines has a corresponding formal formula $\varphi$ in Peano Arithmetic which is equal in size up to a polynomial blow-up: $|\varphi| = O(|P|^k)$ for some fixed $k$ which is independent of $P$?

2. Furthermore if $P$ has an informal short proof (polynomial in $|P|$), is it true that the corresponding $\varphi$ in PA has a polynomial length proof with respect to $|\varphi|$

As a trivial example consider the following Turing machine (in pseudocode):

M:
n=100
while n > 0 do n = n - 1

and the informal proposition: $P \equiv \text{ M doesn't halt in less than 90 steps}$

$P$ can be converted to a formula $\varphi$ in PA; and this $\varphi$ must "embed" a symbolic representation of M and some kind of operational semantic. But can the conversion be done efficiently (polynomial time and space)?

Furthermore there is a trivial "informal" short proof of $P$, but does the corresponding formal proof in PA ($\mathcal F \vdash \varphi$) have a polynomial length size with respect to $|\varphi|$?

Edit: as noted by Kaveh the "informal" term above is confusing.

I could restate the two questions above in this way: if $P$ is a true mathematical statement that is expressible both in ZFC (as $\varphi'$) and PA (as $\varphi$). Is it always true that $| \varphi | \in O(|\varphi'|^k)$ for some fixed $k$ independent of $P$? What about the size of the corresponding proofs in the two axiomatizations (assuming that $\varphi'$ is provable in ZFC and $\varphi$ is provable in PA)?

But this lead to another question:

3. Is it true that every "human written proof" that is expressible in ZFC has indeed an "efficient" representation in ZFC? i.e. a (rather informal) proof of $\#p$ pages in my favourite paper cannot become a $O(2^{\#p})$ long formal proof in ZFC ? :-)

Answer 1

I am not sure I understand the question, specially the informal part. If by it you mean essentially how we generally argue for correctness of things, I woke interpret it as day proofs in ZFC or something like that.

In any case we can express provability of a statement in a computably axiomatizable system in PA (and in fact in weaker systems). Now you are asking if this can be expressed as efficiently in PA as in the stronger system. The answer is yes, just express that the Turing machine that search for a string is a ZFC proof of the formula halts. The size of the description of such a machine is polynomial in the size of the ZFC formula.

The answer to the second question is no. Just consider a computable function that grows so fast that PA cannot prove its totality but ZFC van prove its totality.

---

The key idea really is that the language of ZFC itself is very easy to capture. We can express that string $\pi$ is a ZFC-proof of $\varphi$ in much simpler systems that ZFC (e.g. Cook's $V^0$ which captures computation in $AC^0%).

If we can express that, then we can express anything ZFC can express. That is there is polynomial-time computable function $t$ that maps any well-formed formula in the language of ZFC to a formula in the language of PA such that the formula is provable in ZFC iff there is a string that PA proves it is a ZFC proof of the the translation with: just encode the ZFC proof, PA can verify syntactically that it is a valid ZFC proof, and if there is such a string that PA proves is a ZFC proof of the formula, then it is actually a ZFC proof of the formula.

It is key here that I didn't quantify for the existence of the ZFC proof in the PA translation. The reason is that PA might not be able to prove the existence generally. E.g. let $f$ be computable function whose totality is provable in ZFC but not in PA. Then the formula $\forall x \exists y f(x)=y$ is probable in ZFC but not in PA (with any resonable encoding). The reason is that if we can prove it then we prove the totality.

This is generally related to what is called interpretability and interpretation in logic. Essentially we have L1 and L2 and they have their own semantics, and we ask if everything in L1 can be faithfully expressed in L2. Think of the formulas as capturing the subsets of the standard models of those languages. E.g. for ZFC this would be the standard model $\mathbb{V}$ while for PA this would be standard natural numbers $\mathbb{N}$. Before thinking about expressing things, you need to think about how subsets of these two structure map to each other. What does it mean to map a set in ZFC to a set in PA. We can restrict our interest to subsets of $\omega$ in ZFC. Then the question becomes. We can restrict ourselves to arithmetic subsets of $\omega$. Then these subsets are expressible in PA clearly. For any such set we have a PA formula.

For size we really need to talk about families of formulas. If the family is uniform, that is it is obtained by sectioning another arithmetic formula, then the size relation is still polynomial: let the formulas in ZFC be $\varphi_n(x) := \varphi(n,x)$. To obtain the translation in PA, translate $\varphi$ and then plugin $n$: $[[\varphi_n(x)]] := [[\varphi(x,y)]]_{y/n}$. The only part that changes is $n$, the rest remain the same.

For provability the story is not about standard models but also non-standard models that satisfy the axioms. Is it the case that every function over natural numbers that is total in every model of ZFC is total in every model of PA? The answer is no.

Answer 2

A little consideration about point 3. "Is it true that every "human written proof" that is expressible in ZFC has indeed an "efficient" representation in ZFC?"

It turns out that the question is anything but new. At least it dates back to the late sixties when the idea of computer vierified mathematical proofs came up (e.g. Automath):

In his 'A survey of the project Automath' de Bruijn wrote:

A very important thing that can be concluded from all writing experiments is the constancy of the loss factor. The loss factor expresses what we loose in shortness when translating very meticulous "ordinary" mathematics into Automath. This factor may be quite big, something like 10 or 20, but it is constant: it does not increase if we go further in the book. It would not be too hard to push the constant factor down by efficient abbreviations.

The de Bruijn Factor is the quotient of the size of a formalization of a mathematical text and the size of its informal original (Freek Wiedijk, "The de Bruijn Factor").

The answer to the question seems to be yes at least in practice and all proofs that have been formalized using proof assistants like Mizar, Coq, Isabelle, .... seem to confirm that the blow-up is linear. Some practical investigations about the factor can be found on Freek Wiedijk's site.