Übung Proof Theory

**_m@rt!n** · 02-04-2012, 11:29

Hab mir mal die proof theory Übung vorgenommen.

ich komm auf:
1. contradiction
2. satisfiable
3. valid
4. valid
5. satisfiable
6. satisfiable

wobei ich das 1. mit SC gezeigt hab. für ND bin ich mir nicht ganz sicher wie man da am besten vorgehen soll. wenn man die gesamte formel negiert, bekommt man ja not(A) und daraus lässt sich nur bottom ableiten. von bottom ausgehend kann man zwar ein beliebiges A, not(A) ableiten, aber das ist ja dann reines rumgerate...

zu den interpretation:
es sollte ja kein problem sein, satisfiable/falsifiable mit hilfe von dummy-prädikaten wie isInteger und integer als domain zu zeigen oder?

**Adok** · 02-04-2012, 19:21

Zur Interpretation: Da bin ich auch deiner Meinung.

Was die Natural Deduction betrifft, muss ich gestehen, dass ich aus den Vorlesungsfolien noch nicht ganz schlau geworden bin. In diese Materie muss ich mich erst einlesen.

**Adok** · 03-04-2012, 10:10

Mir ist noch etwas eingefallen: "Negation Allquantor" entspricht ja "Existenzquantor Negation". Vielleicht hilft dir diese Regel beim Natural-Deduction-Beispiel.

**_m@rt!n** · 03-04-2012, 10:50

versteh ich das richtig, dass du folgendes meinst:
$This image was created with the kind support of Paulchen$
darf man die formeln überhaupt verändern, außerhalb der möglichkeiten von ND? ich dachte, umformen sollte man hier nicht...

**Adok** · 03-04-2012, 11:11

Originally Posted by _m@rt!n

versteh ich das richtig, dass du folgendes meinst:
$This image was created with the kind support of Paulchen$

Ja, genau das meinte ich.

Originally Posted by _m@rt!n

darf man die formeln überhaupt verändern, außerhalb der möglichkeiten von ND? ich dachte, umformen sollte man hier nicht...

Das weiß ich nicht. Wie gesagt, habe ich mich mit Natural Deduction noch nicht ausreichend auseinandergesetzt.

Schreibst du die Hausübung mit LaTeX? Wie formatierst du die Beweise?

**Raph_M** · 03-04-2012, 12:09

Originally Posted by _m@rt!n

darf man die formeln überhaupt verändern, außerhalb der möglichkeiten von ND? ich dachte, umformen sollte man hier nicht...

Hab mit den Beispielen zwar noch nicht begonnen, aber ich glaube dass solche Umformungen nicht erlaubt sind.

Man befindet sich bei diesen Proofverfahren ja rein auf der syntaktischen Seite, sprich man darf wirklich nur "pattern-match-mäßig" die Regeln des jeweiligen Kalküls für einen Proof verwenden, aber kein "externes Wissen" über die Semantik der jeweiligen Logik.

**_m@rt!n** · 03-04-2012, 12:10

bussproofs ist gut geeigent:
http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/

**Adok** · 03-04-2012, 14:36

Originally Posted by _m@rt!n

Hab mir mal die proof theory Übung vorgenommen.

ich komm auf:
1. contradiction
2. satisfiable
3. valid
4. valid
5. satisfiable
6. satisfiable

Wie lauten deine Gegenbeispiele bei 3 und 5?

Ich tue mir beim Beweisen von 4 schwer - die Regel für den Existenzquantor links führt bei mir zu einer Aussage P(y) |- P(t), womit ich nichts anfangen kann.

**_m@rt!n** · 03-04-2012, 15:33

3: is bei mir valid
5: nimm zB isOdd und integers: es gibt nen integer der ungerade is, aber nicht alle integer sind ungerade: 1 -> 0

4: immer zuerst die quantoren auflösen, die eine eugenvariable-condition haben, dann sollte es klappen

**Adok** · 03-04-2012, 16:11

Originally Posted by _m@rt!n

5: nimm zB isOdd und integers: es gibt nen integer der ungerade is, aber nicht alle integer sind ungerade: 1 -> 0

