[General boards] [Winter 2019 courses] [Fall 2018 courses] [Summer 2018 courses] [Older or newer terms]

Confused about Question 344 - Fixed Point Construction


I’ve been following along the example in the textbook for the fixed point construction of pow but i’m at a loss as to how to solve this question. Specifically, how are we supposed to use the statements in (a) and (b) to define nat?

For the fixed point construction of pow we use the definition of nat to define pow, but for this question we are trying to define nat. So it seems strange to me that both statements span over nat and that we then use these statements to define nat.

Any sort of help would be greatly appreciated!


We can define pow by fixed-point construction and fixed-point induction. Here are those two axioms.
(pow fixed-point construction) pow = 1, 2×pow
(pow fixed-point induction) B = 1, 2×B ⇒ pow: B
These axioms do not use nat.

In Exercise 344, we are defining nat. We use
(nat fixed-point construction) nat = 0, nat+1
and either one of the two axioms given in the question. Let’s take part (a).
(a) ∀n: nat· 0 ≤ n < n+1
Since (a) is part of the definition of nat, it should mention nat, and it does. It seems to bother you that (a)'s use of nat is as a domain of quantification, but it can use it that way. It is indeed an unusual way to define nat. It is saying that nat is the bunch such that for all its elements n, 0 ≤ n < n+1.

To prove that (nat fixed-point construction) plus (a) together define nat, just use those two to prove the axioms we have previously used to define nat. Prove
(nat fixed-point construction) ∧ (a) ⇒ (nat fixed-point construction) ∧ (nat fixed-point induction)
And we can simplify that to
(nat fixed-point construction) ∧ (a) ⇒ (nat fixed-point induction)
For 344(b), Prove
(nat fixed-point construction) ∧ (b) ⇒ (nat fixed-point induction)
Or, after doing part (a), part (b) can be
(nat fixed-point construction) ∧ (b) ⇒ (a)


I should add that these proofs don’t look easy to me. Maybe that’s why I didn’t do the exercise.


Oh okay I think I understand now, thanks!