Deduzione naturale
+
Logica & Calcolabilità
La nozione di mondo possibile, fondamentale per la
semantica dei linguaggi logici, è tuttavia una nozione
non dominabile, perché evoca per definizione una
infinità di situazioni possibili.
Prendiamo il caso in cui b è conseguenza logica di a:
sappiamo che ciò significa
“in tutti i mondi in cui a è vera, anche b è vera”
quanti mondi? quali?
cosa significa in termini operativi?
Le alternative logicamente concepibili nella sfera dei
mondi possibili sono infinite e risulta estremamente
difficile trattare la nozione di conseguenza con
modalità finitarie.
Come rendere allora dominabile la relazione tra
ipotesi e conclusione?
Mediante il cosiddetto calcolo della deduzione
naturale, un metodo effettivo per costruire concrete
dimostrazioni della validità di argomenti dati.
In termini intuitivi:
Dimostrazione

Successione finita di formule in cui, mediante una
procedura effettiva, si passa in modo controllabile da
un elemento all’altro della successione: formalmente
scriveremo
a1, ..., an ⊢ b
(Conseguenza a lungo termine per la relazione tra
logica e calcolabilità: una procedura effettiva è in
linea di principio eseguibile)
È possibile, in altri termini, ‘ridurre’ le conseguenze
logiche a dimostrazioni e controllare effettivamente
se possiamo ‘produrre’ b a partire da a1,..., an.
In una dimostrazione, le premesse permettono di
ottenere in modo effettivo e procedurale la
conclusione: per questo motivo, l’analisi del concetto
di dimostrazione rimanda alla relazione tra logica e
calcolabilità.
Nel calcolo della deduzione naturale, lo strumento
principale per costruire dimostrazioni è l’insieme
delle regole di inferenza, che sono prescrizioni su
come ricavare un certo enunciato da altri enunciati.
Calcolo enunciativo (CE): sistema di regole di
inferenza per produrre dimostrazioni dentro la logica
enunciativa.
Regole di inferenza per CE:
regole di introduzione e di eliminazione di connettivi
nel corso delle dimostrazioni.
Se § è un connettivo qualsiasi
Introduzione (I-§)
Eliminazione (E-§)
a, b
_______
a§b
a§b
_______
a, b
Forma generale di una dimostrazione a1,..., am ⊢ b
Numeri di riga
(1)
.
.
.
.
(m)
(m+1)
.
(n)
Giustificazione della formula
formula
#
G
formula
#
G
formula
#
G
Le a1,..., am
formula
#
G
occorrono qui
formula
#
G
#
#
……….
G
Qui occorrono
#
……….
G
formule ottenute
#
con regole di inf.
conclusione = b
Numeri che indicano le formule da cui dipende la formula
della riga
La regola più generale di tutte: Regola di Assunzione (Assn)
Regola che consiste semplicemente nell’assumere una
formula in un qualsiasi passo di una dimostrazione.
Se scegliamo per esempio di aprire una dimostrazione con
la formula a  b come assunzione, scriveremo
(1)
1
Questi due numeri sono
uguali perché la fbf a  b
dipende da se stessa.
ab
Assn
Se i connettivi della logica enunciativa LE sono , ,
, , avremo le rispettive regole di inferenza

I, E
Introduzione ed Eliminazione di 

I, E
Introduzione ed Eliminazione di 

I, E
Introduzione ed Eliminazione di 

I, E
Introduzione ed Eliminazione di 
Cominciamo a vedere le regole più semplici.
Eliminazione di  (legge del modus ponens).
Da un condizionale ab e dall’antecedente a,
possiamo inferire il conseguente b. Formalmente:
ab, a
_____
E
b
Es.:
«Se il capo fuma, è nervoso.»
«Il capo fuma»
quindi _____
«Il capo è nervoso.»
(ab) g, ab ⊢ g
(1)
(2)
(3)
1
2
1,2
(ab) g
ab
g
Assn
Assn
1,2 E 
ab, b  g, a ⊢ g
(1)
(2)
(3)
(4)
(5)
1
2
3
1,3
1,2,3
ab
bg
a
b
g
Assn
Assn
Assn
1,3 E 
2,4 E 
Introduzione di  (Regola di ‘scarico’)
Supponiamo di avere una dimostrazione con premesse
a1,..., am , e supponiamo di voler derivare un condizionale
della forma bg.
Possiamo allora cercare di costruire una dimostrazione con
premesse a1,..., am, b: se in questa dimostrazione
riusciremo a derivare g, allora saremo autorizzati a scrivere
bg
Si dice allora che l’assunzione b viene ‘scaricata’.
Formalmente,
a1,..., am
[b]
.
.
.
g
_____
bg
I
Nota: la parentesi quadra [ ] indica l’assunzione scaricata.
Esempio:
Tutti i gatti fanno le fusa
[Fido è un gatto]
____________________
Se Fido è un gatto, allora fa le fusa
a1,..., am
[b]
bg
Introduzione di 
Da due formule qualsiasi a e b possiamo inferire a  b
a, b
_____
ab
I
Eliminazione di 
Da una congiunzione a  b possiamo inferire uno
qualsiasi dei congiunti
ab
_____
a, b
E
Dimostrazione
a (b  g), a ⊢ a  b
1
2
3
4
5
1
2
1,2
1,2,3
1,2,3,4
a (b  g)
a
bg
b
ab
Assn
Assn
1,2 E
3, E
2,4 I
Introduzione di 
Data una formula qualsiasi a, possiamo inferire la
disgiunzione di a con una formula qualsiasi (che
indichiamo con X)
a
_____
aX
I
Eliminazione di 
Da formule della forma ab, bg e ag possiamo
inferire la formula g.
ab, bg, ag
______________
g
E
La regola di eliminazione di  è definita dilemma
costruttivo:
• Oggi o è sabato o è domenica
• Se è sabato ci sarà un concerto
• Se è domenica ci sarà un concerto
____________________________
• Ci sarà un concerto
L’informazione disgiuntiva non serve più!
Eliminazione di 
Da due formula della forma a e a possiamo inferire
b (principio secondo cui da una contraddizione segue
qualsiasi cosa).
Formalmente:
a, a
_____
b
E
Dimostrazione
 a ⊢ a b
