Calcolo dei predicati

Il calcolo dei primi predicati di ordine o di calcolo del rapporto , o la logica del primo ordine , o la logica quantificational o semplicemente calcolo dei predicati è una formalizzazione del linguaggio della matematica proposti da Gottlob Frege , tra la fine del XIX ° secolo e l'inizio del XX ° secolo . La logica del primo ordine ha due parti:

la sintassi definisce il vocabolario simbolico di base e le regole che consentono la costruzione di affermazioni complesse,
la semantica interpreta queste affermazioni come espressione della relazione tra gli elementi di un dominio, detto anche modello .

A livello sintattico, le lingue del primo ordine si oppongono a due grandi classi linguistiche:

i costituenti utilizzati per identificare o denominare elementi del dominio: variabili , simboli di costanti , termini ;
i costituenti utilizzati per esprimere proprietà o relazioni tra questi elementi: predicati e formule .

Un predicato è un'espressione linguistica che può essere collegata a uno o più elementi del dominio per formare una frase. Ad esempio, nella frase "Mars is a planet", la frase "is a planet" è un predicato che è collegato al nome (simbolo costante) "Mars" per formare una frase. E nella frase "Giove è maggiore di Marte", la frase "è maggiore di" è un predicato che si riferisce ai due nomi, "Giove" e "Marte", per formare una frase.

In logica matematica, quando un predicato è legato ad un'espressione, si dice che esprime una proprietà (come la proprietà di essere un pianeta), e quando è legato a due o più espressioni, si dice che esprime una relazione ( come il rapporto di essere maggiore). Quindi possiamo ragionare su affermazioni come "Tutto è bello" e "C'è tale che per tutto , è amico di ", che espresso simbolicamente si traduce nella formula: $X$ $X$ $sì$ $X$ $sì$

{\ displaystyle \ forall x ~ \ mathrm {bello} (x)}

e .

{\ displaystyle \ esiste x \ forall y ~ \ mathrm {amici} (x, y)}

Va notato, tuttavia, che la logica del primo ordine non contiene alcuna relazione specifica (come tale relazione di ordine, inclusione o uguaglianza); si tratta infatti solo di studiare il modo in cui si dovrebbe parlare e ragionare con le espressioni del linguaggio matematico.

Le caratteristiche della logica del primo ordine sono:

l'uso di variabili come , ecc. denotare elementi del campo dell'interpretazione; $X$ $sì,$
l'uso di predicati (o relazioni ) sugli elementi;
l'uso di connettori logici (e, or, implica ecc.);
l'uso di due quantificatori , uno universale ("qualunque", "per tutto" notato ∀ ) e l'altro esistenziale ("ne esiste almeno uno... tale che", notato ∃ ).

Il calcolo dei predicati egualitari di primo ordine aggiunge al calcolo dei predicati un simbolo di relazione, uguaglianza, la cui interpretazione è l'asserzione che due elementi sono uguali e che viene assiomatizzato di conseguenza. A seconda del contesto, possiamo semplicemente parlare del calcolo dei predicati per il calcolo dei predicati egualitari.

Si parla di logica del primo ordine contrapposta a logiche di ordine superiore , dove possiamo quantificare anche su predicati o funzioni oltre che su variabili. Inoltre, questo articolo tratta solo della logica del primo ordine classica , ma si noterà che esiste anche una logica del primo ordine intuizionista .

introduzione

Mentre la logica proposizionale si occupa di semplici proposizioni dichiarative, la logica del primo ordine copre inoltre predicati e quantizzazione.

Un predicato prende come input una o più entità del dominio del discorso e come output è Vero o Falso. Considera le due frasi "Socrate è un filosofo" e "Platone è un filosofo". Nella logica proposizionale, queste frasi sono considerate non correlate e possono essere denotate, ad esempio, da variabili come p e q. Il predicato "è un filosofo" appare in entrambe le frasi, la cui struttura comune è "a è un filosofo". La variabile a è istanziata come "Socrate" nella prima frase, ed è istanziata come "Platone" nella seconda frase. Mentre la logica del primo ordine consente l'uso di predicati, come "è un filosofo" in questo esempio, la logica proposizionale no.

