4 Compilare i seguenti campi:
19 include "didactic/support/natural_deduction.ma".
21 theorem EM: ∀A. A ∨ ¬ A.
23 apply rule (prove (A ∨ ¬A));
24 apply rule (RAA [H] (⊥)).
25 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
26 [ apply rule (discharge [H]).
27 | apply rule (⊥_e (⊥));
28 apply rule (¬_e (¬¬A) (¬A));
29 [ apply rule (¬_i [K] (⊥)).
30 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
31 [ apply rule (discharge [H]).
32 | apply rule (∨_i_r (¬A)).
33 apply rule (discharge [K]).
35 | apply rule (¬_i [K] (⊥)).
36 apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
37 [ apply rule (discharge [H]).
38 | apply rule (∨_i_l (A)).
39 apply rule (discharge [K]).
45 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
46 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
47 apply rule (⇒_i [H] (¬A ∨ ¬B));
48 apply rule (RAA [K] (⊥));
49 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
50 [ apply rule (discharge [K]).
51 | apply rule (∨_i_l (¬A));
52 apply rule (¬_i [L] (⊥)).
53 apply rule (¬_e (¬B) (B));
54 [ apply rule (¬_i [M] (⊥)).
55 apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
56 [ apply rule (discharge [H]).
57 | apply rule (∧_i (A) (B));
58 [ apply rule (discharge [L]).
59 | apply rule (discharge [M]).
62 | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
63 [ apply rule (lem EM);
66 | apply rule (discharge [h1]);