+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
(* Esercizio 0
===========
con premesse multiple sono seguite da `[`, `|` e `]`.
Ad esempio:
- apply rule (∧_i (A∨B) ⊥);
+ apply rule (∧#i (A∨B) ⊥);
[ …continua qui il sottoalbero per (A∨B)
| …continua qui il sottoalbero per ⊥
]
scrivete sopra la linea che rappresenta l'applicazione della
regola stessa. Ad esempio:
- aply rule (∨_e (A∨B) [h1] C [h2] C);
+ aply rule (∨#e (A∨B) [h1] C [h2] C);
[ …prova di (A∨B)
| …prova di C sotto l'ipotesi A (di nome h1)
| …prova di C sotto l'ipotesi B (di nome h2)
assume A: CProp.
apply rule (prove (A ∨ ¬A));
apply rule (RAA [H] (⊥)).
-apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
[ apply rule (discharge [H]).
- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬¬A) (¬A));
- [ apply rule (¬_i [K] (⊥)).
- apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬¬A) (¬A));
+ [ apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
[ apply rule (discharge [H]).
- | apply rule (∨_i_r (¬A)).
+ | apply rule (∨#i_r (¬A)).
apply rule (discharge [K]).
]
- | apply rule (¬_i [K] (⊥)).
- apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ | apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
[ apply rule (discharge [H]).
- | apply rule (∨_i_l (A)).
+ | apply rule (∨#i_l (A)).
apply rule (discharge [K]).
]
]
lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
(*BEGIN*)
-apply rule (⇒_i [h1] (∀x.¬ P x));
-apply rule (∀_i {l} (¬P l));
-apply rule (¬_i [h2] (⊥));
-apply rule (¬_e (¬(∃x.P x)) (∃x.P x));
+apply rule (⇒#i [h1] (∀x.¬ P x));
+apply rule (∀#i {l} (¬P l));
+apply rule (¬#i [h2] (⊥));
+apply rule (¬#e (¬(∃x.P x)) (∃x.P x));
[ apply rule (discharge [h1]);
- | apply rule (∃_i {l} (P l));
+ | apply rule (∃#i {l} (P l));
apply rule (discharge [h2]);
]
(*END*)
lemma ex2: ¬(∀x.P x) ⇒ ∃x.¬ P x.
apply rule (prove (¬(∀x.P x) ⇒ ∃x.¬ P x));
(*BEGIN*)
-apply rule (⇒_i [h1] (∃x.¬ P x));
+apply rule (⇒#i [h1] (∃x.¬ P x));
apply rule (RAA [h2] (⊥));
-apply rule (¬_e (¬(∀x.P x)) (∀x.P x));
- [ apply rule (discharge [h1]);
- | apply rule (∀_i {y} (P y));
+apply rule (¬#e (¬(∀x.P x)) (∀x.P x));
+ [ apply rule (discharge [h2]);
+ | apply rule (∀#i {y} (P y));
apply rule (RAA [h3] (⊥));
- apply rule (¬_e (¬∃x.¬ P x) (∃x.¬ P x));
+ apply rule (¬#e (¬∃x.¬ P x) (∃x.¬ P x));
[ apply rule (discharge [h2]);
- | apply rule (∃_i {y} (¬P y));
+ | apply rule (∃#i {y} (¬P y));
apply rule (discharge [h3]);
]
]
lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
(*BEGIN*)
-apply rule (⇒_i [h1] (∀x.P x ⇒ Q c));
-apply rule (∀_i {l} (P l ⇒ Q c));
-apply rule (⇒_i [h2] (Q c));
-apply rule (⇒_e ((∃x.P x) ⇒ Q c) (∃x.P x));
+apply rule (⇒#i [h1] (∀x.P x ⇒ Q c));
+apply rule (∀#i {l} (P l ⇒ Q c));
+apply rule (⇒#i [h2] (Q c));
+apply rule (⇒#e ((∃x.P x) ⇒ Q c) (∃x.P x));
[ apply rule (discharge [h1]);
- | apply rule (∃_i {l} (P l));
+ | apply rule (∃#i {l} (P l));
apply rule (discharge [h2]);
]
(*END*)
lemma ex4: ((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c.
apply rule (prove (((∀x.P x) ⇒ Q c) ⇒ ∃x.P x ⇒ Q c));
(*BEGIN*)
-apply rule (⇒_i [h1] (∃x.P x ⇒ Q c));
-apply rule (∨_e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
+apply rule (⇒#i [h1] (∃x.P x ⇒ Q c));
+apply rule (∨#e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
[ apply rule (lem 0 EM);
- | apply rule (∃_i {y} (P y ⇒ Q c));
- apply rule (⇒_i [h4] (Q c));
- apply rule (⇒_e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
+ | apply rule (∃#i {y} (P y ⇒ Q c));
+ apply rule (⇒#i [h4] (Q c));
+ apply rule (⇒#e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
[ apply rule (discharge [h1]);
| apply rule (discharge [h3]);
]
- | apply rule (∃_e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
+ | apply rule (∃#e (∃x.¬P x) {y} [h4] (∃x.P x ⇒ Q c));
[ apply rule (lem 1 ex2 (¬(∀x.P x)));
apply rule (discharge [h3]);
- | apply rule (∃_i {y} (P y ⇒ Q c));
- apply rule (⇒_i [h5] (Q c));
- apply rule (⊥_e (⊥));
- apply rule (¬_e (¬P y) (P y));
+ | apply rule (∃#i {y} (P y ⇒ Q c));
+ apply rule (⇒#i [h5] (Q c));
+ apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬P y) (P y));
[ apply rule (discharge [h4]);
| apply rule (discharge [h5]);
]