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.