4 Compilare i seguenti campi:
23 Per digitare i connettivi logici:
28 * `⇒` : `=>`, `\Rightarrow`
32 Per digitare i quantificatori:
37 I termini, le formule e i nomi delle ipotesi
38 ============================================
40 * I termini quantificati da `∀` e `∃`, quando argomenti di
41 una regola, vengono scritti tra `{` e `}`.
43 * Le formule, quando argomenti di
44 una regola, vengono scritti tra `(` e `)`.
46 * I nomi delle ipotesi, quando argomenti di
47 una regola, vengono scritti tra `[` e `]`.
53 include "didactic/support/natural_deduction.ma".
55 theorem pippo : (∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y.
56 apply rule (prove ((∀x.P (f x) ∧ Q x) ⇒ (∃x.Q x) ⇒ ∃y.P y));
58 apply rule (⇒_i [h1] ((∃x.Q x) ⇒ ∃y.P y));
59 apply rule (⇒_i [h2] (∃y.P y));
60 apply rule (∃_e (∃x.Q x) {t} [h3] (∃y.P y));
61 [ apply rule (discharge [h2]);
62 | apply rule (let ft ≝ (f t) in ∃_i {ft} (P ft));
63 apply rule (∧_e_l (P (f t) ∧ Q t));
64 apply rule (∀_e {t} (∀x.P (f x) ∧ Q x));
65 apply rule (discharge [h1]);