First-order logic

Propositinal logic ei käsitle kvantifikaatoreid.

Estimest järku loogika (first-order logic, FOL) ehk predikaatloogika (predicate logic) on lauseloogika (propositional logic) üldistus mis lisab muutujate kvantifikaatorid mis võimaldab tuletada väiteid lõpmatute mudelite kohta. Näiteks: mõned linnud lendavad; vähemalt ühel planeedil on elu; kõik inimesed on imetajad.

Esimest järku loogikas saame kasutada samu lauseloogikas olnud konstante. Naturaalarv 5, koer nimega Tommy:

\begin{equation*} 5, Tommy \end{equation*}

Esimest järku loogika toob sisse muutujad (variable):

\begin{equation*} x \in N - tähistab\:naturaalarvu \end{equation*}

\begin{equation*} d - tähistab\:koera\:nime \end{equation*}

Esimest järku loogika ei käsitle predikaatidele rakendatud kvanifikaatoreid, selle jaoks on teist ja kõrgemat järku loogika.

?? (term) kätkeb endas funktsioone, muutujaid ja konstante.

First-order logic adds predicates to propositional logic: P(x,y,z)

Predicates are like functions, except functions return arbitrary values, but predicates return truth values for certain instantiation.

Süntaks

First-order logic syntax:

\begin{equation*} Sentence \rightarrow AtomicSentence | Sentence Connective Sentence | Quantifier Variable, ... Sentence | !Sentence | (Sentence) \end{equation*}

\begin{equation*} AtomicSentence \rightarrow Predicate(Term, ...) | Term = Term \end{equation*}

\begin{equation*} Term \rightarrow Function(Term, ...) | Constant | Variable \end{equation*}

\begin{equation*} Connective \rightarrow implies, and, or, iff \end{equation*}

\begin{equation*} Quantifier \rightarrow \exists | \forall \end{equation*}

Kvantifikaatorid

Esimest järku loogika puhul saab kvantifitseerida üle muutujate, näiteks: üldsuskvantor, kõigi ... puhul (universal quantifier, for all ...):

\begin{equation*} \forall \end{equation*}

ning olemasolukvantor, eksisteerib ... (there exists ..., existential quantifier):

\begin{equation*} \exists \end{equation*}

Näiteks iga x kohta eksisteerib y, nii et y armastab x:

\begin{equation*} \forall x . \exists y . Armastab(x,y) \end{equation*}

Esimest järku loogikas ei saa kvantifitseerida funktsioone või suhteid, näiteks:

\begin{equation*} \exists loves . \forall x . \exists y . loves(x, y) \end{equation*}

Kvantifikaatorite järjekord on oluline (?).

Predikaat

Predikaat on väide mis kehtib tema argumentide kohta. Predikaat on nagu funktsioon mis tagastab tõeväärtuse. Argumentideta predikaat on väide (proposition):

\begin{equation*} Lauri\:on\:tudeng \end{equation*}

Predikaat on lause või valem (formula), mis sisaldab ühte või mitut muutujat (variables). Predikaatlause tõeväärtus oleneb väärtustatud muutuja(te) tõeväärtus(t)est.

\begin{equation*} P(x) \equiv ... muutujat\:x\:sisaldav\:lause\:või\:valem \end{equation*}

\begin{equation*} P(x, y) \equiv ... muutujaid\:x\:ja\:y\:sisaldav\:lause\:või\:valem \end{equation*}

Ühekohalist predikaati nimetatakse ka omaduseks (property). Kui predikaatmuutuja mingi konkreetse väärtuse n korral predikaatlause P(n) osutub tõeseks, siis ütleme et "n-il on omadus P" (variable n has property P):

\begin{equation*} Tudeng(x) \equiv x\:on\:tudeng \end{equation*}

Predikaadil võib argumente ka rohkem olla:

\begin{equation*} Õpib(x,y) \equiv tudeng\:y\:õpib\:ainet\:x \end{equation*}

Kõik tudengid ei õpi ajalugu ja bioloogiat:

\begin{equation*} \neg[\forall x Tudeng(x) \implies Õpib(Ajalugu, x) \land Õpib(Biologoogia, x)] \end{equation*}

Kus Ajalugu ja Bioloogia on konstandid ning x on muutuja. Sama väite võib ümber kirjutada järgnevalt:

\begin{equation*} \exists Tudeng(x) \land [ \neg Õpib(Ajalugu, x) \lor \neg Õpib(Bioloogia, x) ] \end{equation*}

