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
- 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:
Hvor:
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:
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.
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.