Das ist meines Erachtens kein Gegenbeispiel, denn wenn nicht alle Integer ungerade sind, gibt es einen Integer, der gerade ist, so dass die Implikation stimmt (0 -> 0). Ich glaube, die Formel 5 ist gültig.

**_m@rt!n** · 04-04-2012, 10:21

hast recht, ich war da etwas vorschnell mit dem countermodel. das 5er is tatsächlich valid, man muss nur beim proven etwas herumprobieren. (Tipp: exists verdoppeln, weakening)

hab dazu mal alle formeln durch nen prover geschickt, folgendes müsste demnach stimmen:
1. contradiction
2. satisfiable
3. valid
4. valid
5. valid
6. satisfiable

**_m@rt!n** · 04-04-2012, 12:26

um nochmal auf ND zurückzukommen, ist folgendes erlaubt?

canceln auf unterschiedlichen branches (also ich bekomme das [A] auf einem branch, möchte es aber auf einem anderen verwenden)
mehrfaches canceln (ich bekomme [A] und möchte damit 2mal A canceln)

**Adok** · 05-04-2012, 10:12

Originally Posted by _m@rt!n

hab dazu mal alle formeln durch nen prover geschickt, folgendes müsste demnach stimmen:

Welchen Prover verwendest du? Gibt es ihn auch für DOS bzw. Windows?

**_m@rt!n** · 05-04-2012, 12:51

ich verwende prover9-mace4. in den output von dem ding hab ich mich aber ehrlich gesagt nicht eingelesen. ich verwend es nur, um die ergebnisse zu verifizieren.

**Zapster** · 13-04-2012, 13:12

Originally Posted by _m@rt!n

canceln auf unterschiedlichen branches (also ich bekomme das [A] auf einem branch, möchte es aber auf einem anderen verwenden)

Würde sagen das ist nicht erlaubt. Die Hypothese hat mit dem 'anderen' Branch nichts zutun.

Originally Posted by _m@rt!n

mehrfaches canceln (ich bekomme [A] und möchte damit 2mal A canceln)

Würd sagen ja. Auf dem Branch wo du [A] bekommen hast kannst du es immer zum Schließen des Zweiges verwenden.

Angaben ohne Gewähr

**_m@rt!n** · 14-04-2012, 13:55