Le relazioni tra i predicati possono essere stabilite utilizzando connettori logici. Consideriamo, ad esempio, la formula del primo ordine "se a è un filosofo, allora a è uno studioso". Questa formula è un'affermazione condizionale la cui ipotesi è "a è un filosofo" e la conclusione "a è uno studioso". La verità di questa formula dipende dall'oggetto denotato da a, e dalle interpretazioni dei predicati "è un filosofo" e "è uno studioso".

I quantificatori possono essere applicati alle variabili in una formula. La variabile a della formula precedente può essere quantificata universalmente, ad esempio con la frase di primo ordine "Per tutti a, se a è filosofo, allora a è studioso". Il quantificatore universale "per ciascuno" in questa frase esprime l'idea che l'affermazione "se a è un filosofo, allora a è uno studioso" è valida per tutte le scelte di a.

La negazione della frase "Per tutti a, se a è un filosofo, allora a è uno studioso" è logicamente equivalente alla frase "C'è un tale che a è un filosofo e a non è uno studioso". Il quantificatore esistenziale "esiste" esprime l'idea che l'affermazione "a è un filosofo e a non è uno studioso" è valida per una certa scelta di a.

I predicati "è un filosofo" e "è uno studioso" prendono ciascuno una singola variabile. In generale, i predicati possono accettare più di una variabile. Nella frase di primo ordine "Socrate è il maestro di Platone", il predicato "è il maestro di" prende due variabili.

Storia

Immanuel Kant credeva erroneamente che la logica del suo tempo, quella di Aristotele , fosse una scienza completa e definitivamente compiuta (prefazione alla seconda edizione della critica della ragion pura , 1787). Logici del XIX ° secolo, si rese conto che la teoria di Aristotele dice poco o nulla la logica delle relazioni. Gottlob Frege e molti altri hanno colmato questa lacuna definendo il calcolo dei predicati del primo ordine.

Kurt Gödel dimostrò nel 1929 (nella sua tesi di dottorato) che il calcolo dei predicati è completo, nel senso che possiamo dare un numero finito di principi ( assiomi logici , schemi di assiomi logici e regole di deduzione ) che sono sufficienti per dedurre meccanicamente tutte le leggi logiche (vedi teorema di completezza di Gödel ). Esiste un'equivalenza tra la presentazione semantica e la presentazione sintattica del calcolo dei predicati. Qualsiasi affermazione universalmente valida (cioè vera in qualsiasi modello del linguaggio utilizzato) è un teorema (cioè può essere dedotta da un calcolo, un sistema di regole logiche e assiomi, equivalente a un sistema à la Hilbert , deduzione naturale , o il calcolo di sequenze ) e viceversa. La logica del primo ordine è quindi completa nel senso che vi si risolve il problema della correttezza logica delle dimostrazioni. Tuttavia, continua ad essere una ricerca importante: teoria dei modelli , teoria della prova , meccanizzazione del ragionamento ...

Sintassi

Definizione

Questa sezione fornisce una breve presentazione della sintassi del linguaggio formale del calcolo dei predicati.

Ci diamo per alfabeto:

un insieme di simboli chiamati variabili , sempre infinito: , , ecc. ; $X$ $sì$ $z$
un insieme di simboli chiamati costanti , possibilmente vuoti: , , ecc. ; $a$ $b$ $vs$
un insieme di simboli di funzione: , , ecc. ; $f$ $g$ $h$
un insieme di simboli predicati : , , ecc. $P$ $Q$ $R$

Ogni simbolo di funzione e ogni simbolo di predicato ha un'arity : questo è il numero di argomenti o oggetti a cui è applicato. Ad esempio, il predicato per "è blu" ha un'arità uguale a 1 (diciamo che è unario o monadico ), mentre il predicato per "essere amici" ha un'arità pari a due (diciamo che è binario o diadico ). $B$ ${\ displaystyle friends}$

