2
$\begingroup$

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.

  • 0
    Is induction over the integers an *infinitary proof*?2011-07-14
  • 1
    See [Infinitary Logic.](http://en.wikipedia.org/wiki/Infinitary_logic)2011-07-14
  • 2
    For some reason I don't believe his justification for asking this question.2011-07-14
  • 0
    I thought lie.teller was just paying homage to Sophus and Edward.2011-07-14

3 Answers 3

3

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.

0

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

  • 0
    this is an instance of the $\omega$-rule. :)2011-07-15
0

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.

  • 0
    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.2011-07-15
  • 0
    @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.2011-07-15
  • 0
    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).2011-07-15
  • 0
    @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".2011-07-15
  • 0
    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.2011-07-16
  • 0
    @Kaveh His example still has an infinity of steps. So, how don't you still have an infinity of descending lines with 0+1=1+0 as one line, 0+2=2+0 as another, and so on?2011-07-17
  • 0
    Yes, but it is well-founded. It is a tree of depth 2, the root is connected to an infinite number of children, one for each natural number. This is called $\omega$-rule, i.e. derive $\forall x\ \varphi(x)$ from $\{\varphi(n) : n \in \omega\}$.2011-07-17
  • 0
    @Kaveh Wait... you said everything should eventually reach an axiom. But, consider a natural deduction system of logic which allows only finite proofs and has an empty axiom set. No proofs ever reach an axiom, because the system doesn't have any axioms at all. How exactly is the above proof unsound? The inference rules used in the proof preserve validity (and no axioms need exist), so how does soundness fail?2011-07-19
  • 0
    They have logical axioms, like $\varphi \rightarrow varphi$, deriving from empty sets means there are only logical axioms, there are no non-logical axioms. Check the wikipedida page. To prove soundness you need a form of induction on the structure of the proof, if the proof three is not well-founded there is not an induction. Soundness is a property of a derivation system, it is not a property of a particular proof. The rule that you are using in your proof is not sound since it can derive false statements. Check the references or if you have further questions post them as new questions.2011-07-19
  • 0
    @Kaveh The wikipedia page isn't correct, since a (proof-theoretical) logical axiom consists of a statement form (wff) which comes totally inside the single-turnstile. |-CpCCpqq is a logical axiom which happens in the object language. p, Cpq|-q is a rule of inference which happens in the metalanguage. Rules of inference are not wffs and thus not axioms. Natural deduction needs *no* axioms (not even the principle of the excluded middle). I've used *several* rules of inference in the proof above. Which rule of inference do you claim as not sound? The proof analysis states them all above.2011-07-19
  • 0
    If you specify Natural Deduction completely (in sequent calculus) you will see that it has axioms. Read the references e.g. Basic Proof Theory by Troelstra and Schwichtenberg, if you have a question ask one as a new question, I am not interested in continuing this discussion.2011-07-19
  • 0
    @Kaveh There do exist natural-deduction type systems outside of sequent calculus. E. G. Jaskowski's presentation of such a system which predated Gentzen's. Again, natural deduction systems don't always need axioms, and even example 2 in the wikipedia points out such a system without any axioms (for propositional calculus... another part of wikipedia isn't correct) http://en.wikipedia.org/wiki/Propositional_calculus#Example_2._Natural_deduction_system. You haven't shown a single rule of inference in the above proof as unsound, yet you claim it unsound. On what basis do you claim it unsound?2011-07-19
  • 0
    "**Read the references e.g. Basic Proof Theory by Troelstra and Schwichtenberg, if you have a question ask one as a new question, I am not interested in continuing this discussion.**"2011-07-19