LE TEORIE ASSIOMATICHE |
◆ Lista dei riferimenti bibliografici abbreviati
◆ Linguaggio oggetto e metalinguaggio
◆ Tavole di verità e connettivi logici
◆ Teoria formale del calcolo
delle proposizioni
◆ Definizione di linguaggio del
primo ordine
◆ Interpretazioni.
Soddisfacibilità. Verità. Modelli.
◆ Principali regole di inferenza
del linguaggio del primo ordine
◆ Teorie del primo ordine con eguaglianza
◆ Le definizioni nelle teorie del
primo ordine
◆ Le descrizioni definite nelle
teorie del primo ordine
◆ Esempi di teorie: Teoria dell'ordine parziale
◆ Esempi di teorie : Teoria dei gruppi
◆ Metateoremi sui linguaggi e le
teorie del primo ordine. Teoremi di completezza.
◆ Lista dei
riferimenti bibliografici abbreviati
[Be] Bernays, Axiomatic Set Theory, Dover, 1968
[Ben] Bencivenga, Il primo libro di logica, Boringhieri, 1984
[Co] Borowski-Borwein, Dizionario Collins della matematica, Gremese Editore, 1995
[En] Enderton, Elements of Set Theory, Academic Press,
1977
[Go] Goldrei, Classic Set Theory, Chapman & Hall,
1996
[Gö] Gödel, Opere, vol. I, Boringhieri, 1999
[Ha] Halmos, Naïve Set Theory, Springer Verlag, 1974
[Ho] Holz-Steffens-Weitz, Introduction to Cardinal Arithmetic,
Birkhauser, 1999
[JW] Just-Weese, Discovering Modern Set Theory, vol I,
American Mathematical Association, 1991
[Kl] Kline, Storia del pensiero matematico, Einaudi, 1996
[Lo] Lolli, Dagli
insiemi ai numeri, Boringhieri, 1994
[Lo74] Lolli, Teoria
assiomatica degli insiemi, Boringhieri, 1974
[MB] Mangione-Bozzi, Storia della logica, Garzanti, 1993
[Su] Suppes, Axiomatic Set Theory, Dover, 1960
[TZ] Takeuti-Zaring, Introduction to Axiomatic Set Theory,
Springer Verlag, 1971
[Me] Mendelson, Introduction to Mathematical Logic,
Chapman & Hall, 1997
[Me 34] Una teoria formale S è definita quando sono soddisfatte
le seguenti condizioni:
▸ E' dato un insieme
contabile (cioè finito o numerabile) di segni come simboli di S. Una sequenza
finita di simboli di S è chiamata espressione di S.
▸ Esiste un
sottoinsieme dell'insieme delle espressioni di S chiamato l'insieme
delle formule ben formate (fbf) di S. Deve
esistere una procedura definita per stabilire se una data espressione è una fbf.
▸ C'è un insieme di fbf
chiamate l'insieme degli assiomi di S. Deve esistere un modo per stabilire se una fbf è un assioma. In tal caso S è
chiamata teoria assiomatica.
▸ C'è un insieme finito
R1, …, Rn di relazioni tra fbf, chiamato regole di inferenza. Per ogni Ri
c'è un unico intero positivo j
tale che, per ogni insieme di j fbf
e ogni fbf B si può stabilire se le j fbf
date sono nella relazione Ri con B e, se è così, B è detto seguire
da o essere una diretta conseguenza della menzionata fbf in virtù di Ri.
Un esempio di regola di
inferenza è la regola modus ponens: C segue da B e da
B ➙ C. Questa non è altro che una relazione tra tutte le triple ordinate 〈B, B ➙ C, C〉 dove B e C sono
fbf arbitrarie del sistema formale.
▸ Una prova è una sequenza B1, …, Bk
di fbf tale che, per ogni i, o Bi
è un assioma di S o Bi è una diretta conseguenza di qualcuna delle precedenti fbf nella sequenza in virtù di una delle regole di
inferenza di S.
▸ Un teorema di
S è una fbf B di S tale che B è l'ultima fbf di qualche prova di S. Tale prova è chiamata prova di B in S.
Anche se S è assiomatico, cioè esiste una procedura definita per stabilire se una
qualsiasi fbf sia un assioma, la nozione di "teorema" non è
necessariamente definita dal momento che, in generale, non c'è una procedura definita per determinare, data una
fbf B, se c'è una prova di B. Una teoria per la quale esiste una tale procedura è chiamata
teoria decidibile, altrimenti è teoria indecidibile.
Se una teoria è una teoria
decidibile, idealmente una macchina logica può essere creata per testare se le fbf
sono teoremi laddove, per una teoria
indecidibile, è necessaria la creatività del logico per stabilire se le fbf sono teoremi
▸ Una fbf C è detta
essere una conseguenza in S di un insieme Γ di fbf se
e solo se c'è una sequenza B1, …, Bk di fbf tali che C è
in Bk e, per ogni i, o Bi è un'assioma o Bi
appartiene a Γ o è una diretta conseguenza, mediante qualche regola di
inferenza, di qualcuna delle precedenti fbf nella sequenza. Una tale sequenza è
chiamata prova (o deduzione)
di C da Γ. I membri di Γ sono chiamati le ipotesi
o premesse della prova. Viene utilizzata
l'espressione "Γ ⊦
C" come abbreviazione per "C è una conseguenza di Γ" e
talvolta "Γ ⊦S C" per indicare che la
deduzione avviene nel contesto della Teoria S.
Se Γ è un insieme finito possiamo scrivere "{B1, …, Bm} ⊦ C" o "B1, …, Bm ⊦ C". Se Γ è
l'insieme vuoto ∅ scriviamo "∅ ⊦ C" per indicare che C è
ovviamente un teorema. Normalmente, in questo caso, si omette il simbolo "∅" e si scrive
"⊦ C" per indicare che C è un
teorema.
▸ [Me 69] Per teoria del primo ordine si intende una teoria
formale le cui fbf sono scritte impiegando i simboli del linguaggio logico del
primo ordine, come ad esempio:
∃x1
∀x2 ∀x3 (R11(x1,0)
& R12(f12(x1,x2),x3))
Un linguaggio logico del primo
ordine impiega come simboli logici gli usuali connettivi logici
"&", ➙", "∨", "⇔", ecc. e in più il quantificatore universale "∀" e il
quantificatore esistenziale "∃". Come simboli non logici impiega i simboli Rmn
di relazione, quelli fmn di funzione, le variabili
individuali xi e le costanti individuali ui. In un
linguaggio logico del primo ordine, a differenza che in un linguaggio del
secondo ordine, la quantificazione universale ed esistenziale è ammessa solo in
riferimento alle variabili individuali, mentre non è ammessa in riferimento a
proprietà o funzioni o formule.
◆ Linguaggio oggetto e metalinguaggio
[Me
36] La parola "prova", nei testi di logica e di assiomatica, è usata in
due sensi distinti. Nel primo senso, ha un preciso significato come definito all'interno di una teoria
assiomatica: è un certo tipo di sequenza finita di
formule ben formate di un linguaggio formale L. In un altro senso, indica anche
certe sequenze del linguaggio corrente (integrato da varii termini tecnici) che
dovrebbero servire come una argomentazione che giustifica delle assernzioni
circa un linguaggio formale L o le teorie formali basate su di esso.
In generale, il linguaggio che stiamo studiando
(in questo caso L) è chiamato il linguaggio oggetto, mentre il inguaggio in cui
formuliamo e proviamo proposizioni circa il linguaggio oggetto è chiamato il
metalinguaggio. Il metalinguaggio potrebbe anche essere
formalizzato e essere soggetto di studio a sua volta, studio che sarà condotto
con un meta-metalinguaggio e così via. Per fare un esempio di linguaggio oggetto e metalinguaggio, pensiamo ad un corso di sanscrito. Il Sanscrito è il
linguaggio oggetto, mentre il metalinguaggio, il linguaggio che usiamo per parlare del Sanscrito è
l'italiano. La distinzione tra prova e metaprova (cioè una prova nel metalinguaggio)
conduce a una distinzione tra teoremi del linguaggio oggetto e metateoremi del
metalinguaggio. Per evitare confuzione
normalmente viene utilizzato il termine "proposizione" invece di "metateorema". La parola "metamatematica" si riferisce allo studio
dei linguaggi oggetto logici e matematici; talvolta la parola è ristretta a
quelle indagini che usano i cosiddetti "metodi costruttivi" o
"metodi finitari" in metamatematica.
◆ Tavole di verità e connettivi logici
[Me 11] Le proposizioni possono essere combinate in vari modi per formare proposizioni più complesse. Consideriamo qui le combinazioni ottenute con i
connettivi proposizionali, nelle quali la verità o falsità della nuova proposizione è determinata
dalla verità o falsità delle sue proposizioni componenti.
A |
∼A |
V |
F |
F |
V |
A |
B |
A ∧ B |
V |
V |
V |
V |
F |
F |
F |
V |
F |
F |
F |
F |
A |
B |
A ∨ B |
V |
V |
V |
V |
F |
V |
F |
V |
V |
F |
F |
F |
A |
B |
A ➙ B |
V |
V |
V |
V |
F |
F |
F |
V |
V |
F |
F |
V |
A |
B |
A ⇔ B |
V |
V |
V |
V |
F |
F |
F |
V |
F |
F |
F |
V |
[Me 13] I simboli
"∼", "∧", "∨", "➙", "⇔" sono chiamati connettivi proposizionali. Qualsiasi proposizione costruita applicando questi
connettivi ha un valore di verità che dipende dal valore di
verità delle proposizioni che lo costituiscono
Per rendere evidente ed esplicita questa dipendenza, diamo il nome di forma
enunciativa a un'espressione formata da lettere enunciative A, B, C ecc. applicando appropriatamente i connettivi proposizionali. Più precisamente:
(1) Tutte le lettere enunciative (lettere
maiuscole corsive) eventualmente con indice numerico sono forme enunciative
(2) Se A e B sono forme enunciative, allora lo
sono anche (∼A), (A ∧ B), (A ➙ B) e (A ⇔ B)
(3) Sono forme enunciative solo quelle espressioni determinate per mezzo della (1) e
della (2)
Ad ogni assegnazione di valori di verità V o F
alle lettere enunciative che compaiono in una forma
enunciativa corrisponde un valore di verità
per la forma enunciativa e questo si ottiene per mezzo delle tavole di verità per i connnettivi proposizionali. Perciò ciascuna forma
enunciativa determina una funzione di verità che può essere rappresentata graficamente da una tavola di verità per la forma enunciativa. Per esempio, la forma enunciativa (((∼A) ∨ B) ➙ C) ha la seguente tavola di verità:
A |
B |
C |
∼A |
((∼A) ∨ B) |
(((∼A) ∨ B) ➙ C) |
V |
V |
V |
F |
V |
V |
F |
V |
V |
V |
V |
V |
V |
F |
V |
F |
F |
V |
F |
F |
V |
V |
V |
V |
V |
V |
F |
F |
V |
F |
F |
V |
F |
V |
V |
F |
V |
F |
F |
F |
F |
V |
F |
F |
F |
V |
V |
F |
Ciascuna riga rappresenta un'assegnazione
di valori di verità alle lettere A, B, C e il corrispondente valore di verità assunto dalle forme enunciative che
appaiono nella costruzione di (((∼A) ∨ B) ➙ C).
[Me 15] Una
funzione di verità ad n argomenti si definisce come una funzione a n argomenti,
i cui argomenti e valori sono i valori di verità V e F. Come già visto,
qualsiasi forma enunciativa determina una corrispondente funzione di
verità.
[Me 15] Proposizioni atomiche sono quelle proposizioni che
non sono costituite da altre proposizioni. Ad esempio: "Se Mr Jones è felice,
Mrs. Jones non è felice, e se Mr. Jones on è felice, Mrs. Jones è felice"
non è una proposizione atomica, mentre "Mr. Jones è felice" è una
proposizione atomica.
Una forma enunciativa che sia sempre vera, indipendentemente dai valori
di verità delle sue lettere enunciative, si chiama tautologia.
Le tavole di verità costituiscono una procedura definita ed
efficace che ci permette di determinare
se una forma enunciativa è una tautologia.
Una proposizione A implica logicamente B se e solo se ogni assegnazione di valori di verità alle
lettere di B e C che rende B vera rende
vera anche C.
B e C sono logicamente
equivalenti se e solo se B e C hanno lo stesso valore di verità per qualsiasi assegnazione dei valori di verità alle lettere proposizionali di B e C.
[Me 18] Una forma
enunciativa che sia falsa per tutti i possibili valori di
verità delle sue lettere enunciative è detta una contraddizione.
Una proposizione che derivi da una tautologia sostituendo proposizioni a ogni lettera
enunciativa, una stessa lettera essendo rimpiazzata da una stessa proposizione, si dice logicamente vera.
Una proposizione che derivi per sostituzione da una
contraddizione viene detta logicamente falsa.
[Me 31] Una forma
proposizionale che risulti vera per qualche assegnazione di verità alle lettere
proposizionali da cui è composta è detta soddisfacibile.
◆ Teoria formale del calcolo delle proposizioni
[Me 34] Una teoria formale S è definita quando sono
soddisfatte le seguenti condizioni:
▸ E' dato un insieme
contabile (cioè finito o numerabile) di segni come simboli di S. Una sequenza
finita di simboli di S è chiamata espressione di S
▸ Esiste un sottoinsieme
dell'insieme delle espressione di S chiamato
l'insieme delle formule ben formate (fbf) di S. Deve esistere una "effective
procedure" [trad. it.
"procedimento effettivo"] per stabilire se una data
espressione è una fbf.
▸ C'è un insieme di fbf
chiamate l'insieme degli assiomi di S.
Deve esistere un modo per stabilire se una fbf
è un assioma. In tal caso S è chiamata teoria
assiomatica.
▸ C'è un insieme finito
R1, …, Rn di relazioni tra fbf, chiamato regole di inferenza. Per ogni Ri
c'è un unico intero positivo j tale che, per ogni insieme di j fbf e ogni fbf B si può stabilire se le j fbf date sono nella relazione Ri
con B e, se è così, B è detto seguire da o
essere una diretta conseguenza della
menzionata fbf in virtù di Ri.
Un esempio di regola di
inferenza è la regola modus ponens: C segue da B e da
B ➙ C. Questa non è altro che una relazione tra tutte le triple ordinate 〈B, B ➙ C, C〉 dove B e C sono
fbf arbitrarie del sistema formale.
▸ Una prova è una sequenza B1, …, Bk
di fbf tale che, per ogni i, o Bi
è un assioma di S o Bi è una diretta conseguenza di qualcuna delle precedenti fbf nella sequenza in virtù di una delle regole di
inferenza di S.
▸ Un teorema di
S è una fbf B di S tale che B è l'ultima fbf di qualche prova di S. Tale prova è chiamata prova di B in S.
Anche se S è assiomatico, cioè esiste una procedura definita per stabilire se una
qualsiasi fbf sia un assioma, la nozione di "teorema" non è
necessariamente definita dal momento che, in generale, non c'è una procedura definita per determinare, data una
fbf B, se c'è una prova di B. Una teoria per la quale esiste una tale procedura è chiamata decidibile, altrimenti è indecidibile.
Se una teoria è decidibile, idealmente una macchina logica può essere creata per testare se le fbf
sono teoremi laddove, per una teoria
indecidibile, è necessaria la creatività del logico per stabilire se le fbf sono teoremi.
▸ Una fbf è detta essere
una conseguenza in S di un insieme Γ di fbf se
e solo se c'è una sequenza B1, …, Bk di fbf tali che C è
in Bk e, per ogni i, o Bi è un'assioma o Bi
appartiene a Γ o è una diretta conseguenza, mediante qualche regola di
inferenza, di qualcuna delle precedenti fbf nella sequenza. Una tale sequenza è
chiamata prova (o deduzione) di C da Γ. I membri di Γ sono chiamati le ipotesi o premesse
della prova. Viene utilizzata l'espressione "Γ
⊦ C"
come abbreviazione per "C è una
conseguenza di Γ" e talvolta "Γ ⊦S C" per indicare che la
deduzione avviene nel contesto della Teoria S.
Se Γ è un insieme finito possiamo scrivere "{B1, …, Bm} ⊦ C" o "B1, …, Bm ⊦ C". Se Γ è
l'insieme vuoto ∅ scriviamo "∅ ⊦ C" per indicare che C è
ovviamente un teorema. Normalmente, in questo caso, si omette il simbolo "∅" e si scrive
"⊦ C" per indicare che C è un
teorema.
[Me 34] Viene presentato qui un
linguaggio L del primo ordine per l'assiomatizzazione del calcolo proposizionale
▸ I simboli di L sono
"∼", "➙", "(", ")" e le lettere Ai
con indice intero positivo: A1,
A2, … I simboli "∼" e "➙" sono chiamati connettivi primitivi e le
lettere sono chiamate lettere proposizionali.
▸ Viene definito
ricorsivamente il concetto di formula ben formata
(fbf).
▸ Tutte le lettere proposizionali sono formule
ben formate (fbf)
▸ Se B e C sono fbf, lo
sono anche "(∼B)" e "(B ➙ C)"
▸ Se B, C e D sono fbf
di L allora i seguenti sono assiomi di L
(A1) (B ➙ (C ➙ B))
(A2) ((B ➙ (C ➙ D)) ➙ ((B ➙ C) ➙ (B ➙ D)))
(A3) (((∼C) ➙ (∼B)) ➙ (((∼C) ➙ B) ➙ C))
▸ L'unica regola di
inferenza di L è il modus ponens (abbreviato MP): C è una diretta conseguenza di "B" e "(B ➙ C)"
[Me 40] Un breve sguardo rivela che tutti gli assiomi sono
tautologie. Si può provare che qualsiasi teorema della teoria assiomatica L del
calcolo proposizionale che abbiamo costruito è una tautologia. Infatti,
MP conduce da una tautologia ad un'altra tautologia, ed è l'unica regola di
inferenza ammessa.
[Me 42] Per la teoria assiomatica
del calcolo proposizionale che abbiamo costruito si può provare la completezza: se una fbf B di L è una tautologia, allora è un teorema di
L.
[Me 42] Parimenti si può provare che L è consistente: cioè non esiste alcuna fbf A tale che
tanto A quanto ∼A siano teoremi di L.
[Me 43] Una teoria nella quale
non tutte le fbf sono teoremi si dice assolutamente
consistente.
Un sottoinsieme Y di assiomi si dice indipendente
se qualche fbf in Y non può essere provata dall'insieme degli assiomi che non
sono in Y.
◆ Definizione di linguaggio del primo ordine
[Me 56]
L'aggettivo "del primo ordine" serve
a distinguere un linguaggio con quantificatori da altri linguaggi con
quantificatori che possiedono predicati che hanno come argomenti altri predicati o funzioni o in cui è permessa la quantificazione di predicati o funzioni.
[Me 51] Nel
linguaggio con quantificatori esistono variabili
individuali x1, x2, … costanti
individuali a1, a2, …, lettere
predicative Akn, lettere
funzionali fkn. L'apice "n" indica il
numero di argomenti, mentre il pedice distingue tra predicati o funzioni con lo
stesso numero di argomenti.
I termini
sono:
▸ variabili individuali
▸ costanti individuali
▸ Se fkn
è una lettera funzione e t1, …, tn sono termini, allora fkn(t1,
…, tn) è un termine
Una formula atomica
è data dall'applicazione a termini di una lettera predicativa.
Una formula ben
formata (fbf) è definita nel seguente
modo:
▸ Ogni formula atomica è
una fbf
▸ Se B, C sono fbf
allora B ➙ C, ∼B, ∀x B sono fbf
I simboli indicati sopra sono detti simboli primitivi, in
contrapposizione ad altri simboli, introdotti mediante definizioni.
Nell'espressione "((∀x) B)
"B" è chiamata campo di applicazione del
quantificatore "(∀y)". Si noti che B non necessariamente contiene la
variabile x. In questo caso "((∀x) B)" va interpretata come se dicesse la stessa cosa
di "B".
L'occorrenza di una variabile è detta essere occorrenza vincolata in una fbf B se appare come
la x nel quantificatore ∀x o è nel campo d'azione di un quantificatore "∀x" in B.
Altrimenti è detta occorrenza libera.
Una variabile libera (vincolata) in una fbf è una variabile che ha una occorrenza libera (vincolata)
nella formula. Una variabile può essere sia libera che vincolata nella stessa
fbf. Ad
esempio, nella formula:
A12(x1,x2)
➙ (∀x1) A11(x1)
la
variabile x1 è sia libera che vincolata.
Spesso indicheremo che
qualcuna delle variabili xi1, …, xin sono variabili
libere in una fbf B scrivendo B(xi1,…, xin). Questo non
significa che B contiene queste variabili come variabili libere, né che B non
contiene altre variabili libere. Questa notazione è utile per scrivere B(t1, …, tn) allo scopo di indicare che si è operata la sostituzione in
B dei termini t1,…, tn in tutte le occorrenze libere (se
esistono) di xi1, …, xik rispettivamente.
Se B e una fbf e t è un termine allora si dice
che t è libero per xi in una fbf B
se non esistono occorrenze libere di xi in B nel campo d'azione di
un qualsiasi quantificatore ∀xj, dove xj è una variabile in t. Il succo della faccenda
è che possiamo sostituire t a xi senza pericolo che una variabile xj
di t finisca nell'ambito di un quantificatore ∀xj.
[Me 58] Una fbf chiusa è una fbf senza variabili libere, ed è
detta proposizione (sentence)
I
linguaggi particolari del primo ordine sono concepiti in relazione alla materia
da studiare. Un linguaggio per descrivere l'aritmetica può contenere lettere
funzioni per l'addizione e la moltiplicazione e una lettera predicato per
l'eguaglianza, mentre un linguaggio per la geometria avrebbe lettere predicato
per l'eguaglianza e le nozioni di punto e linea ma non possiederebbe lettere
funzione.
[Me 57] Un
linguaggio del primo ordine L contiene i seguenti simboli:
▸ I connettivi proposizionali ∼ e ➙ e il quantificatore universale ∀
▸ Segni di
interpunzione: le parentesi tonde e la virgola
▸ Un insieme contabile
di variabili individuali x1, x2,
…
▸ Un insieme finito o
contabile, che può anche essere vuoto, di lettere
funzionali.
▸ Un insieme finito o
contabile , che può anche essere vuoto, di costanti
individuali.
▸ Un insieme non vuoto
di lettere predicative.
Le
espressioni (B ∧ C), (B ∨ C) e (B ⇔ C) sono definite nel modo seguente:
(B ∧ C) sta per ∼(B ➙ ∼C)
(B ∨ C) sta per (∼B) ➙ C
(B ⇔ C) sta per (B ➙ C) ∧ (C ➙ B)
((∃x) B) sta per (∼((∀x)(∼B))
Riguardo le parentesi si seguiranno
le seguenti convenzioni:
▸ Possono essere omesse le parentesi più esterne di una fbf
▸ Si conviene il seguente
ordine di applicazione dei
connettivi: "∼", "∧", "∨","∀y", "∃x"," ➙", "⇔"
▸ Per ripristinare le parentesi eliminate in base alle due regole precedenti si segue il seguente procedimento:
(i) Se il connettivo è "∼" e precede una fbf B, si scrive (∼B)
(ii) Se il connettivo è un connettivo binario C ed è
preceduto da una fbf B e seguito da una fbf D, si scrive (B C
D)
(iii) Se non ricorre né il caso (i) né il caso (ii),
si ignorano temporaneamente i connettivi
e si individua l'occorrenza più a sinistra del più forte dei connettivi rimanenti e si ripete il procedimento (i) – (iii)
Ecco un esempio di come si
reintroducono le parentesi di una formula:
A ⇔ (∼B) ∨ C ➙ A
A ⇔ ((∼B) ∨ C) ➙ A
A ⇔ (((∼B) ∨ C) ➙ A)
(A ⇔ (((∼B) ∨ C) ➙ A))
Un termine di L
è un termine i cui simboli sono simboli di L
[Me 87] Un termine chiuso è un termine senza variabili.
Una fbf di L
è una fbf i cui simboli sono simboli di L
Si noti
che in un dato linguaggio ℒ possono mancare alcune o tutte le lettere
funzione e le costanti individuali e alcune (ma non tutte) le lettere
predicato.
Le costanti individuali, le lettere funzionali e
le lettere predicative sono chiamate le costanti non logiche di L.
◆ Interpretazioni. Soddisfacibilità. Verità. Modelli.
[Me 56] Dato un
linguaggio del primo ordine L, una interpretazione
M di L consiste nei seguenti elementi:
▸ Un insieme non vuoto
D, chiamato il dominio dell'interpretazione
▸ Per ogni lettera
predicativa Ajn di L, l'assegnazione di una relazione n-aria (Ajn)M
in D
▸ Per ogni lettera
funzionale fjn di L, l'assegnazione di una operazione
n-aria (fjn)M
in D (cioè una funzione Dn ➙ D)
▸ Per ogni costante
individuale ai di L l'assegnazione di un elemento fisso (ai)M
di D
Si tenga presente che un'interpretazione
comprende un dominio che può avere molti più elementi delle costanti
individuali.
Le variabili variano su tutto D e alle costanti
logiche ∼, ➙ e ∀ viene dato il significato usuale. Si ricordi che una
relazione n-aria è un sottoinsieme di Dn.
Per una data interpretazione una fbf chiusa
(senza variabili libere) rappresenta una proposizione cheè o vera o falsa,
mentre una fbf con variabili libere diventa una relazione sul dominio
dell'interpretazione che può essere soddisfatta (vera) per alcuni valori nel
dominio delle variabili libere e non soddisfatta (falsa) per altri.
[Me 59] Sia M una
interpretazione di un linguaggio L e D il dominio di M. Sia Σ l'insieme di
tutte le successioni contabili di elementi
di D.
Per ogni data sequenza s = s1, s2,
… in Σ definiamo una funzione s* che assegna a ciascun termine t di L un
elemento s*(t) in D:
▸ Se t è una variabile
xj allora s*(t) = sj
▸ Se t è una costante
individuale aj allora s*(t) è l'interpretazione (aj)M
di questa costante
▸ Se fjn
è una lettera funzionale, allora:
s*(fkn(t1, …, tn)) = (fkn)M(s*(t1),
…, s*(tn))
[Me 60]
Procediamo ora a definire la soddisfacibilità.
Definiremo cosa vuol dire che "una successione
s soddisfa una fbf B":
▸ Se B è una fbf Akn(t1,
…, tn) e (Akn)M è la corrispondente
relazione n-aria dell'interpretazione, allora una successione s = s1,
s2, … soddisfa una fbf B sse:
(Akn)M(s*(t1), …,
s*(tn))
cioè sse la n-pla <s*(t1), …, s*(tn)>
è nella relazione (Akn)M
▸ s soddisfa ∼B sse s non soddisfa B
▸ s soddisfa B ➙ C sse non soddisfa B o
soddisfa C
▸ s soddisfa ∀xi B
sse ogni successione s' che differeisce da s al massimo nell'i-esimo componente
soddisfa B
[Me 60] B è una fbf vera per una interpretazione M (scritto ⊨M B) sse ogni successione in Σ soddisfa B
B è una fbf falsa
per una interpretazione M sse nessuna sequenza in Σ soddisfa B
Una interpretazione M è un modello per un insieme di fbf Γ sse ogni fbf in
Γ è vera per M
Per chiusura di una
fbf B intendiamo la formula con premessi a B tanti quantificatori
universali quante sono le variabili libere in B, secondo l'ordine decrescente
degli indici
Un esempio di forma
proposizionale (instance of a statement form)
è una fbf ottenuta dalla forma proposizionale
sostituendo fbf a tutte le lettere proposizionali, tutte le occorrenze
della medesima lettera proposizionale essendo rimpiazzate dalla stessa fbf.
[Me
62] Siano xi1, …, xik
k distinte variabili in ordine crescente di pedice. Sia B(xi1,
.., xik) una fbf che ha xi1, …, xik come sue
uniche variabili. L'insieme di k-ple 〈b1, …, bk〉 di elementi del dominio D tali che una qualsiasi sequenza
con b1, …, bk nel suo i1, …, ik-esimo
posto soddisfa B(xi1, …, xik) è chiamata la relazione (o proprietà)
dell'interpretazione definita da B.
Estendendo la nostra terminologia, diremo che ogni k-pla 〈b1, …, bk〉 nella relazione soddisfa B(xi1, …, xik)
nell'interpretazione M; questo sarà scritto:
⊨M B[b1, …, bk]
[Me 65] B è una fbf logicamente valida sse B è vera per ogni
interpretazione.
B è una fbf
soddisfacibile sse esiste una interpretazione per la quale B soddisfa
almeno una successione
E' ovvio che B è logicamente valido se e solo se
∼B è non
soddisfacibile, e B è soddisfacibile se e solo se ∼B non è logicamente
valido.
Se B è una fbf chiusa, allora sappiamo che B è vera o falsa per ogni data interpretazione; cioè B è soddisfatta da tutte le sequenze o da
nessuna. Dunque, se B è chiusa, allora B è soddisfacibile se e solo se B è vero
per alcune interpretazioni.
Un insieme Γ di fbf è detto soddisfacibile
se e solo se c'è una interpretazione in cui c'è una sequenza che soddisfa ogni
fbf di Γ.
B è una fbf
contraddittoria sse B è falsa per ogni interpretazione
B implica
logicamente C sse, in ogni interpretazione, ogni successione che
soddisfa B soddisfa anche C.
B e C
sono dette logicamente equivalenti se e solo
se si implicano l'un l'altra.
B è una conseguenza logica
di un insieme di fbf Γ sse in
ogni interpretazione ogni successione che soddisfa ogni fbf in Γ soddisfa
anche B
Le fbf di un insieme sono dette fbf compatibili sse la loro congiunzione è
soddisfacibile.
[Me 111] Si dice
che una interpretazione M di qualche linguaggio L è isomorfa ad una
interpretazione M* di L (interpretazioni isomorfe)
sse c'è una corrispondenza biunivoca g (chiamata isomorfismo) tra il dominio D
di M il dominio D* di M* tale che:
▸ Per ogni lettera
predicativa Ajn di L e per ogni b1, …, bn
in D, ⊨M Ajn[b1,…,bn]
sse ⊨M* Ajn[g(b1),…,g(bn)]
▸ Per ogni lettera funzionale
fjn di L e per ogni b1, …, bn in D,
g(fjn(b1, …, bn)) = fjn(g(b1,
…, g(bn))
▸ Per ogni costante
individuale aj di L, g((aj)M) = (aj)M*
Per indicare tale isomorfismo si scrive M
≈ M* e i domini devono essere della stessa cardinalità.
[Me 69] Sia L un
linguaggio del primo ordine. Una teoria del primo
ordine nel linguaggio L è una teoria formale K i cui simboli e fbf sono i simboli e fbf di L e i cui assiomi e
regole di inferenza sono stecificati nel modo seguente.
Gli assiomi di K sono divisi in due classi: gli assiomi logici e gli assiomi
propri o assiomi non logici.
Se B, C, D sono fbf di L, allora i seguenti sono
assiomi logici di K:
▸ B ➙ (C ➙ B)
▸ (B ➙ (C ➙ D)) ➙ ((B ➙ C) ➙ (B ➙ D))
▸ (∼C ➙ ∼B) ➙ ((∼C ➙ B) ➙ C)
▸ (∀xi)
B(xi) ➙ (B(t) se B(xi)
è una fbf di L e t è un termine di L che è libero per xi in B(xi).
Si noti che t può anche essere identico a xi cosicché tutte le fbf (∀xi) B ➙ B sono assiomi in virtà di questo assioma
▸ (∀xi) (B
➙ C) ➙ (B ➙ (∀xi) C) se B non contiene occorrenze libere di xi.
Si noti che sia gli assiomi logici che, molto
spesso, gli assiomi propri, non sono veri assiomi, ma istanze
di assiomi, che comprendono infiniti assiomi singoli, tanti quanti risultano
dalla sostituzione dei simboli che stanno al posto di termini o fbf.
Vedi Mendelson p. 104 per l'impiego del concetto
di istanza di assioma
Gli assiomi propri non possono essere specificati, dal momento che variano da teoria a teoria. Una
teoria del primo ordine in cui non
ci sono assiomi propri è chiamato un calcolo predicativo del primo ordine
[Me 109] Un
calcolo predicativo in cui non vi sono lettere funzionali o costanti
individuali e in cui, per ogni intero positivo n, ci sono infinite lettere predicative
con n argomenti, prende il nome di puro calcolo
predicativo.
Le regole di inferenza di una teoria del primo ordine sono:
▸ Modus Ponens: C segue da B ➙ C e da B
▸ Generalizzazione: (∀xi) B segue da B
Sono spesso utilizzate delle regole
derivate, che possono derivarsi dalle
due precedenti (Modus Ponens e
Generalizzazione) ma che è più pratico utilizzare direttamente (vedi il paragrafo dedicato
alle principali regole di inferenza)
[Me 70] Sia K una
teoria del primo ordine nel
linguaggio L. Per modello di K intendiamo una interpretazione di L per cui tutti gli assiomi
di K sono veri.
Se le regole modus ponens e generalizzazione sono applicate a fbf che sono vere per una data interpretazione allora i risultati di queste applicazioni son anche veri. Quindi ogni teorema di K è vero in
ogni modello di K.
[Me 72] Una teoria coerente (ingl. consistent) K è quella in
cui nessuna fbf B e la sua negazione ∼B sono entrambe provabili in K.
Una teoria incoerente
(ingl. inconsistent) è una teoria non-consistente.
[Me 86] Una
teoria K è una teoria completa se, per ogni fbf chiusa B di K, si ha ⊦K B oppure ⊦K ∼B
[Me 94] Una
teoria K è finitamente assiomatizzabile se
c'è un insieme finito di proposizioni Γ tale che, per qualsiasi
proposizione B si ha ⊦K B sse Γ ⊦ B (si ricordi che una
proposizione è lo stesso che una fbf chiusa cioè senza variabili libere)
[Me 116] Una teoria decidibile è una teoria in cui esiste una
procedura effettiva per stabilire se una data fbf sia un teorema.
◆ Principali regole di inferenza del linguaggio del primo
ordine
▸ Regola
dell'inserzione di "∀"
[Ben 101] Data una fbf che
contiene una variabile individuale a che non compare né nelle premesse né compare nella fbf dopo l'inserzione, si può premettere "∀x" alla formula e sostituire tutte le occorrenze di a
con la variabile x (cioè "a", oltre che nelle premesse, non deve
comparire nella fbf dopo la trasformazione)
▸ Regola
dell'inserzione di "∃"
Da "∀x B(x)" si inferisce "∃x Bx"
▸ Regola dell'eliminazione
di "∀"
▸ Regola
dell'eliminazione di "∃"
▸ Regola della
sostituzione di una variabile con una costante
▸ Particolarizzazione: Se t è libero per x in B(x), allora (∀x) B(x) ⊦ B(t)
▸ Regola
dell'esistenza: Sia t un termine libero per x in una fbf B(x,t),
e B(t,t) sia ricavabile da B(x,t) sostituendo tutte le occorrenze libere di x
con t. (si noti che B(x,t) potrebbe contenere o non
contenere occorrenze di t). Allora, B(t,t) ⊦ (∃x) B(x,t)
▸ Altre regole
derivate:
∼∼B ⊦ B
B ⊦ ∼∼B
B ∧ C ⊦ B
B ∧ C ⊦ C
∼(B ∧ C) ⊦ ∼B ∨ ∼C
B,C ⊦ B ∧ C
B ∨ C, ∼B ⊦ C
B ∨ C, ∼C ⊦ B
∼(B ∨ C) ⊦ ∼B ∧ ∼C
B ➙ D, C ➙ D, B ∨C ⊦ D
B ⊦ B ∨ C
C ⊦ B ∨ C
B ➙ C, ∼C ⊦ ∼B
B ➙ ∼C,C ⊦ ∼B
∼B ➙ C, ∼C ⊦ B
∼B ➙ ∼C,C ⊦ B
∼(B ➙ C) ⊦ B
∼(B ➙ C) ⊦ ∼C
B,∼C ⊦ ∼(B ➙ C)
B ➙ C ⊦ ∼C ➙ ∼B
∼C ➙ ∼B ⊦ B ➙ C
B ⇔ C, B ⊦ C
B ⇔ C, ∼B ⊦ ∼C
B ⇔ C, C ⊦ B
B ➙ C, C ➙ B ⊦ B ⇔ C
B ⇔ C ⊦ ∼B ⇔ ∼C
∼B ⇔ ∼C ⊦ B ⇔ C
◆ Teorie del primo ordine con eguaglianza
[Me 94] Sia K una
teoria che ha come una delle sue lettere predicato la lettera A12.
Scriviamo t = s come abbreviazione per A12(t,s)
e t ≠
s come abbreviazione per ∼A12(t,s)
Allora K è chiamata una teoria del primo ordine con eguaglianza (o semplicemente teoria con eguaglianza)
se i seguenti sono teoremi di K:
(1) ∀x1 x1
= x1 (riflessività
dell'eguaglianza)
(2) x = y ➙ (B(x,x) ➙ B(x,y)) (sostitutività dell'eguaglianza)
dove
x e y sono variabili qualsiasi, B(x,x) è una qualsiasi fbf e B(x,y) proviene da
B(x,x) mediante sostituzione di alcune, ma non necessariamente tutte, le
occorrenze libere di x mediante y, con la condizione che y sia libero per x in B(x,x). Così, B(x,y) può contenere o
non contenere occorrenze libere di x.
Da
(1) e (2) derivano le seguenti proprietà dell'eguaglianza:
▸ t = t
per qualsiasi termine t
▸ t = s ➙ s = t
▸ r = s ➙ (s = t ➙ r = t)
▸ ∀x (B(x) ⇔ (∃y (x = y & B(y)))
▸ ∀x (B(x) ⇔ (∀y (x = y ➙ B(y))
▸ ∀x ∃y (x = y)
▸ (x = y) ➙ (f(x) = f(y))
dove f è una lettera funzionale di un solo argomento
▸ (B(x) & x = y) ➙ B(y)
se y è libero per x in B(x)
I
teoremi (1) e (2) sono veri in ogni interpretazione M in cui (A12)M
è la relazione di identità sul dominio D.
[Me
99]
Si noti che l'eguaglianza mediante (1) e (2) è stata introdotta utiilzzando
metalinguaggio (si è utilizzato il simbolo B(x,x) e B(x,y)). In talune teorie è
possibile introdurla mediante definizione, cioè è formulabile una fbf E(x,y) da
cui discendono (1) e (2). Anche a queste si estende la definizione di teorie
con uguaglianza.
Nelle
teorie con uguaglianza è possibile introdurre un nuovo simbolo ∃1x, mediante la seguente definizione:
∃1x B(x) sta per ∃x B(x) & ∀x ∀y (B(x) & B(y) ➙ x = y)
[Me
100]
In ogni modello di una teoria K con identità, la relazione E nel modello che
corrisponde alla lettera predicativa "=" è una relazione di
equivalenza. Se questa relazione E è la relazione di identità sul dominio del
modello, allora il modello è detto essere un modello
normale.
[Me
100]
Un qualsiasi modello M di una teoria K con identità può essere contratto in un modello normale M* per K prendendo
come dominio D* di M* l'insieme delle classi di equivalenza determinate dalla
relazione E nel dominio D di M.
◆ Le definizioni nelle teorie del primo ordine
[Me
104]
Data una teoria K con identità, assumiamo che:
⊦K ∃1u (B(u, y1, …, yn).
Sia K# la teoria con
identità ottenuta aggiungendo a K una nuova lettera funzionale f di n argomenti
e l'assioma proprio:
B(f(y1,
…, yn), y1, …, yn)
ovvero,
con forma lievemente diversa:
∀u (u = f(y1, …, yn)
➙ B(u, y1, …, yn)
Vanno
aggiunte inoltre tutte le istanze di assiomi logici che possano contenere f.
Allora esiste una funzione effettiva (ingl. effective) che porta ciascuna fbf C
di K# in una fbf C# di K tale che:
▸ Se f non occorre in C, allora C# è
C
▸ (∼C)# = ∼(C#)
▸ (C ➙ D)# +
C# ➙ D#
▸ (∀x C)# è ∀x C#
▸ ⊦K# (C ⇔ C#)
▸ Se ⊦K# C allora ⊦K C#
◆ Le descrizioni definite nelle teorie del primo ordine
[Me
106]
Frasi descrittive del tipo "l'oggetto u tale che B(u,y1, …, yn)
sono molto comuni nel linguaggio ordinario e anche in matematica. Tali frasi
sono chiamate descrizioni definite. Denotiamo con:
ιu(B(u,y1,…,yn))
l'unico
oggetto u tale che B(u,y1, …, yn) se tale oggetto esiste.
Se non esiste possiamo stabilire che ιu(B(u,y1,…,yn))
sia un oggetto prefissato o possiamo considerare l'espressione priva di senso.
◆ Esempi di teorie: Teoria dell'ordine parziale
[Me 71] Supponiamo che il linguaggio L abbia una singola lettera predicativa A22 e nessuna lettera
funzione e costanti individuali. Scriveremo xi < xj
invece di A22(xi,xj). La teoria K
ha due assiomi propri:
▸ ∀x1 (∼x1 < x1) (irriflessività)
▸ ∀x1 ∀x2 ∀x3 (x1
< x2 ∧ x2 < x3 ➙ x1 < x3) (transitività)
Un modello di questa teoria è chiamato una
struttura di ordine parziale
◆ Esempi di teorie: Teoria dei gruppi
[Me 71] Il
linguaggio L abbia una sola lettera predicativa A12,
una sola lettera funzione f12, e una sola costante
individuale a1. Per conformarci alla
notazione ordinaria scriveremo t = s invece di A12(t,s),
t + s invece di f12(t,s) e 0 invece di a1. Gli
assiomi propri di K sono:
▸ ∀x1 ∀x2 ∀x3 (x1 + (x2 + x3)
= (x1 + x2) + x3) (associatività)
▸ ∀x1 (0
+ x1 = x1)
(identity)
▸ ∀x1 ∃x2 (x2
+ x1 = 0) (inverso)
▸ ∀x1 (x1
= x1) (riflessività di
"=")
▸ ∀x1 ∀x2 (x1
= x2 -> x2 = x1) (simmetria di "=")
▸ ∀x1 ∀x2 ∀x3 (x1
= x2 ∧ x2 = x3 -> x1 = x3) (transitività di "=")
▸ ∀x1 ∀x2 ∀x3 (x2
= x3 -> x1 + x2 = x1 + x3
∧ x2
+ x1 = x3 + x1) (sostitutività di "=")
Un modello per questa teoria, in cui
l'interpretazione di
"=" è la relazione di identità è chiamato un gruppo. Un gruppo è detto abeliano se,
in aggiunta, la fbf:
∀x1 ∀x2 (x1
+ x2 = x2 + x1)
è vera.
Le
teorie di ordine parziale e dei gruppi sono entrambe assiomatiche. In generale,
una teoria con un numero finito di assiomi propri è assiomatica, dal momento
che è ovvio che si può effettivamente decidere se una data fbf sia un assioma
logico.
◆ Metateoremi sui linguaggi e le teorie del primo ordine.
Teoremi di completezza.
▸ [Me 84] Come già detto, una
teoria del primo ordine in cui non
ci sono assiomi propri è chiamato un calcolo predicativo del primo ordine.
[Me 86] Come già detto, una
teoria K è una teoria completa se, per ogni fbf chiusa B di K, si ha ⊦K B oppure ⊦K ∼B
(Teorema di completezza di Gödel, 1936) Si può dimostrare che
i teoremi del calcolo predicativo del primo ordine K coincidono esattamente con
le fbf logicamente valide di K.
▸ [Me 90] Ogni teoria coerente ha
un modello numerabile
▸ [Me 92] (Teorema di Skolem-Löwenheim) Ogni teoria che ha un modello ha anche un modello numerabile
▸ [Me 116] Se una teoria K è
assiomatica e completa, allora è decidibile
▸ [Me 100] (Godel, 1930) Ogni
teoria con identità K che sia coerente ha un modello normale finito o
numerabile
▸ [Me 101] (Estensione del teorema
di Skolem-Löwenheim) Ogni teoria con identità
K che ha un modello normale infinito ha un modello numerabile