=Is their a proof in predicate logic of Mathematical induction?=--Philogo (talk) 00:31, 29 February 2008 (UTC) --Philogo (talk) 21:50, 25 February 2008 (UTC) —Preceding unsigned comment added by Philogo (talk • contribs) 21:46, 25 February 2008 (UTC)





first edit

Yes I know Usually induction is given as an axiom or axiom scheme; but I have not seen a proof in predicate logic. Have you seen one? where can I see a proof in higher-order logic. --Philogo (talk) 13:21, 26 February 2008 (UTC)
It is not strange that you haven't seen a proof in predicate logic, because the principle cannot even be formulated in predicate logic. Usually mathematicians do not give theit proofs in a formal proof system. Proofs of the axiom of induction for various higher-order logics are given in (Hatcher, William S., 1982. The Logical Foundations of Mathematics. Pergamon).  --Lambiam 19:54, 26 February 2008 (UTC)
Thanks I see if I can lay my hands on same. I am not sure whether it is true to say that the principal cannot be formulated in predicate logic. If as you say it can be proven in higher-order logic, and any higher-order logic is a predicate logic, then it msut be expressible in that higher-order logic and so a fortiori in predicate logic. Mendelson, Mathematical Logic, Van Nosran Reinhold, 1964, page 103 has

