pathterminuspages/brkmnd.dk/aboutcontactabout me

Ækvivalenser

27-07-2017|Prædikatlogik

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?