I simboli ( qualunque cosa ) e ( ci sono ), chiamati quantificatori . $\ per tutti$ $\esiste$
I simboli ( non ), ( e ), ( o ) e ( implica ), che sono connettori che hanno anche il calcolo delle proposizioni . $\ non$ $\ terra$ $\ lor$ $\ per$
I simboli di punteggiatura ")" e "(".

Ci si potrebbe accontentare di un singolo quantizzatore e due connettori logici e definendo da essi gli altri connettori e il quantizzatore. Ad esempio è definito come . $\ per tutti$ $\ non$ $\ terra$ ${\ displaystyle \ esiste x \; P (x)}$ ${\ displaystyle \ lnot (\ forall x \; \ lnot P (x))}$

Le formule per il calcolo dei predicati del primo ordine sono definite per induzione:

${\ displaystyle P (t_ {1}, \ punti, t_ {n})}$ se un simbolo predicato di arity n e t 1 ,…, t n sono termini (tale formula è chiamata atomo o formula atomica ); $P$
¬ e se e è una formula;
( e 1 ∧ e 2 ) se e 1 ed e 2 sono formule;
( e 1 ∨ e 2 ) se e 1 ed e 2 sono formule;
( e 1 → e 2 ) se e 1 ed e 2 sono formule;
$\ forall x \; e$ se e è una formula;
$\ esiste x \; e$ se e è una formula.

Un'affermazione è detta formula in cui tutte le variabili sono collegate da un quantificatore (quindi che non ha variabili libere).

Esempi

Esempio 1

Se ci diamo come costanti i due simboli 0 e 1, per i simboli delle funzioni binarie + e., e per i simboli dei predicati binari i simboli = e <, allora il linguaggio utilizzato può essere interpretato come quello dell'aritmetica. x ed y variabili denota, x + 1 è un termine , 0 + 1 + 1 è un chiuso termine , x < y + 1 è una formula, 0 + 1 + 1 <0 + 1 + 1 + 1 è una formula chiusa.

Esempio 2

Se ci diamo un insieme arbitrario di variabili, una costante indicata con e , un simbolo di funzione binaria indicato con *, un simbolo di funzione unario indicato con -1 , un simbolo di relazione binaria =, allora il linguaggio utilizzato può essere interpretato come quello della teoria dei gruppi . Se x ed y variabili denotano, x * y è un termine, e * e è un termine chiuso, x = y * y è una formula, e = e * e -1 e ( e -1 * e ) -1 = ( e -1 ) -1 sono formule chiuse.

Predicati, formule chiuse, formule raffinate, variabili libere, variabili vincolate

Quando una variabile appartiene a una sottoformula preceduta da un quantificatore, o , si dice che è collegata da questo quantificatore. Se una variabile non è vincolata da alcun quantificatore, è libera. $X$ $\ per tutti x$ $\ esiste x$

La distinzione tra variabile libera e variabile vincolata è importante. Una variabile collegata non ha un'identità propria e può essere sostituita da qualsiasi altro nome di variabile che non compare nella formula. Quindi, è identico a ma non a e ancor meno a . $\ esiste x (x <y)$ $\ esiste z (z <y)$ $\ esiste x (x <z)$ $\ esiste y (y <y)$

Una formula chiusa è una formula in cui tutte le variabili sono collegate. Un predicato è una formula che contiene una o più variabili libere. Possiamo considerare i predicati come concetti. Quindi, è una formula chiusa del linguaggio dell'aritmetica. è un predicato sulla variabile z . $\ forall x \ esiste y (x <y)$ $\ pertutti x (x <z)$

Una formula si dice gentile quando, da un lato, nessuna variabile ha occorrenze sia libere che collegate e, dall'altro, nessuna variabile collegata è soggetta a più di una mutazione (si dice che un segno è mutante quando conferma l'ipotesi di una variabile collegata).

Semantica

La teoria della verità delle formule del calcolo dei predicati è stata chiamata da Tarski la sua semantica .

