Section Predicate_calculus.

(* Some possible hints for Assignment 1 
part (vii) *)

Variable N:Set.
Variable zero:N.
Variable S:N -> N.

Hypothesis Peano3: (forall x y:N, S x = S y -> x=y).
Hypothesis Peano4: (forall x:N, ~ (S x = zero)).
Hypothesis IND: 
(forall P:N ->Prop,
 (P zero) -> (forall n:N, (P n) -> (P (S n))) 
 -> (forall n:N, P n)).


(* The following lemma may be useful
    to prove first *)

Lemma L1: (forall n:N, ~(S n = n)).

(* To prove the actual theorem it is helpful 
to introduce a new predicate that fixes one
of the arguments. *)
 
Definition Q (m:N) := (forall n:N, n = m \/ ~ (n = m)).

(* Now  the problem to be solved 
can be formulated as follows. Just replace
Q m by its definition. *)

Theorem EqDec: (forall m:N, Q m).

(* The definition of Q may be unfolded during a
proof using the "unfold" command, e.g. write 
"unfold Q" or "unfold Q in H" *)