# How can we define infinitary proofs?

In the first order logic the usual notion of a formal proof for a sentence $\sigma$ from a theory $T$ is a "finite" sequence ($<\omega$ - sequeance) of sentences which each one of them is a valid sentence or an axiom of $T$ or is produced by deduction rules from former sentences. Also this sequence "ends" by $\sigma$.

Question 1: Is it possible to generalize the notion of a formal proof infinitarily? Precisely is it well-defined to discuss about proofs in the lenght of an arbitrary ordinal $\alpha$ by defining an $\alpha$-sequence of sentences? Is it necessary for $\alpha$ to be a successor ordinal ,like $\alpha =\beta +1$ which has an end point $\beta$, in order to define $\beta$ th term of the $\alpha$- sequence as $\sigma$?

Question 2: Is there any first order theory which is consistent by finitary proofs but inconsistent with infinitary proofs? In the other words, is there a theory $T$ such that there is no finitary proof from $T$ for a contradiction but there are two infinitary proofs for two sentences $\theta$ and $\neg\theta$?

1. Yes, of course. We might need to "go one level higher" so to speak, and base our discussion in some given model of set theory (instead of on the metalanguage, where the behaviour of infinite objects is more shaky), but there are no real problems.

2. Barring the introduction of new, infinitary proof rules, the answer is no. For, we have:

Let $\Sigma\vdash \Delta$ be a sequent (with the important case $\varnothing \vdash \phi$ corresponding to $\phi$ being a theorem). Suppose there exists a (possibly infinitary) proof of $\Sigma\vdash\Delta$.

Then there exists a finite proof of $\Sigma\vdash\Delta$.

Proof: By transfinite induction on the length $\alpha$ of the proof. For $\alpha<\omega$, there is nothing to prove. Suppose that the result holds for all $\beta<\alpha$, and let $\Sigma_\alpha\vdash\Delta_\alpha$ be the sequent at stage $\alpha$.

Since all proof rules are finite, there must exist $\beta_1,\ldots,\beta_n$ such that

From $\Sigma_{\beta_1}\vdash\Delta_{\beta_1},\ldots \Sigma_{\beta_n}\vdash\Delta_{\beta_n}$ infer $\Sigma_\alpha\vdash\Delta_\alpha$.

is an instance of a proof rule. By induction hypothesis, each of the former sequents has a finite proof. Hence so does $\Sigma_\alpha\vdash\Delta_\alpha$. $\Box$

Basically, a sequent can only depend on finitely many sequents above it. Extracting this finite tree will yield a finite proof.

In conclusion: Yes, infinite proofs are admissible, but we do not gain anything if we don't have any rules to take advantage of them.

On the other hand, infinite proofs do crop up in certain proof systems. A common example is a version of induction:

Given $\Sigma \vdash \phi(S^n 0)$ for all $n \in \Bbb N$, infer $\Sigma \vdash \forall x \phi(x)$.

• If I understand well we have here three possibilities : An infinte set $\Sigma$ of assumptions (this is common in FOL, and we apply Compactness). An infinite tree of subproofs, as in Induction. The third possibility is something like a proof "running forever" (a formal derivation with an infinite number of steps) : you ruled out this possibility, because : "a sequent can only depend on finitely many sequents above it". But this does not contradict Induction ? Nov 29, 2013 at 11:13
• @MauroALLEGRANZA No, the two talk about different situations. I assumed that there were no infinite inference rules. Induction (in the form mentioned) is an infinite rule. Nov 29, 2013 at 11:19
• I'm not sure to understand your distinction between "infinite inference rules" and "infinite rule". You are saying that - in case of Induction - I can "see" at the meta-level that there is a pattern : a rule that can , for all $n \in \Bbb N$ reproduce a proof of $\phi(S^n 0)$ ? Nov 29, 2013 at 11:29
• There is no distinction. "Rule", "proof rule" and "inference rule" all mean the same here. An infinite proof rule indeed requires some means to "see" that every premise is satisfied. I assume there are no infinite proof rules, in particular, that the induction rule I mentioned is not present. Nov 29, 2013 at 11:50

Regarding the second question, "Is there any first order theory which is consistent by finitary proofs but inconsistent with infinitary proofs?" The answer is yes, when particular additional infinitary inference rules are used. Lord_Farin's answer shows that infinitary inference rules are necessary to make this happen.

It is well known that the set $X$ of formulas that are provable from Peano Arithmetic with the usual deductive system for first-order logic is a proper subset of the set of formulas $T$ that are true in the standard mode of arithmetic. This is a corollary of the incompleteness theorems.

On the other hand, every formula in $T$ is provable from Peano arithmetic with an additional infinitary $\omega$-rule; see here. Therefore, if we take $\phi \in T \setminus X$, then $X \cup \{\lnot \phi\}$ is consistent in the usual deductive system and inconsistent when we also have the $\omega$-rule.

This also shows that the incompleteness theorems do depend, to some extent, on the finitary nature of the inference rules.