0
$\begingroup$

From Enderton's mathematical logic book sec 1.1, there is a thing called construction sequence for wffs. For example, $P\wedge Q\to R$ can be thought as $\langle P,~Q,~P\wedge Q,~R,~P\wedge Q\to R\rangle$. And then he used it to prove a theorem, which he called Induction Principle, saying that if a set $S$ of wffs contains primitive sentential symbols and is closed under $\vee,\wedge,~\cdots$ etc, then $S$ is no more or less the set of all wffs.

My problem is that, in his proof he used mathematical induction on the position of the construction sequence. However, does it mean that he implicitly assumed the Peano axioms (of course I especially refers to the mathematical induction axiom)? But when I look closer to this, I somehow feel that the induction used here is very "intuitive" and reflects the human mind ... you know what I mean. So my question is stated blurred as "whenever we use mathematical induction (even if we are not explicitly dealing with a predicate for $\Bbb N$), are we inevitably admitting Peano axioms for $\Bbb N$ indeed?"

$\endgroup$
2
  • 1
    $\begingroup$ The proofs in Enderton's book, like almost all mathematics, don't specify the specific axioms being used. It is safe to pretend that the entire book assumes ZFC, because all the proofs could be formalized into that system. This not strictly necessary - we could view the proofs as being formalized in some other system if we preferred. However, the point of the proofs Enderton presents is not to study the axioms required to prove hist theorems, the point is simply to prove the mathematical theorems. This is the same as most other mathematical proofs. $\endgroup$
    – Carl Mummert
    Mar 12, 2018 at 10:51
  • $\begingroup$ @CarlMummert Thanks. I see. $\endgroup$
    – Eric
    Mar 12, 2018 at 10:57

1 Answer 1

Reset to default
1
$\begingroup$

Not necessarily.

See Structural induction:

Structural induction is a proof method that is used in mathematical logic, computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural numbers.

Structural induction is used to prove that some proposition $P(x)$ holds for all $x$ of some sort of recursively defined structure, such as formulas, lists, or trees. A well-founded partial order is defined on the structures ("subformula" for formulas, "sublist" for lists, and "subtree" for trees). The structural induction proof is a proof that the proposition holds for all the minimal structures, and that if it holds for the immediate substructures of a certain structure $S$, then it must hold for $S$ also.

$\endgroup$
6
  • $\begingroup$ Do we need to prove the validity of "Structural induction" itself? If so, does such proof get rid of the traditional mathematical induction (and/or Peano axioms for $\Bbb N$)? $\endgroup$
    – Eric
    Mar 12, 2018 at 10:34
  • $\begingroup$ @Eric - it depends on the context... we cannot prove all. In set theory, induction is proved (both structural and mathematical). $\endgroup$
    – Mauro ALLEGRANZA
    Mar 12, 2018 at 10:36
  • $\begingroup$ I see the point. Actually the construction sequence in Enderton's book is formalized under ZFC, and so the induction is justified (to be clear, included as an axiom) by the "ZFC axiom". Is it? $\endgroup$
    – Eric
    Mar 12, 2018 at 10:37
  • $\begingroup$ @Eric - Yes; recursion is justified (i.e. proved from axioms) in $\mathsf {ZFC}$. See Enderton, page 73. $\endgroup$
    – Mauro ALLEGRANZA
    Mar 12, 2018 at 10:41
  • 1
    $\begingroup$ @Eric - as said above, we have to start from somewhere. Our intuition about the natural numbers (formalized with Peano's axioms) is probably the "best and deepest" intuition we have. At the intuitive level, it is the source for any other "more abstract" form of induction. It is hard to mantain that e.g. the Axiom of infinity has any ground "outside" of our intuition about the succession of natural numbers. $\endgroup$
    – Mauro ALLEGRANZA
    Mar 12, 2018 at 10:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .