Deduzione naturale e quantificatori

[cozzataddeo]

Ciao a tutti!
In questi giorni uggiosi di pioggia autunnale sto cercando di preparare l'esame di Logica Matematica, tuttavia tra i vari problemi su cui sto sbattendo la mia testa dura, ci sono gli esercizi di deduzione naturale in cui compaiono i quantificatori. Le dispense del prof. sono criptiche e stringate al riguardo e riportano un unico esempio semplicissimo mentre nei compiti in classe vengono richieste derivazioni che necissitano di qualche decina di passaggi... .
Ho provato a fare una rapida ricerca in rete ma non mi pare di aver trovato niente di utile (ho trovato invece materiale utile per la deduzione naturale senza i quantificatori, infatti quella parte ora mi è molto piú chiara).
Qualcuno di voi saprebbe indicarmi qualche link che potrebbe fare al caso mio?

Entrando nello specifico il primo ostacolo che incontro riguarda l'affermazione per cui la derivazione

$A/(\forallx.A)$

può essere fatta solo se "la $x$ non compare come variabile libera in nessuna delle ipotesi attive". La stessa frase è riportata per un altra regola che riguarda il quantificatore esistenziale. Il senso credo di averlo capito ma non ho capito invece come questa condizione influenzi l'esecuzione pratica delle derivazioni. Per questo motivo cerco degli esercizi relativamente semplici che possano chiarirmi innanzitutto questo aspetto.

Grazie!

[cozzataddeo]

Nessuno ha qualche minimo indizio al riguardo?
A dire il vero ieri, con gran fatica, ho trovato qualcosina in rete ma si tratta comunque di documenti abbastanza frammentari, per cui qualunque segnalazione è bene accetta!

Buona matematica a tutti!

[_Tipper]

Dato che qualunque segnalazione è ben accetta..

http://www.dii.unisi.it/~freno/didattic ... dicati.pdf

anche se dubito possano farti veramente comodo, dato che sono appunti di logica per un corso di AI...

[adaBTTLS1]

visto che grandi suggerimenti non sono venuti, mi associo a Tipper nel dire "...dato che qualunque segnalazione è ben accetta...", ma non ho da suggerire un link, vorrei proporre un confronto tra la mia interpretazione del simbolo e quella che invece è la tua idea (a proposito, mi sembrerebbe interessante la versione con il quantificatore esistenziale, perché non me la immagino analoga a quella con i quantificatore universale).
secondo me è una sorta di "trasposizione" del principio d'identità dalla logica proposizionale alla logica dei predicati: A è vero indipendentemente da qualsiasi ipotesi su x. è possibile usare il teorema A perché è sempre valido. questo è vero appunto se il teorema non contiene x tra i suoi predicati, cioè è indipendente da x. ciao.

[cozzataddeo]

Grazie per la segnalazione a Tipper e per l'interessamento ad adaBTTLS!
Questo fine settimana ho fatto un po' di chiarezza sull'uso dei quantificatori anche grazie a quei documenti frammentari scaricati dalla rete.
La frase in questione riguarda il fatto che per poter introdurre il quantificatore universale non ci devono essere ipotesi attive che vedano coinvolta la $x$ come variabile libera (nel senso della deduzione naturale un'ipotesi è una proposizione che si assume per vera come ipotesi di lavoro e che poi può essere "scaricata" durante la catena delle deduzioni in base alle regole stabilite).
Un'analoga limitazione compare per il quantificatore esistenziale nella regola

$(\EE x . A(x) \quad \quad [A(x)]...C)/C$

che vale solo se nella proposizione $C$ la $x$ NON compare come variabile libera e, oltre all'ipotesi $[A(x)]$, non ci sono altre ipotesi in cui la $x$ compare come variabile libera.