Natural Deduction Calculus: alternative Or-Elimination herleiten
-
Hallo,
Ich rechne gerade ein paar alte Prüfungsaufgaben durch und obwohl ich sonst mit dem Natural Deduction Calculus eigentlich keine Schwierigkeiten habe, beiße ich mir an dieser Aufgabe hier vollkommen die Zähne aus:
Your boss proposes a new rule $$\lor e^*$$, where the negation of the assumption of the first case can be additionally used in the second case:
$\cfrac{ \begin{matrix} && [\phi]\_j && [\psi]\_j [\lnot \phi]_j\\ && \vdots && \vdots\\ \phi \lor \psi && \chi && \chi \\ \end{matrix} } {\chi} [\lor e^*]_j$Show her that you can simulate the new rule in NK without derived rules. Compare the length of both deductions? What is your finding?
Während ich natürlich verstehe, dass man hier bei einer entsprechenden Fallunterscheidung im Psi-Zweig $$\lnot \phi$$ annehmen kann, fehlt mir jeglicher Ansatz, wie ich das formal in NK zeigen können soll.
Habt Ihr vielleicht irgendwelche Tips oder Ideen? Vielleicht stehe ich hier auch nur gerade sehr auf der Leitung, sonst habe ich mit derartigen Beweisen eigentlich nie Schwierigkeiten.
-
Ok, ich habe mittlerweile wohl eine Lösung. Stand natürlich wiedermal unheimlich auf der Leitung.
Sollte irgendjemanden die Lösung interessieren, bitte hier posten. Ich müsste die nämlich erst transkribieren und dazu fehlt mir momentan ein bisschen die Zeit.