pathterminuspages/brkmnd.dk/aboutcontactabout me

Syntaks

25-06-2017|Prædikatlogik

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

  • En hver variabel er en term.
  • Lad c være en konstant, og c er en term.
  • Lad t_1, t_2, ... , t_n være termer, og lad f være en funktion med aritet n > 0. Da er f(t_1,t_2, ... ,t_n) en 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

  • Lad P være et prædikat med aritet større end 0. Lad t_1,t_2, ... ,t_n .isin termer. Da er P(t_1,t_2, ... , t_n) en formular.
  • Lad %phi være en formular. Da er \not %phi også en formular.
  • Lad %phi, %psi være formularer. Da er %phi .and %psi, %phi .or %psi, %phi .drarrow %psi også formularer.
  • Lad %phi, x være en formular hhv. en variabel. Da er (\forall x %phi), (\exist x %phi) 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.