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]).
46 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
47 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
48 apply rule (⇒_i [H] (¬A ∨ ¬B));
49 apply rule (RAA [K] (⊥));
50 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬B));
51 [ apply rule (discharge [K]).
52 | apply rule (∨_i_l (¬A));
53 apply rule (¬_i [L] (⊥)).
54 apply rule (¬_e (¬B) (B));
55 [ apply rule (¬_i [M] (⊥)).
56 apply rule (¬_e (¬(A ∧ B)) (A ∧ B));
57 [ apply rule (discharge [H]).
58 | apply rule (∧_i (A) (B));
59 [ apply rule (discharge [L]).
60 | apply rule (discharge [M]).
63 | apply rule (∨_e (B ∨ ¬B) [h1] (B) [h2] (B));
64 [ apply rule (lem EM);
67 | apply rule (discharge [h1]);