MenuForside/BlogadenTeksterUfnetMusikNoerderierSozialOm

Prædikatlogik : Ækvivalenser - 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=12.

Herunder bevises nogle ækvivalenser vedrørende prædikatlogik. Ækvivalenserne er små sætninger, de er ret brugbare, og nogle af dem er ret omstændelige at bevise, så vi får brugt alle de forskellige introduktions- og eliminationsregler.

A1

Ækv : \exist x (\not P(x)) .assert .not\forall x (P(x))

\exist x (\not P(x)) __(præmis) .scopeStart \forall x (P(x)) __(antagelse) .scopeStart b __(scope) \not P(b) __(antagelse) P(b) __(.and e) .contra __(.not e) .scopeSlut .contra __(.not e) .scopeSlut .not\forall x (P(x)) __(.not i)

A2

Ækv : .not\forall x (P(x)) .assert \exist x (\not P(x))

.not\forall x (P(x)) __(præmis) .scopeStart .not\exist x (\not P(x)) __(antagelse) .scopeStart b __(scope) .scopeStart \not P(b) __(antagelse) \exist x (P(x)) __(.exist i) .contra __(.not e) .scopeSlut P(b) __(PBC) .scopeSlut \forall x (P(x)) __(.forall i) .contra __(.not e) .scopeSlut \exist x (\not P(x)) __(PBC)

B1

Ækv : \forall x (\not P(x)) .assert .not\exist x (P(x))

.not\forall x (P(x)) __(præmis) .scopeStart \exist x (P(x)) __(antagelse) .scopeStart b __(scope) .scopeStart P(b) __(antagelse) \not P(b) __(.forall e) .contra __(.not e) .scopeSlut .contra __(.exist e) .scopeSlut .contra __(.exist e) .scopeSlut .not\exist x (\not P(x)) __(.not i)

B2

Ækv : .not\exist x (P(x)) .assert \forall x (\not P(x))

.not\exist x (P(x)) __(præmis) .scopeStart a __(scope) .scopeStart P(a) __(antagelse) \exist xP(x) __(.exist i) .contra __(.not e) .scopeSlut \not P(a) __(.not i) .scopeSlut \forall x(\not P(x)) __(.forall i)

C1

Ækv : \forall x P(x) .and \forall x Q(x) .assert \forall x (P(x) .and Q(x))

\forall x P(x) __(præmis) \forall x Q(x) __(præmis) .scopeStart a __(scope) P(a) __(.forall e) Q(a) __(.forall e) P(a) .and Q(a) __(.and i) .scopeSlut \forall x (P(x) .and Q(x)) __(.forall i)

C2

Ækv : \forall x (P(x) .and Q(x)) .assert \forall x P(x) .and \forall x Q(x)

.not\exist x (P(x)) __(præmis) .scopeStart a __(scope) P(a) .and Q(a) __(.forall e) P(a) __(.and e1) .scopeSlut \forall x P(x) __(.forall i) .scopeStart b __(scope) P(b) .and Q(b) __(.forall e) Q(b) __(.and e2) .scopeSlut \forall x Q(x) __(.forall i) \forall x P(x) .and \forall x Q(x) __(.and i)

D

Ækv : \exist x (P(x) .and Q(x)) .assert \exist x P(x) .and \exist x Q(x)

