OBS! Denne artikel får stadig besøg ind i mellem. Den er ikke blevet opdateret siden jeg skrev den. Der er en masse tegn i artiklen der ikke er korrekt formateret. Indholdet her er i stedet på vej over på min engelsksprogede del af siden: https://brkmnd.com/pages/logic/Default.aspx?id=9.
Prædikatlogik - meget formelt. Givet reglerne for konnektiver kan prædikatlogik beskrives som termer og formularer. Så det gør vi:
(Eksempler gives med parsetræer. Jeg synes de letter forståelsen)
Definition af term
Bemærk at en konstant, c, kan beskrives som en funktion der ingen argumenter tager. En nullfunktion.
Denne definition kan beskrives som en produktion:
Hvor:
Definition af formularer
Eller som produktionsregler:
Hvor der gælder:
Begge produktionsregler er rekursive da de på højresiden indeholder ikke-terminaler. Den sidste produktion indeholder endda den første - formularer indeholder termer.
Eksempel(1)
Betragt \forall x((P(x) .drarrow Q(x)) .and S(x,y)). Vi får træet:
Eksempel(2)
Definitionen for konvergens i matematisk analyse er givet som følger:
Uden at forstå hvad den egentligt betyder, kan vi lave en grammatisk analyse og fremkalde et parsetræ - deraf navnet kontekstfri grammatik. Læg mærke til at > og < er prædikater og dermed formularer, og at - (minus) er en funktion og dermed en term.
Definition
Lad φ være en formular. En foremkomst af x i φ er fri i φ hvis x er et blad i det tilhørende parsetræ, og hvis der ikke er nogen sti fra bladet og op til en kvantor-node med x i, altså \forall x, \exist x. Hvis dette ikke er tilfældet, siges x at være bundet i φ.
For \forall x %phi, \exist x %phi kaldes den gren der former sig under den givne kvantor, for det scope der udgør den givne kvantor. Dette gælder ikke hvis x bliver bundet igen af en ny kvantor i samme scope - i dette tilfælde fanges x af et nyt scope.
Eksempel(3)
Betragt (\forall x(P(x) .and Q(x))) .drarrow (\not P(x) .or Q(y)) hvilken giver træet:
I træet er de to x'er på venstresiden bundet og under scopet af ∀x. På højresiden er alle variable, x og y, frie.
Definition
Lad x, t, %phi være en variabel, en term hhv. en formular. Da er %phi[t/x] den formular der fås ved at erstatte enhver fri foremkomst af x i φ med t.
Eksempel(3a)
Lad træet og formularen i Eksempel(3) være φ. Da er φ[x/t] det træ der fremkommer ved at udskifte x'et nederst på højre side med termen t.
Definition
Lad t, x, %phi være en term, variabel hhv. formular. Vi siger at t er fri for x i φ hvis der intet frit blad, x, er i φ i et scope under \forall y, \exist y samtidig med at at t indeholder en fri variabel y.
Den sidste definition her gør sig gældende i den situation hvor vi prøver at substituere x med t, hvor t indeholder et y der så bliver fanget af en kvantor. Denne situation er uhænsigtsmæssig.
Eksempel(4)
Betragt %phi = (\forall y(P(x) .and Q(y))) .and (\forall x(S(x,y))) som giver træet:
Lad derudover %psi, %upsilon = \forall y(P(x) .and Q(y)), \forall x(S(x,y)) samt t = y + 3.
Her er t fri for y i υ, men ikke i hverken ψ eller φ. Hvis vi foretager ψ[t/x] (Den eneste anden mulige substitution da y er bundet i ψ), vil y + 3 blive fanget af kvantoren ∀y.