Logica Predicativa PDF

Preview

Summary

Appunti sulla Logica Predicativa...

Description

LOGICA PREDICATIVA 1 – Sintassi della logica predicativa Le formule predicative sono asserzioni riguardo alle relazioni che intercorrono fra certi oggetti. Per poter parlare di oggetti useremo espressioni che non sono formule: i termini. A differenza delle formule, anche dopo lo sviluppo della semantica, i termini non saranno né veri né falsi. Un linguaggio predicativo contiene i seguenti elementi comuni:   

Variabili I simboli logici: connettivi e quantificatori Virgole e parentesi

Un linguaggio predicativo consiste dei seguenti insiemi:   

Un insieme di simboli di costante Un insieme di simboli di funzione, ciascuno fornito della propria arietà Un insieme non vuoto di simboli di relazione, ciascuno fornito della propria arietà

L’arietà di un simbolo di funzione/relazione indica a quanti elementi esso si può applicare. Se un simbolo di funzione o relazione ha arietà n , diciamo che è n -ario. I termini di un linguaggio fissato sono costituiti utilizzando solo alcuni dei suoi elementi: le variabili e i simboli di costante e di funzione, inoltre le virgole e le parentesi. Un termine è chiuso se in esso non compare nessuna variabile, x (aperto), 1 (chiuso), +( x , 0 ) (aperto). La sostituzione di x con t in s (indicata da s {x /t } ) è il termine ottenuto rimpiazzando ogni occorrenza di x in s con t . è una variabile e Se x sostituzione si definisce così:

s 1

e

t

sono termini, la

  

Se s è la variabile x , allora s {x /t } è t x oppure un è una variabile diversa da Se s simbolo di costante allora s {x /t } è s f ( s1 … s n ) s {x /t } s + allora è Se f (s 1 {x /t }… s n {x / t }) .

L’insieme delle formule di segue:    

L

è definito per ricorsione come

Ogni formula atomica di L è una formula di L è una formula di L allora (¬ F) è una Se F formula di L F G L e sono formule di allora Se ( F ∧G ), ( F ∨ G ) e (F → G) sono formule di L Se F è una formula di L e x è una varabile, allora (∀xF) e (∃xF ) sono formule di L

Se T è un insieme di formule, il linguaggio di T , denotato con L(T ) e consiste dei simboli di costante, formule e relazione che compaiono in qualche elemento di T . Il grado della formula, indicato con   

g (F )=0 se F è atomica g (¬ F ) =g (∀xF ) =g (∃xF )=g ( F )+1 g (F ∧G ) =g( F ∨G )=g ( F → G )=g ( F )+ g ( G ) +1

Sia F una formula e x occorrenze libere di x in F 



una variabile. Definiamo le come segue:

x in è atomica allora ogni occorrenza di è libera Se F è ¬G allora le occorrenze libere di x in F sono le occorrenze libere di x in G Se F è G ∧ H ,G ∨ H , G → H , allora le occorrenze libere di x in F sono le occorrenze libere di x in G e le occorrenze libere di x in H Se

F

F



g(F) , è definito da:

2

 

Se F è ∀xG o ∃xG allora nessuna occorrenza di x in F è libera Se F è ∀yG o ∃yG dove y è una variabile diversa da x , allora le occorrenze di x in F sono le occorrenze libere di x in G .

Le occorrenze di una variabile in F che non sono libere si dicono occorrenze legate. Le variabili libere di una formula F sono quelle che hanno almeno un’occorrenza libera in F . Una formula priva di variabili libere è chiamata enunciato o formula chiusa. Una formula aperta, o priva di quantificatori, è una formula in cui non compaiono ∀ e ∃. Se p(s1 … sk ) , x è una F è una formula atomica variabile e t un termine, la sostituzione di x con t in F è p(s1 {x /t }… sk {x /t }) ed è denotata da F {x /t } . La sostituzione della variabile x con il termine t è ammissibile in F se t è libero per la sostituzione al posto di ogni occorrenza libera di x in F . In questo caso la formula F {x /t } è ottenuta sostituendo in F ogni formula atomica in cui compare libera con A x A {x /t } .

2 – Semantica della logica predicativa Dato un linguaggio data da:  

una interpretazione

Un insieme non vuoto dell’interpretazione Per ogni simbolo di costante I



L

c ∈D

DI , c

in

I

per

detto

L

è

dominio

L , un elemento

I

Per ogni simbolo di funzione n funzione f I : ( D I ) → D I 3

n -ario

f in

L , una



Per ogni simbolo di relazione n insieme pI ∈ ( D I )

n -ario

p

in

L , un

