How can we define infinitary proofs?

Question

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$?

Answer 1

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)$.

Answer 2

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.