Førsteordens logikk

Førsteordens predikatlogikk er i logikk et språk, med tilhørende semantikker og kalkyler, som beskriver objekter og deres relasjon til hverandre.

Førsteordens språk, termer og formler

Førsteordens språk

Et førsteordens språk er et tripel $\langle C,F,{\mathcal {R}}\rangle$, hvor $C=\{c_{1},\ldots \}$ er en mengde konstantsymboler, $F=\{f_{1},\ldots \}$ er en mengde funksjonssymboler, og ${\mathcal {R}}=\{R_{1},\ldots \}$ er en mengde relasjonssymboler. Assosiert med hvert funksjon- og relasjonssymbol er ariteten, som er et naturlig tall som forteller hvor mange argumenter symbolet forventer.

Disse symbolene kalles de ikke-logiske symbolene.

Førsteordens termer

Gitt et språk ${\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle$ så er ${\mathcal {L}}$-termer definert induktivt som:

• Alle variabler $x$ er ${\mathcal {L}}$-termer.
• Alle konstantsymboler $c\in C$ er ${\mathcal {L}}$-termer.
• Hvis $f\in F$ er et funksjonssymbol med aritet $n$, og $t_{1}$ til $t_{n}$ er ${\mathcal {L}}$-termer, så er $f(t_{1},\ldots ,f_{n})$ er ${\mathcal {L}}$-term.

Førsteordens formler

Gitt et språk ${\mathcal {L}}$, så er mengden med ${\mathcal {L}}$-formler definert induktivt som:

• $\top$ er en ${\mathcal {L}}$-formel. Les topp eller sant (eng: top).
• $\bot$ er en ${\mathcal {L}}$-formel. Les bunn eller usann (eng: bottom).
• Hvis $R\in {\mathcal {R}}$ er et relasjonssymbol med aritet $n$, og $t_{1}$ til $t_{n}$ er ${\mathcal {L}}$-termer, så er $R(t_{1},\ldots ,t_{n})$ en ${\mathcal {L}}$-formel.
• Hvis $A$ og $B$ er ${\mathcal {L}}$-formeler og $x$ er en variabel, så er følgende ${\mathcal {L}}$-formler:
  • $\neg A$: negasjonen av $A$.
  • $A\land B$: konjunksjon. Les A og B.
  • $A\lor B$: disjunksjon. Les A eller B.
  • $A\to B$: implikasjon. Les hvis A, så B eller A impliserer B. (Notasjonen $A\supset B$ brukes også.)
  • $\forall x.\,A$: all-kvantor. Les "for alle x, så holder A. Legg merke til at x kan forekomme som en variabel i A.
  • $\exists x.\,A$: eksistens-kvantor. Les "det eksisterer en x, sånn at A holder". Igjen så kan x forekomme som en variabel i A.

Modellteori for førsteordens logikk

En standard måte å beskrive modeller for førsteordens logikk på er som følger.

Modell

En modell ${\mathcal {M}}$ for et språk ${\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle$ er en ikke-tom mengde $D$, kalt domenet, sammen med en tolkning $(.)^{\mathcal {M}}$ av alle symbolene i ${\mathcal {M}}$ slik at:

• $c^{\mathcal {M}}\in D$ for alle konstansymboler $c\in C$.
• $f^{\mathcal {M}}:D^{n}\to D$ for alle funksjonssymboler $f\in F$ med aritet $n$.
• $R^{\mathcal {M}}\subset D^{n}$ for alle relasjonssymboler $R\in {\mathcal {R}}$ med aritet $n$.

Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet $D$.

Variabeltilordning og tolkning av termer

Før denne tolkningen kan løftes opp til alle termer, må en tolkning av variabler gis. En funksjon $\delta :\mathbb {B} \to D$ kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:

• $[x]_{\delta }^{\mathcal {M}}=\delta (x)$.
• $[c]_{\delta }^{\mathcal {M}}=c^{\mathcal {M}}$.
• $[f(t_{1},\ldots ,t_{n})]_{\delta }^{\mathcal {M}}=f^{\mathcal {M}}([t_{1}]_{\delta }^{\mathcal {M}},\ldots ,[t_{n}]_{\delta }^{\mathcal {M}})$.

Tolkning av formler

Det at en formel $A$ er sann i en modell ${\mathcal {M}}$ med en variabeltilordning $\delta$ skrives som

${\mathcal {M}},\delta \models A$.

og er definert som følger:

• ${\mathcal {M}},\delta \models \top$ holder alltid.
• ${\mathcal {M}},\delta \models \bot$ holder aldri.
• ${\mathcal {M}},\delta \models R(t_{1},\ldots ,t_{n})$ holder hvis og bare hvis $\langle [t_{1}]_{\delta }^{\mathcal {M}},\ldots ,[t_{n}]_{\delta }^{\mathcal {M}}\rangle \in R^{\mathcal {M}}$.
• ${\mathcal {M}},\delta \models \neg A$ holder hvis og bare hvis ${\mathcal {M}},\delta \models A$ ikke holder.
• ${\mathcal {M}},\delta \models A\land B$ holder hvis og bare hvis ${\mathcal {M}},\delta \models A$ holder og ${\mathcal {M}},\delta \models B$ holder.
• ${\mathcal {M}},\delta \models A\lor B$ holder hvis og bare hvis ${\mathcal {M}},\delta \models A$ holder eller ${\mathcal {M}},\delta \models B$ holder.
• ${\mathcal {M}},\delta \models A\to B$ holder hvis og bare hvis: hvis ${\mathcal {M}},\delta \models A$ holder, så holder ${\mathcal {M}},\delta \models B$.
• ${\mathcal {M}},\delta \models \forall x.\,A$ holder hvis og bare hvis ${\mathcal {M}},\delta [x\mapsto d]\models A$ holder for alle $d\in D$.
• ${\mathcal {M}},\delta \models \exists x.\,A$ holder hvis og bare hvis: det eksisterer en $d\in D$ slik at ${\mathcal {M}},\delta [x\mapsto d]\models A$ holder.

Basert på dette sier vi at en modell ${\mathcal {M}}$ oppfyller en formel $A$, notasjon ${\mathcal {M}}\models A$, hvis ${\mathcal {M}},\delta \models A$ for alle variabel-tilordninger $\delta$.

Hvis $\Gamma$ er en mengde formler, så skriver vi ${\mathcal {M}},\delta \models \Gamma$ hvis ${\mathcal {M}},\delta \models A$ for alle $A\in \Gamma$. Videre, hvis $B$ er en formel, så er $B$ en logisk konsekvens av $\Gamma$, notasjon $\Gamma \models A$, hvis for alle modeller ${\mathcal {M}}$ og tilordninger $\delta$, så impliserer ${\mathcal {M}},\delta \models \Gamma$ at ${\mathcal {M}},\delta \models B$ holder. Et særtilfelle er når $\Gamma =\emptyset$, hvor man kun skriver $\models B$ i stede for $\emptyset \models B$.

Kalkyler

Det finnes flere forskjellige kalkyler. I motsetning til semantiske modeller, så fanger kalkyler inn meningen til formelen ved syntaktiske ressonement. Mest kjent er naturlig deduksjon, sekventkalkyle og Hilbert system. Man skriver gjerne $\Gamma \vdash A$ hvis det finnes en utledig i en gitt kalkyle for $A$ fra antagelsene $\Gamma$.

Det er tre viktige egenskaper en kalkyle kan besitte:

• Konsistent: Det er umulig å gi en utledning for $\vdash \bot$.
• Sunn: Hvis $\Gamma \vdash A$, så $\Gamma \models A$.
• Komplett: Hvis $\Gamma \models A$, så $\Gamma \vdash A$.

Litteratur

Dirk Van Dalen. Logic and Structure, Universitext. ISBN 978-3-540-20879-2.