Åpne hovedmenyen

Førsteordens språk, termer og formlerRediger

Førsteordens språkRediger

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 termerRediger

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 formlerRediger

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 logikkRediger

En standard måte å beskrive modeller for førsteordens logikk på er som følger.

ModellRediger

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 termerRediger

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 formlerRediger

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  .

KalkylerRediger

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å  .

LitteraturRediger

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