Logische Äquivalenzen als Beweisregeln

#Studium #Informatik #Definition #FoG

Formale Definition:
Wenn eine logische Äquivalenz $φ \equiv ψ$ bewiesen ist, kann diese im natürlichen Schließen als Inferenzregel "geschenkt" verwendet werden:

(\Rightarrow) \frac{φ}{ψ} und (\Leftarrow) \frac{ψ}{φ}

Auf der Zielseite einer Sequenz lassen sich damit Ziele direkt austauschen:

{} \Rightarrow φ_{1} \mapsto {} \Rightarrow φ_{2}

Auf der Annahmeseite lassen sich durch Äquivalenzen zusätzliche Annahmen generieren:

{φ_{1}} \Rightarrow ψ ⇝ {φ_{1}, φ_{2}} \Rightarrow ψ

Erklärung:
Anstatt logisch offensichtliche Umformungen (wie De Morgan oder Kommutativität) in jedem Beweisbaum mühsam Schritt für Schritt durch die Basisregeln herzuleiten, darfst du bekannte Äquivalenzen direkt als Ersetzungsregel anwenden. Das verkürzt lange Beweise massiv.

Links