BC1b: Inne spójniki? [TODO]
From Typonomikon Require Export BC1a.
Różnica między "lub" i "albo" (TODO)
Definition xor (A B : Prop) : Prop :=
(A /\ ~ B) \/ (~ A /\ B).
Infix "`xor`" := xor (at level 85, right associativity).
Section xor_lemmas.
Context (P Q R : Prop).
Lemma xor_True_l :
True `xor` P <-> ~ P.
Lemma xor_True_r :
P `xor` True <-> ~ P.
Lemma xor_False_l :
False `xor` P <-> P.
Lemma xor_False_r :
P `xor` False <-> P.
Lemma xor_True_l' :
P -> P `xor` Q <-> ~ Q.
Lemma xor_True_r' :
Q -> P `xor` Q <-> ~ P.
Lemma xor_False_l' :
~ P -> P `xor` Q <-> Q.
Lemma xor_False_r' :
~ Q -> P `xor` Q <-> P.
Lemma xor_spec :
xor P Q <-> (P \/ Q) /\ (~ P \/ ~ Q).
Lemma xor_irrefl :
P `xor` P <-> False.
Lemma xor_irrefl_true :
P -> Q -> P `xor` Q <-> False.
Lemma xor_irrefl_false :
~ P -> ~ Q -> P `xor` Q <-> False.
Lemma xor_comm :
P `xor` Q <-> Q `xor` P.
Lemma Irrefutable_xor_assoc :
~ ~ (P `xor` (Q `xor` R) <-> (P `xor` Q) `xor` R).
Lemma or_xor :
P `xor` Q -> P \/ Q.
Lemma and_xor_l :
(P `xor` Q) /\ R <-> (P /\ R) `xor` (Q /\ R).
Lemma and_xor_r :
P /\ (Q `xor` R) <-> (P /\ Q) `xor` (P /\ R).
Lemma Irrefutable_not_xor_l :
~ ~ (~ (P `xor` Q) <-> ~ P `xor` Q).
Lemma Irrefutable_not_xor_r :
~ ~ (~ (P `xor` Q) <-> P `xor` ~ Q).
Lemma Irrefutable_xor_not :
~ ~ ((~ P) `xor` ~ Q -> P `xor` Q).
Lemma not_iff_xor :
xor P Q -> ~ (P <-> Q).
Lemma Irrefutable_xor_not_iff :
~ ~ (~ (P <-> Q) -> xor P Q).
Lemma xor_not_conv :
P `xor` Q -> ~ P `xor` ~ Q.
Lemma xor_isolation :
(P /\ ~ Q) `xor` (P /\ Q) -> P.
Lemma Irrefutable_xor_isolation_conv :
~ ~ (P -> (P /\ ~ Q) `xor` (P /\ Q)).
Lemma Irrefutable_xor_cotrans :
~ ~ (xor P Q -> xor P R \/ xor Q R).
Lemma Irrefutable_dd_and_xor :
~ ~ (P /\ (~ P `xor` Q) -> P /\ Q).
Lemma dd_and_xor_conv :
P /\ Q -> P /\ (~ P `xor` Q).
Lemma dd_or_xor_r :
P \/ (P `xor` Q) -> P \/ Q.
Lemma Irrefutable_dd_or_xor_r_conv :
~ ~ (P \/ Q -> P \/ (P `xor` Q)).
Lemma dd_impl_xor_r :
P -> (~ P `xor` Q) <-> P -> Q.
Lemma dd_impl_xor_l :
(P `xor` Q) -> Q <-> P -> Q.
End xor_lemmas.
Zdecyduj się pan, czyli spójnik "i/lub" (TODO)
Definition andor (P Q : Prop) : Prop :=
P \/ Q \/ (P /\ Q).
Infix "`andor`" := andor (at level 85, right associativity).
Section andor_lemmas.
Context (P Q R : Prop).
Lemma or_and :
P /\ Q -> P \/ Q.
Lemma andor_or :
P `andor` Q <-> P \/ Q.
End andor_lemmas.
Zdecyduj się pan po raz drugi, czyli spójnik "i/albo" (TODO)
Definition andxor (P Q : Prop) : Prop :=
P `xor` Q `xor` (P /\ Q).
Infix "`andxor`" := andxor (at level 85, right associativity).
Section andxor_lemmas.
Context (P Q R : Prop).
Lemma andxor_or :
(forall P : Prop, P \/ ~ P) ->
P `andxor` Q <-> P \/ Q.
Lemma Irrefutable_andxor_or :
~ ~ (P `andxor` Q <-> P \/ Q).
End andxor_lemmas.
Ani w tę ani we wtę, czyli negacja dysjunkcji (TODO)
Definition nor (P Q : Prop) : Prop :=
~ (P \/ Q).
Infix "`nor`" := nor (at level 85, right associativity).
Section nor_lemmas.
Context (P Q R : Prop).
Lemma nor_comm :
nor P Q <-> nor Q P.
Lemma not_nor_assoc :
exists P Q R : Prop,
nor (nor P Q) R /\ ~ nor P (nor Q R).
Lemma nor_True_l :
nor True P <-> False.
Lemma nor_True_r :
nor P True <-> False.
Lemma nor_False_l :
nor False P <-> ~ P.
Lemma nor_False_r :
nor P False <-> ~ P.
Lemma nor_antiidempotent :
nor P P <-> ~ P.
End nor_lemmas.
W nieco innej wersji (TODO)
Definition nor' (P Q : Prop) : Prop :=
~ P /\ ~ Q.
Notation "'neither' P 'nor' Q" := (nor' P Q) (at level 85, right associativity).
Section nor'_lemmas.
Context (P Q R : Prop).
Lemma nor'_comm :
nor' P Q <-> nor' Q P.
Lemma not_nor'_assoc :
exists P Q R : Prop,
nor' (nor' P Q) R /\ ~ nor' P (nor' Q R).
Lemma nor'_True_l :
nor' True P <-> False.
Lemma nor'_True_r :
nor' P True <-> False.
Lemma nor'_False_l :
nor' False P <-> ~ P.
Lemma nor'_False_r :
nor' P False <-> ~ P.
Lemma nor'_antiidempotent :
nor' P P <-> ~ P.
Równoważność
Lemma nor_nor' :
P `nor` Q <-> neither P nor Q.
End nor'_lemmas.
nand, czyli negacja koniunkcji
Definition nand (P Q : Prop) : Prop :=
~ (P /\ Q).
Infix "`nand`" := nand (at level 85, right associativity).
Section nand_lemmas.
Context (P Q R : Prop).
Lemma nand_comm :
nand P Q <-> nand Q P.
Lemma not_nand_assoc :
exists P Q R : Prop,
nand (nand P Q) R /\ ~ nand P (nand Q R).
Lemma nand_True_l :
nand True P <-> ~ P.
Lemma nand_True_r :
nand P True <-> ~ P.
Lemma nand_False_l' :
nand False P.
Lemma nand_False_l :
nand False P <-> True.
Lemma nand_False_r :
nand P False <-> True.
Lemma nand_antiidempotent :
nand P P <-> ~ P.
End nand_lemmas.
Antyimplikacja, czyli negacja implikacji
Definition nimpl (P Q : Prop) : Prop :=
~ (P -> Q).
Infix "`nimpl`" := nimpl (at level 85, right associativity).
Section nimpl_lemmas.
Context (P Q R : Prop).
Lemma nimpl_False_l :
~ nimpl False P.
Lemma nimpl_False_r :
nimpl P False <-> ~ ~ P.
Lemma nimpl_True_l :
nimpl True P <-> ~ P.
Lemma nimpl_True_r :
~ nimpl P True.
Lemma nimpl_conv :
nimpl (~ Q) (~ P) -> nimpl P Q.
Lemma nimpl_conv' :
nimpl P Q -> nimpl (~ Q) (~ P).
End nimpl_lemmas.
Zadania (TODO)
Ćwiczenie (conditioned disjunction)
Wikipedia podaje poniższą definicję pewnego dziwnego spójnika:
Definition conditioned_disjunction (P Q R : Prop) : Prop :=
(Q -> P) /\ (~ Q -> R).
Wyraź za jego pomocą wszystkie podstawowe spójniki, tj. implikację, dysjunkcję,
koniunkcje i negację.
Udowodnij też garść twierdzeń mówiących, co się stanie, gdy za
P,
Q lub
R
wstawić
True lub
False.