@user525966 It depends on where the induction is. First you should understand what exactly is induction in PA:

Then the messages starting here:

After you understand and can use induction in PA, then we can talk about induction in other places.

@user525966 That is why I said I am not in favour of attempting to learn about logic before one can even use logic. My criterion of being able to use logic includes being able to prove the theorem I stated in the above messages within PA.

I will answer your question briefly now, but it will make little sense until you actually can use logic. Induction always refers to some collection of axioms, and exactly what that is depends on what the base system is. For PA, the base system is first-order logic plus the non-logical symbols 0,1,+,·,<, and hence the induction schema for PA is as described in the above-linked messages.

When you study logic as a mathematical object, you must yourself be working in some foundational system, which may or may not support induction (in whatever sense). If it does not, then you would be simply unable to prove certain things, including the deduction theorem for first-order logic.

So I am going to give you homework. Use PA to prove the theorem I stated in Fitch-style or sequent-style. Once you can complete such proofs on your own, you will not only truly understand the nature of induction, but also you will see why the induction that is often done in introductory logic textbooks is nebulous and imprecise, because they often do not even set out the foundational system (or they do not adhere to it).

Feel free to ask me for help if you get stuck. But I want you to make a proper effort to learn an actual deductive system. You can use this Fitch-style system or this sequent-style system. If you use something else, you must provide me with a public link to a full description of all the rules. Read the linked messages for the axioms of PA.

@famesyasd If you do it this way, using recursion repeatedly, you either need choice or uniqueness of the recursive function. But you can avoid both via the trick I mentioned earlier:

In other words, your way is to define · pointwise via recursion at each point. My trick applied here would be to define · by defining the multiply-by-y function for each y via recursion.

@famesyasd That would be like the type-theoretic approach, where "x in S" just means "x is of type S" and you still have cartesian product types and function types. If you do not axiomatize ordering as part of PA, you will have to define it via something like "forall m,n in N ( m<n iff exists b in N ( m+b=n and m!=n ) )" as you said.

There are two issues here. Firstly, I am not in favour of non-algebraic axiomatizations of PA, for both pragmatic and philosophical reasons.

The pragmatic reason is obvious; we intuitively understand and need to often use the linear ordering properties of N, so might as well build it in. The philosophical reason is that ultimately the linear ordering structure is more fundamental than the successor operation structure. It makes no sense to axiomatize S to be injective and surjective except missing 0, unless we already had the desire to force it to be a linear chain!

(Even from the viewpoint of transfinite induction, well-orderings are not generated by the successor functions, whereas all are linear orders.)

Secondly, the reason why set theorists define ordering on ω to be ∈ is that it literally is the case because they chose a very particular choice of set and a very particular choice of successor function on that set. From the abstract viewpoint one should not tie the abstraction (PA) down to the implementation (such as von Neumann ordinals), and so it would be wrong to define ordering on N in terms of ∈.

@user21820 Prove that forall A subset N exists y in A forall x in A x >= y. [Well-ordering]
Given any A subset N.
    if forall y in A exists x in A x < y
        forall t t in M iff t in N and forall n in N (n < t) -> (n not in A) [subset axiom]
        0 in M.
        Given any k in M.
             k in N and forall n in N (n < k) -> (n not in A)
             Given any r in N
                  if r < S(k)
                        r <= k.
                        r < k or r = k.
                        if r < k

@famesyasd Correct. (A small issue is that the first "r not in A" is redundant. Also we usually omit all restated lines.)

We use this same proof structure to prove the purely logical well-ordering principle from induction. Yours is the version sitting inside a set theory. The purely logical versions are as follows:

Induction: For any property P of naturals, "P(n)" denotes "n satisfies P", and we have ( P(0) ∧ ∀n∈N ( P(n) ⇒ P(n+1) ) ⇒ ∀n∈N ( P(n) ) ).

Strong induction: For any property P of naturals, we have ( ∀n∈N ( ∀k∈N ( k<n ⇒ P(k) ) ⇒ P(n) ) ⇒ ∀n∈N ( P(n) ) ).

Well-ordering: For any property P of naturals, we have ∃n∈N ( P(n) ) ⇒ ∃m∈N ( P(m) ∧ ∀n∈N ( P(n) ⇒ n≥m) ).

Well-ordering 2: For any property P of naturals, we have ∃n∈N ( P(n) ) ⇒ ∃m∈N ( P(m) ∧ ∀n∈N ( n<m ⇒ ¬P(n) ) ).

All these are schemas 'outside' the foundational system. Induction and strong induction are equivalent under weak assumptions, and LeakyNun once gave a formal proof of the forward implication.

They are equivalent to both variants of well-ordering under slightly stronger assumptions, such as classical logic.

Note that these purely logical versions have nothing to do with set theory; the "∈" in the restricted quantifiers is just syntax. The core proof is still the same; if well-ordering fails for P then you can show by strong induction that every natural number does not satisfy P.

I mention this so that it is clear that you can perform strong induction and well-ordering over a weak system like PA, without even any notion of sets.

In particular, using the axioms of PA over classical logic you can prove any instance of any of the above schemas, and so the theory remains unchanged (conservative extension) if you add those schemas to any classical first-order theory that includes PA.

Better still, if you are working in higher-order arithmetic, then each of those schemas can once again be expressed as a single statement, for example:

Well-ordering in HOA: ∀P∈func(nat,bool) ( ∃n∈N ( P(n) ) ⇒ ∃m∈N ( P(m) ∧ ∀n∈N ( P(n) ⇒ n≥m) ) ).

And it is useful to note that you can actually prove:

∀P∈func(nat,bool) ( ∃n∈N ( P(n) ) ⇒ ∃!m∈N ( P(m) ∧ ∀n∈N ( P(n) ⇒ n≥m ) ) ).

Which means you can define min∈func(func(nat,bool),nat) so that min(P) is the minimum natural satisfying P if there is any at all:

∀P∈func(nat,bool) ( ∃n∈N ( P(n) ) ⇒ P(min(P)) ∧ ∀n∈N ( P(n) ⇒ n≥min(P) ) ) ).

@user21820

how is card(X) = A introduced? some predicate for X,A? so that "=" is part of its symbolic name? clearly this can't be a functional symbol if we take it to mean any set A with which X is in a bijection

Do you mean in a set theory? (too lazy to read everything above :P)

In most set theories with Choice A will be an initial ordinal, so it's uniquely determined by X.