LE TEORIE ASSIOMATICHE

 

back to HomePage

 

 

 

 

◆  Lista  dei riferimenti bibliografici abbreviati

◆  Linguaggio oggetto e metalinguaggio

◆  Tavole di verità e connettivi logici

◆  Teoria formale del calcolo delle proposizioni

◆  Definizione di teoria formale. Definizione di teoria assiomatica. Definizione di teoria del primo ordine

◆  Definizione di linguaggio del primo ordine

◆  Interpretazioni. Soddisfacibilità. Verità. Modelli.

◆  Teorie del primo ordine

◆  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

 

back to Index

 

 

 

[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

 

 

 

 

 

◆  Definizione di teoria formale. Definizione di teoria assiomatica. Definizione di teoria del primo ordine.

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

 [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

 

back to Index

 

 

 

[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.

 

back to Index

 

 

 

[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à.

 

 

 

 

 

◆  Teorie del primo ordine

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

▸  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

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

[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

 

back to Index

 

 

 

[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.

 

back to Index

 

 

 

▸  [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