1
2
3
4
a
a
b
a b
Assn
Assn
1,2 E 
2,3 I 
Eliminazione di  (alternativa)
Da una formula della forma  a possiamo inferire
a (legge della doppia negazione).
Formalmente:
a
_____
a
E
Dimostrazione
 a    b,    a ⊢ b
1
2
3
4
5
1
2
2
1,3
1,2,3,4
ab
a
a
b
b
Assn
Assn
2 E
1,3 E
4 E
Introduzione di 
Se da una formula a deriviamo una contraddizione,
cioè deriviamo sia una formula b sia la sua negazione
b, allora possiamo scrivere  a, introducendo il
connettivo  .
[a] [a]
.
.
.
.
.
.
b,  b
______
a
I
Principio della
dimostrazione
per assurdo
Dimostrazione
a  b, a   b ⊢  a
1
2
3
4
5
6
ab
ab
a
b
b
a
Assn
Assn
Assn
1,3 E 
2,3 E 
3,4,5 I 
Le nozioni di DECIDIBILITÀ e COMPUTABILITÀ
e i loro limiti
Formulazione della logica in termini di teorie
formalizzate e di dimostrazioni (all’interno di teorie
formalizzate)

Soluzione effettiva di tutti i problemi logici?
NO!
Problema della Decisione
Data una qualsiasi proposizione A della logica
predicativa, è possibile determinare se A è vera o
falsa?
Esiste cioè un algoritmo capace di decidere se, per
una qualsiasi proposizione A, quella proposizione è
vera o falsa?
Il problema nascosto è: cos’è un algoritmo?
ALGORITMO
Concetti vaghi e indefiniti
‘PROCEDURA’, METODO’,...
MACCHINA
DI TURING (MdT)
Concetto preciso
LOGICA
Decidibilità/Indecidibilità
Ricorsività
COMPUTABILITÀ
TEORIA DEGLI ALGORITMI
Linguaggio come strumento cognitivo
(‘Produzione’ linguistica come fenomeno computabile)
LINGUISTICA
I sistemi cognitivi umani
producono espressioni
linguistiche ‘adeguate’
al contesto e in tempi ‘corretti’
Chiarificazione della nozione di algoritmo

Definizione di un modello astratto di computazione
(Macchina di Turing [MdT])

Assunzione:
la MdT (modello astratto) include in realtà le caratteristiche
fondamentali di ogni possibile procedura di calcolo, cioè di
ogni possibile algoritmo.
I FONDAMENTI DELLA NOZIONE DI MdT