Un’interpretazione I per il linguaggio L associa ad ogni termine chiuso t in L la sua interpretazione in I , che è un elemento t I ∈ D I definito ricorsivamente da:  

Se Se

t è un simbolo di costante c allora I I I I t=f (t 1 … t n) allora t =f (t1 … t n )

I

t =c

I

Se un termine non è chiuso (e quindi contiene delle variabili) l’interpretazione non è sufficiente a stabilire quale elemento del dominio associare al termine. Uno

stato

σ :Var → D dominio di termine t da:  

Se Se



Se

I

dell’interpretazione è una funzione I che ad ogni variabile associa un elemento del I . Uno stato σ di I associa ad ogni un valore, σ ( t ) ∈ D I , definito ricorsivamente

t è una variabile x allora σ (t )=σ (x) t è una costante c allora σ (t )=c I I t=f (t 1 … t n) allora σ (t )=f ( σ (t1 ) … σ ( t n) )

σ è uno stato dell’interpretazione I , x una Se variabile e d ∈ D I indichiamo con σ [ x /d ] (da leggersi σ perturbato mandando x in d ) lo stato che coincide con σ su tutte le variabili diverse da x , e assegna a x il valore d . F L , I Siano la formula di un linguaggio L σ I . un’interpretazione per e uno stato di Definiamo la relazione I , σ ⊨ F (da leggersi I allo stato σ soddisfa F ) per ricorsione su F :   

I I , σ ⊨ p(t1 … tn ) se e solo se ( σ ( t 1) … σ ( t n)) ∈ p I , σ ⊨¬ G se e solo se I , σ ⊨ G I , σ ⊨G ∧ H se e solo se I , σ ⊨ G e I , σ ⊨ H

4



I , σ ⊨G ∨ H I,σ ⊨H I , σ ⊨G → H I ,σ ⊨H I , σ ⊨ ∀xG se I , σ [ x /d ] ⊨ G I , σ ⊨∃xG se I , σ [ x /d 0 ] ⊨ G

  

se

e

solo

se

I , σ ⊨G

oppure

se

e

solo

se

I , σ ⊨G

oppure

e solo se per ogni

d ∈D

si ha che

e solo se esiste

d0 ∈ D

tale che

I F , e scriviamo I⊨F Diciamo che soddisfa se I , σ ⊨ F per ogni stato σ di I . In questo caso si dica anche che F è vera in I oppure che I è un modello di F . T

è un insieme di formule, diciamo che I allo stato soddisfa T , e scriviamo I , σ ⊨ T , se I allo stato soddisfa ogni F ∈T . Anche in questo caso diciamo che I soddisfa T , o che T è vera in I oppure che I è un modello di T , e scriviamo I ⊨T , se I , σ ⊨T per ogni stato σ di I .

Se

σ σ

Le definizioni di equivalenza e conseguenza logica sono analoghe alle corrispettive proposizionali.

F ≡G sse per ogni interpretazione I e stato σ , I , σ ⊨ F sse I , σ ⊨ G F ⊨G sse per ogni interpretazione I e stato σ , se I , σ ⊨ F allora I , σ ⊨ G T ⊨G sse per ogni I e σ tali che I , σ ⊨ T si ha I , σ ⊨ G .

   Se

F  



è una formula diciamo che: per F è valida se per ogni interpretazione I L(F) e ogni stato σ di I si ha che I , σ ⊨ F F è soddisfacibile se esistono un’interpretazione tali che I per L(F) e uno stato σ di I I,σ ⊨F F è insoddisfacibile se per ogni interpretazione I per L(F) e ogni stato σ di I si ha I , σ ⊨ F 5

Se

T  



è un insieme di formule diciamo che: per T è valida se per ogni interpretazione I L(T ) e ogni stato σ di I si ha che I , σ ⊨ T T è soddisfacibile se esistono un’interpretazione I per L(T ) e uno stato σ di I tali che I , σ ⊨T T è insoddisfacibile se per ogni interpretazione I per L(T ) e ogni stato σ di I si ha I , σ ⊨ T , I ,σ ⊨F cioè se per qualche F ∈T ( F può dipendere da I e σ ).

Siano σ variabile,   Per

uno stato di un’interpretazione I , x una e due termini e una formula. Allora: s t F

σ (s { x /t })= σ [x /σ (t )]( s ) Se la sostituzione {x /t } è ammissibile in F , allora I , σ ⊨ F {x /t } se e solo se I , σ [ x /σ (t)]⊨ F . ogni

formula

F

si

ha

¬ ∀xF ≡ ∃x ¬ F

e

