Udsagnslogik : Æ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=6.

Med eliminations- og introduktionsreglerne kan vi lave nogle sammensatte regler, eller ækvivalenser, der bliver brugt ret tit. To udsagn, φ og ψ, er ækvivalente hvis vi kan vise både φ ⊦ ψ og ψ ⊦ φ. B, C og D er de regler der kan udledes ved at negere et helt konnektiv, feks. ¬(p ∧ q). Alle regler er bevist.

A1

Ækv : \not p .or q .assert p .drarrow q

\not p .or q __(præmis) .scopeStart \not p __(antagelse) p __(antagelse) .contra __(.not e) q __(.contra e) .scopeSlut p .imp q __(.imp i) .scopeStart q __(antagelse) p __(antagelse) q __(fra antagelse) .scopeSlut p .imp q __(.imp i) p .imp q __(.or e)

A2

Ækv : p .drarrow q .assert \not p .or q

p .imp q __(præmis) .scopeStart .not(\not p .or q) __(antagelse) .scopeStart p __(antagelse) q __(.imp e) \not p .or q __(.or i2) .contra __(.not e) .scopeSlut \not p __(.not i) \not p .or q __(.or i1) .contra __(.not e) .scopeSlut \not p .or q __(PBC)

B1

Ækv : p .and \not q .assert \not (p .drarrow q)

p .and \not q __(præmis) .scopeStart p .imp q __(antagelse) \not q __(.and e2) p __(.and e1) q __(.imp e) .contra __(.not e) .scopeSlut \not (p .imp q) __(.not i)

B2

Ækv : .not(p .drarrow q) .assert p .and \not q

.not(p .imp q) __(præmis) .scopeStart .not(p .and \not q) __(antagelse) .scopeStart p __(antagelse) .scopeStart \not q __(antagelse) p .and \not q __(.and i) .contra __(.not e) .scopeSlut q __(PBC) .scopeSlut p .imp q __(.imp i) .contra __(.not e) .scopeSlut p .and \not q __(PBC)

C1 - De Morgans

Ækv : \not p .or \not q .assert .not(p .and q)

\not p .or \not q __(præmis) .scopeStart p .and q __(antagelse) .scopeStart \not p __(antagelse) p __(.and e) .contra __(.not e) .scopeSlut .scopeStart \not q __(antagelse) q __(.and e) .contra __(.not e) .scopeSlut .contra __(.or e) .scopeSlut .not(p .and q) __(.not i)

C2 - De Morgans

Ækv : .not(p .and q) .assert \not p .or \not q

.not(p .and q) __(præmis) .scopeStart .not(\not p .or \not q) __(antagelse) .scopeStart p __(antagelse) .scopeStart q __(antagelse) p .and q __(.and i) .contra __(.not e) .scopeSlut \not q __(.not i) \not p .or \not q __(.or i) .contra __(.not e) .scopeSlut \not p __(.not i) \not p .or \not q __(.or i) .contra __(.not i) .scopeSlut \not p .or \not q __(PBC)

D1 - De Morgans

Ækv : \not p .and \not q .assert .not(p .or q)

\not p .and \not q __(præmis) .scopeStart p .or q __(antagelse) .scopeStart p __(antagelse) \not p __(.and e) .contra __(.not e) .scopeSlut .scopeStart q __(antagelse) \not q __(.and e) .contra __(.not e) .scopeSlut .contra __(.or e) .scopeSlut .not(p .or q) __(.not i)

D2 - De Morgans

Ækv : .not(p .or q) .assert \not p .and \not q

.not(p .or q) __(præmis) .scopeStart p __(antagelse) p .or q __(.or i1) .contra __(.not e) .scopeSlut \not p __(.not i) .scopeStart q __(antagelse) p .or q __(.or i2) .contra __(.not e) .scopeSlut \not q __(.not i) \not p .and \not q __(.and i)

Teoremer

Følgende er ikke ækvivalente da de ikke kan bevises begge veje. Teoremer tjener det formål at de kan forkorte et bevis. E1, F1 og G1 kaldes syllogismer - et udsagn der består af 2 præmisser og en konklusion.

E1 - Modus Tollens

Teorem : p .drarrow q, \not q .assert \not p

p .imp q __(præmis) \not q __(præmis) .scopeStart p __(antagelse) q __(.imp e) .contra __(.not e) .scopeSlut \not p __(.not i)

F1 - Modus Tollendo Ponens

Teorem: p .or q, \not q .assert p

p .or q __(præmis) \not q __(præmis) .scopeStart p __(antagelse) .scopeSlut .scopeStart q __(antagelse) .contra __(.not e) p __(.contra e) .scopeSlut p __(.or e)

G1 - Modus Ponendo Tollens

Teorem : .not(p .and q), p .assert \not q

.not(p .and q) __(præmis) p __(præmis) .scopeStart q __(antagelse) p .and q __(.and i) .contra __(.not e) .scopeSlut \not q __(.not i)

Det svære ved disse beviser er for det meste at antage et negeret konnektiv. For disse skal åbnes indirekte. Feks. kan ¬(p ∧ q) ikke elimineres med de regler vi har til rådighed.