Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Mathematik » Logik, Mengen & Beweistechnik » Einbettung höher stufiger Logiken in die erste Stufe
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule Einbettung höher stufiger Logiken in die erste Stufe
Simon_St
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.02.2011
Mitteilungen: 272
Aus: Bielefeld
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2017-07-03


Hallo,
ich habe gelesen, dass man die Prädikatenlogik zweiter Stufe (und höherer Stufen) in die Prädikatenlogik erster Stufe "einbetten" kann. Ich habe dazu allerdings nichts weiteres gefunden.

Meine Fragen:
1. Wie geht man bei dieser Einbettung vor?

2. Die Prädikatenlogik zweiter Stufe ist echt ausdrucksstärker als die erster Stufe. Was also geht bei der Einbettung verloren.

Hat die Einbettung was hier mit zu tun: In einem Logikbuch stand, dass die Prädikatenlogik erster Stufe im Prinzip für die Mathematik ausreicht, da man über den Umweg der Mengen auch (beliebige) Relationen beschreiben kann.



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Simon_St
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.02.2011
Mitteilungen: 272
Aus: Bielefeld
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, vom Themenstarter, eingetragen 2017-07-04


Hallo noch mal,
hier die Textstelle, wo ich das gefunden habe. Vll kann mir das jemand erklären:

"Logik höherer Stufe lässt sich ähnlich wie mehrsortige Logik in Prädikatenlogik erster
Stufe einbetten:
Grundidee: Die unterschiedlichen Typen werden als separate Typen von Basistypen
interpretiert; Applikation als Operation wird geeignet eingeschränkt; Typ-Konsistenz
wird durch zusätzliche Axiome (die die Modellklasse einschränken) gefordert."





Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Simon_St
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.02.2011
Mitteilungen: 272
Aus: Bielefeld
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, vom Themenstarter, eingetragen 2017-07-05


Hallo noch mals,
ich habe die Arbeit gefunden, in der die Einbettung angeblich gezeigt wird:
Manfred Kerber, "On the Representation of Mathematical Concepts and their Translation into First-Order Logic"

Weiß jemand was da gemacht wurde und kanns erklären?



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Simon_St
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.02.2011
Mitteilungen: 272
Aus: Bielefeld
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, vom Themenstarter, eingetragen 2017-07-05


Meine Hypothese:

Hallo,
ich erklär mal warum mich so eine Einbettung oder Kodierung in die erste Stufe interessiert.

Ich vermute, dass jeder semantisch korrekte Beweis, der zur Formalisierung höherstufige Logiken benutzt, in die erste Stufe eingebettet werden kann. In der ersten Stufe findet sich zu jedem semantischen Beweis eine syntaktische Ableitung (Gödelscher Vollständigkeitssatz). Das würde heißen, dass JEDER semantische Beweis erststufig syntaktisch nachvollzogen werden kann.

Es wird gesagt, dass Kalkülregeln für die zweite Stufe aufgestellt werden können, die semantisch korrekt sind. Allerdings kann nie ein vollständiger Kalkül für die zweite Stufe aufgestellt werden. Meine Vermutung (die irgendwo sicherlich bewiesen wurde, wenn sie korrekt ist und zeigbar) würde bedeuten, dass jede dieser Kalkülregeln für die zweite Stufe, die semantisch korrekt ist, bei einer Einbettung in eine Kalkülregel der ersten Stufe übergeht.

Hierzu müsste man in der ersten Stufe einen getypten Träger einführen. Das ist mengentheoretisch kein Problem, da höhere Typen wieder Mengen sind.

Freilich müsste bei der Einbettung der zweiten Stufe in die erste etwas verloren gehen, da die zweite Stufe echt ausdrucksstärker ist (Aber was?). Meine Vermutung würde bedeuten, dass das was verloren geht, nicht semantisch "relevant" ist. Dass kein semantischer Beweis der zweiten Stufe gefunden werden kann, der die ausdrucksstärkeren Mittel tatsächlich unreduzierbar verwendet.

Mich interessieren vor allem Beweise, in denen man mithilfe der ersten Stufe, Aussagen über die Ausdrucksstärke der ersten Stufe selbst macht. Meines Wissens wird angenommen, dass man den Gödelschen Vollständigkeitssatz und den Gödelschen Unvollständigkeitssatz allein mit Mitteln der ersten Stufe syntaktisch nachvollziehen kann.

Beim Gödelschen Vollständigkeitssatz fällt auf, dass man Quantoren verwendet, die über alle möglichen Modelle der ersten Stufe sprechen. Das wäre zunächst nur höherstufig ausdrückbar. Führt man einen getypten Träger ein, und spricht mithilfe der Mengenlehre über verschiedene Typen, so sollte der Vollständigkeitssatz nur mit Mitteln der ersten Stufe beweisbar sein.

Damit das alles funktioniert, müsste man zunächst die Semantik einer Logik vollständig darstellen können. Die Semantik spricht über ALLE Modelle einer Logik mit entsprechender Signatur. Indem gesagt wird, dass ein Beweis semantisch korrekt ist, wenn der bewiesene Satz in JEDEM Modell wahr ist, in dem auch die Axiome wahr sind. Angenommen man hat eine Logik erster Stufe mit entsprechender Signatur, dann müsste man doch die Menge aller Modelle bilden können (eingeschränkt auf eine Trägermenge mit spezifizierter Kardinalität).

Hierzu müsste ich erstmal folgende Frage klären: Bei der Spezifizierung eines Modells legt man zunächst eine Trägermenge fest. Dann folgt die Definition einer Struktur über diesen Träger. Spielt bei der Trägermenge nur die Kardinalität eine Rolle? D.h., dass die möglichen Modelle einer bestimmten Kardinalität sich NUR durch die definierte Struktur unterscheiden?



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Simon_St
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.02.2011
Mitteilungen: 272
Aus: Bielefeld
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, vom Themenstarter, eingetragen 2017-07-06


Hallo,
ich muss meine Vermutung verifizieren. Scheinbar ist es "echt" leichter einen Widerspruchsbeweis zu führen als die Konsistenz nachzuweisen.

Beim Nachweis der Konsistenz muss man ein Modell konstruieren, das vollständig charakterisiert ist. Nach dem Gödelschen zweiten Unvollständigkeitssatz werden dazu stärkere Mittel benötigt (die nicht z.B. durch eine Einbettung, reduziert werden können).

Gleichzeitig sagt er:"Sei T ein konsistentes formales System, das so stark ist, dass darin der erste Unvollständigkeitssatz formalisiert und bewiesen werden kann."

Das heißt, dass eine Theorie T seine eigene Unvollständigkeit beweisen kann, nicht jedoch seine eigene Konsistenz.

Weiss jemand dazu mehr?




Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Simon_St wird per Mail über neue Antworten informiert.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2020 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]