Un'interpretazione di un linguaggio del primo ordine in un dominio di interpretazione, chiamato anche un linguaggio di modello , descrive i valori assunti dai costituenti del primo ordine (variabili, simboli di costanti, termini) e le relazioni associate ai predicati. Ad ogni affermazione viene assegnato un valore di verità. Lo studio delle interpretazioni dei linguaggi formali è chiamato semantica formale o teoria dei modelli . Quella che segue è una descrizione della semantica standard o tarskiana per la logica del primo ordine. Esistono altri tipi di semantica, inclusa la semantica del gioco , che non sono descritti in dettaglio in questo articolo.

Modello

Un modello M di un linguaggio del primo ordine è una struttura: è un insieme di elementi (chiamato dominio) in cui diamo significato ai simboli del linguaggio. In genere, se il linguaggio ha un predicato binario per il simbolo di uguaglianza =, la sua interpretazione nella struttura è l'uguaglianza.

Condizioni di verità

Un modello assegna un valore di verità ( vero o falso ) a qualsiasi formula chiusa del linguaggio. Le condizioni di verità sono definite per induzione strutturale sulle formule. Ad esempio, nel modello a fianco:

${\ displaystyle \ esiste x \ forall y ~ \ mathrm {come} (x, y)}$ è vero nel modello M perché c'è un elemento (l'uccello) che tutti amano;
${\ displaystyle \ esiste x \ forall y ~ \ lnot \ mathrm {like} (x, y)}$ è vero nel modello M perché c'è un elemento (la ciliegia) che non piace a nessuno.

Formula soddisfacente

Una formula è soddisfacibile se esiste un modello M che la rende vera. Ad esempio è soddisfacente. ${\ displaystyle \ esiste x \ forall y ~ \ mathrm {come} (x, y)}$

Formula valida

Diciamo che una formula F di linguaggio è una formula valida se questa formula è vera in qualsiasi modello di linguaggio, che notiamo . Ad esempio, la formula è una formula valida. In un modello M, se è vero, c'è qualcosa nel dominio che piace a tutti. Ma poi tutti sono amati e quindi la formula è vera nel modello M. Essendo l'implicazione vera in qualsiasi modello M, la formula è valida. $\ vDash F$ ${\ displaystyle \ esiste x \ forall y ~ \ mathrm {mi piace} (x, y) \ a \ forall y \ esiste x ~ \ mathrm {mi piace} (x, y)}$ ${\ displaystyle \ esiste x \ forall y ~ \ mathrm {come} (x, y)}$ $X$ ${\ displaystyle \ forall y \ esiste x ~ \ mathrm {come} (x, y)}$

Tuttavia, la formula non è valida. Infatti, in un modello con due elementi { a , b } e dove è interpretato da a ama solo a e b ama solo b, la formula è vera mentre è falsa. L'implicazione è quindi falsa nel modello e la formula non è valida. ${\ displaystyle \ forall y \ esiste x ~ \ mathrm {mi piace} (x, y) \ a \ esiste x \ forall y ~ \ mathrm {mi piace} (x, y)}$ ${\ displaystyle \ mathrm {mi piace}}$ ${\ displaystyle \ forall y \ esiste x \; ~ \ mathrm {like} (x, y)}$ ${\ displaystyle \ esiste x \ forall y \; ~ \ mathrm {like} (x, y)}$

conseguenza semantica Se

Diciamo che F è una conseguenza semantica di una teoria T se ogni modello che soddisfa tutte le formule di T soddisfa anche F.

Sistema di detrazione

Nel calcolo dei predicati si possono dedurre formule anche mediante deduzioni derivanti da un calcolo. Una deduzione consiste nel partire da ipotesi, o assiomi, per progredire per tappe logiche fino ad una conclusione secondo regole predefinite. Ci sono diverse possibili presentazioni di questi assiomi e regole.