Näide

\begin{equation*} P(x) \equiv (x > 2) \land (x < 4) \end{equation*}

Analoogselt saame Pythonis kirja panna funktsiooni P:

def P(x):
    return (x > 2) and (x < 4)

Pythonis nagu ka paljudes teistes funktsionaalsetes programeerimiskeeltes on lambda notatsioon mis näeb pisut matemaatilisem välja ning võimaldab luua anonüümseid ehk nimeta funktsioone:

P = lambda x: (x > 2) and (x < 4)

Kui predikaadi muutujad asendada mingite konkreetsete väärtustega lubatud väärtustehulgast, siis predikaat muutub lauseks ehk omandab tõeväärtuse.

Predikaate tähistatakse suurtähtedega ning temas sisalduvaid (predikaat)muutujaid väiketähtedega. Pythoni koodimistavad näevad küll ette, et funktsioonide nimed kui ka muutujate nimed on väiketähtedega.

Laused, väärtustamine ning funktsioonide välja kutsumine

Väärtustades x = 3 saame tõese predikaatlause, ehk võib öelda, et täisarvul 3 on omadus P:

\begin{equation*} P(3) = (3 > 2) \land (x < 4) = 1\:ehk\:tõene \end{equation*}

Pythonis tähendaks see funktsiooni välja kutsumist teatud argumentidega:

>>> P = lambda x: (x > 2) and (x < 4)
>>> P(3)
True

Predikaatmuutujate kohta tuleb eelnevalt täpsustada, milliseid väärtusi ta võib omandada ehk milline on predikaadi määramispiirkond. Programeerimiskeeltes võib leida erinevaid vahendeid määramispiirkonna paika panemiseks: andmetüübid, erindid, klassid (?). Pythoni puhul näiteks:

>>> 5/0
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ZeroDivisionError: integer division or modulo by zero

Näide

Kasutame prdikaadina Luhtus(x, y), mis tähendab tudeng y kukkus läbi aine x:

\begin{equation*} Luhtus(x,y) \equiv tudeng\:y\:kukkus\:läbi\:aine\:x \end{equation*}

Ainult üks tudeng kukkus läbi ajaloos:

\begin{align*} \exists x [ Tudeng(x) \land Luhtus(Ajalugu, x) \land \\ \forall y [ ( \neg ( x = y ) \land Tudeng(y) ) \implies \\ \neg Luhtus(Ajalugu, y)]] \end{align*}

Predikaat vs funktsioon

Näiteks "Iga ema armastab oma last" võib kirja järgnevalt kui Ema on kahe argumendiga predikaat:

\begin{equation*} \forall x \exists y Ema(x, y) \land Armastab(x, y) \end{equation*}

Esimest järku loogikas funktsioonid esinevad vaid predikaatides: Siin on Ema kasutusel kui funktsioon:

\begin{equation*} \forall x Armastab(x, Ema(x)) \end{equation*}

Kuna predikaat käsitleb vaidtõeväärtusi tuleb numbriliste väärtuste jaoks funktsiooni kasutada:

\begin{equation*} Hinne(x, y) \equiv tagastab\:tudengi\:x\:hinde\:aines\:y \end{equation*}

Küll aga saab jällegi predikaati kasutada nende võrdlemiseks:

\begin{equation*} SuuremKui(x,y) \equiv x > y \end{equation*}

Parim hinne ajaloos oli suurem kui (parim) suvaline hinne bioloogias:

\begin{align*} \forall x [ Tudeng(x) \land Õpib(Bioloogia, x) \implies \\ \exists y [ Tudeng(x) \land Õpib(Ajalugu, y) \land \\ SuuremKui(Hinne(Ajalugu, y), Hinne(Bioloogia, x))]] \end{align*}

\begin{equation*} \forall x [ Professor(x) \land \neg Tark(x) \implies \forall y \neg Likes(x,y)] \end{equation*}

Rahuldatavus

A formula is valid when it holds for all interpretations, i.e. ways of interpreting the domain of objects as D = ∅, constants as elements of D, function symbols as functions D n → D and relations as subsets of D n , and valuations of the variables as elements of D

In fact, first-order validity is undecidable (Church/Turing).

In second-order logic we allow quantification over functions and predicates with object-level arguments, e.g. in the induction principle

In higher-order logic we even allow predicates and functions with predicates and functions for arguments, and allow quantification over those, for infinitely many ‘orders’.

QAoES TU Berlin