das entspricht leider genau dem was ich vermutet hatte und vernichtet damit meinen proof :-(

hat schon wer den ND-proof fürs erste beispiel geschafft?

**Dimitrij** · 14-04-2012, 15:10

Originally Posted by _m@rt!n

hat schon wer den ND-proof fürs erste beispiel geschafft?

Ich denk schon:
man nimmt an, dass die Formel 1 wahr ist.
R(b,b) -> -R(b,b).
Annahme: R(b,b).
-R(b,b).
falsum.
-R(b,b)
Annahme: Formel 1 ist wahr.
-R(b,b)->R(b,b)
R(b,b)
falsum
nicht Formel 1

**_m@rt!n** · 15-04-2012, 17:43

deine beschreibung hat mich zwar irgendwie verwirrt, aber zumindest so weit zum denken angeregt, dass ich ne lösung finden konnte

(ich hab allerdings falsumx3 und eine RAA)

eine letzte frage hab ich noch:
wie formal habt ihr das mit der interpretation bei satisfiable/not valid gemacht?

bei mir schaut das in etwa so aus:
Domain=irgendwas
$This image was created with the kind support of Paulchen$

und dann noch ein paar sätze warum es unter dieser interpretation (k)ein model ist.

möglicherweise ist das zu informell, aber andererseits denk ich mir, dass eine strikt formale interpretation irgendwie übertrieben ist.

**Dimitrij** · 15-04-2012, 19:45

Originally Posted by _m@rt!n

eine letzte frage hab ich noch:
wie formal habt ihr das mit der interpretation bei satisfiable/not valid gemacht?

bei mir schaut das in etwa so aus:
Domain=irgendwas
$This image was created with the kind support of Paulchen$

und dann noch ein paar sätze warum es unter dieser interpretation (k)ein model ist.

möglicherweise ist das zu informell, aber andererseits denk ich mir, dass eine strikt formale interpretation irgendwie übertrieben ist.

Für die Domain D nehm ich eine Menge mit möglichst wenigen Elementen (aber natürlich mindestens eins) z.B. D={a,b}
Meistens reichen ein, zwei oder drei Elemente.
Den Prädikatsymbolen muss man Mengen zuordnen, z.B. m(A)={a} (A ist ein einstelliges Prädikat) oder m(A)={(a,b)} (A ist ein zweistelliges Prädikat). Diese Mengen können natürlich auch leer sein. Den Konstantensymbolen ordnet m ein Element aus D zu (z.B. m(b)=b), den Funktionssymbolen Funktionen über D (z.B. m(f)(a)=b, m(f)(b)=b).
Für die freien Variablen definier ich eine assignment, z.B. a(x)=b. Oder ich sag, dass die assignment beliebig sein kann.

**Dimitrij** · 17-04-2012, 19:44

die Angabe zu Proof Theory wurde am 13.April geändert (nur Anmerkungen hinzugefügt)

**Adok** · 18-04-2012, 08:39

Originally Posted by Dimitrij

die Angabe zu Proof Theory wurde am 13.April geändert (nur Anmerkungen hinzugefügt)

Wie definiert man eine Interpretation "in a formal and correct way"?

**_m@rt!n** · 24-04-2012, 15:08

was die formal korrekte interpretation angeht, bin ich jetzt nochmal ins grübeln gekommen.

wie behandelt man den fall, wenn eine variable gebunden und frei vorkommt?
normalerweise argumentiert man bei einem forall ja so: $This image was created with the kind support of Paulchen$

doch wenn es jetzt schon ein freies x gab, das unter dem assignment zugewiesen wurde, ist diese notation doch problematisch oder? wie kann man das umgehen? eines von beiden x umbenennen?

**Raph_M** · 26-04-2012, 15:07

Nicht zu kompliziert denken, wie Dimitrij schon geschrieben hat:

Eine Interpretation ist eine Menge + eine Definition der Relationen und Funktionen bezüglich dieser Menge.
Man soll bei SAT but not VALID Formeln einfach eine Interpretation angeben unter der die Formel true wird und eine Interpretation unter der die Formel false wird.

@Adok: Mit dem "define the interpretation in a formal and correct way" ist nur gemeint dass man das ganze mathematisch korrekt (z.B. sind Relationen Subsets vom k-fachen kartesischen Produkt) anschreiben soll.

@Martin: Du bist anscheinend schon mitten in der semantischen Auswertung der Formeln bezüglich deiner Interpretation - das ist imo garnicht gefordert, man soll die beiden Interpretationen jeweils nur angeben.

**Dimitrij** · 26-04-2012, 15:42

Originally Posted by _m@rt!n

was die formal korrekte interpretation angeht, bin ich jetzt nochmal ins grübeln gekommen.

wie behandelt man den fall, wenn eine variable gebunden und frei vorkommt?
normalerweise argumentiert man bei einem forall ja so: $This image was created with the kind support of Paulchen$

doch wenn es jetzt schon ein freies x gab, das unter dem assignment zugewiesen wurde, ist diese notation doch problematisch oder? wie kann man das umgehen? eines von beiden x umbenennen?

Da gibt es kein Problem. Die Variablenbelegung wird nur für die Formel geändert, die zum Quantor gehört.
Beispiel:
Gegeben sei die Formel F, der Frame M und die Variablenbelegung a. Wir wollen den Wahrheitswert berechnen.
$This image was created with the kind support of Paulchen$ .

M=(D,m)
D={0,1}
m(A)={(0,1),(1,1)}
m(B)={0}

$This image was created with the kind support of Paulchen$

$This image was created with the kind support of Paulchen$ gdw.
$This image was created with the kind support of Paulchen$ und $This image was created with the kind support of Paulchen$ .
Das zweite ist wahr, da a(x)=0 und 0 ist in m(B).
Das erste ist wahr gdw. $This image was created with the kind support of Paulchen$ für alle $This image was created with the kind support of Paulchen$ .
$This image was created with the kind support of Paulchen$ wobei a2 diese Belegung ist:
$This image was created with the kind support of Paulchen$
$This image was created with the kind support of Paulchen$ , da a(x)=0 und a(y)=1 und (0,1) ist in m(A)
$This image was created with the kind support of Paulchen$ , da a2(x)=1 und a2(y)=1 und (1,1) ist in m(A)

Daher: $This image was created with the kind support of Paulchen$

**Raph_M** · 26-04-2012, 21:22

Jetzt stehe ich noch beim Sequenzkalkül #3 beim folgenden Zwischenschritt etwas an:

$This image was created with the kind support of Paulchen$

Angenommen ich mache $This image was created with the kind support of Paulchen$ mit der Wahl $This image was created with the kind support of Paulchen$ - kommt dann $This image was created with the kind support of Paulchen$ oder $This image was created with the kind support of Paulchen$ heraus?

Ich vermute ersteres, da in $This image was created with the kind support of Paulchen$ noch immer gebundene $This image was created with the kind support of Paulchen$ vorkommen und die durch das $This image was created with the kind support of Paulchen$ nicht verändert werden?

Anders ausgedrückt geht es mir um die Definition von "bound Variable" bei geschachtelten Quantoren über die gleiche Variable - gilt der Bindingbereich des äußeren Quantors über den ganzen Ausdruck oder nur "bis zum" inneren Quantor?

**Dimitrij** · 27-04-2012, 09:32

Originally Posted by Raph_M

Jetzt stehe ich noch beim Sequenzkalkül #3 beim folgenden Zwischenschritt etwas an:

$This image was created with the kind support of Paulchen$

a ist deine Eigenvariable? Das geht aber nicht. Bei Anwendung einer Regel mit Eigenvariable darf die Eigenvariable im unteren Sequent nicht frei vorkommen. Man weiß aber nicht, ob a in C frei vorkommt. Das weiß man nur von x.

siehe:
http://www.cis.upenn.edu/~jean/gbooks/logic.html
http://sakharov.net/sequent.html

**Adok** · 27-04-2012, 10:05

Originally Posted by Dimitrij

a ist deine Eigenvariable? Das geht aber nicht. Bei Anwendung einer Regel mit Eigenvariable darf die Eigenvariable im unteren Sequent nicht frei vorkommen. Man weiß aber nicht, ob a in C frei vorkommt. Das weiß man nur von x.

siehe:
http://www.cis.upenn.edu/~jean/gbooks/logic.html
http://sakharov.net/sequent.html

Die Eigenvariable-Condition muss nur berücksichtigt werden, wenn der Allquantor rechts vom \vdash steht. Somit ist OK, was Raph_M gemacht hat. Ich würde auch sagen, Cx bleibt Cx, weil es ja noch an Quantoren gebundene Vorkommnisse von x enthält.

**Dimitrij** · 27-04-2012, 10:07

Originally Posted by Adok

Die Eigenvariable-Condition muss nur berücksichtigt werden, wenn der Allquantor rechts vom \vdash steht.

Stimmt. Und das A(a) ist ja aus dem forall x A(x) auf der rechten Seite entstanden. Daher ist es nicht korrekt.

**Adok** · 27-04-2012, 11:43

Originally Posted by Dimitrij

Stimmt. Und das A(a) ist ja aus dem forall x A(x) auf der rechten Seite entstanden. Daher ist es nicht korrekt.

Wieso? Die Eigenvariable-Bedingung besagt nur, dass die Variable a nicht in der Konklusion stehen darf, wo die Regel \forall r angewandt wurde. In den Prämissen darf sie sehr wohl stehen.

**Dimitrij** · 27-04-2012, 11:53

Originally Posted by Adok

Wieso? Die Eigenvariable-Bedingung besagt nur, dass die Variable a nicht in der Konklusion stehen darf, wo die Regel \forall r angewandt wurde. In den Prämissen darf sie sehr wohl stehen.

in der Konklusion kommt die Formel C vor, und man weiß nicht, ob C ein freies a enthält

**Raph_M** · 27-04-2012, 13:34

Danke fürs Durchdenken Dimitrij, die Annahme dass mein geposteter Zwischenschritt durch ein $This image was created with the kind support of Paulchen$ entstanden ist war richtig.

Wenn ich dich richtig verstehe bedeutet das, dass $This image was created with the kind support of Paulchen$ die einzig gültige Wahl als Eigenvariable für dieses vorhergehende $This image was created with the kind support of Paulchen$ ist, ich dann einfach dieselbe Wahl für das $This image was created with the kind support of Paulchen$ treffe, mein gepostetes Dilemma garnicht auftritt und ich so relativ einfach zu Axiomen komme.

Aber als abschließende Frage: Ist $This image was created with the kind support of Paulchen$ bei den Quantorenregeln als Ersetzung überhaupt erlaubt (sofern $This image was created with the kind support of Paulchen$ nicht in den anderen Sequenten auftritt)?

Kleiner edit für die Nachwelt damit jeder versteht worums hier geht und warum die Verwirrung zustande kam:

Die QuantorenRegeln mit eigenvariable Condition stehen etwas schlecht in den Folien erklärt, z.B. $This image was created with the kind support of Paulchen$ :

$This image was created with the kind support of Paulchen$
------------------
$This image was created with the kind support of Paulchen$

$This image was created with the kind support of Paulchen$ is an eigenvariable, i.e. $This image was created with the kind support of Paulchen$ <- ungenau!
$This image was created with the kind support of Paulchen$ is an eigenvariable, i.e. $This image was created with the kind support of Paulchen$ <- besser, free()... freie Variablen im jeweiligen Termset

Im diskutierten Beispiel ist $This image was created with the kind support of Paulchen$ nicht bekannt, das heisst es kann potenziell jede Variable als freie Variable vorkommen, ausser eben $This image was created with the kind support of Paulchen$ wegen dem Angabetext

.

**Dimitrij** · 27-04-2012, 14:26

Originally Posted by Raph_M

Danke fürs Durchdenken Dimitrij, die Annahme dass mein geposteter Zwischenschritt durch ein $This image was created with the kind support of Paulchen$ entstanden ist war richtig.

Wenn ich dich richtig verstehe bedeutet das, dass $This image was created with the kind support of Paulchen$ die einzig gültige Wahl als Eigenvariable für dieses vorhergehende $This image was created with the kind support of Paulchen$ ist, ich dann einfach dieselbe Wahl für das $This image was created with the kind support of Paulchen$ treffe, mein gepostetes Dilemma garnicht auftritt und ich so relativ einfach zu Axiomen komme.

genau

Aber als abschließende Frage: Ist $This image was created with the kind support of Paulchen$ bei den Quantorenregeln als Ersetzung überhaupt erlaubt (sofern $This image was created with the kind support of Paulchen$ nicht in den anderen Sequenten auftritt)?

ja, ich denk schon.

Kleiner edit für die Nachwelt damit jeder versteht worums hier geht und warum die Verwirrung zustande kam:

Die QuantorenRegeln mit eigenvariable Condition stehen etwas schlecht in den Folien erklärt, z.B. $This image was created with the kind support of Paulchen$ :

$This image was created with the kind support of Paulchen$
------------------
$This image was created with the kind support of Paulchen$

$This image was created with the kind support of Paulchen$ is an eigenvariable, i.e. $This image was created with the kind support of Paulchen$ <- ungenau!
$This image was created with the kind support of Paulchen$ is an eigenvariable, i.e. $This image was created with the kind support of Paulchen$ <- besser, free()... freie Variablen im jeweiligen Termset

Beide Bedingungen sind nicht ganz richtig, glaube ich.
Richtig ist: die Eigenvariable darf in der gesamten Konklusion nicht frei vorkommen, also auch nicht in forall x A. So steht es jedenfalls bei Gallier, bei Sakharov und bei Kleene (Introduction to Metamathematics).

Im diskutierten Beispiel ist $This image was created with the kind support of Paulchen$ nicht bekannt, das heisst es kann potenziell jede Variable als freie Variable vorkommen, ausser eben $This image was created with the kind support of Paulchen$ wegen dem Angabetext

.

genau

**Raph_M** · 27-04-2012, 14:53

Dann nochmal danke für die Hilfe, hab deine Anmerkung noch in meinen Post editiert - die Erklärung sollte jetzt komplett richtig sein damit die Anderen nicht in die gleiche Falle wie ich tappen.

**Seimuun** · 03-05-2012, 17:37

Hi. ich hab bei den natural deductions noch irgendwie probleme. hat vielleicht irgendwer einen link auf ein einfaches durchgerechnetes beispiel? ich konnte keines finden und nur aus den regeln auf den folien werd ich nicht schlau. vielen dank im vorraus

**Dimitrij** · 04-05-2012, 00:32

Originally Posted by Seimuun

Hi. ich hab bei den natural deductions noch irgendwie probleme. hat vielleicht irgendwer einen link auf ein einfaches durchgerechnetes beispiel? ich konnte keines finden und nur aus den regeln auf den folien werd ich nicht schlau. vielen dank im vorraus

Wir müssen nur bei einer Formel ND anwenden.
Im Buch Logic in Computer Science (Huth; Ryan) steht viel über Natural Deduction. Im Internet findet man auch einiges. Man kann auch bei Gentzen nachlesen: http://gdz.sub.uni-goettingen.de/dms...g/?IDDOC=17178

**Deldrarim** · 04-05-2012, 11:40

Wenn 5) valid ist, müsste ich dies doch mit |-F im SC zeigen können. Nachdem ich dann aber die Regeln Exist r und Impl. r angewandt habe, müsste ich Forall r anwenden und eine neue Eigenvariable einführen -> dann komm ich aber auf keine Axiome sondern nur auf Antiaxiome :/