La detrazione naturale . I principi logici sono presentati lì in un modo il più vicino possibile al ragionamento naturale. Consiste in un elenco di tredici regole. Potrebbero essere ridotti a un numero minore, ma l'ovvietà dei principi sarebbe meno naturale.
Il calcolo delle successioni .
La risoluzione .
Gli assiomi logici . Si possono proporre diversi sistemi di assiomi equivalenti. Questo approccio, adottato da quasi tutti i logici dai Principia Mathematica di Whitehead e Russell , ha un grande significato sia metamatematico che storico. Uno dei più brevi sistemi di assiomi è costituito dalla seguente tripletta: Gli assiomi del calcolo delle proposizioni $f \ a (g \ a f)$ $(f \ a (g \ a h)) \ a ((f \ a g) \ a (f \ a h))$ $(\ non f \ in g) \ in ((\ non f \ in \ non g) \ in f)$ assiomi relativi al quantificatore $\ per tutti$ $\ forall x (f \ to g (x)) \ to (f \ to \ forall xg (x))$ dove x non è libero in f $\ forall xf (x) \ to f (a)$ dove x non ha occorrenza libera in una parte ben formata di f della forma (questo per evitare scomode sostituzioni se, ad esempio, f ( x ) è della forma ). $\ pertutti a, h$ ${\ displaystyle \ esiste a, a <x}$ La regola del modus ponens se abbiamo dimostrato e , allora abbiamo dimostrato $f \ a g$ $f$ $g$ La regola della generalizzazione se abbiamo dimostrato , allora abbiamo dimostrato (poiché la x della prima dimostrazione gioca un ruolo arbitrario). $f(x)$ $\ pertutti xf (x)$

Ma se la ricerca di sistemi di assiomi minimi mette in luce i principi elementari su cui può fondarsi ogni ragionamento, non mostra la natura di evidenza naturale di principi logici più generali.

La logica del dialogo getta anche un'altra luce sulla natura delle leggi logiche.
Vedi anche corrispondenza Curry-Howard .

Qualunque sia la presentazione affrontata, gli assiomi e le regole possono essere codificati in modo che una macchina possa verificare la validità o meno di una deduzione che porta a una formula F. Se la deduzione è corretta, la formula F è chiamata teorema . Diciamo anche che è dimostrabile , cosa che notiamo . $\ vdash F$

Proprietà

Completezza

Il teorema di completezza dice che F è valido è equivalente a F è dimostrabile. Meglio, si parla di completezza forte: se F è una conseguenza semantica di una teoria T allora F è dimostrabile da T.

indecidibilità

Non tutti i sistemi logici sono decidibili, in altre parole pur essendo perfettamente definiti, non sempre esiste un algoritmo per dire se una formula è o meno un teorema. Inoltre, storicamente la teoria della computabilità è stata costruita per dimostrare con precisione la loro indecidibilità. Prima di sviluppare questi risultati, ecco un riassunto di ciò che sappiamo sulla decidibilità e indecidibilità dei sistemi logici.

