# Proving proof system properties within the proof system itself?

While reading about Frege proof systems in [1], I came across the completeness theorem and its proof, which involves a few lemmas introduced first. Here are the first two of those lemmas:

$$$$\vdash \phi \supset \phi \tag{1}$$$$ $$$$\Gamma, \phi \vdash \psi \space \text{if and only if} \space \Gamma \vdash \phi \supset \psi \tag{2}$$$$

The first one is easy to prove using the axioms and inference rule of Frege proof system. The proof of the second one uses induction. This confused me a bit and prompted the following questions:

1. Are proof systems "self-contained", in the sense that their properties can be proven within themselves? Or are properties such as soundness and completeness "external" to the system? The rationale being part of the motivation for proof systems to formalize proofs and thus serve as a foundation of sorts for other math.
2. Is there some "strange loop" going on when using something like induction (which is defined on the natural numbers) to prove such properties? Also, $$\Gamma$$ is a set, which is not really part of this proof system vocabulary. For example, if you use a sound but incomplete proof system $$P$$ to prove the soundness and completeness of another proof system $$Q$$, does that imply that $$Q$$ can't "express" $$P$$ somehow, since that would be paradoxical?

Sorry if my question is ill-posed. I'm a beginner to this topic, so I would appreciate any advice on formulating the question correctly as well.

[1] Buss, Samuel R. (ed.), Handbook of proof theory, Studies in Logic and the Foundations of Mathematics. 137. Amsterdam: Elsevier. 811 p. (1998). ZBL0898.03001.

The first problem is what does is even mean that a propositional proof system can prove its own properties: there is a serious discrepancy of the languages, because the propositional proof system can only express propositional formulas, whereas properties of the proof system are first-order statements in a language that can reason about finite strings, i.e., basically, in the language of arithmetic. Common solutions are:

1. If the property in question can be formulated as a universal statement $$\forall x\,\phi(x)$$ where $$\phi(x)$$ is polynomial-time computable, it can be encoded by a sequence of propositional tautologies $$\{[\![\phi]\!]_n(p_0,\dots,p_{n-1}):n\in\mathbb N\}$$, where $$[\![\phi]\!]_n$$ expresses the truth of $$\phi(x)$$ for $$x$$ of length $$n$$. You can then ask whether these tautologies have polynomial-size, or even polynomial-time constructible, $$P$$-proofs.

2. Many common propositional proof systems $$P$$ have a “corresponding” first-order arithmetical theory $$T$$. The correspondence is a somewhat loose notion, but generally it means that on the one hand, universal statements provable in $$T$$ translate (as in 1) to sequences of tautologies that have polynomial-time constructible $$P$$-proofs, and on the other hand, $$T$$ can prove the soundness of $$P$$. In a sense, this says that the arithmetical theory $$T$$ is a “uniform version” of the propositional proof system $$P$$. When you have such a correspondence, you may explicate the informal statement “$$P$$ proves this and this property” as formally meaning that $$T$$ proves the property.

Now, if a proof system “proves” (in sense 1 or 2) a given property of itself of course depends on the property and on the proof system, there is no general answer:

• There is usually no difficulty with formalizing basic efficient syntactic manipulation. For example, (the bounded arithmetic corresponding to) the Frege system can prove that Frege satisfies the deduction theorem (your (2)).

• Whether a proof system can prove its own soundness is an important property that’s discussed a lot in the literature. The propositional translations of the soundness of $$P$$ are called the reflection principles for $$P$$. Proof systems that have a “corresponding” theory of arithmetic have polynomial-time constructible proofs of their own reflection principles more or less by definition of the “correspondence”. For example, this holds for Frege, and for most typical sufficiently strong proof systems. Moreover, under mild assumptions, if a proof system $$P$$ has polynomial-time proofs of the reflection principle for a proof system $$Q$$, then $$P$$ polynomially simulates $$Q$$.

• Under the most reasonable interpretation, (likely) no proof system can prove its own completeness. First, this is not a universal statement, but a $$\forall\exists$$ statement (with an unbounded, or at best exponentially bounded, existential quantifier), hence directly translating it in the sense 1 is not possible: “for every formula $$A$$, there exists a $$P$$-proof of $$A$$, or an unsatisfying assignment to $$A$$”. One can ask about its provability in the corresponding theory of arithmetic (i.e., in sense 2), but Parikh’s theorem (that holds for any such theories) implies that this completeness statement is not provable unless one can place a polynomial bound on the existential quantifiers, i.e., unless the proof system $$P$$ is polynomially bounded, which implies NP = coNP.

One may cheat by encoding the completeness statement only for logarithmically short formulas: that is, by considering propositional tautologies $$A_n$$ suitably expressing “every formula of length $$\le\log n$$ has a $$P$$-proof of size $$\le n^c$$” (or the corresponding arithmetical sentence). In systems like Frege, this should be provable with no difficulty.

You may find further information e.g. in

[1] Stephen A. Cook and Phuong Nguyen: Logical foundations of proof complexity. Perspectives in Logic, Cambridge University Press, New York, 2010.

[2] Jan Krajíček: Proof complexity. Encyclopedia of Mathematics and Its Appplications, vol. 170, Cambridge University Press, 2019.

There is no loop. The purpose of a formal system is to make reasoning principles explicit and to explain more precisely how reasoning works. The word "foundation" in "foundations of mathematics" does not mean "create a secure base for mathematics out of nothing" – that would be an indifensible position.

There is absolutely nothing wrong with a logicians using sets to describe a formal system. Should a number theorist not be allowed to use numbers? Are logicians allowed to use strings of symbols? Where do you draw the line?

On the technical side of things, there are formal systems that can talk about their own syntax and proof rules. After all, that is the gist of Gödel's incompleteness theorems: he shows that as soon as a formal system contains arithmetic, it can speak about syntax and its own provability.

• "create a secure base for mathematics out of nothing - that would be an indefensible position" - I agree. I thought historically this was precisely the position that Hilbert, Russell, Frege, etc. were aiming for. Do you know this aspect of the history? – Joshua Grochow May 5 at 16:57

In general, proof systems can sometimes prove some of their properties within themselves.

A nice example of this is the fact that NL=Co-NL can be proved "within NL".

This video might also be useful: https://www.youtube.com/watch?v=TLjRGm8ZfyQ