Ableiten mit Hilberts Axiomen


Sie können aus den 15 Hilbertschen Axiomen
H1  = A -> (B -> A)
H2  = ((A -> B) -> A) -> A
H3  = (A -> B) -> ((B -> C) -> (A -> C))
H4  = A & B -> A
H5  = A & B -> B
H6  = (A -> B) -> ((A -> C) -> (A -> B & C))
H7  = A -> A | B
H8  = B -> A | B
H9  = (A -> C) -> ((B -> C) -> (A | B -> C))
H10 = A <-> B -> (A -> B)
H11 = A <-> B -> (B -> A)
H12 = (A -> B) -> ((B -> A) -> A <-> B)
H13 = (A -> B) -> (not B -> not A)
H14 = A -> not (not A)
H15 = not (not A) -> A
mit Abtrennungs- (mopo) und Einsetzungsregel (sub) weitere Formeln erzeugen.

Beispiel: wir wollen x -> x ableiten.

Quelltexte


best viewed with any browser


http://www.informatik.uni-leipzig.de/~joe/ mailto:joe@informatik.uni-leipzig.de