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 , hvor 
er en mengde konstantsymboler,  er en mengde funksjonssymboler,
og  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  så er -termer definert induktivt
som:
 Alle variabler  er -termer.
 Alle konstantsymboler  er -termer.
 Hvis  er et funksjonssymbol med aritet , og  til  er -termer, så er  er -term.

Førsteordens formler 
Gitt et språk , så er mengden med -formler definert induktivt som:
  er en -formel. Les topp eller sant (eng: top).
  er en -formel. Les bunn eller usann (eng: bottom).
 Hvis  er et relasjonssymbol med aritet , og  til  er -termer, så er  en -formel.
 Hvis  og  er -formeler og  er en variabel, så er følgende -formler:
 : negasjonen av .
 : konjunksjon. Les A og B.
 : disjunksjon. Les A eller B.
 : implikasjon. Les hvis A, så B eller A impliserer B. (Notasjonen  brukes også.)
 : all-kvantor. Les "for alle x, så holder A. Legg merke til at x kan forekomme som en variabel i 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  er en
ikke-tom mengde , kalt domenet, sammen med en tolkning  av alle symbolene i  slik at:
  for alle konstansymboler .
  for alle funksjonssymboler  med aritet .
  for alle relasjonssymboler  med aritet .
Det er altså en tolkning av alle de ikke-logiske symbolene inni domenet .

 Variabeltilordning og tolkning av termer 
Før denne tolkningen kan løftes opp til alle termer, må en tolkning av variabler gis. En funksjon 
kalles en variabeltilordning. Gitt en variabeltilordning, så er det en unik funksjon som løfter tolkningen til alle termer:
 .
 .
 .

 Tolkning av formler 
Det at en formel  er sann i en modell  med en variabeltilordning  skrives som
.
og er definert som følger:
  holder alltid.
  holder aldri.
  holder hvis og bare hvis .
  holder hvis og bare hvis  ikke holder.
  holder hvis og bare hvis  holder og  holder.
  holder hvis og bare hvis  holder eller  holder.
  holder hvis og bare hvis: hvis  holder, så holder .
  holder hvis og bare hvis  holder for alle .
  holder hvis og bare hvis: det eksisterer en  slik at  holder.

Basert på dette sier vi at en modell  oppfyller en formel , notasjon ,
hvis  for alle variabel-tilordninger .

Hvis  er en mengde formler, så skriver vi  hvis  for alle .
Videre, hvis  er en formel, så er  en logisk konsekvens av , notasjon ,
hvis for alle modeller  og tilordninger , så impliserer  at  holder.
Et særtilfelle er når , hvor man kun skriver  i stede for .

 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  hvis
det finnes en utledig i en gitt kalkyle for  fra antagelsene .

Det er tre viktige egenskaper en kalkyle kan besitte:
 Konsistent: Det er umulig å gi en utledning for .
 Sunn: Hvis , så .
 Komplett: Hvis , så .

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

Logikk