**Dimitrij** · 04-05-2012, 11:50

Originally Posted by Deldrarim

Wenn 5) valid ist, müsste ich dies doch mit |-F im SC zeigen können. Nachdem ich dann aber die Regeln Exist r und Impl. r angewandt habe, müsste ich Forall r anwenden und eine neue Eigenvariable einführen -> dann komm ich aber auf keine Axiome sondern nur auf Antiaxiome :/

Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent. Nach forall r macht man wieder exist r.

**Deldrarim** · 04-05-2012, 11:59

Originally Posted by Dimitrij

Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent. Nach forall r macht man wieder exist r.

oO? Das steht aber hier -> http://www.logic.at/lvas/wiki/images...ooftheory2.pdf nicht !?!? Da wird doch nur als Bedingung bei forall r und exist l angegeben, dass die eingeführte Variable y eine Eigenvariable sein muss.

**Dimitrij** · 04-05-2012, 12:19

Originally Posted by Dimitrij

Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent. Nach forall r macht man wieder exist r.

Originally Posted by Deldrarim

oO? Das steht aber hier -> http://www.logic.at/lvas/wiki/images...ooftheory2.pdf nicht !?!? Da wird doch nur als Bedingung bei forall r und exist l angegeben, dass die eingeführte Variable y eine Eigenvariable sein muss.

