MenuForside/BlogadenTeksterUfnetMusikNoerderierSozialOm

Prædikatlogik : Syntaks - Nørderier/Teori

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)

Syntaks

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:

t .rarrow x | c | f(t, ... ,t)

Hvor:

x .isin vars, c er nullfunktion, f's aritet > 0

Definition af formularer

Eller som produktionsregler:

%phi .rarrow P(t_1,t_2, ... ,t_n) | (\not %phi) | (%phi .and %phi) | (%phi .or %phi) | (%phi .drarrow %phi) | (\forall x %phi) | (\exist x %phi)

Hvor der gælder:

t_1,t_2, ... ,t_n .isin termer

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:

\forall %epsilon > 0 \exist N .isin setN \forall n .isin setN (n .ge N .drarrow |a - a_n| .lt %epsilon)

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.

Frie og bunde variable

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.

Substitution

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.