(** 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.