ja eh.
Ich meinte: nach Anwenden der Regel forall-r wendet man die Regel exist-r an (mit der gleichen Variablenersetzung).

**Deldrarim** · 04-05-2012, 12:23

Originally Posted by Dimitrij

ja eh.
Ich meinte: nach Anwenden der Regel forall-r wendet man die Regel exist-r an (mit der gleichen Variablenersetzung).

Nur, dass ich Exist r als erstes anwenden muss, da es am äußersten steht.. :/

**Dimitrij** · 04-05-2012, 12:26

Originally Posted by Deldrarim

Nur, dass ich Exist r als erstes anwenden muss, da es am äußersten steht.. :/

ja, also von unten nach oben betrachtet:
exist-r
implication-r
forall-r
exist-r
implication-r

**Deldrarim** · 04-05-2012, 12:31

Originally Posted by Dimitrij

ja, also von unten nach oben betrachtet:
exist-r
implication-r
forall-r
exist-r
implication-r

sry, ich steh da irgendwie grad komplett auf der leitung.. wenn ich exist-r und implication-r angewandt habe, hab ich doch keine implication/exists mehr.. dann kann ich nur noch forall anwenden und dann is es aus..

**Raph_M** · 04-05-2012, 12:48

Der Tipp war schon oben irgendwo - ganz zu Beginn die Formel verdoppeln.