\exist x ((P(x) .and Q(x)) __(præmis) .scopeStart a __(scope) P(a) .and Q(a) __(antagelse) P(a) __(.and e1) \exist x P(x) __(.exist i) .scopeSlut \exist x P(x) __(.exist e) .scopeStart a __(scope) P(a) .and Q(a) __(antagelse) Q(a) __(.and e2) \exist x Q(x) __(.exist i) .scopeSlut \exist x Q(x) __(.exist e) \exist x P(x) .and \exist x Q(x) __(.and i)

E1

Ækv : \exist x (P(x) .or Q(x)) .assert \exist x P(x) .or \exist x Q(x)

\exist x (P(x) .or Q(x)) __(præmis) .scopeStart a __(scope) P(a) .or Q(a) __(antagelse) .scopeStart P(a) __(antagelse) \exist x P(x) __(.exist i) \exist x P(x) .or \exist x Q(x) __(.or i1) .scopeSlut .scopeStart Q(a) __(antagelse) \exist x Q(x) __(.exist i) \exist x P(x) .or \exist x Q(x) __(.or i) .scopeSlut \exist x P(x) .or \exist x Q(x) __(.or e) .scopeSlut \exist x P(x) .or \exist x Q(x) __(.exist e)

E2

Ækv : \exist x P(x) .or \exist x Q(x) .assert \exist x (P(x) .or Q(x))

\exist x P(x) .or \exist x Q(x) __(præmis) .scopeStart \exist x P(x) __(antagelse) .scopeStart a __(scope) P(a) __(antagelse) P(a) .or Q(a) __(.or i1) \exist x (P(x) .or Q(x)) __(.exist i) .scopeSlut \exist x (P(x) .or Q(x)) __(.exist e) .scopeSlut .scopeStart \exist x Q(x) __(antagelse) .scopeStart a __(scope) Q(a) __(antagelse) P(a) .or Q(a) __(.or i2) \exist x (P(x) .or Q(x)) __(.exist i) .scopeSlut \exist x (P(x) .or Q(x)) __(.exist e) .scopeSlut \exist x (P(x) .or Q(x)) __(.or e)

F1

Ækv : \forall x \forall y (P(x) .and Q(y)) .assert \forall y \forall x (P(x) .and Q(y))

\forall x \forall y (P(x) .and Q(y)) __(præmis) .scopeStart a __(scope) .scopeStart b __(scope) \forall y (P(b) .and Q(y)) __(.forall e) P(b) .and Q(a) __(.forall e) .scopeSlut \forall x (P(x) .and Q(a)) __(.forall i) .scopeSlut \forall y \forall x (P(x) .and Q(y)) __(.forall i)

F2

Ækv : \forall y \forall x (P(x) .and Q(y)) .assert \forall x \forall y (P(x) .and Q(y))

\forall y \forall x (P(x) .and Q(y)) __(præmis) .scopeStart a __(scope) .scopeStart b __(scope) \forall x (P(x) .and Q(b)) __(.forall e) P(a) .and Q(b) CN_(.forall e) .scopeSlut \forall y (P(x) .and Q(y)) __(.forall i) .scopeSlut \forall x \forall y (P(x) .and Q(y)) __(.forall i)

G1

Ækv : \exist x \exist y (P(x) .and Q(y)) .assert \exist y \exist x (P(x) .and Q(y))

\exist x \exist y (P(x) .and Q(y)) __(præmis) .scopeStart a __(scope) \exist x (P(a) .and Q(y)) __(antagelse) .scopeStart b __(scope) P(a) .and Q(b) __(antagelse) \exist x (P(x) .and Q(b)) __(.exist i) \exist y \exist x (P(x) .and Q(y)) __(.exist i) .scopeSlut \exist y \exist x (P(x) .and Q(y)) __(.exist e) .scopeSlut \exist y \exist x (P(x) .and Q(y)) __(.exist e)

G2

Ækv : \exist y \exist x (P(x) .and Q(y)) .assert \exist x \exist y (P(x) .and Q(y))

\exist y \exist x (P(x) .and Q(y)) __(præmis) .scopeStart a __(scope) \exist x (P(x) .and Q(a)) __(antagelse) .scopeStart b __(scope) P(b) .and Q(a) __(antagelse) \exist y (P(b) .and Q(y)) __(.exist i) \exist x \exist y (P(x) .and Q(y)) __(.exist i) .scopeSlut \exist x \exist y (P(x) .and Q(y)) __(.exist e) .scopeSlut \exist x \exist y (P(x) .and Q(y)) __(.exist e)

Læg mærke til at D kun vises den ene vej. Jeg begyndte på den anden vej, men indså at denne ikke giver mening. Hvorfor?