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.
** <math> \exists x.\, A</math>: 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 <math>\mathcal{M}</math> for et språk <math>\mathcal{L} = \langle C, F, \mathcal{R}\rangle </math> er en
ikke-tom mengde <math>D</math>, kalt domenet, sammen med en tolkning <math>(.)^\mathcal{M}</math> av alle symbolene i <math>\mathcal{M}</math> slik at:
* <math>c^\mathcal{M} \in D</math> for alle konstansymboler <math>c \in C</math>.
* <math>f^\mathcal{M} : D^n \to D</math> for alle funksjonssymboler <math>f \in F</math> med aritet <math>n</math>.
* <math>R^\mathcal{M} \subset D^n</math> for alle relasjonssymboler <math>R \in \mathcal{R}</math> med aritet <math>n</math>.
Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet <math>D</math>.

=== Variabeltilordning og tolkning av termer ===
Før denne tolkningen kan *løftes* opp til alle termer, må en tolkning av variabler gis. En funksjon <math>\delta : \mathbb{B} \to D</math>
kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:
* <math>[x]^\mathcal{M}_\delta = \delta(x)</math>.
* <math>[c]^\mathcal{M}_\delta = c^\mathcal{M}</math>.
* <math> [f(t_1, \ldots, t_n)]^\mathcal{M}_\delta = f^\mathcal{M}([t_1]^\mathcal{M}_\delta, \ldots, [t_n]^\mathcal{M}_\delta)</math>.

=== Tolkning av formler ===
Det at en formel <math>A</math> er sann i en modell <math>\mathcal{M}</math> med en variabeltilordning <math>\delta</math> skrives som
:<math> \mathcal{M}, \delta \models A</math>.
og er definert som følger:
* <math> \mathcal{M}, \delta \models \top</math> holder alltid.
* <math> \mathcal{M}, \delta \models \bot</math> holder aldri.
* <math> \mathcal{M}, \delta \models R(t_1, \ldots, t_n)</math> holder hvis og bare hvis <math>\langle [t_1]^\mathcal{M}_\delta, \ldots, [t_n]^\mathcal{M}_\delta\rangle \in R^\mathcal{M}</math>.
* <math> \mathcal{M}, \delta \models \neg A</math> holder hvis og bare hvis <math> \mathcal{M}, \delta \models A</math> ikke holder.
* <math> \mathcal{M}, \delta \models A \land B</math> holder hvis og bare hvis <math> \mathcal{M}, \delta \models A</math> holder og <math> \mathcal{M}, \delta \models B</math> holder.
* <math> \mathcal{M}, \delta \models A \lor B</math> holder hvis og bare hvis <math> \mathcal{M}, \delta \models A</math> holder eller <math> \mathcal{M}, \delta \models B</math> holder.
* <math> \mathcal{M}, \delta \models A \to B</math> holder hvis og bare hvis: hvis <math> \mathcal{M}, \delta \models A</math> holder, så holder <math> \mathcal{M}, \delta \models B</math>.
* <math> \mathcal{M}, \delta \models \forall x. \, A</math> holder hvis og bare hvis <math> \mathcal{M}, \delta[x \mapsto d] \models A</math> holder for alle <math> d \in D</math>.
* <math> \mathcal{M}, \delta \models \exists x.\, A</math> holder hvis og bare hvis: det eksisterer en <math> d \in D</math> slik at <math> \mathcal{M}, \delta[x \mapsto d] \models A</math> holder.

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

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

== 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 <math>\Gamma \vdash A</math> hvis
det finnes en utledig i en gitt kalkyle for <math>A</math> fra antagelsene <math>\Gamma</math>.

Det er tre viktige egenskaper en kalkyle kan besitte:
* *Konsistent*: Det er umulig å gi en utledning for <math>\vdash \bot</math>.
* *Sunn*: Hvis <math>\Gamma \vdash A</math>, så <math>\Gamma \models A</math>.
* *Komplett*: Hvis <math>\Gamma \models A</math>, så <math>\Gamma \vdash A</math>.

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