BC4b: Logika klasyczna jako logika silnych i słabych spójników [TODO]


From Typonomikon Require Export BC4a.

Silna implikacja


Definition simpl (P Q : Prop) : Prop := ~ P \/ Q.

Lemma impl_simpl :
  forall P Q : Prop,
    simpl P Q -> (P -> Q).

Lemma simpl_simpl_impl :
  LEM ->
    forall P Q : Prop,
      simpl (simpl P Q) (P -> Q).

Lemma simpl_impl_classically :
  LEM ->
    forall P Q : Prop,
      (P -> Q) -> simpl P Q.

Lemma simpl_impl_tabu :
  (forall P Q : Prop, (P -> Q) -> simpl P Q) ->
    LEM.

Słaba implikacja


Definition wimpl (P Q : Prop) : Prop := ~ Q -> ~ P.

Lemma wimpl_alternative :
  forall P Q : Prop, wimpl P Q <-> ~ (P /\ ~ Q).

Lemma wimpl_impl :
  forall P Q : Prop,
    (P -> Q) -> wimpl P Q.

Lemma impl_wimpl_irrefutable :
  forall P Q : Prop,
    ~ ~ (wimpl P Q -> (P -> Q)).

Lemma wimpl_impl_classically :
  LEM ->
    forall P Q : Prop,
      wimpl P Q -> (P -> Q).

Lemma impl_wimpl_wimpl :
  forall P Q : Prop,
    wimpl (P -> Q) (wimpl P Q).

Lemma impl_wimpl_tabu :
  (forall P Q : Prop, wimpl P Q -> (P -> Q)) ->
    LEM.

Słaba dysjunkcja


Definition wor (P Q : Prop) : Prop := ~ P -> Q.

Lemma wor_or :
  forall P Q : Prop,
    P \/ Q -> wor P Q.

Lemma wor_introl :
  forall P Q : Prop,
    P -> wor P Q.

Lemma wor_intror :
  forall P Q : Prop,
    Q -> wor P Q.

Lemma wor_False_l :
  forall P : Prop,
    wor False P <-> P.

Lemma wor_False_r :
  LEM ->
    forall P : Prop,
      wor P False <-> P.

Lemma wor_True_l :
  forall P : Prop,
    wor True P <-> True.

Lemma wor_True_r :
  forall P : Prop,
    wor P True <-> True.

Lemma wor_assoc :
  forall P Q R : Prop,
    wor (wor P Q) R <-> wor P (wor Q R).

Lemma wor_comm :
  LEM ->
    forall P Q : Prop,
      wor P Q <-> wor Q P.

Lemma or_wor_classically :
  LEM ->
    forall P Q : Prop,
      wor P Q -> P \/ Q.

Lemma or_wor_tabu :
  (forall P Q : Prop, wor P Q -> P \/ Q) ->
    LEM.

Słaba dysjunkcja przemienna


Definition wor2 (P Q : Prop) : Prop := (~ P -> Q) \/ (~ Q -> P).

Lemma wor2_or :
  forall P Q : Prop,
    P \/ Q -> wor2 P Q.

Lemma wor_wor2 :
  LEM ->
    forall P Q : Prop,
      wor2 P Q -> wor P Q.

Lemma wor2_wor :
  forall P Q : Prop,
    wor P Q -> wor2 P Q.

Lemma wor2_introl :
  forall P Q : Prop,
    P -> wor2 P Q.

Lemma wor2_intror :
  forall P Q : Prop,
    Q -> wor2 P Q.

Lemma wor2_False_l :
  LEM ->
    forall P : Prop,
      wor2 False P <-> P.

Lemma wor2_False_r :
  LEM ->
    forall P : Prop,
      wor2 P False <-> P.

Lemma wor2_True_l :
  forall P : Prop,
    wor2 True P <-> True.

Lemma wor2_True_r :
  forall P : Prop,
    wor2 P True <-> True.

Lemma wor2_comm :
  forall P Q : Prop,
    wor2 P Q <-> wor2 Q P.

Lemma wor2_assoc :
  LEM ->
    forall P Q R : Prop,
      wor2 (wor2 P Q) R <-> wor2 P (wor2 Q R).

Lemma or_wor2_classically :
  LEM ->
    forall P Q : Prop,
      wor2 P Q -> P \/ Q.

Lemma or_wor2_tabu :
  (forall P Q : Prop, wor2 P Q -> P \/ Q) ->
    LEM.

Słaba koniunkcja


Definition aand (P Q : Prop) : Prop := ~ (~ P \/ ~ Q).

Lemma and_aand :
  forall P Q : Prop,
    P /\ Q -> aand P Q.

Lemma aand_and_classically :
  LEM ->
    forall P Q : Prop,
      aand P Q -> P /\ Q.

Lemma aand_and_tabu :
  (forall P Q : Prop, aand P Q -> P /\ Q) ->
    LEM.

Lemma aand_elim :
  forall P Q R : Prop,
    (P -> R) -> (Q -> R) -> (~ ~ R -> R) -> ~ (~ P /\ ~ Q) -> R.

Silna równoważność


Definition siff (P Q : Prop) : Prop := P /\ Q \/ ~ P /\ ~ Q.

Lemma iff_siff :
  forall P Q : Prop,
    siff P Q -> P <-> Q.

Lemma siff_iff :
  LEM ->
    forall P Q : Prop,
      P <-> Q -> siff P Q.

Lemma siff_iff_iff :
  LEM ->
    forall P Q : Prop,
      P <-> Q <-> siff P Q.

Lemma siff_siff_iff :
  LEM ->
    forall P Q : Prop,
      siff (siff P Q) (P <-> Q).

