Vis at følgende sekvenser er valide.
De er løst i Coq. Flere af dem kan findes som fitchbeviser under teori/logik/udsangslogik i bevisteorien og under ækvivalenser.
Require Import Classical. Variables p q r s t u n h c : Prop. (* a *) Lemma PBCa : (~p -> False) -> p. tauto. Qed. Goal (~p -> p) -> p. intro H. apply PBCa. intro H0. absurd p. exact H0. apply H. exact H0. (* b *) Goal ~p -> p -> q. intro H. intro H0. absurd p. exact H. exact H0. (* c *) Goal p \/ q -> ~q -> p. intro H. intro H0. destruct H. exact H. absurd q. exact H0. exact H. (* d *) Goal ~p -> (p -> (p -> q)). intro H. intro H0. absurd p. exact H. exact H0. (* e *) Goal ~(p -> q) -> q -> p. intro H. intro H0. absurd (p -> q). exact H. intro H1. exact H0. (* f *) Lemma LEMf : (p \/ ~p). tauto. Qed. Goal (p -> q) -> ~p \/ q. intro H. assert (p \/ ~p). apply LEMf. destruct H0. right. apply H. exact H0. left. exact H0. (* g *) Goal ~p \/ q -> (p -> q). intro H. intro H0. destruct H. absurd p. exact H. exact H0. exact H. (* h *) Goal (p -> (q \/ r)) -> ~q -> ~r -> ~p. intro H. intro H0. intro H1. intro. assert (q \/ r). apply H. exact H2. destruct H3. absurd q. exact H0. exact H3. absurd r. exact H1. exact H3. (* i *) Goal ((c /\ n) -> t) -> h /\ ~s -> (h /\ (~(s \/ c) -> p)) -> (n /\ ~t) -> p. intro H. intro H0. intro H1. intro H2. apply H1. intro. destruct H3. absurd s. apply H0. exact H3. absurd t. apply H2. apply H. split. exact H3. apply H2. (* j1 *) Goal ~(r \/ s -> q) /\ (r \/ s -> q) -> (p -> q) /\ ~(p -> q). intro H. exfalso. absurd (r \/ s -> q). apply H. apply H. (* j2 *) Goal (p -> q) /\ ~(p -> q) -> ~(r \/ s -> q) /\ (r \/ s -> q). intro H. exfalso. absurd (p -> q). apply H. apply H. (* k *) Goal q -> (p /\ q) \/ (~p /\ q). intro H. assert (p \/ ~p). apply LEMf. destruct H0. left. split. exact H0. exact H. right. split. exact H0. exact H. (* l *) Goal ~(p /\ q) -> ~p \/ ~q. intro H. assert (p \/ ~p). apply LEMf. destruct H0. right. intro. absurd (p /\ q). exact H. split. exact H0. exact H1. left. exact H0. (* m *) Goal (p /\ q -> r) -> (p -> r) \/ (q -> r). intro H. assert (p \/ ~p). apply LEMf. destruct H0. right. intro H1. apply H. split. exact H0. exact H1. left. intro H1. absurd p. exact H0. exact H1. (* n *) Goal p /\ q -> ~(~p \/ ~q). intro H. intro. destruct H0. absurd p. exact H0. apply H. absurd q. exact H0. apply H. (* o *) Lemma PBCo : (~q -> False) -> q. tauto. Qed. Goal ~(~p \/ ~q) -> p /\ q. intro H. split. apply PBCa. intro H0. absurd (~p \/ ~q). exact H. left. exact H0. apply PBCo. intro H0. absurd (~p \/ ~q). exact H. right. exact H0. (* p *) (* Uden brug af LEM *) Lemma PBCp : (~(~p \/ q) -> False) -> ~p \/ q. tauto. Qed. Goal (p -> q) -> (~p \/ q). intro H. apply PBCp. intro H0. absurd (~p \/ q). exact H0. left. intro. absurd (~p \/ q). exact H0. right. apply H. exact H1. (* q *) (* Ved at bruge LEM *) Lemma LEMq : (p -> q) \/ ~(p -> q). tauto. Qed. Goal (p -> q) \/ (q -> r). assert ((p -> q) \/ ~(p -> q)). apply LEMq. destruct H. left. exact H. right. intro H0. absurd (p -> q). exact H. intro H1. exact H0. (* r *) Lemma MTr : (~q -> ~r) -> r -> q. tauto. Qed. Goal (p -> q) -> (~p -> r) -> (~q -> ~r) -> q. intro H. intro H0. intro H1. assert (p \/ ~p). apply LEMf. destruct H2. apply H. exact H2. apply MTr. exact H1. apply H0. exact H2. (* s *) Goal (p -> q) -> (r -> ~t) -> (q -> r) -> p -> ~t. intro H. intro H0. intro H1. intro H2. apply H0. apply H1. apply H. exact H2. (* t *) Lemma MTt : (s -> ~p) -> p -> ~s. tauto. Qed. Goal ((p -> q) -> r) -> (s -> ~p) -> t -> (~s /\ t -> q) -> r. intro H. intro H0. intro H1. intro H2. apply H. intro H3. apply H2. split. apply MTt. exact H0. exact H3. exact H1. (* u *) Lemma MTu1 : (s -> p) -> ~p -> ~s. tauto. Qed. Lemma MTu2 : (t -> q) -> ~q -> ~t. tauto. Qed. Lemma LEMu : q \/ ~q. tauto. Qed. Goal (s -> p) \/ (t -> q) -> (s -> q) \/ (t -> p). intro H. assert (p \/ ~p). apply LEMf. destruct H. destruct H0. right. intro H1. exact H0. left. intro H1. absurd s. apply MTu1. exact H. exact H0. exact H1. assert (q \/ ~q). apply LEMu. destruct H1. left. intro H2. exact H1. right. intro H2. absurd t. apply MTu2. exact H. exact H1. exact H2. (* v *) Goal ((p /\ q) -> r) -> (r -> s) -> (q /\ ~s) -> ~p. intro H. intro H0. intro H1. intro. absurd s. apply H1. apply H0. apply H. split. exact H2. apply H1.