Hallo,
ich habe eine Frage zum Hilbertkalkül bzw. zu Ableitungen mit ihm:
Dass ich aus (A ^ B) semantisch A und B folgern kann, ist klar. Aber wie kann ich (A ^ B) zu A oder zu B ableiten?
Wahrscheinlich ist es ganz einfach und ich seh den Wald vor lauter Bäumen nicht… [28]
A "und" B
[latex]A \wedge B[/latex]
du hast (A and B) sowies das Axiom H6a (( A and B ) => A )
Modus Ponens anwenden und dann hast du A, wenn ich mich nicht täusche.
sorry, gerade habe ich es auch erkannt….
so wie ich es weiß, muss doch, wenn {(A -> B) und A} gilt, dann gilt auch B! Modus Ponens…
wie du aus (A ^ B) A oder B gültig machen möchtest weiß ich auch nicht… es gibt soviele Regeln… Axiome, da muss mal viel Puzzeln!!
arrgh, ich sags ja. wald und bäume.
danke :)
hoffe aber dass es richtig ist. bin mir unsicher ob das wirklich so einfach mit den axiomen geht
man kann sich kram aus der menge holen oder eins der axiome..
man kann sich also das axiom (A AND B) => A holen und weil man (A AND B) aus der Menge hat kann man mit diesen beiden sachen den Modus Ponens benutzen. mit sub(A)=(A AND B) und sub(B)=A so bekommt man A… das gleiche geht auch mit B.
So… das ist im Prinzip das was die anderen schon vor mir geschrieben habe, aber ich bin mir sicher, dass es so einfach ist.
ok wie schreibe ich das jetzt formal richtig?
(A and B) |- A mit Axiom H_6a und sub…..
runde klammern? oder doch so
{A and B} |- A
also ich hab es in einer tabelle wie im skript gemacht
In einer Spalte die Formel die man Abgeleitet hat und in der nächsten Spalte die Begründung für die Aufnahme (also dann Axiom H_6a und die substitutionen)…das macht man dann für jeden schritt. Einfach mal im Skript gucken… ist sehr übersichtlich so
fehlt nur noch das axiom H3…;-)
