Logica del primo ordine

Note

La logica del primo ordine è un linguaggio composto da un alfabeto di:

  1. Costanti: (al più numerabile)
  2. Variabili: (al più numerabile)
  3. Lettere funzionali: (al più numerabile), dove indica la molteplicità delle variabili di ingresso della lettera funzionale
  4. Lettere predicative: (al più numerabile), dove indica la molteplicità delle variabili di ingresso della lettera predicativa
  5. Connettivi:
  6. Quantificatori: (quantificativa) e (esistenziale)
  7. Simboli ausiliari
Termini

I termini sono composizioni di lettere funzionali che descrivono composizioni di operazioni.

Ogni variabile e costante sono dei termini. Inoltre se ho termini e se è una lettera funzionalità di arità , allora è un termine.

Formule atomiche

Se è una lettera predicativa di arità e sono termini, allora è una forma atomica.

Formule Ben Formate
  1. Ogni formula atomica è una FBF
  2. Se è una FBF, allora , , sono FBF
  3. Se sono FBF, allora , , , sono FBF
Priorità degli operatori

Introduco una priorità sugli operatori, come in aritmetica:

  • , , vengono associati con l'ordine in cui vengono letti.
  • I connettivi uguali sono associati a sinistra.

Le sottoformule e l'albero delle sottoformule si costruiscono in modo analogo al caso proposizionale.

Definiamo il campo di azione di un quantificatore come la sottoformula a cui quel quantificatore si riferisce. Se una variabile cade nel campo d'azione allora si dice vincolata, altrimenti si dice libera.

Una FBF si dice chiusa se non ha variabili libere, se invece ha variabili libere possiamo:

  • Chiudere universalmente ()
  • Chiudere esistenzialmente ()

Una variabile è libera per la variabile libera , cioè è libera nel campo di azione di o .

Semantica

Note

L'interpretazione (o struttura) è una coppia dove:

  • è un insieme, detto dominio su cui le variabili prendono valori
  • sono tre funzioni tali che:
    • dove è lettera funzionale di arità , allora
    • dove è una lettera predicativa di arità , allora

La verità di una FBF dipende dagli assegnamenti delle variabili.

Assegnamento

Dato un linguaggio del primo ordine, e una interpretazione , un assegnamento è una funzione: Questo assegnamento può essere esteso ai termini di : Nel seguente modo:

  3. Induttivamente è una lettera funzionale di di arità , e , allora .
Soddisfacibilità di una FBF

Sia un interpretazione di un linguaggio del primo ordine e sia: un assegnamento, diciamo che la FBF è soddisfatta da e scriviamo: Se:

  1. nel caso è una formula atomica:
  2. nel caso se non è soddisfatta da :
  3. nel caso (oppure ) se:
  4. nel caso (oppure ) se:
  5. nel caso allora se: dove indica l'assegnazione uguale ad tranne in un in cui vale .
  6. nel caso se:

Data un interpretazione su un linguaggio del primo ordine e FBF su L diciamo che è:

  • soddisfacibile: se esiste un assegnamento che soddisfa , in questo caso è chiamato modello di .
  • vera: se ogni assegnamento , in questo caso scriviamo
  • falsa: se non esiste nessun assegnamento . Quindi è falsa quando non ha modelli.
  • logicamente valida: se per ogni interpretazione , scriviamo
  • logicamente contraddittoria/insoddisfacibile: se per ogni interpretazione non ho modelli.

In generale è vera se e solo se la sua chiusura universale è vera. Inoltre è soddisfacibile se e solo se la sua chiusura esistenziale è vera.

Modello e conseguenza semantica

Note

Una terna ( assegnamento) tale che si dice un modello di .
Dato un inseme di FBF, diciamo che è un modello di se è modello di ogni . Diciamo che è conseguenza semantica di (scriviamo ) se ogni modello di è modello di .

Tip

Se non ha modelli, allora è insoddisfacibile o logicamente contraddittoria. Per estensione diciamo che è insoddisfacibile se non ha modelli.

Per il teorema di insoddisfacibilità e conseguenza semantica:
èInoltre per il teorema di deduzione semantica:

Due FBF si dicono semanticamente equivalenti () se e (cioè hanno gli stessi modelli).

Tip

è

Forma normale prenessa

Note

Una FBF si dice in forma normale prenessa se è della forma: Dove è una FBF che non contiene quantificatori nelle variabili libere ( è chiamata la matrice di ).

Data una FBF , esiste sempre una FBF tale che e è in forma normale prenessa (FNP). Inoltre c'è un algoritmo per portare in FNP.

Uso le seguenti equivalente semantiche per portare in testa i quantificatori:

  1. e con variabile libera in . è una variabile che è un termine libero per se non succede o . Questo succede se per esempio non compare in . Con indico la forma in cui alla variabile libera sostituisco .
  2. o se non compare in e è libera per in .
  3. o se non compare in e è libera per in .
  4. o .

Ricordando che se non contiene occorrenze libere di la sostituzione è inutile.

Forma di Skolem

Note

Partendo da una FBF in FNP, la forma di Skolem trasforma in una FBF che non contiene quantificatori esistenziali.

Uso il seguente algoritmo per portare una FBF in FNP in forma di Skolem:

  1. Chiudiamo universalmente le variabili non quantificate:
  2. Finché ci sono quantificatori universali nella FBF: Costruisci la nuova FBF: Dove è una nuova lettera funzionale di arità , cioè quanti sono i quantificatori universali che ho prima di .
Tip

non è in generale semanticamente equivalente a , ma si dimostra che se è modello di , allora lo è per : Tuttavia, visto che in ci sono nuove lettere funzionali, non è vero che un modello di lo è anche di , ma si dimostra che si può estendere ad un modello di :