Library ex5
Blatt 5 —- Logic
SemProg SoSe 2013, Set 5
Require Export Logic.
Exercise 1: 5 points (or_distributes_over_and)
Definition or_distributes_over_and_1 : forall P Q R : Prop,
P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R) := admit.
Definition or_distributes_over_and_2 : forall P Q R : Prop,
(P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R) := admit.
Exercise 2: 5 points (True)
Inductive True : Prop := .
Definition true_top : forall P, P -> True := admit.
Definition true_prem_l : forall P, (True -> P) -> P := fun P h => admit.
Definition true_prem_r : forall P, P -> (True -> P) := fun P h t => admit.
Exercise 3 : 7.5 points (georgous_is_trivial)
Definition georgous_is_trivial : forall n, gorgeous (n + 8) := admit.
Hint: remember how we proved equivalence of two definitions of evenness (or oddity) during the lecture? Which connective did we use? The lemma georgous_is_trivial_helper has to use the same connective. It should be a superficially stronger statement, yet obviously equivalent to forall n, gorgeous (n + 8). Of course, you're more than welcome to come up with another proof strategy
Exercise 4: 10 points (classical_equivalences)
Definition peirce := forall P Q: Prop,
((P->Q)->P)->P.
Definition classic := forall P:Prop,
~~P -> P.
Definition excluded_middle := forall P:Prop,
P \/ ~P.
Definition gen_ex_middle := forall P Q : Prop,
P \/ (P -> Q).
Definition de_morgan_not_and_not := forall P Q:Prop,
~(~P/\~Q) -> P\/Q.
Definition implies_to_or := forall P Q:Prop,
(P->Q) -> (~P\/Q).
Definition classical_contra := forall P Q : Prop,
(~Q -> ~P) -> (P -> Q).
Prove the following implications:
Theorem pei_cla : peirce -> classic.
Proof. Admitted.
Theorem cla_gem : classic -> gen_ex_middle.
Proof. Admitted.
Theorem gem_em : gen_ex_middle -> excluded_middle.
Proof. Admitted.
Theorem dm_ior : de_morgan_not_and_not -> implies_to_or.
Proof. Admitted.
Theorem em_dm : excluded_middle -> de_morgan_not_and_not.
Proof. Admitted.
Theorem ior_em: implies_to_or -> excluded_middle.
Proof. Admitted.
Theorem class_contr : classic -> classical_contra.
Proof. Admitted.
Theorem contr_class : classical_contra -> classic.
Proof. Admitted.
Optionally: can you prove the remaining ones?
Exercise 5 : 10 points (constructive_existential_quantification)
Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
(exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof. Admitted.
Theorem forallnot_equiv_notexists : forall (X:Type) (P : X -> Prop),
(forall x, ~ P x) <-> ~ (exists x, P x).
Proof. Admitted.
Theorem forallnotnot_equiv_notexistsnot : forall (X:Type) (P : X -> Prop),
(forall x, ~~ P x) <-> ~ (exists x, ~ P x).
Proof. Admitted.
Theorem notforallnot_equiv_notnotexists : forall (X:Type) (P : X -> Prop),
~(forall x, ~ P x) <-> ~~ (exists x, P x).
Proof. Admitted.
Theorem existsnot_notforall : forall (X:Type) (P : X -> Prop),
(exists x, ~ P x) -> ~ (forall x, P x).
Proof. Admitted.
Theorem forall_notexistsnot : forall (X:Type) (P : X -> Prop),
(forall x, P x) -> ~ (exists x, ~ P x).
Proof. Admitted.
Theorem constructive_Berg_quantif : forall (R : Prop) (X: Type) (P : X -> Prop), (exists x, P x -> R) -> (forall x : X, P x) -> R.
Proof. Admitted.
Exercise 6 : 7.5 points (notexistsnot_forall)
The converse of forall_notexistsnot requires classical logic. Compare it with forallnotnot_equiv_notexistsnot above!Theorem notexistsnot_forall :
excluded_middle ->
forall (X:Type) (P : X -> Prop),
~ (exists x, ~ P x) -> (forall x, P x).
Proof. Admitted.
This is the end of obligatory exercises
Here is an axiom significantly weaker than those of the classical logic:
BONUSAUFGABE: 10 points
Definition kuroda := forall (X:Type) (P : X -> Prop), (forall x, ~~ P x) -> ~~ (forall x, P x).
Prove this as a warm-up:
Theorem class_kuroda : classic -> kuroda.
Proof. Admitted.
As it turns out, this axioms also yields additional interactions between universal and existential quantification:
Theorem notforall_notnotexistsnot : kuroda -> forall (X:Type) (P : X -> Prop),
~ (forall x, P x) -> ~~ (exists x, ~ P x).
Proof. Admitted.
However, to prove really interesting ones, we need full strength of the classical logic:
Theorem notforallnot_exists : classic ->
forall (X:Type) (P : X -> Prop),
~ (forall x, ~ P x) -> (exists x, P x) .
Proof. Admitted.
Theorem notforall_existsnot : classic ->
forall (X:Type) (P : X -> Prop),
~ (forall x, P x) -> (exists x, ~ P x) .
Proof. Admitted.
And finally, if you feel some post-Berg-nostalgia, here is the full version of the Bergikirchweih paradox. Note that we need also to assume non-emptiness (inhabitation) of X for this one: we don't have it for free!
Theorem Berg_quantif : classic -> forall (R : Prop) (X: Type) (P : X -> Prop), (exists x: X, x=x) -> ((forall x : X, P x) -> R) -> (exists x, P x -> R).
Proof. Admitted.