Diskussion:Consequentia mirabilis

Zur Herleitung

Ich hätte eine Frage zu der Herleitung mit den PM-Axiomen: Aus der Definition des Pfeils soll folgen, dass $\neg p\rightarrow p=p\vee p$. Aber die Ersetzung ergibt erst einmal nur $\neg p\rightarrow p=\neg \neg p\vee p$; man müsste erst noch die doppelte Negation beseitigen. Wie würde man das im PM-Kalkül machen? In der verlinkten Axiomenliste habe ich dazu nichts gefunden. Danke. --37.5.23.242 (11:13, 19. Aug. 2015 (CEST), Datum/Uhrzeit nachträglich eingefügt, siehe Hilfe:Signatur)