Example of infinite proof

Question

Is there a reasonably simple example of an infinitary proof in logic? I need mostly an example in which the total height or level of a derivation is infinite, i.e. there is at least an axiom from which we begin somewhere and applying inference rules we end with a theorem after infinite steps.

Answer 1

You can find a very nice survey of proof theory, including infinitary methods, in Feferman's Highlights in Proof Theory. See especially the last section devoted to infintary methods, for example, the $\omega$-rule, which states that you are allowed to deduce $\rm\:\forall x\ A(x)\:$ once you have proved $\rm\:A(n)\:$ for each natural $\rm\:n\:.\:$ See also the Wikipedia article on Infinitary Logic.

Answer 2

Not clear what you want. Maybe prove commutative law for addition of natural numbers like this:

Check 0+1=1+0; check 0+2=2+0; check 1+2=2+1; etc.; after infinitely many steps we have checked all cases...

Answer 3

I'd think any "formalization" of an argument by induction would work, but as something perhaps simpler, suppose we have a system with an infinity of axioms, and one particular axiom p. Now consider an infinite sequence of conditionals which has one unique member of the axiom set for each conditional and ends with axiom "p" as the consequent of the very last conditional, as in "if p, then if q, then if r... then if z, then p". Or CpCqCr...Czp. The proof of such a theorem could go "p, CqCr...Czp, q, Cr...Czp, ..., Czp, z, p".

Also, consider any proof you have of any theorem. Before that proof think of some sequence of formulas which repeats in a loop. Perhaps you introduce an assumption, get rid of it, then re-introduce it, and repeat the process whereby you got rid of the assumption. You don't even need any axioms for this to work as follows:

1 | p assumption
2 | App 1 alternation introduction
3 | KpApp 1, 2 conjunction introduction
4 | p 3 conjunction elimination
5 Cpp 1-4 conditional introduction
6 | p assumption
7 | App 6 alternation introduction
8 | KpApp 6, 7 conjunction introduction
9 | p 8 conjunction elimination
10 Cpp 6-9 conditional introduction
.
.
. (where the sequence of five formulas repeats ad infinitum)
n   | Kpq assumption
n+1 | p n conjunction elimination
n+2 CKpqp n, n+1 conditional introduction.

So, given "infinitary proofs" as permissible, unless I'm mistaken, "there" lies an infinitary "proof" of "if the conjunction of p and q, then p", unless you can deny the validity of any of the steps above as permissible in propositional calculus. If you need to have an axiom, just tack one on at the beginning of such a proof.