Assunzione ‘qualitativa’ di Turing:
le condizioni più generali di un modello astratto di un
generico processo di calcolo sono proprio i vincoli ai
quali deve sottostare un qualsiasi generico agente
razionale che debba eseguire un calcolo.
Idea di fondo: questi vincoli sono legati ai limiti percettivi e
computazionali generali di sistemi cognitivi
Intuizione fondamentale alla base della MdT
Un agente razionale C dispone di una memoria e di
capacità percettive limitate.
Se assumiamo che lo spazio a disposizione di C per
eseguire il calcolo sia rappresentato da un nastro
unidimensionale potenzialmente infinito, quali sono
le possibili operazioni che C è in grado di eseguire?
1. C può osservare delle caselle sul nastro e scrivere
sul nastro dei simboli tratti da un alfabeto finito;
2. C può ricordare risultati determinati da passi
precedenti del calcolo e utilizzare tale informazione
nel seguito del calcolo;
3. Ogni operazione elementare che C può eseguire
è determinata univocamente da ciò che C osserva e
ricorda (cioè dal contenuto delle caselle osservate e
dal contenuto degli stati interni).
Se con Turing assumiamo che le condizioni 1-3 siano
le condizioni che possiamo assumere per un generico
processo di calcolo, allora è possibile sostenere la
seguente tesi:
TESI DI CHURCH-TURING
Ogni processo di calcolo effettivo (cioè ogni
‘algoritmo’) può essere realizzato mediante una
macchina di Turing.
IMPORTANTE! LA TESI DI CHURCH-TURING NON È
UN TEOREMA MA ‘SOLO’ UNA TESI SULLA NATURA
DELLA CALCOLABILITÀ
Infatti nella formulazione della tesi di Church-Turing
«Ogni processo di calcolo effettivo (cioè ogni
‘algoritmo’) può essere realizzato mediante una
macchina di Turing»
si utilizza il concetto di algoritmo, che come abbiamo
visto, è in sé un concetto vago.
La tesi di Church-Turing non è dunque altro che la
formulazione esplicita della convinzione che la
nozione di MdT rappresenti in modo adeguato il
concetto intuitivo di calcolabilità, algoritmicità o
risolvibilità mediante procedura effettiva.
Ma come è fatta una MdT?
Una MdT è definita da:
–
–
–
–
–
un nastro
una testina
uno stato interno
un programma
uno stato iniziale
Il nastro
Il nastro è
* Infinito (cioè potenzialmente illimitato)
* suddiviso in celle
In una cella può essere contenuto un simbolo preso
da un alfabeto opportuno
Un alfabeto è semplicemente un insieme di simboli
Una cella deve contenere un simbolo che appartiene
all’alfabeto
Lo stato interno e la testina
La macchina è dotata di una testina di
lettura/scrittura
La testina è in grado di leggere e scrivere il
contenuto della cella del nastro su cui si trova
La macchina ha uno stato interno
Uno stato è un elemento appartenente all’insieme
degli stati
Il programma di una MdT
Il comportamento della macchina è determinato da
un insieme di regole
Una regola ha la forma seguente:
(A, a, B, b, dir)
Una regola viene applicata se lo stato corrente della
macchina è A e il simbolo letto dalla testina è a
L’applicazione della regola scrive sul nastro b, cambia
lo stato in B ed eventualmente sposta la testina di
una cella a sinistra o a destra (dir)
Il funzionamento di una MdT
La macchina opera come segue:
 Determina la regola da applicare in base allo stato
interno e al simbolo corrente (quello letto dalla
testina)
 Se esiste una tale regola cambia lo stato, scrive il
simbolo sulla cella corrente si sposta come indicato
dalla regola
 Se non esiste la regola l’esecuzione termina
In questo modello non può esistere più di una regola per
uno stato ed un simbolo corrente: la MdT è un sistema
deterministico
Torniamo al nostro
Problema della Decisione
Data una qualsiasi proposizione A di L2, è possibile
determinare se A è vera o falsa? Esiste cioè un
‘algoritmo’ capace di decidere se, per una qualsiasi
proposizione A di L2, quella proposizione è vera o
falsa?
Ora sappiamo cos’è un ‘algoritmo’: una MdT!
Vediamo allora il Problema della Decisione in
termini di MdT:
Data una qualsiasi proposizione A, esiste una MdT
capace di decidere se, per una qualsiasi proposizione
A, quella proposizione è vera o falsa?
Teorema di Turing (1936)
Non esiste alcuna MdT capace di risolvere
il problema della decisione!
Vediamo perché (in termini qualitativi).
Intuitivamente, possiamo indicare una MdT come un
algoritmo con input e output: l’input rappresenta il
‘dato in ingresso’ della MdT, mentre l’output
rappresenta il risultato dell’applicazione della MdT
all’input.
input
MdT
output
Possiamo cioè indicare una generica MdT usando i
simboli di variabile n e m, cioè:
MdTn
 la n-esima MdT
m
 possibile input per MdTn
MdTn(m)  output di MdTn per input m
Consideriamo ora la seguente domanda (Problema
della fermata): per m e n generici, la macchina di
Turing MdTn si fermerà per l’input m?
Intuitivamente
“MdTn si ferma
per l’input m”
MdTn calcola
l’output MdTn (m)
“MdTn non si ferma
per l’input m”
MdTn non calcola
l’output MdTn (m)
La domanda
"Per m e n generici, la macchina di Turing MdTn si
fermerà per l’input m?"
può avere però risposta soltanto se esiste un'altra
macchina di Turing, che calcola – dati n, m qualsiasi –
se MdTn si ferma per l'input m o no.
Si dimostra tuttavia che questo algoritmo non può esistere:
il problema della fermata ha soluzione NEGATIVA. Ma se il
problema della fermata non è risolvibile, allora nemmeno il
problema della decisione è risolvibile: perché?
Formula A

MdT
A è vera
[MdT si ferma
per l’input A]
A non è vera
[MdT non si
ferma per l’input A]
Riassumendo:
Problema della Decisione
RISOLVIBILE per LE
Esiste un algoritmo capace
di decidere (  tavole di verità)
NON RISOLVIBILE per LP
Non esiste un algoritmo
generale capace di decidere