Stile fitch per deduzioni naturali

Nella logica matematica , lo stile di deduzione naturale di Fitch è una variante della deduzione naturale . È stato proposto dal logico Frederic Brenton Fitch . Le dimostrazioni sono presentate in modo lineare, rinunciando alla struttura ad albero proposta da Gentzen .

introduzione

Le regole esposte in questo paragrafo sono quelle per il calcolo delle proposizioni . Consentono di concatenare logicamente le frasi, ovvero di introdurre nuove frasi come conseguenze logiche di quanto detto prima. A ciascuno degli operatori logici fondamentali sono associate due regole di deduzione. Una delle regole è una regola introduttiva : spiega come provare una proposizione con l'operatore. L'altra regola è una regola di eliminazione : spiega come utilizzare una proposizione avendo l'operatore per continuare il ragionamento.

Sono necessarie introduzione ed eliminazione per poter smontare e rimontare le formule. La ricerca di una deduzione logica consiste proprio nell'analizzare le premesse, cioè nel smontarle, e nel rimontare i pezzi per realizzare formule collegabili logicamente alla conclusione. A volte si crede che sia molto difficile dimostrare la matematica, ma in linea di principio non è molto diverso da un gioco di costruzione con i cubi.

Regole relative al coinvolgimento

La regola per introdurre l'implicazione o la regola per abbandonare un'ipotesi provvisoria afferma che, per provare un'implicazione "se P allora Q", è sufficiente procedere come segue: poniamo P come ipotesi provvisoria, quindi deduciamo da tutte le precedenti frasi più P per raggiungere Q. Una volta raggiunto Q, possiamo dedurre "se P allora Q". Insistiamo su un punto: Q è dimostrato sotto l'ipotesi P ma “se P allora Q”, dipende solo dalle premesse precedenti. Se usiamo il metodo di Fitch, possiamo introdurre un'ipotesi provvisoria in una deduzione in qualsiasi momento. Basta spostarlo a destra rispetto alle altre premesse. Tutto ciò che viene dedotto in base a un'ipotesi provvisoria deve essere sotto di esso o alla sua destra, ma mai alla sua sinistra. La regola introduttiva ci permette di concludere che abbiamo dimostrato “se P allora Q” senza l'ipotesi P. Possiamo spostare “se P allora Q” a sinistra rispetto a P, ma non rispetto alle altre premesse utilizzate. la prova di Q. Noteremo:

{\ displaystyle 1 \ quad \ quad P}

(ipotesi provvisoria)

{\ displaystyle 2 \ quad \ quad Q}

(proprietà dedotta da 1)

{\ displaystyle 3 \ quad P \ to Q}

(introduzione dell'implicazione tra le due righe 1 e 2)

La regola di eliminazione dell'implicazione , o regola di distacco o modus ponens, afferma che dalle due frasi "P" e "se P allora Q" possiamo dedurre "Q". Permette di passare da condizioni già note, P, a condizioni nuove, Q, purché esista una legge che lo autorizzi, “if P then Q”, che si annoterà:

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad P \ to Q}

{\ displaystyle 3 \ quad Q}

