Deduzione naturale al I ordine

[JoyJoy1]

Ciao a tutti,
sto cercando di capire come si svolge la deduzione naturale per i linguaggi del primo ordine, ma non mi sono chiare queste cose:
-parto dal basso verso l'alto e via via devo scaricare qualcosa utilizzando le regole elementari e condizionali, giusto?
-quando e' scritto che si scarica significa in un certo senso che devo semplificare utilizzando sempre le famose regole?Quando mi devo fermare?

grazie per i chiarimenti

[pic2]

Per quel poco che ne ho visto, è buona cosa iniziare con degli esempi. Ma lascio a te di postarli, poi vediamo come fare le dimostrazioni.

In teoria, l'obiettivo è quello di lasciare in alto (cioè senza nulla sopra) soltanto le ipotesi, e in basso la tesi. Tutte le altre ipotesi che assumi le devi in un qualche modo scaricare. E lo si fa attraverso le regole di eliminazione.

[JoyJoy1]

dovrei risolvere questo esercizio ma non saprei da dove iniziare:

dimostrare usando il calcolo della deduzione naturale che la formula seguente e' valida

[∃y(B(y) → C (y)) or ∀x B(x)] → ∃ x C(x)

help me!!

[pic2]

Sicuro? Se metti B= vero e C = falso ottieni Vero-> falso...

[JoyJoy1]

ehmm..
dovrei dimostrarlo con il metodo della deduzione naturale e no con la tabella di verita'...
grazie lo stesso!

[pic2]

La mia osservazione era per dire che quella frase è falsa. Di solito si dimostrano le cose vere. Quindi, a mio avviso, c'è un errore nel testo.


Domanda: studi informatica in quale città?

[JoyJoy1]

Mi spiace ma la formula e' valida (ho davanti a me la soluzione del prof) pero' vorrei capire come ha fatto ad arrivarci..ma non fa niente
ciauz

[fields1]

"JoyJoy":[∃y(B(y) → C (y)) or ∀x B(x)] → ∃ x C(x)

Un modo per renderla vera e' sostituire l'or con l'implica e cambiare le parentesi:

∃y(B(y) → C (y)) → [∀x B(x) → ∃ x C(x)]

[pic2]

Oppure sostituire or con and (che di fatto è equivalente alla soluzione di Fields)