Aufgabe:
die Formel "not not p -> p" soll hergeleitet werden.
Gegeben sind die Axiome:
A1 = A -> (B -> A)
A2 = (A -> (B -> C)) -> ((A -> B) -> (A -> C))
A3 = (not A -> not B) -> ((not A -> B) -> A)
Problem/Ansatz:
Der generelle Ansatz ist mir klar: ich nehme mir ein Axiom, ersetze darin die Variablen durch meine Zielformel und versuche danach den linken Teil der Resultatformel durch gezieltes Einsetzen anderer Axiome zu "eliminieren". Leider bin ich hier bei zahlreichen Versuchen zu keinem Ergebnis gekommen.
Kann mir jemand einen Ansatz geben?
Danke!
Emil
