7.3

[Gerros]

hab mal ne Lösung, die hoffentlich stimmt. mal schauen ob ichs halbwegs beschreiben kann:
als erstes brauchen wir mal A > A (">" steht für das impliziert zeichen), und das bekommt man auf die selbe Art, wie es im Skriptum bzw. in den VO Folien steht, da die ersten beiden gegebenen Axiome jeweils ident sind.
Ich geb mal nur die Ersetzungen an, und nicht immer die ganze Wurscht:
jetzt nimmt man AX5 mit (B->A, C->A). mit dem daraus resultierenden AX5 und dem abgeleiteten A>A wendet man den mp (modus ponens) an. mit dem was da rauskommt und A>A wieder den mp andwenden, wobei bei den beiden anwendungen des mp jeweils das A>A links oben beim mp steht.
jetzt müsste man haben: (AoderA)>A, das nehmen wir jetzt links oben beim nächsten mal modus ponens und oben rechts nehmen wir das AX1 mit (A->((AoderA)>A) ... fertig!?!?

[david.mihola]

Also, soweit ich das jetzt nachvollziehen konnte, stimmt deine Lösung!

Darf man fragen, wie du darauf gekommen bist? Einfach stundenlanges herumprobieren, oder irgendwie mit Methode? Oder irgendwo dazwischen?

LG, David

[Bianconeri]

Genial, die Lösung sollte wirklich stimmen. Mich würde allerdings auch interessieren wie man darauf kommt. Habe das schon ewig probiert und bin nicht drauf gekommen.

[jperl]

also ich habe jetzt mal versucht die lösung nachzuvollziehen. kann natürlich sein, dass ich mich irre, aber ein punkte sind mir unklar bzw. ich denke nicht, dass diese lösung richtig ist.

wenn wir A -> A wie angegeben wie im skriptum s. 125 (version oktober 08) erhalten, dann ist das doch unser B des mp.
somit ist an dieser stelle doch imho sense, weil wir das B durch die axiome nicht mehr weiter zerlegen können.

weiters würde ich sagen (A->((AvA)->A ist != B->((AvA)->A).

jperl

ps: ich werde natürlich auch gerne vom gegenteil überzeugt, dass diese lösung richtig ist.
nachdem ich mich jedoch kurz damit beschäftigt habe, bin ich nicht dieser meinung.

[david.mihola]

(A->((AvA)->A ist != B->((AvA)->A).


Ja, das hab ich zunächst auch so verstanden wie du und mich gewundert. Ich denke aber, dass es so gemeint war:

Wir verwenden Axiom 1 und ersetzen: A ↦ ((A ∨ A) ⊃ A)
Dann ist Axiom 1 (rechte Prämisse im MP): ((A ∨ A) ⊃ A) ⊃ (B ⊃ ((A ∨ A) ⊃ A))
und gemeinsam mit der linken Prämisse (die wir vorher mühevoll gebildet haben): ((A ∨ A) ⊃ A)
folgt daraus: (B ⊃ ((A ∨ A) ⊃ A)). Ta-DAH!

So stimmt's doch dann, oder?

Und zu deiner ersten Frage: Ja, das (A ⊃ A) ist schon das B im MP, aber man kann's ja trotzdem als eine der beiden Prämissen (in unserem Fall zweimal als linke) für weitere MPs verwenden.

LG, David

[schrankk]

hab mal ne Lösung, die hoffentlich stimmt. mal schauen ob ichs halbwegs beschreiben kann:
als erstes brauchen wir mal A > A (">" steht für das impliziert zeichen), und das bekommt man auf die selbe Art, wie es im Skriptum bzw. in den VO Folien steht, da die ersten beiden gegebenen Axiome jeweils ident sind.
Ich geb mal nur die Ersetzungen an, und nicht immer die ganze Wurscht:
jetzt nimmt man AX5 mit (B->A, C->A). mit dem daraus resultierenden AX5 und dem abgeleiteten A>A wendet man den mp (modus ponens) an. mit dem was da rauskommt und A>A wieder den mp andwenden, wobei bei den beiden anwendungen des mp jeweils das A>A links oben beim mp steht.
jetzt müsste man haben: (AoderA)>A, das nehmen wir jetzt links oben beim nächsten mal modus ponens und oben rechts nehmen wir das AX1 mit (A->((AoderA)>A) ... fertig!?!?

Wirklich genial!! :thumb:

ich denke mir mal, dass man /*einfach*/ rückrechnen versuchen muss! Also aus welchen Axiomen Endformel konstruierbar ist, etc. und etc. :shiner:

[jperl]

Und zu deiner ersten Frage: Ja, das (A ⊃ A) ist schon das B im MP, aber man kann's ja trotzdem als eine der beiden Prämissen (in unserem Fall zweimal als linke) für weitere MPs verwenden.

hab das jetzt auch im skriptum gefunden. alles was aus den axiomen via formel ableitbar ist, ist auch ein axiom.

dann schauts natürlich gut aus.

jperl

[Gedor@]

Blöde Frage : Macht man das auch wie beim Sequentialkalkül von Unten nach Oben (scheint mit viel leichter), oder anders herum ???

[KatzeImSack]

Blöde Frage : Macht man das auch wie beim Sequentialkalkül von Unten nach Oben (scheint mit viel leichter), oder anders herum ???

nein, von oben nach unten.
prinzipiell läuft das so ab: alles was man mit hilfe von den axiomen + modus nonsens ableiten kann ist "gültig" (quasi das B unterm bruchstrich beim MP)

jetzt versucht man durch geschickte umformung der start-axiome das endergebnis herauszubekommen.

wenns gelingt: endergebnis gültig(Tautologie)...
wenn nicht hat man eigentlich gar keine andere erkenntnis gewonnen glaub ich...

grüße!

€dit: hmm... lt. Tutor geht man scheinbar doch auch von unten nach oben!
vermutlich jenachdem wie man sich leichter tut...
(vermutlich tut man sich wirklich von u nach o leichter....)