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 ${\displaystyle \langle C,F,{\mathcal {R}}\rangle }$, hvor ${\displaystyle C=\{c_{1},\ldots \}}$ er en mengde konstantsymboler, ${\displaystyle F=\{f_{1},\ldots \}}$ er en mengde funksjonssymboler, og ${\displaystyle {\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 ${\displaystyle {\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle }$ så er ${\displaystyle {\mathcal {L}}}$-termer definert induktivt som:

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

Førsteordens formler

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

• ${\displaystyle \top }$ er en ${\displaystyle {\mathcal {L}}}$-formel. Les topp eller sant (eng: top).
• ${\displaystyle \bot }$ er en ${\displaystyle {\mathcal {L}}}$-formel. Les bunn eller usann (eng: bottom).
• Hvis ${\displaystyle R\in {\mathcal {R}}}$ er et relasjonssymbol med aritet ${\displaystyle n}$, og ${\displaystyle t_{1}}$ til ${\displaystyle t_{n}}$ er ${\displaystyle {\mathcal {L}}}$-termer, så er ${\displaystyle R(t_{1},\ldots ,t_{n})}$ en ${\displaystyle {\mathcal {L}}}$-formel.
• Hvis ${\displaystyle A}$ og ${\displaystyle B}$ er ${\displaystyle {\mathcal {L}}}$-formeler og ${\displaystyle x}$ er en variabel, så er følgende ${\displaystyle {\mathcal {L}}}$-formler:
  • ${\displaystyle \neg A}$: negasjonen av ${\displaystyle A}$.
  • ${\displaystyle A\land B}$: konjunksjon. Les A og B.
  • ${\displaystyle A\lor B}$: disjunksjon. Les A eller B.
  • ${\displaystyle A\to B}$: implikasjon. Les hvis A, så B eller A impliserer B. (Notasjonen ${\displaystyle A\supset B}$ brukes også.)
  • ${\displaystyle \forall x.\,A}$: all-kvantor. Les "for alle x, så holder A. Legg merke til at x kan forekomme som en variabel i A.
  • ${\displaystyle \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 ${\displaystyle {\mathcal {M}}}$ for et språk ${\displaystyle {\mathcal {L}}=\langle C,F,{\mathcal {R}}\rangle }$ er en ikke-tom mengde ${\displaystyle D}$, kalt domenet, sammen med en tolkning ${\displaystyle (.)^{\mathcal {M}}}$ av alle symbolene i ${\displaystyle {\mathcal {M}}}$ slik at:

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

Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet ${\displaystyle 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 ${\displaystyle \delta :\mathbb {B} \to D}$ kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:

• ${\displaystyle [x]_{\delta }^{\mathcal {M}}=\delta (x)}$.
• ${\displaystyle [c]_{\delta }^{\mathcal {M}}=c^{\mathcal {M}}}$.
• ${\displaystyle [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 ${\displaystyle A}$ er sann i en modell ${\displaystyle {\mathcal {M}}}$ med en variabeltilordning ${\displaystyle \delta }$ skrives som

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

og er definert som følger:

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

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

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

Det er tre viktige egenskaper en kalkyle kan besitte:

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

Litteratur

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