Sequentialkalkül

[Zentor]

Ich hab da ein Problem mit dem Bsp 4.31 zum Sequenzialkalkül auf der Seite 72. Wieso kann man für
A impliziert B, A |-- B die Formel impliziert-L anwenden?
die heißt
F,A impliziert B |-- G
Wenn ich jetzt {A} als F und {B} als G annehm schaut das wie
A, A impliziert B |-- B
aus und nicht
A impliziert B, A |-- B
???
Das ist doch nicht equivalent oder?
mfg Zentor

[shabby]

Doch das ist äquivalent

F|--G mit F={F1,..Fn},G={G1,..,Gn} bedeutet
sind F1,F2,..,Fn in allen Interpretatationen war, dann ist mindestens ein Gi war
da wir in G nur einen Sequent haben, heißt das:
Semantisch: Wenn alle Fi war sind, ist G war
Syntaktisch F1^F2^..^Fn wahr, dann G war
Ich nehme an du könntest irgendwie auch eine Implikation hinschreiben, aber aus mir bisher unerfindlichen Gründen, schränkt das die Allgemeinheit ein, d.h. ich glaube im Allgemeinen sind "impliziert" und "läßt sich ableiten aus" nicht ident.
ABER: Im Speziellen ist die UND-Verknüpfung kommutativ, sicher aber die Menge der Formeln in F, weil es ja egal ist ob ich "Sind F1 und F2 wahr" oder "Sind F2 und F1 wahr" meine.

btw: wie in vielen anderen Fächern auch (Paradebeispiel: Mathe), ist es auch in TheoInf für uns, die die Tiefen der Logik nicht kennen, nicht leicht ersichtlich, warum viele anscheinend logisch klingende Sachen im Allgemeinen nicht gültig sind (Vektorräume !)

[Zentor]

Was bedeutet dann F, A ??
und wo ist der Unterschied zwischen F,G und A,B in den Formeln?
Wie kann man dann schlussendlich sagen das die Gesamtformel ableitbar ist, müssen alle Variablen je links und rechts von |-- zu finden sein?
mfg Zentor

[shabby]

1)

F,G sind Mengen von Formeln
A,B sind einzelne Formeln

F,A |-- B bedeutet:

F1,F2,..Fn,A |-- B wobei wir aber die Fi Formeln zu einer Zusammenfassen, weil sie uns im entsprechenden Axiom nicht interessieren. zum Beispiel

die NOT(l) - Ableitung:

F,not B |-- G ===> F |-- G,A

bedeutet

wenn wir auf der linken Seite eine endliche Menge von Formeln haben, von den EINE SPEZIELLE not B ist (der Rest ist uns Egal), dann können wir sie von der linken Formelmenge weggeben und zur rechten in nicht-negierter Form dazu (informell gesprochen)

2)
Die Ableitung ist gültig wenn am Ende nur Axiome in den obersten Ableitungen stehen. (einziges Axiom des SeqKalküls: Wenn es Formeln gibt, die links und rechts von |-- vorkommen dann folgt daraus -> F |-- G)

Ähmm, mit einem Wort: so isses.

[funky]

ableitbar is es dann wenn links und rechts von |-- ein und die selbe variable vorkommt

A|--A,B ist ableitbar weil A links und rechts von dem haxn steht.

ich hab aber auch probleme mit der implikation links bei bsp 4.31

und bei oder links bei bsp 4.32 1. Variante
die 2. ist sonnenklar

ich hätt ma dacht dass das so ausschaut

A v B, not A |--b

B,not A ist B
b ist G
A ist A

aber was ist dann F?

so kanns ja wohl net stimmen weil ich so net weiterkomm

[funky]

sorry! wollte keine verwirrung stiften! Problem ist gelöst!

is ja wurscht wie ichs anschreibt

zu Bsp 4.31

A impliziert B, A |-- B is ja das selbe wie A, A impliziert B |--B

und dann passt eh eins zu eins mit implikation links zusammen

und zu Bsp 4.32

A v B, not A |-- B is das selbe wie not A, A v B |--B und dann passts eins zu eins zu oder links

vielleicht konnte ich damit auch zentor helfen mit dem was ist F und G Problem

funky