LK gentzen system solution (ita)

Non valido
Devo trovare un contromodello in modo che sia vero: A(t) → C(t) )D (−) : D −→ {0, 1}
Banalmente vale per qualsiasi modello in cui il predicato A!=C
D ≡ Nat
A(z)^D(d) = 1 sse d>1
C(z)^D(d) = 1 sse d<=1

È soddisfacibile per i modelli in cui A==C, per esempio:
D ≡ Nat
A(z)^D(d) = 1 sse d>1
C(z)^D(d) = 1 sse d>1

    non termina              ax id                       ax id                   non termina
Schifo, A(w) ⊢ C(w)      Schifo, C(w) ⊢ C(w)        Schifo, A(w) ⊢ A(w)      Schifo, C(w) ⊢ A(w)
____________________________________________ vS     ______________________________________________ vS
Schifo, A(w) ∨ C(w) ⊢ C(w)                          Schifo, A(w) ∨ C(w) ⊢ A(w)
______________________________ ¬S                   ______________________________ ¬S
Schifo, A(w) ∨ C(w), ¬C(w)  ⊢                       Schifo, A(w) ∨ C(w), ¬A(w) ⊢
__________________________________________________________________________________ vS
Schifo=[∀y ( ¬C(w) ∨ ¬A(y) ), ∀x ∀y ( ¬C(x) ∨ ¬A(y) )], A(w) ∨ C(w), ¬C(w) ∨ ¬A(w)  ⊢
_______________________________________________________________________________________ScS
A(w) ∨ C(w), ∀x ∀y ( ¬C(x) ∨ ¬A(y) ), ∀y ( ¬C(w) ∨ ¬A(y) ),  ¬C(w) ∨ ¬A(w)  ⊢
_______________________________________________________________________________ ∀S (nessuna restrizione)
A(w) ∨ C(w), ∀x ∀y ( ¬C(x) ∨ ¬A(y) ), ∀y ( ¬C(w) ∨ ¬A(y) )  ⊢
_______________________________________________________________ ∀S (nessuna restrizione)
A(w) ∨ C(w), ∀x ∀y ( ¬C(x) ∨ ¬A(y) )  ⊢
_________________________________________ ScS
∀x ∀y ( ¬C(x) ∨ ¬A(y) ),  A(w) ∨ C(w) ⊢
_____________________________________________ ∃S y può diventare w perchè non è libera
∀x ∀y ( ¬C(x) ∨ ¬A(y) ), ∃y ( A(y) ∨ C(y) ) ⊢
_____________________________________________ ¬D
∀x ∀y ( ¬C(x) ∨ ¬A(y) ) ⊢ ¬∃y ( A(y) ∨ C(y) )