# Example of infinite proof

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.

-
Is induction over the integers an infinitary proof? – Henry Jul 14 '11 at 0:07
– Bill Dubuque Jul 14 '11 at 0:09
For some reason I don't believe his justification for asking this question. – Quinn Culver Jul 14 '11 at 2:19
I thought lie.teller was just paying homage to Sophus and Edward. – Gerry Myerson Jul 14 '11 at 6:00

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.

-

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

-
this is an instance of the $\omega$-rule. :) – Kaveh Jul 15 '11 at 16:53

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.

-
The proof tree needs to be well-founded, otherwise we can derive arbitrary results: line $-n$: $0=1$, for $n\in N$. Each line follows from the previous one. A proof with an infinite descending sequence of lines is not sound. – Kaveh Jul 15 '11 at 16:55
@Kaveh What do you mean by "well-founded"? Also, why do you say a proof with an infinite descending sequence of lines is not sound, and what exactly do you mean by sound here? Granted, such a proof requires that we use a different definition of a formal proof than usual since it's not a finite sequence of wffs, and the definition of a formal theorem differs also, but I don't see any problem with such a concept per se. Also, deriving falsities isn't a problem even in standard propositional logic. You can start a proof with a contradiction and re-derive it, just so long as its not a theorem. – Doug Spoonwood Jul 15 '11 at 22:12
The example I gave has no assumption, so it is deriving a false formula from empty assumption. Well-founded means that these is no infinite descending lines of proof, everything should eventually reach an axiom. Soundness means that if you derive a formula it is true, and no, standard propositional logic is sound, you cannot derive a false formula (from empty assumption). – Kaveh Jul 15 '11 at 22:22
@Kaveh An infinitary proof, as I understand the term, has an infinity of formulas, and thus by its very nature has an infinity of descending lines in the proof. So, I don't see your objection since the author asks for that. Here's how I define "derive": a formula can get said to have gotten derived iff it comes as the result of some formula via an inference rule. E. G. We have KpNp as a formula, then p can get derived via a conjunction elimination rule. Under this definition we can derive a falsity. I think you've used the term "derive" in the same way as I would use the term "prove". – Doug Spoonwood Jul 15 '11 at 23:01
No, an infinite proof can be well-founded like GEdgar's example which uses the $\omega$-rule. (hint: a proof is a tree!). This topic is well studied in proof theory, if you are interested check Jean-Yves Girard's book "Proof theory and logical complexity", 1987. I should say not an easy book, actually it is one of the most advanced ones out there. – Kaveh Jul 16 '11 at 5:34
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://math.stackexchange.com/questions/51329/example-of-infinite-proof", "fetch_time": 1469434374000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2016-30/segments/1469257824217.36/warc/CC-MAIN-20160723071024-00007-ip-10-185-27-174.ec2.internal.warc.gz", "warc_record_offset": 159749773, "warc_record_length": 19759, "token_count": 1352, "char_count": 5305, "score": 3.546875, "int_score": 4, "crawl": "CC-MAIN-2016-30", "snapshot_type": "latest", "language": "en", "language_score": 0.9277233481407166, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00030-of-00064.parquet"}