Calcolo proposizionale: decidibile e completo. Per la decidibilità esiste quindi una procedura efficace per decidere se una formula del calcolo proposizionale è soddisfacente, vale a dire che si possono assegnare alle variabili proposizionali valori di verità che la rendono vera, ma il problema, denominato problema SAT , è NP-completo , ovvero tutti gli algoritmi deterministici noti per trovare una soluzione sono in tempo esponenziale rispetto al numero di variabili (vedi l'articolo SAT Problem ).
Calcolo dei predicati monadici del primo ordine , cioè ridotti a relazioni unarie e senza funzioni: decidibili e completi, per riduzione al calcolo proposizionale.
Calcolo dei predicati del primo ordine: riducibile al calcolo dei predicati diadici, cioè con al più predicati binari (come nel caso della teoria degli insiemi che ha come simboli primitivi solo l'appartenenza e l'uguaglianza): semidecidibile e completo .
Calcolo di predicati del secondo ordine : [ quid sulla sua decidibilità], e teorema di completezza parziale su una sottoclasse di formule .
Calcolo dei predicati di ordine superiore :

Il calcolo dei predicati è semidecidibile, nel senso che una macchina può enumerare i teoremi uno dopo l'altro. Ma, a differenza del calcolo delle proposizioni , non è in generale decidibile nel senso che non esiste un mezzo "meccanico" che, se ci diamo una formula F, ci permetta di decidere se F è un teorema o meno. . La semidecidibilità non consente una conclusione: il confronto di F con l'elenco dei teoremi terminerà se F è davvero un teorema, ma in attesa della conclusione, a priori non sappiamo se il calcolo dei teoremi non ha non è stato portato abbastanza lontano da identificare F come un teorema o se questo calcolo non finirà perché F non è un teorema.

Tuttavia, questo dipende dal linguaggio utilizzato, in particolare dalla scelta dei simboli primitivi (la firma). Il calcolo dei predicati egualitari monadici (che hanno solo simboli predicati unari e nessun simbolo di funzione) è decidibile. Il calcolo dei predicati egualitari per un linguaggio comprendente almeno un simbolo di predicato binario è indecidibile (algoritmicamente).

I frammenti sintattici sono decidibili come la logica monadica del primo ordine o la classe Bernays-Schönfinkel .

Compattezza

Vedi teorema di compattezza .

Espressività

Un'applicazione interessante del teorema di compattezza è che non esistono formule che esprimano "il dominio è infinito".

Teorema di Löwenheim-Skolem

Vedi il teorema di Löwenheim-Skolem .

Incompletezza

In un altro senso, le teorie "ragionevoli" che consentono di formalizzare sufficientemente l'aritmetica intuitiva, come l'aritmetica di Peano , o la teoria degli insiemi, non sono complete : esiste un'affermazione indimostrabile la cui negazione è anche indimostrabile (vedi il teorema di incompletezza di Gödel ).

Frammenti determinabili

Il problema della soddisfacibilità di una formula di logica del prim'ordine è indecidibile. Ma limitandosi a certe classi di formule, il problema della soddisfacibilità diventa decidibile. La tabella seguente elenca alcuni frammenti decidibili.

frammenti
Frammento monadico e simboli di funzione di arity 1
Frammento con solo due variabili
Classe Bernays-Schönfinkel , Classe senza funzione e simboli di uguaglianza ${\ displaystyle \ esiste ^ {} \ forall ^ {}}$
Classe senza simboli di funzione ${\ displaystyle \ esiste ^ {} \ forall ^ {2} \ esiste ^ {}}$
Classe con simboli di funzione ${\ displaystyle \ esiste ^ {} \ forall \ esiste ^ {}}$
Classe con simboli di funzione e uguaglianza ${\ displaystyle \ esiste ^ {*}}$
Frammento monadico con simboli di funzione di arietà e uguaglianza
Classe con simboli di funzione di arietà uno e uguaglianza ${\ displaystyle \ esiste ^ {} \ forall \ esiste ^ {}}$

varianti

Il calcolo delle proposizioni è un frammento sintattico di logica del primo ordine dove non ci sono variabili e dove tutti i predicati sono di arity 0 .

La logica modale proposizionale e descrittiva sono frammenti sintattici della logica del primo ordine . Inoltre, qualsiasi formula del primo ordine invariante per bisimulazione è equivalente a una formula logica modale: è il teorema di Van Benthem . La logica del primo ordine è stata estesa anche alla logica modale del primo ordine . La logica di dipendenza ( logica dipendenza ) è una generalizzazione logica del primo ordine in cui le dipendenze tra le variabili sono esplicitamente descritte nella lingua .

Note e riferimenti

Appunti

ricorsivamente assiomatizzabile e coerente.

Riferimenti

Immanuel Kant, " Prefazione alla critica della ragion pura " , su https://fr.wikisource.org ,1787
" logician - Wiktionary " , su fr.wiktionary.org (consultato il 25 maggio 2020 )
" Logica (matematica) / Deduzione naturale - Wikiversità " , su fr.wikiversity.org (consultato il 25 maggio 2020 )
(in) Il problema decisionale classico | Egon Börger | Springer ( leggi online ) , Th. 6.02 p. 240

Appendici

Bibliografia

Stephen Kleene, Logica matematica , Armand Colin, 1971 o Gabay 1987 ( ISBN 2-87647-005-5 )
R. David, K. Nour e C. Raffalli, Introduzione alla logica. Teoria della dimostrazione. Corsi ed esercizi corretti , Dunod, 2001 ( ISBN 2-10-006796-6 )