Peano arithmetic

In this course, all theorems must be proved in the following context of hypotheses, which corresponds to Peano's axioms of arithmetic (without induction):

∀ x : ℕ. 0 ≠ x⊕1,
∀ x : ℕ. ∀ y : ℕ. x⊕1 = y⊕1 ⇒ x = y,
∀ x : ℕ. x + 0 = x,
∀ x : ℕ. ∀ y : ℕ. x + y⊕1 = (x + y)⊕1,
∀ x : ℕ. x ⋅ 0 = 0,
∀ x : ℕ. ∀ y : ℕ. x ⋅ y⊕1 = (x ⋅ y) + x

Induction

Proofs by induction can be made by double clicking on a green item (of type nat). The goal is then duplicated; in the first version you find an additional equation that the item is equal to 0, in the second goal, it is a successor and you can find the induction hypothesis.

Equality

Goals of the form x=x are proved by double-clicking on them.

Hypotheses of the form a=b can be dragged on a goal in order to replace (an) occurence(s) of b by a. One can first select the occurences which are to be rewritten in the goal, or the left (resp. right) hand part of the equation in order to specify a left-to-right (resp. right-to-left) rewrite.

Pretty-Printing

The syntax x⊕n stands for the n-th successor of x. Closed terms are written as standard numerals. For instance 1 stands for 0⊕1, 2 stands for 1⊕1, 3 for 2⊕1 or 1⊕2, etc...

Exercises

Standard of truth

; forall x : nat. ~(Z() = S(x)), forall x : nat. forall y : nat. S(x) = S(y) -> x = y, forall x : nat. add(x, Z()) = x, forall x : nat. forall y : nat. add(x, S(y)) = S(add(x, y)), forall x : nat. mult(x, Z()) = Z(), forall x : nat. forall y : nat. mult(x, S(y)) = add(mult(x, y), x) |- add(S(Z()), S(Z())) = S(S(Z()))

Courses