(S9) For any wf Ά(x) of S, Ά(0)   ((x)(Ά(x)   ((x)(Ά(x'))  (x)Ά(x))
... (S9) is an axiom schema providing an infinite number of axioms.
These axioms would be expressible in just first order predicate logic. So my question is whether there is any proof that any wf Ά(x) of S, Ά(0)   ((x)(Ά(x)   ((x)(Ά(x'))  (x)Ά(x)) is a theorem. --Philogo (talk) 20:55, 26 February 2008 (UTC)

If the induction formulas have not been added as axioms, then for specific wfs there may be a proof, like when (∀x)ℬ(x) is a theorem, but lacking axioms for induction, such induction formulas cannot be proved in general, since there are nonstandard models of the integers for which induction does not hold. A simple nonstandard model is to adjoin an extra element ω to the standard naturals for which ω' = ω. Then if ℬ(x) is the wf x' ≠ x, the induction formula for this wf fails to hold in the model and should therefore not be provable (unless you're working with an unsound system).  --Lambiam 22:18, 26 February 2008 (UTC)
The first=order theory S referred to has a single two place predicate letter A and we may t=s for A(t,s); one individual constant a (written as 0) and three function letters f,g and h and we may write t' for f(t); t+s instead of g(t,s) and t' instead of h. S has eight proper axioms (I will not bother to list them) and the and axiom schema (S9) referred to above. ((S1) thru (S9) together correspond to - with one proviso - Peano's Postulates).

S, with the proper axioms, is of interest since adequate for the proofs of all the basic results of elementary number theory - according to Mendelson. What I am interested in is whether, for any wf Ά(x) of S,
"Ά(0)   ((x)(Ά(x)   ((x)(Ά(x'))  (x)Ά(x))"
is a theorem; presumably not otherwise we would not need it as an axiom schema! But for any wf Ά(x),
"Ά(a)   ((x)(Ά(x)   ((x)(Ά(x'))  (x)Ά(x))"
eg
"F(a)   ((x)(F(x)   ((x)(F(x'))  (x)F(x))"

intuitively looks like a logical truth. Were it one, or were it included as a (logical) axiom, we would not need it as a proper axiom. Hence my original question, "Is their a proof in predicate logic of Mathematical induction?" or more precisely perhaps, is their a proof in predicate logic, (not necessarily first-order) of any wf of the form:
"Ά(a)   ((x)(Ά(x)   ((x)(Ά(x'))  (x)Ά(x))"

Perhaps the answer is in Hatcher, William S., 1982. The Logical Foundations of Mathematics. --Philogo (talk) 00:24, 29 February 2008 (UTC)

No, it isn't possible to prove arbitrary induction instances using logic alone. It's easy to create structures in which various induction principles fail - start with the natural numbers and adjoin some extra elements greater than all the natural numbers. In the division between "logical axioms" and "mathematical axioms", the induction ones fall in the latter category. — Carl (CBM · talk) 02:23, 29 February 2008 (UTC)
it follows, does it not, that there is no proof of, eg

"F(a)   ((x)(F(x)   ((x)(F(x'))  (x)F(x))"
no matter what interpretation we have of the ' function.--Philogo (talk) 13:34, 29 February 2008 (UTC)

It will depend on what formula F is. If F(x) is "x=x" then that particular induction axiom will of course be provable. Or maybe F is a logically valid sentence with no free variables at all. But there are many formulas F for which the corresponding induction axiom is not provable. — Carl (CBM · talk) 14:55, 29 February 2008 (UTC)

Thanks for that. On reflection I I believe I should have said, it follows that the sentence
(S9a) F(a)  ((x)(F(x)   ((x)(F(x'))  (x)F(x))
is not logically true because there is at least one interpretation where it is false when the domain of the argument to F is not denumerable. I had thought that the function ”’” ensured that the domain of x was denumerable. Assuming not, then, were there some wff, G x, which would be true just in case the domain of x was denumerable then its conjunction with (S9a), i.e. (S9a) & G(x) i.e.
F(a)  ((x)(F(x)  ((x)(F(x'))  (x)F(x)) & G(x)
might be a logical truth and if it were a logical truth but there were no proof of it in any theory, T, then any such theory T would not be complete. My apologies if this is all old stuff but I have not found much relevant discussion on this post Frege.--Philogo (talk) 18:22, 29 February 2008 (UTC) --Philogo (talk) 18:17, 29 February 2008 (UTC)--Philogo (talk) 18:29, 29 February 2008 (UTC)

I'm not sure what you mean by "logically true". Many theories are incomplete, and you cannot hold that against truths that are not covered by some such theory, but are included in another one.
In the counterexample I gave above to (S9), namely with the domain of non-standard "naturals" N ∪ {ω}, the domain is denumerable, so non-denumerability is not the issue.
The formulas you give for (S9) and variants are hard to interpret because the parentheses are not balanced. I don't have the 1964 edition of Mendelson, but the axiom schema (S9) I see in Mendelson (4th edition, 1997, ISBN 978-0412808302, page 155) is:
(0)   ⇒   ((∀x)((x) ⇒ (x ))  ⇒  (∀x)(x)).
Forming the conjunction (S9) & G(x) is meaningless, since the variable x is not bound. There is no predicate of first-order theory expressing that some domain is denumerable. In giving proofs in logic, it is irrelevant what properties a predicate such as G is meant to have or not have in an intended interpretation ("true just in case the domain of x was denumerable"), since in the proof you have no access to the interpretation, so you cannot use this extra-logical knowledge.
The successor function " " is just an arbitrary symbol in logic; like all predicate and function symbols, it has no other properties than follow from given axioms.
Basically everything CBM wrote above repeats points I already made in my reply from 22:18, 26 February 2008. I am sorry I was not clearer, but let me once more repeat the situation:
  1. If you add induction as an axiom schema, then (of course) you can now prove it for any wf of your logic, since each axiom is a theorem.
  2. If you do not add induction as an axiom schema, you can not prove it for arbitrary wfs. (That is precisely the reason it is added as an axiom schema: that you cannot prove it otherwise.)
  3. It is possible to prove the induction rule for some specific wfs, such as the tautological wf x = x.
 --Lambiam 15:06, 1 March 2008 (UTC)
Also, the issue of denumerability isn't important. Any first-order structure has an elementarily equivalent denumerable substructure, by the Lowenheim-Skolem theorem, so we could assume all structures are denumerable if we are only interested in whether they satisfy specific sentences. — Carl (CBM · talk) 15:14, 1 March 2008 (UTC)

Second edit

Talk:Mathematical induction

  • Apologies
    • Mendelson 1964 p 103 has "(S9) For any wf Ά(x) of S Ά(0)   ((x)(Ά(x)   Ά(x'))  (x)Ά(x))".
      • This is equivalent to his 1997 page 155: (0)   ⇒   ((∀x)((x) ⇒ (x ))  ⇒  (∀x)(x))
    • When I said logically true above I should have said logically valid, i.e. true for every interpretations (Mend, '64, p 54)
    • The example I gave of such an wf should have been F(a)   ((x)(F(x)   (F(x'))  (x)F(x))
  • I understood that there was no proof of the Principal of Mathematical Induction in predicate calculus (hence Mendelson's need to represent it by a proper axiom schema) and sought confirmation Two issues have arisen
    • Whether the Principal of Mathematical Induction can be expressed in predicate calculus
    • If it can, is the expression logically valid and (therefore) there is a proof of it in predicate calculus.
  • Mendelson (1964: p. 102) says that Peano's Postulates can be formulated by five statements (P1) through (P5):
    • (P1) 0 is a natural number
    • (P2) If x is a natural number then, there is another natural number denoted by x' (and called the successor of x).
    • (P3) 0 ≠ x' for any natural number x
    • (P4) If x'=y', then x=y.
    • (P5) If Q is a property which may or may not hold of natural numbers, and if (I) 0 has the property Q, and (II) whenever a natural number x has the property Q, then x' has the property Q, then all natural numbers have the property Q (Principle of Induction)
  • Mendelson describes a first-order theory S that is based on Peano's postulates. He gives nine proper axioms for S including
    • (S3) 0 ≠ x
    • (S4) (x1)' = (x2)'   x1=x2
    • (S9) For any wf Ά(x) of S Ά(0)   ((x)(Ά(x)   Ά(x'))  (x)Ά(x)). He says he will call (S9) the Principal of Mathematical Induction which he grants does not fully correspond to (P5) since (S9) can only take care of the denumerable number of properties defined by wfs of S.
    • He says (S3) and (S4) correspond to (P3) and (P4) and that (P1) and (P2) are taken care of by the presence of 0 and as an individual constant and f1 as a function letter.
  • (S9 ) For any wf Ά(x) of S: Ά(0)   ((x)(Ά(x)   Ά(x'))  (x)Ά(x)) can be written:
  • (S9a) For any wf Ά(x) of S: Ά(a)   ( x(Ά(x)  Ά(x'))   xΆ(x)).
  • If we seek an expression which in predicate calculas which is logiocally valdi then it must be true in all interpretations, not just in S or other particualr theories, and the qualification in S in (S9) and (S9a) has to go.
  • Consider the axiom schema (S9b) For any wf Ά(ά),

Ά(β)   ( x(Ά(ά)  Ά(ά'))   άΆ(ά)) ( where ά is any variable and β is any individual constant)

    • This does not generate just logically valid axioms since:
      • Let the wf Ά(x) be (Fx & ~Fb) then
      • (Fa & ~Fb)   ( x((Fa&~Fb)  (F(x')& ~Fb))   x(Fx&~Fb) is an axiom but it is not logically valid.
  • Consider (S9c) : For any wf Ά(ά),

Ά(β)   ( x( ( x=β    y(x=y'))   Ά(ά)  Ά(ά'))    άΆ(ά)) (where ά is any variable and β is any individual constant)