Redigerer 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 <math>\langle C, F, \mathcal{R} \rangle</math>, hvor <math>C = \{c_1, \ldots \}</math>
er en mengde konstantsymboler, <math>F = \{f_1, \ldots \}</math> er en mengde funksjonssymboler,
og <math>\mathcal{R} = \{R_1, \ldots \}</math> 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 <math>\mathcal{L} = \langle C, F, \mathcal{R} \rangle</math> så er <math>\mathcal{L}</math>-termer definert induktivt
som:
* Alle variabler <math>x</math> er <math>\mathcal{L}</math>-termer.
* Alle konstantsymboler <math>c \in C</math> er <math>\mathcal{L}</math>-termer.
* Hvis <math>f \in F</math> er et funksjonssymbol med aritet <math>n</math>, og <math>t_1</math> til <math>t_n</math> er <math>\mathcal{L}</math>-termer, så er <math>f(t_1, \ldots, f_n)</math> er <math>\mathcal{L}</math>-term.

=== Førsteordens formler ===
Gitt et språk <math>\mathcal{L}</math>, så er mengden med <math>\mathcal{L}</math>-formler definert induktivt som:
* <math>\top</math> er en <math>\mathcal{L}</math>-formel. Les ''topp'' eller ''sant'' (eng: ''top'').
* <math>\bot</math> er en <math>\mathcal{L}</math>-formel. Les ''bunn'' eller ''usann'' (eng: ''bottom'').
* Hvis <math>R \in \mathcal{R}</math> er et relasjonssymbol med aritet <math>n</math>, og <math>t_1</math> til <math>t_n</math> er <math>\mathcal{L}</math>-termer, så er <math>R(t_1, \ldots, t_n)</math> en <math>\mathcal{L}</math>-formel.
* Hvis <math>A</math> og <math>B</math> er <math>\mathcal{L}</math>-formeler og <math>x</math> er en variabel, så er følgende <math>\mathcal{L}</math>-formler:
** <math>\neg A</math>: negasjonen av <math>A</math>.
** <math> A \land B</math>: konjunksjon. Les ''A og B''.
** <math> A \lor B</math>: disjunksjon. Les ''A eller B''.
** <math> A \to B</math>: implikasjon. Les ''hvis A, så B'' eller ''A impliserer B''. (Notasjonen <math>A \supset B</math> brukes også.)
** <math> \forall x.\, A </math>: 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.

{{Autoritetsdata}}

[[Kategori:Logikk]]