Talk:Mathematical induction

From Wikipedia, the free encyclopedia

WikiProject Mathematics
Mathematics Portal
This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.
Mathematics rating: A-BB+ Class Top Priority  Field: Foundations, logic, and set theory
One of the 500 most frequently viewed mathematics articles.

Older discussion is at /Archive

[edit] Equivalence to WOP

In the intro I read:

Indeed, the validity of mathematical induction is logically equivalent to the well-ordering principle.

what is it referring to? We have a section "proof or reformulation of mathematical induction" where it is shown that MI can be proven assuming WOP and some other axioms, but this is something different from "logical equivalence".--Pokipsy76 17:32, 28 August 2007 (UTC)

I've simply removed the sentence.  --Lambiam 13:31, 9 January 2008 (UTC)

It seems to me that the idea is that an analogous proof would go through for any well-ordered set. That is, that any well-ordered set admits a proof technique analogous to mathematical induction.

For example, on the ordinals, we have transfinite induction; on trees or lists over well-ordered sets we have the appropriate varieties of structural induction, and so forth.

-- Dominus (talk) 15:07, 9 January 2008 (UTC)

There is in fact a discussion of the issue that almost says this (and certainly implies it) at Structural induction#Well-ordering. In fact, we don't need a (total) well-order; a (partial) well-founded relation suffices. The following two statements are logically equivalent in standard predicate logic: (1) induction is valid for some domain with a given relation where the induction process does not use a "base case" but only an induction step, which consists of concluding to the validity of a property for some element from the inductive hypothesis of the validity of that property for all predecessors of that element in the given relation, and: (2) the given relation is well-founded. I'd be happy to add this to the encyclopedia, if it were not for the requirement of citing published reliable sources, which I don't have for this.
For the naturals specifically, however, the article Well-ordering principle seems an obfuscation to me, what with the naturals being a subset of the integers and the consideration of the embedding of the naturals into the reals as a complete space, and the mention of Modus Tollens.  --Lambiam 00:49, 10 January 2008 (UTC)


[edit] 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)

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) \to ((x)(Ά(x) \to ((x)(Ά(x'))\to (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) \to ((x)(Ά(x) \to ((x)(Ά(x'))\to (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) \to ((x)(Ά(x) \to ((x)(Ά(x'))\to (x)Ά(x))"
is a theorem; presumably not otherwise we would not need it as an axiom schema! But for any wf Ά(x),
"Ά(a) \to ((x)(Ά(x) \to ((x)(Ά(x'))\to (x)Ά(x))"
eg
"F(a) \to ((x)(F(x) \to ((x)(F(x'))\to (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) \to ((x)(Ά(x) \to ((x)(Ά(x'))\to (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) \to ((x)(F(x) \to ((x)(F(x'))\to (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)\to ((x)(F(x) \to ((x)(F(x'))\to (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) \to((x)(F(x)\to ((x)(F(x')) \to(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)

[edit] Axiom of Induction

Is not the formula for Axiom of Induction wrong? It should be a & there it is a ^. Reko (talk) 06:05, 10 April 2008 (UTC)

The wedge is used in formal logic to mean "and" (or more accurately, in the intended interpretation, the wedge is interpreted as "and). --196.209.178.209 (talk) 20:05, 10 April 2008 (UTC)
For the notations used, see Logical connective.  --Lambiam 22:13, 10 April 2008 (UTC)