¬∃xF ≡ ∀x ¬ F Siano ⋆ uno fra ∧ ,∨ e Q uno di ∀ e ∃ . Per ogni formula F , ogni variabile x e ogni formula G in cui non è libera, si ha e QxF ⋆G ≡Qx (F ⋆G ) x G ⋆ QxF ≡Qx (G ⋆ F) . Per ogni formula F , ogni variabile G in cui x non è libera, si ha:     Siano   

∀xF → G ≡ ∃x (F → G) ∃xF →G ≡∀x (F → G) G→ ∀xF ≡ ∀x(G→ F) G→ ∃xF ≡∃x (G → F ) F

e

G formule, allora:

∀xF ∧ ∀xG≡ ∀x(F ∧G) ∃xF ∨∃xG ≡∃x( F ∨ G ) ∀xF → ∃xG ≡∃x (F →G ) 6

x

e ogni formula

Una formula F si dice in forma prenessa se è priva di Q 1 x 1 …Q k x k G dove quantificatori oppure è della forma G è una formula priva di quantificatori e Q 1 … Q k sono quantificatori.

3 – Metodo dei Tableaux γ formula

istanza

δ formula

istanza

∀xF ¬∃xF

F {x /a } ¬ F { x /a}

∃xF ¬ ∀xF

F {x /a } ¬ F { x /a}

Diciamo che F {x /a } o ¬ F { x /a} δ -formula relativa ad a .

G è una G ⊨ G1

Se

γ -formula e

G1

è l’istanza della

γ

e

una sua istanza allora

T un insieme di formule, G una δ -formula e una istanza di G relativa ad una costante che non compare né in T né in G . Se T , G è soddisfacibile, allora T , G1 è insoddisfacibile. Siano

G1

Una formula è di uno e uno solo dei tipi seguenti:      

Un letterale Una doppia negazione Una α -formula Una β -formula Una γ -formula Una δ -formula

L’algoritmo per la risoluzione dei tableaux nel caso predicativo è non deterministico, non gode della terminazione forte ed è una procedura per la semidecisione della validità o dell’insoddisfacibilità. 7

Da questo si deduce che se un enunciato è F insoddisfacibile o valido, l’algoritmo si fermerà. Se è soddisfacibile forse si fermerà o forse proseguirà all’infinito. Si noti che anche l’algoritmo di costruzione dei tableaux non prevede la sostituzione di un formula con un’altra logicamente equivalente ad essa. In questa versione dell’algoritmo escludiamo i simboli di funzione. Si noti quindi che gli unici termini chiusi sono i simboli di costante. L’algoritmo è uguale al caso proposizionale, ma si aggiungono i seguenti casi: 1. Se G è una γ -formula, sia a un simbolo di costante relativo alla variabile che compare nel nodo; se esso non esiste, sia a un nuovo simbolo di costante. Nel nuovo nodo aggiungo l’istanza di G relativa ad A , senza rimuovere le γ -formule 2. Se G è una δ -formula e a una costante che non compare nel nodo. Sia G' una istanza di G relativa ad a . Nel nuovo nodo si sostituisce G con G' . Si noti che le γ -formule vanno applicate a tutte le costanti introdotte: anche quelle introdotte successivamente all’aver istanziato la γ -formula. Per questo le γ -formule non vanno mai cancellate dalle etichette dei nodi. Sulla base di quest’ultima affermazione si deduce che l’ordine migliore sia α , β , γ , δ . I tableaux, nei confronti della conseguenza comportano come nel caso proposizionale.

logica, si

Costruzione sistematica del tableaux. Ad ogni passo, 

Se un nodo contiene una coppia complementare di letterali oppure se un nodo contiene solo letterali e γ -formule senza costanti assegnabili allora il nodo è una foglia 8

 

Se un nodo contiene solo letterali e γ -formule con costanti assegnabili allora è un γ -nodo. Negli altri casi è un nodo ordinario

Procediamo quindi in questo modo: 1. Se c’è un nodo ordinario lavoro prima su quello, come di consueto 2. Poi lavoro sugli δ -nodi: aggiungo tutte le istanze della γ -formula al nodo successivo un enunciato, se F insoddisfacibile allora ogni Sia F tableau sistematico per F è chiuso. Un insieme T si dice insieme di Hintikka se gode delle proprietà degli insiemi di Hintikka della logica proposizionale e: 1. Se una γ -formula appartiene a T , allora almeno un simbolo di costante appartiene a T 2. Se una δ -formula appartiene a T , allora almeno una delle sue istanze appartiene a T Come nella logica proposizionale, ogni insieme di Hintikka è soddisfacibile.

9...