Lemma siff_xor :
  forall P Q : Prop,
    siff P Q -> xor P Q -> False.

Lemma siff_id :
  LEM ->
    forall P : Prop,
      siff P P.

Lemma siff_comm :
  LEM ->
    forall P Q : Prop,
      siff (siff P Q) (siff Q P).

Lemma siff_assoc :
  LEM ->
    forall P Q R : Prop,
      siff (siff (siff P Q) R) (siff P (siff Q R)).

Silna antyimplikacja


Definition snimpl (P Q : Prop) : Prop := P /\ ~ Q.

(* TODO: jakieś lematy *)

Definition NI : Prop :=
  forall P Q : Prop, ~ (P -> Q) -> P /\ ~ Q.

Lemma NI_LEM :
  NI -> LEM.

Definition wxor (P Q : Prop) : Prop := ~ (P <-> Q).

Lemma wxor_irrefl :
  forall P : Prop, ~ wxor P P.

Lemma wxor_comm :
  forall P Q : Prop, wxor P Q -> wxor Q P.

Lemma wxor_cotrans :
  LEM ->
    (forall P Q R : Prop, wxor P Q -> wxor P R \/ wxor Q R).

Lemma wxor_assoc :
  forall P Q R : Prop,
    wxor P (wxor Q R) <-> wxor (wxor P Q) R.

Lemma wxor_xor :
  forall P Q : Prop, xor P Q -> wxor P Q.

Lemma xor_wxor_classically :
  LEM ->
    forall P Q : Prop, wxor P Q -> xor P Q.

Lemma wxor_False_r_classically :
  LEM ->
    forall P : Prop, wxor P False <-> P.

Lemma wxor_False_l_classically :
  LEM ->
    forall P : Prop, wxor False P <-> P.

Lemma wxor_True_l :
  forall P : Prop, wxor True P <-> ~ P.

Lemma wxor_True_r :
  forall P : Prop, wxor P True <-> ~ P.

Klasyczna dysjunkcja (TODO)


Definition cor (P Q : Prop) : Prop :=
  ~ ~ (P \/ Q).

Lemma cor_in_l :
  forall P Q : Prop,
    P -> cor P Q.

Lemma cor_in_r :
  forall P Q : Prop,
    Q -> cor P Q.

Lemma cor_assoc :
  forall P Q R : Prop,
    cor (cor P Q) R <-> cor P (cor Q R).

Lemma cor_comm :
  forall P Q : Prop,
    cor P Q -> cor Q P.

Lemma cor_True_l :
  forall P : Prop,
    cor True P <-> True.

Lemma cor_True_r :
  forall P : Prop,
    cor P True <-> True.

Lemma cor_False_l :
  forall P : Prop,
    cor False P <-> ~ ~ P.

Lemma cor_False_r :
  forall P : Prop,
    cor P False <-> ~ ~ P.

Lemma cor_or :
  forall P Q : Prop,
    P \/ Q -> cor P Q.

Lemma cor_LEM :
  forall P : Prop,
    cor P (~ P).

Lemma or_cor_classically :
  LEM -> forall P Q : Prop, cor P Q -> P \/ Q.

Lemma or_cor_tabu :
  (forall P Q : Prop, cor P Q -> P \/ Q) ->
    LEM.

Lemma cor_spec :
  forall P Q : Prop,
    cor P Q <-> ~ (~ P /\ ~ Q).

Lemma cor_wor :
  forall P Q : Prop,
    wor P Q -> cor P Q.

Lemma cor_wor2 :
  forall P Q : Prop,
    wor2 P Q -> cor P Q.

Bonus: klasyczna koń-junkcja (TODO)


Lemma cand_and_LEM :
  (forall P Q : Prop, ~ ~ (P /\ Q) -> P /\ Q) ->
    LEM.

Bonus 2: klasyczny kwantyfikator egzystencjalny (TODO)


Lemma weak_ex_elim :
  forall (A : Type) (P : A -> Prop) (R : Prop),
    (forall x : A, P x -> R) -> (~ ~ R -> R) ->
      ~ (forall x : A, ~ P x) -> R.

Słaby kwantyfikator egzystencjalny


Definition wexists {A : Type} (P : A -> Prop) : Prop :=
  ~ forall x : A, ~ P x.

Lemma wexists_exists :
  forall {A : Type} (P : A -> Prop),
    ex P -> wexists P.

Lemma exists_wexists_classically :
  LEM ->
    forall {A : Type} (P : A -> Prop),
      wexists P -> ex P.

Lemma exists_wexists_tabu :
  (forall {A : Type} (P : A -> Prop), wexists P -> ex P)
    ->
  LEM.

Słaby kwantyfikator uniwersalny


Definition wforall {A : Type} (P : A -> Prop) : Prop :=
  ~ exists x : A, ~ P x.

Lemma wforall_forall :
  forall {A : Type} (P : A -> Prop),
    (forall x : A, P x) -> wforall P.

Lemma forall_wforall_classically :
  LEM ->
    forall {A : Type} (P : A -> Prop),
      wforall P -> forall x : A, P x.

Lemma forall_wforall_tabu :
  (forall {A : Type} (P : A -> Prop), wforall P -> forall x : A, P x)
    ->
  LEM.

Wymyśl to sam...

Ćwiczenie

Jeżeli jeszcze ci mało, spróbuj sam wymyślić jakieś spójniki logiczne, których nie ma w logice konstruktywnej ani klasycznej.
Zastanów się, czy taki spójnik ma sens matematyczny, czy nadaje się do użytku jedynie w językach naturalnych. Da się go jakoś wyrazić za pomocą znanych nam spójników, czy nie bardzo? Twój spójnik jest fajny czy głupi? Użyteczny czy bezużyteczny?