HÜ 12 G2 (Sequenzenkalkül)

M.Scholz
Windoof-User
Windoof-User
Beiträge: 31
Registriert: 18. Sep 2009 10:19

HÜ 12 G2 (Sequenzenkalkül)

Beitrag von M.Scholz » 13. Aug 2010 11:16

Servus,

sitze gerade an der 12. Hausübung Aufgabe G2. In der Musterlösung zum Sequenzenkalkül werden die Konklusionen "mitgeschleppt". Dies macht das Kalkül meiner Meinung nach sehr unübersichtlich. In der AL wurden die Konklusionen jedoch nicht "mitgeschleppt".

Ist in der Klausur die Vorgehensweise aus der Musterlösung verlangt oder reicht die kürzere Variante?


Gruß Michael

Benutzeravatar
olg
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 297
Registriert: 1. Okt 2008 19:24

Re: HÜ 12 G2 (Sequenzenkalkül)

Beitrag von olg » 15. Aug 2010 11:13

M.Scholz hat geschrieben:Servus,

sitze gerade an der 12. Hausübung Aufgabe G2. In der Musterlösung zum Sequenzenkalkül werden die Konklusionen "mitgeschleppt". Dies macht das Kalkül meiner Meinung nach sehr unübersichtlich. In der AL wurden die Konklusionen jedoch nicht "mitgeschleppt". (ich meine die V der G2 wäre eine solche Aufgabe)

Ist in der Klausur die Vorgehensweise aus der Musterlösung verlangt oder reicht die kürzere Variante?


Gruß Michael
In den Folien von Prof. Otto werden die Originalformen nach Ersetzungen nicht weiter mitgeführt. Im letzten Jahr (SS2009 bei Prof. Kohlenbach) war das anders.
Man kommt manchmal nicht drum herum, sie mitzuschleppen, weil man sonst ggf. das Sequenzenkalkül nicht auflösen kann.

Als ich diesbezüglich meinen Übungstutor gefragt hatte, meinte er dass man sie eigentlich immer mitschleppt, Prof. Otto die Abwesenheit in den Regeln aber mit "Die kann man aus den Restmengen \(\Delta, \Gamma\) wieder herstellen" begründet.

Im Zweifelsfall würde ich in der Klausur fragen, ob es reicht wenn man einen Hinweis setzt, dass sie noch in der Menge vorhanden sind ;)
"To Perl, or not to Perl, that is the kvetching." ~Larry Wall

kartzow
Mausschubser
Mausschubser
Beiträge: 55
Registriert: 8. Apr 2010 14:12

Re: HÜ 12 G2 (Sequenzenkalkül)

Beitrag von kartzow » 18. Aug 2010 09:24

Hallo,

wenn man einen Sequenzenkalkuel-Beweis von unten nach oben aufzubauen versucht um die Allgemeingueltigkeit einer Sequenz zu zeigen, dann erlauben die Regeln aus dem Skript beim Aufloesen von Quantoren z.B. die urspruengliche Formel nach oben "mitzuschleppen" oder eben auch nicht. Beides sind korrekte Rueckwaerts-Anwendungen der entsprechenden Sequenzenregeln.
Es ist richtig, dass man beim grundsaetzlichen mitschleppen schnell bei unuebersichtlichen Sequenzen landet. Auf der anderen Seite gibt es Faelle, in denen man bestimmte Formeln mitschleppen muss um einen vollstaendigen Beweis erhalten zu koennen.

Fuer die Klausur ergeben sich also 2 grundlegende Strategien: Entweder man schleppt alles immer mit, dann wird es unuebersichtlich, aber man bleibt dann sicher nicht stecken, weil man eine Formel vergessen hat mitzunehmen. Oder man schleppt erstmal wenig mit um die Uebersicht zu behalten, muss sich dann aber vorher (oder waehrend des Beweisens) klar machen, ob man nicht eventuell bestimmte Quantoren doch mehrmals mit verschiedenen konkreten Termen ersetzen muss und dafuer die Formel zu mindest eine zeitlang mitschleppen muss.

Wenn man bereits semantisch verstanden hat, warum eine bestimmte Aussage allgemeingueltig ist, dann laesst sich daraus meistens ablesen, welche Formeln man eventuell im Sequenzenkalkuel mitschleppen sollte und welche man nach dem aufloesen einfach vergessen kann.

Mit freundlichen Gruessen,

Alexander Kartzow
Assistent zur FGDI

Antworten

Zurück zu „Archiv“