0
$\begingroup$

If I start by constructing the natural numbers formally in a reasonably standard way...

Type: NaturalNumber
Constructors: zero:NaturalNumber;successor(NaturalNumber):NaturalNumber

...rather than axiomatising them, then it is straightforward to derive the first eight Peano axioms as theorems, in the sense that it would be relatively easy to write a verifier to do it. I asked myself then why it isn't possible to derive the ninth axiom, namely the axiom of induction?

My motivation for this is that, if you axiomatise the natural numbers rather than construct them, then as I understand it the axiom of induction is necessary in order to exclude the possibility of non-standard sets of natural numbers. Put simply, it rules out the circle of dominoes and allows only the straight line of dominoes in the following picture:

Wikipedia: Domino effect visualizing exclusion of junk term by induction axiom.jpg

I'm aware of, although can hardly claim to be fully versed in, results such as Dedekind's, namely that with the axiom of induction stated using second order logic the Peano axioms define the natural numbers up to isomorphism. And I'm wondering whether these kinds of meta-logical arguments are needed at least to prove that such a proof as this isn't possible, perhaps?

$\endgroup$

closed as unclear what you're asking by Andrés E. Caicedo, Namaste, Leucippus, Daniel W. Farlow, JMP Jul 7 '17 at 4:51

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ I haven't defined precisely what my model of the natural numbers is, just thrown in some set theory and choice. I'm hoping this fuzziness will be tolerated. $\endgroup$ – James Smith May 7 '17 at 14:30
  • $\begingroup$ Look here for proofs of the first eight Peano axioms: github.com/jecs-imperial/Core-Mathematics/blob/master/…, where most of the proofs follow directly from the definitions I've given at the top of my question. $\endgroup$ – James Smith May 7 '17 at 15:19
  • $\begingroup$ I'm sad to say that it's all a bit of a mess at the moment. I plan to pull the Peano axioms out into a separate repository soon. You can find the Intuitionistic Logic definitions in the Propositional Logic repo, which is at least in a passable state: github.com/jecs-imperial/Propositional-Logic $\endgroup$ – James Smith May 7 '17 at 15:27
  • 1
    $\begingroup$ @JamesSmith: The communication problem, I think, is that for what you say "here is a construction of Nat", most mathematicians would say "let Nat be the free model of the algebraic theory with this constant and unary operation". $\endgroup$ – Excluded and Offended May 8 '17 at 13:32
  • 1
    $\begingroup$ ... and subsequently, would take $s$ as an operation. Its action on (one way to notate the the usual construction of) the free model would be that $s$ sends $[x]$ to $[s(x)]$. (I would normally use quotes to indicate 'between here lies a string of formal symbols' but I don't recall how to format them properly in mathmode) $\endgroup$ – Excluded and Offended May 8 '17 at 13:38
7
$\begingroup$

Yes, it is possible to prove that a "natural numbers type structure" satisfies the induction axiom. The proof will be carried out in the same set theory that is used to form the natural number type structure. The only challenge is to formalize the structure appropriately. There are many ways of specifying a "natural numbers type structure".

However, even though there are several ways to formalize inductively defined sets such as the one mentioned in the question, as long as care is taken to do it appropriately the nature of the inductive definition will ensure that the resulting structure satisfies induction. This is because, by nature, an inductive definition forms the smallest set possible. If the resulting set $S$ failed to satisfy the induction axiom because of some proper inductive subset, this would show that the resulting set $S$ is not actually as small as possible, leading to a contradiction.

For example, in the proof at the end of the question, we would look at the set $\{n : P(n)\}$. This would be a set that contains $0$ and is closed under successor. By the inductive definition of the construction, that set has to contain every number in the structure that was constructed - there is no need to worry about a least element or anything like that.

$\endgroup$
  • $\begingroup$ Carl, firstly let me write: I knew it! Let me mull over your answer, do some digging, and come back to you with questions if I may. $\endgroup$ – James Smith May 9 '17 at 17:58
  • $\begingroup$ Some more thoughts having read through your answer again...yes, I take your point, although I don't fully understand it yet, about the 'natural numbers type structure' essentially satisfying the induction axiom. $\endgroup$ – James Smith May 9 '17 at 18:42
  • $\begingroup$ One way I might put it is that if I extended the definition about to define a set of natural numbers, fuzzily creating what I refered to as a model, then the set would satisfy the induction axiom a priori. Again, I'm struggling for the words. $\endgroup$ – James Smith May 9 '17 at 18:44
  • $\begingroup$ The reason why I asked this question is that I don't want to build an induction axiom into Occam, because I want Occam to be more low level than that. But I understand that if I build in the capacity to construct terms, well, essentially inductively, I might end up doing that. I wish I could find the right words! But if I could, I would probably have the full and formal answer to my own question... $\endgroup$ – James Smith May 9 '17 at 18:46
  • 2
    $\begingroup$ The main issue with proving the induction axiom is that we need to specify which properties the structure is assumed to have, if induction is not assumed. In set theory, the assumption might be that there is no proper inductive subset. In other contexts, induction is taken to be a rule of inference corresponding to an inductive definition. So the main challenge is to clearly state what we do want to assume $\endgroup$ – Carl Mummert May 10 '17 at 21:05
3
$\begingroup$

Put simply, it rules out the circle of dominoes and allows only the straight line of dominoes...

Induction does not rule out such a circular structure on the natural numbers. In fact, induction can be shown to hold even on the set $M=\{0\}$ with $S(0)=0$. We would have:

$$\forall P\subset M:[0\in M \land \forall x\in P: S(x)\in P \implies P=M]$$

In Peano's axioms, it is the axiom $\forall x\in N: S(x)\ne 0$ that ensures an infinite, straight-line structure starting at $0$. Induction simply rules out the possibility of not being able to reach any particular number by repeated succession if we start at $0$.

I asked myself then why it isn't possible to derive the ninth axiom, namely the axiom of induction.

If you want to derive Peano's Axioms including the principle of induction, you can start by assuming the existence of an arbitrary Dedekind infinite set $X$. From any such set, we can extract at least one "copy" of the set of natural numbers. For any such set, there exists $x_0\in X$ and an injective but non-surjective function $f:X\to X$ such that $\forall x\in X: f(x)\ne x_0$.

It can then be shown that there exists a subset $N\subset X$ with $x_0 \in N$ such that $(N,f,x_0)$ satisfies Peano's axioms with $f$ being the usual successor function and $x_0$ being the "first element" of set $N$.

Informally, we would have $N=\{x_0, f(x_0), f(f(x_0)\cdots \}$.

$\endgroup$
  • 3
    $\begingroup$ The first paragraph should be a comment rather than an answer, and the second paragraph isn't relevant to the question. $\endgroup$ – Noah Schweber May 8 '17 at 21:16
  • 1
    $\begingroup$ The OP seemed to be interested in somehow deriving the induction principle, but he didn't seem to quite understand its actual role. I hope my answer will be helpful in his quest. $\endgroup$ – Dan Christensen May 8 '17 at 23:14
  • $\begingroup$ @NoahSchweber Think of it as a hint if not a complete answer. I believe hints are seen as legitimate answers here. $\endgroup$ – Dan Christensen May 9 '17 at 2:28
  • 3
    $\begingroup$ I'm certainly not against hints, I just don't think this addresses the OP's question at all. I think the mistake you point out is just a superficial error which doesn't reflect real misunderstanding on their part, and your second paragraph has no actual relevance to the question; but I'll let the OP decide. $\endgroup$ – Noah Schweber May 9 '17 at 2:39
  • $\begingroup$ It could be that I don't fully understand the role of induction and that my assertion that it 'rules out the circle of dominoes' is something of a simplification. However, $s(z)$ does not equal $z$, it equals $s(z)$, so I don't see what your counter example proves. Finally, your link to Wolfram's page on induction provides no useful information at all as far as I can see. The second paragraph also doesn't make sense to me but to be honest, I should probably give it a more careful read. $\endgroup$ – James Smith May 9 '17 at 8:56
-1
$\begingroup$

So, at last, I have what I think is an acceptable answer. I'll write out the vernacular and explain as I go along.

Firstly, the construction of the natural numbers (which would be imported from elsewhere):

Type NaturalNumber

Constructors zero:NaturalNumber;successor(NaturalNumber):NaturalNumber

Next, some abbreviations and declarations:

Abbreviations z for zero,s for successor,Nat for NaturalNumber

Metavariables R,S,T(Nat)

Contexts ρ,σ,τ(Nat)

Next, the rule itself, which you would need if you wanted to prove things by Induction. I'll leave off the proof for a moment:

Rule (Induction)
  Premises
    ρ ⊢ R::P(z)
    σ ⊢ S::P(k)=>P(s(k))
  Conclusion
    τ(n) ⊢ T(n)::P(n)

The first premise ρ ⊢ R::P(z) reads 'given a context ρ, the theorem R proves P(z)'. This is the propositions as types paradigm in action, if you like. The context is the axioms and proven theorems that are referenced by the theorem. Similarly for the second premise. So we are taking as premises for the rule the base case and the induction step. The conclusion τ(n) ⊢ T(n)::P(n) states that for each natural number n, a theorem T(n) can be constructed that proves P(n), given a context τ(n).

So the job is to define these contexts τ(n) and to construct the theorems T(n). I'll give the theorems first:

Theorem (T(z))
  P(z)
Proof
  P(z) from T

Theorem (T(s(k)))
  P(s(k))
Proof
  P(k)=>P(s(k)) from S
  P(k) from T(k)
Therefore
  P(s(k)) by ModusPonens

These are worth a few comments. They would not verify standalone, so to speak, because they both rely on contexts that won't be in the main context. The verifier might return something like the following message (recall that this question is about how to implement a verifier as much as anything):

Theorem T(z) verified but the conclusion P(z) has not been added to the 
main context because T is not in the main context.

These are generic theorems that are structurally correct but do not hold standalone. It should be clear that the context needed for the first to verify fully is just going to be ρ. Similarly for the second theorem. The context that it needs is going to be σ,T(k)::P(k). This leads to the recursive definition of the contexts, which is the crucial bit and comes at the top of the proof that follows:

let τ(z)=T
let τ(s(k))=S,T(k)::P(k)

After the above definitions the proof of the Induction rule itself is broken down into the cases n=z and n=s(k). I'll leave out the derivations which prove the implications for the moment, so as to get across the gist of the proof as a whole:

Proof
  ...
  n=z ∨ n=s(k)
  Suppose
    n=z
  Then
    ...
  Hence
    ρ(n) ⊢ T(n)::P(n)
  n=z => ρ(n) ⊢ T(n)::P(n)

  Suppose
    n=s(k)
  Then
    ...
  Hence
    ρ(n) ⊢ T(n)::P(n)
  n=s(k) => ρ(n) ⊢ T(n)::P(n)

Therefore 
  ρ(n) ⊢ T(n)::P(n) by ProofByCases

Now I'll write out the derivations themselves. Firstly for the case n=z:

  Suppose
    n=z
  Then
    ρ ⊢ R::P(z)
    τ(z) ⊢ R::P(z)
    τ(z) ⊢ T(z)::P(z)
  Hence
    τ(n) ⊢ T(n)::P(n)

In the derivation we begin by re-stating the first premise and then, since we have defined τ(z) to be ρ, the next line follows. And now note that the next line verifies. It reads 'theorem T(z) is a proof of P(z) given τ(z). Well, it verifies! Because given ρ we can prove R, whatever R happens to be, and since our own generic theorem T(z) relies on nothing but R, the assertion τ(z) ⊢ T(z)::P(z) holds. And since n is just z, we are done. For the case n=s(k), the reasoning is along similar lines.

Update: The complete proof is now here.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.