5) ist das einzige Beispiel wo der Sequenzkalkül nicht "automatisch" aufgeht sondern man etwas tricksen muss

.

**Dimitrij** · 04-05-2012, 12:59

Originally Posted by Deldrarim

sry, ich steh da irgendwie grad komplett auf der leitung.. wenn ich exist-r und implication-r angewandt habe, hab ich doch keine implication/exists mehr.. dann kann ich nur noch forall anwenden und dann is es aus..

Originally Posted by Raph_M

Der Tipp war schon oben irgendwo - ganz zu Beginn die Formel verdoppeln.

5) ist das einzige Beispiel wo der Sequenzkalkül nicht "automatisch" aufgeht sondern man etwas tricksen muss

.

Oder man verwendet die exists-r-Regel, wo die exists-Formel auch oben steht. Das meinte ich, als ich schrieb "Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent".

Es gibt mindestens zwei Varianten des Sequentialkalküls. Ich glaube, man kann sich aussuchen, welche man für diese Aufgaben verwendet.

**Deldrarim** · 04-05-2012, 12:59

ahh.. tricky

**Deldrarim** · 04-05-2012, 13:01

Originally Posted by Dimitrij

Oder man verwendet die exists-r-Regel, wo die exists-Formel auch oben steht. Das meinte ich, als ich schrieb "Beim Anwenden von Exist r schreibt man die exists-Formel ins obere Sequent".

