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 $⟨C,F,ℛ⟩$, hvor $C=\{c_1,\dots \}$ er en mengde konstantsymboler, $F=\{f_1,\dots \}$ er en mengde funksjonssymboler, og $ℛ=\{R_1,\dots \}$ 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 $ℒ=⟨C,F,ℛ⟩$ så er $ℒ$-termer definert induktivt som:

• Alle variabler $x$ er $ℒ$-termer.
• Alle konstantsymboler $c\in C$ er $ℒ$-termer.
• Hvis $f\in F$ er et funksjonssymbol med aritet $n$, og $t_1$ til $t_n$ er $ℒ$-termer, så er $f(t_1,\dots ,f_n)$ er $ℒ$-term.

Førsteordens formler

Gitt et språk $ℒ$, så er mengden med $ℒ$-formler definert induktivt som:

• $\mathrm{\top }$ er en $ℒ$-formel. Les topp eller sant (eng: top).
• $\mathrm{\perp }$ er en $ℒ$-formel. Les bunn eller usann (eng: bottom).
• Hvis $R\in ℛ$ er et relasjonssymbol med aritet $n$, og $t_1$ til $t_n$ er $ℒ$-termer, så er $R(t_1,\dots ,t_n)$ en $ℒ$-formel.
• Hvis $A$ og $B$ er $ℒ$-formeler og $x$ er en variabel, så er følgende $ℒ$-formler:
  • $\mathrm{\neg }A$: negasjonen av $A$.
  • $A\wedge B$: konjunksjon. Les A og B.
  • $A\vee 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å.)
  • $\mathrm{\forall }x.A$: all-kvantor. Les "for alle x, så holder A. Legg merke til at x kan forekomme som en variabel i A.
  • $\mathrm{\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 $ℳ$ for et språk $ℒ=⟨C,F,ℛ⟩$ er en ikke-tom mengde $D$, kalt domenet, sammen med en tolkning $(.{)}^{ℳ}$ av alle symbolene i $ℳ$ slik at:

• $c^{ℳ}\in D$ for alle konstansymboler $c\in C$.
• $f^{ℳ}:D^n\to D$ for alle funksjonssymboler $f\in F$ med aritet $n$.
• $R^{ℳ}\subset D^n$ for alle relasjonssymboler $R\in ℛ$ 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 :𝔹\to D$ kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:

• $[x{]}_{\delta }^{ℳ}=\delta (x)$.
• $[c{]}_{\delta }^{ℳ}=c^{ℳ}$.
• $[f(t_1,\dots ,t_n){]}_{\delta }^{ℳ}=f^{ℳ}([t_1{]}_{\delta }^{ℳ},\dots ,[t_n{]}_{\delta }^{ℳ})$.

Tolkning av formler

Det at en formel $A$ er sann i en modell $ℳ$ med en variabeltilordning $\delta$ skrives som

$ℳ,\delta \models A$.

og er definert som følger:

• $ℳ,\delta \models \mathrm{\top }$ holder alltid.
• $ℳ,\delta \models \mathrm{\perp }$ holder aldri.
• $ℳ,\delta \models R(t_1,\dots ,t_n)$ holder hvis og bare hvis $⟨[t_1{]}_{\delta }^{ℳ},\dots ,[t_n{]}_{\delta }^{ℳ}⟩\in R^{ℳ}$.
• $ℳ,\delta \models \mathrm{\neg }A$ holder hvis og bare hvis $ℳ,\delta \models A$ ikke holder.
• $ℳ,\delta \models A\wedge B$ holder hvis og bare hvis $ℳ,\delta \models A$ holder og $ℳ,\delta \models B$ holder.
• $ℳ,\delta \models A\vee B$ holder hvis og bare hvis $ℳ,\delta \models A$ holder eller $ℳ,\delta \models B$ holder.
• $ℳ,\delta \models A\to B$ holder hvis og bare hvis: hvis $ℳ,\delta \models A$ holder, så holder $ℳ,\delta \models B$.
• $ℳ,\delta \models \mathrm{\forall }x.A$ holder hvis og bare hvis $ℳ,\delta [x\mapsto d]\models A$ holder for alle $d\in D$.
• $ℳ,\delta \models \mathrm{\exists }x.A$ holder hvis og bare hvis: det eksisterer en $d\in D$ slik at $ℳ,\delta [x\mapsto d]\models A$ holder.

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

Hvis $\mathrm{\Gamma }$ er en mengde formler, så skriver vi $ℳ,\delta \models \mathrm{\Gamma }$ hvis $ℳ,\delta \models A$ for alle $A\in \mathrm{\Gamma }$. Videre, hvis $B$ er en formel, så er $B$ en logisk konsekvens av $\mathrm{\Gamma }$, notasjon $\mathrm{\Gamma }\models A$, hvis for alle modeller $ℳ$ og tilordninger $\delta$, så impliserer $ℳ,\delta \models \mathrm{\Gamma }$ at $ℳ,\delta \models B$ holder. Et særtilfelle er når $\mathrm{\Gamma }=\mathrm{\varnothing }$, hvor man kun skriver $\models B$ i stede for $\mathrm{\varnothing }\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 $\mathrm{\Gamma }⊢A$ hvis det finnes en utledig i en gitt kalkyle for $A$ fra antagelsene $\mathrm{\Gamma }$.

Det er tre viktige egenskaper en kalkyle kan besitte:

• Konsistent: Det er umulig å gi en utledning for $⊢\mathrm{\perp }$.
• Sunn: Hvis $\mathrm{\Gamma }⊢A$, så $\mathrm{\Gamma }\models A$.
• Komplett: Hvis $\mathrm{\Gamma }\models A$, så $\mathrm{\Gamma }⊢A$.

Litteratur

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