(eliminazione dell'implicazione tra le righe 1 e 2)

Mostriamo ad esempio che con queste due regole possiamo dedurre “se P allora R” dalle due frasi “se P allora Q” e “se Q allora R”:

{\ displaystyle 1 \ quad P \ to Q}

(ipotesi)

{\ displaystyle 2 \ quad Q \ to R}

(ipotesi)

{\ displaystyle 3 \ quad \ quad P}

(ipotesi provvisoria)

{\ displaystyle 4 \ quad \ quad Q}

(modus ponens su 3 e 1)

{\ displaystyle 5 \ quad \ quad R}

(modus ponens su 4 e 2)

{\ displaystyle 6 \ quad P \ to R}

(regola per l'introduzione dell'implicazione tra 3 e 5, abbandono dell'ipotesi provvisoria P).

Le regole relative alla congiunzione

Per la congiunzione, le regole sono molto semplici.

La regola per l' introduzione della congiunzione afferma che dalle due frasi A e B possiamo dedurre la frase (A e B).

{\ displaystyle 1 \ quad A}

{\ displaystyle 2 \ quad B}

{\ displaystyle 3 \ quad A \ land B}

(introduzione della congiunzione tra 1 e 2)

La regola di eliminazione delle congiunzioni afferma che, dalla frase (A e B), possiamo dedurre le due frasi A e B prese separatamente.

{\ displaystyle 1 \ quad A \ land B}

{\ displaystyle 2 \ quad A}

(eliminazione della congiunzione 1)

{\ displaystyle 3 \ quad B}

(eliminazione della congiunzione 1)

Queste regole consentono di riunire o, al contrario, di separare affermazioni che sono tutte considerate vere. È la forma logica della capacità della ragione di analizzare il mondo, cioè di studiarne le parti separatamente, e di sintetizzarlo, cioè di riunire gli elementi di uno studio. In un tutto. Questo è il motivo per cui queste regole sono anche chiamate regole di analisi e riepilogo.

Le regole in materia di TFR

Le due regole di detrazione per la disgiunzione sono le seguenti.

La regola introduttiva di disgiunzione o regola dell'indebolimento di una tesi afferma che, dalla frase P possiamo dedurre la frase (P o Q) così come la frase (Q o P), qualunque sia la frase Q. Questa regola può non sembra interessante, ma in effetti è molto importante. A volte è vantaggioso dedurre (P o Q) dopo aver dimostrato P, perché possiamo anche sapere che (P o Q) ha altre conseguenze.

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad P \ lo Q}

(introduzione della disgiunzione da 1)

e lo stesso

{\ displaystyle 1 \ quad Q}

{\ displaystyle 2 \ quad P \ lo Q}

(introduzione della disgiunzione da 1)

La regola di eliminazione della disgiunzione o regola di disgiunzione di ipotesi o regola di distinzione di caso, afferma che, se abbiamo dimostrato (P o Q) e abbiamo anche dimostrato (se P allora R) e (se Q poi R), allora abbiamo dimostrato R. Questa regola è utile quando esaminiamo diversi casi possibili che portano alla stessa conclusione.

{\ displaystyle 1 \ quad P \ lo Q}

{\ displaystyle 2 \ quad \ quad P}

(ipotesi provvisoria)

{\ displaystyle 3 \ quad \ quad R}

(proprietà dedotta da 2)

{\ displaystyle 4 \ quad P \ to R}

(introduzione dell'implicazione tra 2 e 3)

{\ displaystyle 5 \ quad \ quad Q}

(ipotesi provvisoria)

{\ displaystyle 6 \ quad \ quad R}

(proprietà dedotta da 5)

{\ displaystyle 7 \ quad Q \ to R}

(introduzione dell'implicazione tra 5 e 6)

{\ displaystyle 8 \ quad R}

(eliminazione della disgiunzione tra 1, 4, 7)

Le regole relative alla negazione

La regola per introdurre la negazione afferma che, se proviamo una contraddizione da un'ipotesi P, quest'ultima è necessariamente falsa e quindi la sua negazione è vera. Quindi, se in una deduzione sotto l'ipotesi provvisoria P, abbiamo trovato una contraddizione (Q e non Q), anche annotata , allora possiamo dedurre nonP da tutte le premesse precedenti eccetto P. Con il metodo di Fitch, quindi spostiamo (non P ) a sinistra rispetto a P, che è rappresentata come segue: $\ bot$

{\ displaystyle 1 \ quad \ quad \ quad P}

{\ displaystyle 2 \ quad \ quad \ quad \ bot}

{\ displaystyle 3 \ quad \ lnot P}

(introduzione della negazione tra 1 e 2)

La regola dell'eliminazione della negazione o regola dell'eliminazione della doppia negazione o del ragionamento per assurdo afferma che, da (nonP) possiamo dedurre P.È infatti ragionare per assurdo perché in, un tale ragionamento, per provare P , assumiamo (non P) e cerchiamo di ottenere una contraddizione. Se questo è il caso, abbiamo dimostrato (non P) secondo la regola di introduzione della negazione, ed è proprio la regola di eliminazione della doppia negazione che permette di concludere con P:

{\ displaystyle 1 \ quad \ lnot \ lnot P}

{\ displaystyle 2 \ quad P}

(eliminazione della doppia negazione 1)

{\ displaystyle 1 \ quad \ quad \ lnot P}

(ipotesi provvisoria [ragionamento per assurdo])

{\ displaystyle 2 \ quad \ quad \ bot}

{\ displaystyle 3 \ quad \ lnot \ lnot P}

(introduzione della negazione tra 1 e 2)

{\ displaystyle 4 \ quad P}

(eliminazione della doppia negazione 3)

Quando consideriamo che ogni frase è necessariamente vera o falsa, la validità di quest'ultima regola è evidente. È caratteristico della logica classica , che viene presentata qui ed è utilizzata dalla stragrande maggioranza degli scienziati. A volte è contestato a causa di un problema importante, quello delle prove di esistenza dall'assurdo. A volte puoi provare che un problema ha una soluzione senza essere in grado di trovarlo. Per questo è sufficiente dimostrare che l'assenza di soluzione porta a una contraddizione. Il ragionamento dell'assurdo permette poi di concludere che non è vero che il problema non ha soluzione: no no (il problema ha una soluzione). Nella logica classica, rimuoviamo la doppia negazione per concludere che il problema ha una soluzione. Tuttavia, l'approccio così seguito non fornisce alcun processo costruttivo per la soluzione ricercata. Questa obiezione è stata sollevata da alcuni matematici e logici, tra cui Brouwer , che ha contestato questo metodo e si è opposto a Hilbert che lo ha difeso. I matematici costruttivisti o intuizionisti ritengono che una prova dell'esistenza non abbia senso se non fornisce anche un processo costruttivo per l'oggetto in questione. Anche questi ultimi rigettano la regola della soppressione della doppia negazione per sostituirla con la seguente regola: da P e (non P) si può dedurre una contraddizione, e da questa contraddizione qualsiasi proposizione Q (principio di ex falso quodlibet ).

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad \ lnot P}

{\ displaystyle 3 \ quad \ bot}

{\ displaystyle 4 \ quad Q}

(eliminazione della negazione 2 nella logica intuizionista)

Negli esempi, useremo questa seconda regola di eliminazione quando è possibile fare a meno della regola di eliminazione doppia negativa.

Possiamo introdurre altre regole per gli altri operatori booleani, in particolare l'operatore di equivalenza, ma ciò non è necessario, perché questi operatori possono essere definiti dai precedenti e le loro regole di deduzione possono poi essere dedotte dalle regole precedenti. (P è equivalente a Q) è definito da ((se P allora Q) e (se Q allora P)).

Esempi

Forniamo di seguito alcuni esempi di utilizzo della deduzione naturale. Nella prima parte non useremo la regola per eliminare la doppia negazione. Nella seconda parte useremo questa regola. Le formule dedotte in questa seconda parte non sono riconosciute valide dai matematici intuizionisti . Useremo i seguenti simboli: for if ... then ... , for or , for and , for no . Il simbolo designa una contraddizione, vale a dire una falsa proposizione. $\ per$ $\ lor$ $\ terra$ $\ lnot$ $\ bot$

Esempi che non utilizzano l'eliminazione della doppia negazione

Esempio 1 : ${\ Displaystyle (\ lnot A \ land \ lnot B) \ to \ lnot (A \ lo B)}$

{\ Displaystyle 01 \ quad \ quad \ lnot A \ land \ lnot B}

(ipotesi provvisoria)

{\ displaystyle 02 \ quad \ quad \ lnot A}

(eliminazione della congiunzione 01)

{\ displaystyle 03 \ quad \ quad \ lnot B}

(eliminazione della congiunzione 01)

{\ Displaystyle 04 \ quad \ quad \ quad A \ lo B}

(ipotesi provvisoria)

{\ displaystyle 05 \ quad \ quad \ quad \ quad A}

(ipotesi provvisoria)

{\ displaystyle 06 \ quad \ quad \ quad \ quad \ bot}

contraddizione tra 02 e 05

{\ displaystyle 07 \ quad \ quad \ quad A \ to \ bot}

(introduzione dell'implicazione tra 05 e 06)

{\ displaystyle 08 \ quad \ quad \ quad \ quad B}

(ipotesi provvisoria)

{\ displaystyle 09 \ quad \ quad \ quad \ quad \ bot}

contraddizione tra 03 e 08

{\ displaystyle 10 \ quad \ quad \ quad B \ to \ bot}

(introduzione dell'implicazione tra 08 e 09)

{\ displaystyle 11 \ quad \ quad \ quad \ bot}

(eliminazione della disgiunzione tra 04, 07, 10)

{\ Displaystyle 12 \ quad \ quad \ lnot (A \ lo B)}

(introduzione della negazione tra 04 e 11)

{\ Displaystyle 13 \ quad (\ lnot A \ land \ lnot B) \ to \ lnot (A \ lo B)}

(introduzione dell'implicazione tra 01 e 12 e fine della detrazione)

Dimostriamo che vale anche il contrario . Dimostriamo anche che , ma per il contrario di quest'ultima proprietà, usiamo l'eliminazione della doppia negazione. ${\ Displaystyle \ lnot (A \ lo B) \ to (\ lnot A \ land \ lnot B)}$ ${\ displaystyle (\ lnot A \ lor \ lnot B) \ to \ lnot (A \ land B)}$

Esempio 2 : ${\ Displaystyle A \ to \ lnot \ lnot A}$

{\ displaystyle 01 \ quad \ quad A}

(ipotesi provvisoria)

{\ displaystyle 02 \ quad \ quad \ quad \ lnot A}

(ipotesi provvisoria)

{\ displaystyle 03 \ quad \ quad \ quad \ bot}

(eliminazione della negazione tra 01 e 02)

{\ Displaystyle 04 \ quad \ quad \ lnot \ lnot A}

(introduzione della negazione tra 02 e 03)

{\ Displaystyle 05 \ quad A \ to \ lnot \ lnot A}

(introduzione dell'implicazione tra 01 e 04, fine della detrazione)

Il contrario segue direttamente dall'eliminazione della doppia negazione ed è rifiutato dagli intuizionisti. Ma curiosamente, non è la stessa cosa con chi si dimostra senza questa ipotesi e chi, da parte sua, è accettato dagli intuizionisti. ${\ Displaystyle \ lnot \ lnot A \ to A}$ ${\ Displaystyle \ lnot \ lnot \ lnot A \ to \ lnot A}$

Esempio 3 : ${\ Displaystyle \ lnot \ lnot \ lnot A \ to \ lnot A}$

{\ Displaystyle 01 \ quad \ quad \ lnot \ lnot \ lnot A}

(ipotesi provvisoria)

{\ displaystyle 02 \ quad \ quad \ quad A}

(ipotesi provvisoria)

{\ Displaystyle 03 \ quad \ quad \ quad A \ to \ lnot \ lnot A}

(teorema dell'esempio 2)

{\ Displaystyle 04 \ quad \ quad \ quad \ lnot \ lnot A}

(eliminazione del coinvolgimento o modus ponens tra 02 e 03)

{\ displaystyle 05 \ quad \ quad \ quad \ bot}

(eliminazione della negazione tra 01 e 04)

{\ Displaystyle 06 \ quad \ quad \ lnot A}

(introduzione della negazione tra 02 e 05)

{\ Displaystyle 07 \ quad \ lnot \ lnot \ lnot A \ to \ lnot A}

(introduzione dell'implicazione tra 01 e 06, fine della detrazione)

Esempi che utilizzano l'eliminazione della doppia negazione

I seguenti esempi utilizzano l'eliminazione della doppia negazione. Si può dimostrare che questo uso è necessario. Non sono quindi accettati nella logica intuizionista .

Esempio 4 : ${\ Displaystyle \ lnot (A \ land B) \ to (\ lnot A \ lo \ lnot B)}$

{\ Displaystyle 01 \ quad \ quad \ lnot (A \ land B)}

(ipotesi provvisoria [ragionamento per assurdo])

{\ Displaystyle 02 \ quad \ quad \ quad \ lnot (\ lnot A \ lo \ lnot B)}

(ipotesi provvisoria)

{\ Displaystyle 03 \ quad \ quad \ quad \ lnot (\ lnot A \ lor \ lnot B) \ to (\ lnot \ lnot A \ land \ lnot \ lnot B)}

(teorema, reciproco dell'esempio 1)

{\ Displaystyle 04 \ quad \ quad \ quad \ lnot \ lnot A \ land \ lnot \ lnot B}

(eliminazione del coinvolgimento o modus ponens tra 02 e 03)

{\ displaystyle 05 \ quad \ quad \ quad A \ land B}

(eliminazione della doppia negazione in 04)

{\ displaystyle 06 \ quad \ quad \ quad \ bot}

(eliminazione della negazione tra 01 e 05)

{\ Displaystyle 07 \ quad \ quad \ lnot \ lnot (\ lnot A \ lo \ lnot B)}

(introduzione della negazione tra 02 e 06)

{\ Displaystyle 08 \ quad \ quad \ lnot A \ lo \ lnot B}

(eliminazione della doppia negazione in 07)

{\ Displaystyle 09 \ quad \ lnot (A \ land B) \ to (\ lnot A \ lo \ lnot B)}

(introduzione dell'implicazione tra 01 e 08)

Esempio 5 : se non richiede l'eliminazione della doppia negazione, questa è necessaria per provare il contrario . ${\ Displaystyle (A \ to B) \ to (\ lnon B \ to \ lnot A)}$ ${\ Displaystyle (\ lnon B \ to \ lnot A) \ to (A \ to B)}$

Esempio 6 : possiamo dimostrarlo . Infatti se abbiamo e , abbiamo (falso) e quindi abbiamo . ${\ Displaystyle \ lnon A \ to (A \ to B)}$ $\ lnon A$ $A$ $\ bot$ $B$

Esempio 7 : analogamente la prova della validità del terzo escluso utilizza l'eliminazione della doppia negazione. Supponendo che , deduciamo (reciproco dell'esempio 1), quindi una contraddizione e la validità di . $A \ lo \ lnon A$ ${\ Displaystyle \ lnot (A \ lo \ lnot A)}$ ${\ Displaystyle \ lnot A \ land \ lnot \ lnot A}$ ${\ Displaystyle \ lnot \ lnot (A \ lo \ lnot A)}$

Se gli intuizionisti rifiutano gli esclusi, accettano ovviamente il principio di non contraddizione . In effetti, l'ipotesi è una contraddizione. Abbiamo quindi introducendo la negazione. $\ lnot (A \ land \ lnot A)$ ${\ displaystyle A \ land \ lnot A}$ $\ lnot (A \ land \ lnot A)$

Esempio 7 conosciuto sotto il nome di legge di Peirce : . Stranamente, sebbene non contenga una negazione, la deduzione di questa legge richiede l'eliminazione della doppia negazione, ad esempio attraverso l'uso del terzo escluso. Supponiamo di averlo fatto . Secondo il terzo escluso: ${\ displaystyle ((A \ to B) \ to A) \ to A}$ ${\ displaystyle ((A \ to B) \ to A)}$

o abbiamo , $A$

oppure abbiamo e quindi abbiamo (esempio 6) e siccome abbiamo con il modus ponens, abbiamo . $\ lnon A$ ${\ displaystyle A \ to B}$ ${\ displaystyle ((A \ to B) \ to A)}$ $A$

Le regole di detrazione per i quantificatori

L'uso di nomi di variabili nelle teorie del primo ordine

Le regole di deduzione per gli operatori universali ed esistenziali regolano l'uso dei nomi delle variabili. Questo uso conferisce a una teoria il potere della generalità, vale a dire la possibilità di conoscere non ogni individuo preso isolatamente, ma tutti gli individui dello stesso genere, in una singola frase.

Le regole per l'utilizzo delle variabili specificano le condizioni in base alle quali i nomi delle variabili possono essere introdotti e cosa si può dire su di essi. Queste regole sono naturali ma ci sono alcune difficoltà tecniche sulle nozioni di termine, ricorrenza libera o collegata di una variabile, sostituzione di un termine per occorrenze di una variabile e sostituzione di una variabile per occorrenze di un termine.

Perché una teoria possa utilizzare la logica del primo ordine è necessario aver definito un dominio di oggetti ed è necessario che i predicati attribuiti dalla teoria ai suoi oggetti non siano essi stessi oggetti della teoria.

Il significato del nome di una variabile oggetto è rappresentare qualsiasi oggetto della teoria: sia x un numero. Spesso introduciamo un nome di variabile nei locali che determinano le condizioni generali su questo oggetto. x è un qualsiasi oggetto della teoria purché soddisfi queste condizioni: sia x un numero primo ... Una teoria generalmente contiene nomi per i suoi oggetti. La teoria dei numeri interi contiene, ad esempio, nomi per tutti i numeri: 0, 1, 2, ..., -1, -2, ...

I termini possono essere semplici o composti. Questi sono i nomi degli oggetti, i nomi delle variabili oggetto e tutte le espressioni composte che possono essere formate da essi applicando gli operatori oggetto della teoria. Ad esempio, 1, x, x + 1 e (x + x) +1 sono termini della teoria dei numeri.

Ricordiamo innanzitutto l'importantissima distinzione tra le variabili legate da un operatore e le altre, le variabili libere. Le occorrenze di un nome di variabile in una frase sono tutte le posizioni in cui appare quel nome. Un evento può essere gratuito o collegato. Quando un operatore esistenziale o universale in x viene applicato a una frase complessa, tutte le occorrenze di x vengono collegate da questo operatore. Tutti gli eventi che non sono così collegati sono gratuiti.

Se una frase contiene diversi operatori esistenziali e universali, è auspicabile che questi operatori si riferiscano tutti a nomi di variabili differenti. Questa regola non è essenziale. Non viene rispettato quando mettiamo il calcolo dei predicati sotto forma di algebra cilindrica (un'algebra cilindrica è un'algebra booleana completata da leggi specifiche di operatori universali ed esistenziali). Ma è sempre rispettato nella pratica perché aiuta a evitare confusione.

Una frase si ottiene da un'altra sostituendo un termine t per le occorrenze di una variabile x quando tutte le occorrenze libere di x sono state sostituite da t. Ad esempio, (il padre di x è umano e il padre di x è onesto) si ottiene sostituendo il termine padre di x alla variabile y nella formula (y è umano ey è onesto).

Questi preliminari consentono di formulare le regole di deduzione per operatori universali ed esistenziali.

Le regole relative al quantificatore universale

La regola introduttiva del quantificatore universale o regola di generalizzazione afferma che, da P (x) possiamo dedurre (per ogni x, P (x)) purché il nome della variabile x non compaia mai nelle ipotesi da cui dipende P (x) .

{\ displaystyle 1 \ quad P (x)}

{\ displaystyle 2 \ quad \ forall x \; P (x)}

(introduzione di qualunque cosa , dove x non è libera nei locali di P)

Molto spesso le variabili vengono introdotte in ipotesi provvisorie. Quindi ragioniamo su di loro come se fossero oggetti. Possiamo quindi dedurne leggi generali, perché quanto abbiamo dedotto vale per tutti gli oggetti che soddisfano le stesse ipotesi. Sono le regole per abbandonare un'ipotesi provvisoria e per la generalizzazione che ci permettono di concludere.

La regola di eliminazione del quantificatore universale o regola di singolarizzazione afferma che, da una frase della forma (per tutti x) P (x), possiamo dedurre P (t), per qualsiasi termine t di cui le variabili non sono correlate in P (x ). P (x) designa qualsiasi frase che contiene x come variabile libera, P (t) designa la frase ottenuta da P (x) sostituendo t per tutte le occorrenze libere di x. La regola della singolarizzazione consiste semplicemente nell'applicare una legge universale a un caso singolare.

{\ displaystyle 1 \ quad \ forall x \; P (x)}

{\ displaystyle 2 \ quad P (t)}

(eliminazione di qualunque cosa )

Regole relative al quantificatore esistenziale

La regola introduttiva del quantificatore esistenziale , o regola delle prove dirette di esistenza, afferma che, dalla proposizione P (t), possiamo dedurre che esiste una x tale che P (x) per ogni variabile x che non appaiono in P (t) e per ogni termine t i cui nomi di variabili non sono correlati in P (x).

P (t) designa qualsiasi frase che contiene il termine t almeno una volta. P (x) si ottiene da P (t) sostituendo x per t in una o più delle sue occorrenze. In questa regola, non è necessario sostituire x per tutte le occorrenze di t.

{\ displaystyle 1 \ quad P (t)}

{\ displaystyle 2 \ quad \ esiste x \; P (x)}

(l'introduzione di esiste )

La regola di eliminazione del quantificatore esistenziale o regola delle conseguenze dell'esistenza permette, da una proposizione (esiste x, P (x)), di introdurre una nuova ipotesi provvisoria P (y) dove y è un nome di variabile che non ha mai stato usato prima e dove P (y) è ottenuto da P (x) sostituendo y per tutte le occorrenze di x. Possiamo quindi ragionare sotto questa ipotesi. La regola delle conseguenze dell'esistenza permette quindi di concludere quanto segue: dalla frase (esiste una x tale che P (x)) possiamo dedurre R quando R è stato dedotto sotto l'unica ipotesi provvisoria aggiuntiva P ( y) e che y non compare nelle premesse prima di P (y) né in R. y è una specie di essere ipotetico. Serve solo come intermediario in una detrazione ma non compare né nelle sue premesse né nella sua conclusione.

{\ displaystyle 1 \ quad \ esiste x \; P (x)}

(ipotesi)

{\ displaystyle 2 \ quad \ quad P (y)}

( y nuova variabile)

{\ displaystyle 3 \ quad \ quad R}

(deduzione da 2, R non coinvolge y )

{\ displaystyle 4 \ quad R}

(l'eliminazione esiste in 1 e 3)

Esempi

Esempio 1 ${\ displaystyle (\ esiste x \; \ lnot A (x)) \ to (\ lnot \ forall x \; A (x))}$

{\ displaystyle 1 \ quad \ quad \ esiste x \; \ lnon A (x)}

(ipotesi provvisoria)

{\ displaystyle 2 \ quad \ quad \ quad \ forall x \; A (x)}

(ipotesi provvisoria)

{\ Displaystyle 3 \ quad \ quad \ quad \ quad \ lnot A (y)}

( y nuova variabile da 1)

{\ displaystyle 4 \ quad \ quad \ quad \ quad A (y)}

(eliminazione di qualunque cosa in 2)

{\ displaystyle 5 \ quad \ quad \ quad \ quad \ bot}

(eliminazione della negazione 3, 4)

{\ displaystyle 6 \ quad \ quad \ quad \ bot}

(l'eliminazione è compresa tra 1 e 5)

{\ Displaystyle 7 \ quad \ quad \ lnot (\ forall x \; A (x))}

(introduzione della negazione tra 2 e 6)

{\ Displaystyle 8 \ quad (\ exist x \; \ lnot A (x)) \ to (\ lnot \ forall x \; A (x))}

(introduzione dell'implicazione 1, 7)

Esempio 2 : abbiamo anche noi , ma la dimostrazione richiede l'eliminazione della doppia negazione, e questo teorema della logica classica non è accettato nella logica intuizionista. ${\ Displaystyle \ lnot (\ forall x \; A (x)) \ to \ exist x (\ lnot A (x))}$

Come verificare la correttezza di un ragionamento?

A queste dodici regole, o quattordici, se contiamo che la regola per eliminare la congiunzione è in realtà una doppia regola, e lo stesso per la regola per introdurre la disgiunzione, dobbiamo aggiungere una quindicesima, molto semplice, la regola della ripetizione: puoi sempre ripetere una tesi precedente, a meno che non dipenda da un'ipotesi abbandonata. Possiamo quindi ripetere tutte le tesi purché non le spostiamo a sinistra. Questa regola è necessaria quando si vuole ripetere una premessa in una conclusione o quando è necessaria una tesi precedente nel corpo di una deduzione in ipotesi provvisoria per applicare una regola.

L'elenco delle precedenti quindici regole è completo nel senso che è sufficiente per fare tutte le deduzioni corrette. Kurt Gödel ha dimostrato, ( Teorema di completezza ) per un sistema logico diverso, ma equivalente a quello appena presentato, che è sufficiente formalizzare tutte le deduzioni corrette del Calcolo dei predicati del primo ordine .

Le detrazioni corrette sono prima di tutto quelle che rispettano rigorosamente queste regole fondamentali. Tutte le frasi devono essere assiomi o ipotesi provvisorie o conseguenze delle frasi che le precedono in virtù di una delle quindici regole. Per motivi di velocità, puoi anche utilizzare regole derivate (ad esempio avanti di ). Una regola derivativa è corretta quando si può dimostrare che tutto ciò che può essere dedotto con essa può essere dedotto anche senza di essa con le sole regole di base. ${\ displaystyle \ lnot (A \ lo B)}$ ${\ displaystyle (\ lnot A \ land \ lnot B}$

Fintanto che le detrazioni sono formalizzate, è sempre possibile riconoscere, anche da un programma, se una detrazione è corretta perché le regole di detrazione sono di numero finito ed è sempre possibile verificare in un tempo finito se una formula è la conseguenza di uno o più altri in base a una di queste regole. Questo approccio svolge parte del programma a volte chiamato finitaire proposto da David Hilbert per risolvere i problemi dei fondamenti della matematica. Hilbert era alla ricerca di un metodo efficiente che permettesse di decidere per qualsiasi enunciato matematico se si tratta di un teorema, cioè di una verità matematica. Il calcolo dei predicati ha permesso di ridurre il problema alla questione di sapere se una formula è o meno una legge logica.

Ma mentre è possibile verificare la validità di una deduzione che porta a una formula, viceversa, la questione se una data formula sia o meno una legge logica non può essere risolta in generale. In effetti, non esiste un metodo universale che consenta di dire se una formula è una legge logica o meno. Questa inesistenza è dedotta dal teorema di incompletezza di Gödel . Si dice che la questione se una formula sia una legge logica è indecidibile.

Controllare la correttezza delle deduzioni nella lingua corrente è più difficile. È prima necessario tradurre le frasi familiari in un linguaggio formalizzato del calcolo dei predicati. Questo passaggio a volte pone un problema se hai dubbi sull'accuratezza della traduzione. Ma la difficoltà maggiore deriva dal fatto che le attuali detrazioni generalmente lasciano un ampio spazio all'implicito. Anche i rapporti di dipendenza da un'ipotesi non sono sempre esplicitati. Al contrario, le deduzioni formali non lasciano nulla nell'oscurità. Quelle qui proposte sono molto simili alle attuali deduzioni tranne che spiegano tutto. Per certificare il consueto ragionamento e le dimostrazioni corrette, tutto ciò che è implicito deve essere spiegato. Per questo spesso è necessario studiare molto e conoscere tutto l'implicito prima di sapere se un ragionamento è corretto.

Bibliografia

Jon Barwise e John Etchemendy , Language proof and logic , Seven Bridges Press e CSLI, 1999.
Pelletier, Jeff, " A History of Natural Deduction and Elementary Logic Textbooks " .