bekomm ich dann nicht nen infinite branch? oder kann ich dann danach einfach die exist regel anwenden, bei der oben kein exist hinkommt?

**Dimitrij** · 04-05-2012, 13:18

Originally Posted by Deldrarim

bekomm ich dann nicht nen infinite branch?

nein
Man erhält dann eh ein Axiom (ein Sequent, wo die linke und die rechte Seite eine Formel gemeinsam haben).

oder kann ich dann danach einfach die exist regel anwenden, bei der oben kein exist hinkommt?

Naja, dann würde man die Varianten des Sequentialkalküls vermischen. Ich weiß nicht, ob man das darf/soll.

Die eine Variante des Sequentialkalküls stammt von Gentzen (in den Folien: LK):
http://sakharov.net/sequent.html
Das ist eine zweite Variante (G4 von Kleene; in den Folien: LK'; ich verwende diese; wird auch in TIL verwendet, aber nur für Aussagenlogik):
http://sakharov.net/sequent.html#formulation

**Raph_M** · 04-05-2012, 14:47

Originally Posted by Dimitrij[/QUOTE

Es gibt mindestens zwei Varianten des Sequentialkalküls. Ich glaube, man kann sich aussuchen, welche man für diese Aufgaben verwendet.

Stimmt, in den Folien sind auch beide Varianten.

**daLois** · 04-05-2012, 17:08

Bin grad am übertragen der aufgabe in Latex, wie formatiert ihr das ganze? Speziell, tragt ihr bei jedem step die zugehörige regel ein?
oder reicht das hier (Aufgabe1, SC):

**Raph_M** · 04-05-2012, 17:27

Ist das "manuell" erstellt?

Mit http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/ gehts sehr komfortabl, z.B. werden die Sequenzsymbole ausgerichtet und man kann auch die Regeln seitlich annotieren (wie ist im Manual auf der Seite sehr gut beschrieben).

Ah und weil ichs grad seh - die $This image was created with the kind support of Paulchen$ und $This image was created with the kind support of Paulchen$ sind überflüssig.

**Madnebular** · 04-05-2012, 17:29

Originally Posted by daLois

Bin grad am übertragen der aufgabe in Latex, wie formatiert ihr das ganze? Speziell, tragt ihr bei jedem step die zugehörige regel ein?
oder reicht das hier (Aufgabe1, SC):

Braucht man das Gamma und Delta bei uns? Dachte die wären leere Mengen.

Außerdem hätt ich noch eine Frage zur Natural Deduction, das mir iwie nicht einleuchtet... Bei Beispiel 5 müssen wir ja " |- ! phi " zeigen. Und kann ich dann nicht einfach die Assumption " phi " treffen, daraus Falsum ableiten, und dann beweisen wie ich lustig bin? Das kommt mir halt relativ spanisch vor...

**Dimitrij** · 04-05-2012, 17:34

Originally Posted by Madnebular

Braucht man das Gamma und Delta bei uns? Dachte die wären leere Mengen.

stimmt

Außerdem hätt ich noch eine Frage zur Natural Deduction, das mir iwie nicht einleuchtet... Bei Beispiel 5 müssen wir ja " |- ! phi " zeigen. Und kann ich dann nicht einfach die Assumption " phi " treffen, daraus Falsum ableiten, und dann beweisen wie ich lustig bin? Das kommt mir halt relativ spanisch vor...

Bei Beispiel 5 brauchen wir nicht ND machen, da die Formel gültig ist.

**Madnebular** · 04-05-2012, 17:41

Originally Posted by Dimitrij

stimmt

Bei Beispiel 5 brauchen wir nicht ND machen, da die Formel gültig ist.

Ich meinte eh 1. Man nimmt ja die negierte Formel an. Und nachdem man ja sonst keine Formeln zum Arbeiten hat, muss man was annehmen. Also hab ich die ursprüngliche Formel angenommen. Und damit hab ich schon mein Falsum. Kann mich bitte jemand kurz aufklären? Ich hab das Gefühl ich überseh da was.

**Dimitrij** · 04-05-2012, 17:43

Originally Posted by Madnebular

Ich meinte eh 1. Man nimmt ja die negierte Formel an. Und nachdem man ja sonst keine Formeln zum Arbeiten hat, muss man was annehmen. Also hab ich die ursprüngliche Formel angenommen. Und damit hab ich schon mein Falsum.

Wieso hast du damit schon ein Falsum? Das musst du ja erst ableiten.

**Madnebular** · 04-05-2012, 17:53

Ergibt sich das nicht sofort aus der Assumption von phi? Phi, !phi |- Falsum?
Oder funktioniert das eher so?

1. !phi prämisse
2. phi assumption
4. phi[x/b] forall e 2
5. r(b,b) > !r(b,b) and e_1 4
6. r(b,b) assumption
7. !r(b,b) > e 5
8. Falsum !e 6,7

Mir ist das halt nicht wirklich klar wann ich was annehmen darf, und wie sich das auswirkt, weil das in den Folien nicht wirklich vorkommt...

Nicht? Das ist eben das, was ich nicht verstehe...

**Dimitrij** · 04-05-2012, 18:00

Originally Posted by Madnebular

Ergibt sich das nicht sofort aus der Assumption von phi? Phi, !phi |- Falsum?
Oder funktioniert das eher so?

1. !phi prämisse
2. phi assumption
4. phi[x/b] forall e 2
5. r(b,b) > !r(b,b) and e_1 4
6. r(b,b) assumption
7. !r(b,b) > e 5
8. Falsum !e 6,7

Mir ist das halt nicht wirklich klar wann ich was annehmen darf, und wie sich das auswirkt, weil das in den Folien nicht wirklich vorkommt...

Nicht? Das ist eben das, was ich nicht verstehe...

!phi ist keine Prämisse. Man muss !phi herleiten, ohne irgendwelche Prämissen.

**Madnebular** · 04-05-2012, 18:02

Originally Posted by Dimitrij

!phi ist keine Prämisse. Man muss !phi herleiten, ohne irgendwelche Prämissen.

Dh ich muss |- !phi aus |- phi herleiten?

**Dimitrij** · 04-05-2012, 18:08

Originally Posted by Madnebular

Dh ich muss |- !phi aus |- phi herleiten?

Du musst !phi aus nichts herleiten. Du darfst aber Annahmen treffen, die du dann wieder aufhebst durch passende Regelanwendungen.

**Dimitrij** · 04-05-2012, 18:12

verbale Kurzfassung des ND-Beweises von Beispiel 1:
Angenommen, die Formel aus Beispiel 1 wäre wahr (in einer Interpretation). Dann lässt sich herleiten, dass -R(b,b) wahr ist. Dann lässt sich auch herleiten, dass R(b,b) wahr ist. Widerspruch! Also ist die Formel nicht wahr.