(** Introduction to Formal Reasoning (G52IFR)
    Nuo Li and Nicolai Kraus

    T02 Predicate Logic
**)




Section Family.


Variable People : Set.

(** some people **)

Hypothesis Ann : People.
Hypothesis Kate : People.
Hypothesis Peter : People.


(** We have two predicates about the gender **)
Variables Male Female : People -> Prop.
(** Male x = "x is male" **)

Variables Child : People -> People -> Prop.
(** Child x y = "x is the Child of y" **)


(** Kate is the daughter of Ann **)
Hypothesis h1 : 


(** Kate and Peter are (half or full) siblings **)
Hypothesis h2 : 


(** Kate and Peter are 'full' siblings **)
Hypothesis h3 : 


(** same again! **)
Hypothesis h4 : 


(** No one is the parent of all the others **)
Hypothesis h5 :


(** There is someone with exactly one child **)
Hypothesis h6 : 










End Family.






Section Misc.

Variable A : Set.
Variable P : A -> Prop.
Variable Q : Prop.



Lemma curry_dependend : (exists x : A, P x) -> Q 
                      <->
           forall x : A, P x -> Q.




Lemma sym : forall x y : A, x = y -> y = x.



(** if there is much time, we can do the following: **)

Lemma TND_NNPP : (forall P : Prop, P \/ ~P) <-> (forall P : Prop, ~~P -> P).



Require Import Coq.Logic.Classical.

Lemma reductio_ad_absurdum : (forall P : Prop, ~~P -> P).


Lemma reductio_ad_absurdum2 : (forall P : Prop, ~~P -> P).


End Misc.