Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Logik, Mengen & Beweistechnik » Prädikatenlogik » suche für eine Formel zugehörige Stufe der Prädikatenlogik
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule suche für eine Formel zugehörige Stufe der Prädikatenlogik
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1197
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2021-03-07


Hallo allerseits,
Will folgenden Sachverhalt (für Formeln der Prädikatenlogik 1. Stufe) formalisieren:
Für alle Formelmengen $\Sigma, \Sigma'$ gilt:
Wenn $\Sigma$ Obermenge von $\Sigma'$ ist, dann folgt für alle Formeln $\alpha$:
$\Sigma \vdash \alpha \Rightarrow \Sigma' \vdash \alpha$  

D.h. das Folgende soll formalisiert werden.
$\forall \Sigma \forall \Sigma' (\Sigma \supset \Sigma' \rightarrow \forall \alpha (\Sigma \vdash \alpha \rightarrow \Sigma' \vdash \alpha)) $  
Das geht so nicht, weil in der Prädikatenlogik Prädikate verwendet werden müssen, also hier die Prädikate T und B:
T intendiert die Teilmengenbeziehung
B intendiert die Beweisbarkeitsbeziehung

Ich komme also auf die folgende Formel:

$\forall \Sigma \forall \Sigma' (T(\Sigma', \Sigma) \rightarrow \forall \alpha  (B(\Sigma, \alpha) \rightarrow B(\Sigma', \alpha))) $

Fragen:
Ist das so korrekt?
In welcher Sprache ist diese Formel geschrieben?
In der Prädikatenlogik 2. Stufe ?

mfg
cx








Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 02.12.2013
Mitteilungen: 247
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2021-03-07


2021-03-07 09:05 - carlox im Themenstart schreibt:
D.h. das Folgende soll formalisiert werden.
$\forall \Sigma \forall \Sigma' (\Sigma \supset \Sigma' \rightarrow \forall \alpha (\Sigma \vdash \alpha \rightarrow \Sigma' \vdash \alpha)) $  
Das geht so nicht, weil in der Prädikatenlogik Prädikate verwendet werden müssen, also hier die Prädikate T und B:
T intendiert die Teilmengenbeziehung
B intendiert die Beweisbarkeitsbeziehung

$ \supset $ und $ \vdash $ sind doch Prädikate. Der Unterschied zu T und B ist doch nur, daß im ersten Fall infix-Schreibweise und im zweiten Fall prefix-Schreibweise verwendet wird.

2021-03-07 09:05 - carlox im Themenstart schreibt:
Ich komme also auf die folgende Formel:

$\forall \Sigma \forall \Sigma' (T(\Sigma', \Sigma) \rightarrow \forall \alpha  (B(\Sigma, \alpha) \rightarrow B(\Sigma', \alpha))) $

Fragen:
Ist das so korrekt?
In welcher Sprache ist diese Formel geschrieben?
In der Prädikatenlogik 2. Stufe ?

Was ist mit "korrekt" gemeint? Beide Sätze beschreiben einen identischen Sachverhalt, nur mit unterschiedlichen Prädikatensymbolen. Schaut man in irgendein Logikbuch nach der Definition der Sprache 1. Stufe, so stellt man fest: Beide Sätze 1. Stufe.

Allerdings drückt der Satz nicht das gewünschte aus, denn man hat ja 2 Diskursbereiche - Formelmengen und Formeln. Das kann (und muß) man auch mit Prädikaten ausdrücken. Also etwa "wenn Sigma eine Formelmenge ist, dann ...", "wenn alpha eine Formel ist, dann ...".

Um das dann zu beweisen, benötigt man noch die Definitionen aller Prädikate. Hier verläßt man die 1. Stufe, denn Formeln und Herleitung sind rekursiv (oder induktiv) definierte Begriffe und damit ist man in der 2. Stufe bzw. in der Prädikatenlogik 1. Stufe + Induktion. Das gilt schon, wenn sich Formelmengen, Formeln und Herleitung im Satz lediglich auf die Aussagenlogik beziehen.  



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1197
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, vom Themenstarter, eingetragen 2021-03-08


Hallo Zwerg_Allwissend,
vielen Dank für deine Antwort.

Allerdings drückt der Satz nicht das gewünschte aus, denn man hat ja 2 Diskursbereiche - Formelmengen und Formeln. Das kann (und muß) man auch mit Prädikaten ausdrücken. Also etwa "wenn Sigma eine Formelmenge ist, dann ...", "wenn alpha eine Formel ist, dann ...".

Um das dann zu beweisen, benötigt man noch die Definitionen aller Prädikate. Hier verläßt man die 1. Stufe, denn Formeln und Herleitung sind rekursiv (oder induktiv) definierte Begriffe und damit ist man in der 2. Stufe bzw. in der Prädikatenlogik 1. Stufe + Induktion. Das gilt schon, wenn sich Formelmengen, Formeln und Herleitung im Satz lediglich auf die Aussagenlogik beziehen.  
Ja, man muß den Satz _innerhalb_ von PL2 (Prädikatenlogik 2. Stufe) formulieren.
Was Terme und Formeln sind wird ja in PL1 nicht _innerhalb_ PL1 formuliert, sondern in der Metasprache, also außerhalb PL1.
Jetzt muß man Terme, Formeln, Formelmenge _innerhalb_ PL2 formulieren.
Ich weiß zwar wie man das außerhalb (in der Metasprache) PL1 macht (induktiv definierte Menge), habe keine Ahnung wie man innerhalb von PL2 machen kann.
Konkret:
Wie definierte man Terme _innerhalb_ PL2 ?

mfg
cx




Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 02.12.2013
Mitteilungen: 247
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2021-03-09


2021-03-08 18:40 - carlox in Beitrag No. 2 schreibt:
Ja, man muß den Satz _innerhalb_ von PL2 (Prädikatenlogik 2. Stufe) formulieren.
Was Terme und Formeln sind wird ja in PL1 nicht _innerhalb_ PL1 formuliert, sondern in der Metasprache, also außerhalb PL1.
Jetzt muß man Terme, Formeln, Formelmenge _innerhalb_ PL2 formulieren.
Ich weiß zwar wie man das außerhalb (in der Metasprache) PL1 macht (induktiv definierte Menge), habe keine Ahnung wie man innerhalb von PL2 machen kann.

Nein, man braucht nicht PL2. PL1 + Induktion reicht. Dabei ist Induktion durch ein Axiom (= Formel aus PL1) gegeben, so wie in der Peano-Arithmetik. Das ist schwächer als die Peano-Axiome, denn das "eigentliche" Induktionsaxiom ist nicht in PL1 formulierbar.

Entsprechend kann man für andere Datenobjekte verfahren, also für Terme, Formeln, Herleitung usw.



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1197
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, vom Themenstarter, eingetragen 2021-03-09


2021-03-09 00:38 - Zwerg_Allwissend in Beitrag No. 3 schreibt:

Nein, man braucht nicht PL2. PL1 + Induktion reicht. Dabei ist Induktion durch ein Axiom (= Formel aus PL1) gegeben, so wie in der Peano-Arithmetik. Das ist schwächer als die Peano-Axiome, denn das "eigentliche" Induktionsaxiom ist nicht in PL1 formulierbar.
Entsprechend kann man für andere Datenobjekte verfahren, also für Terme, Formeln, Herleitung usw.

Hallo Zwerg_Allwissend,
Was ist das Induktionsaxiom?
Ich kenne nur das Axiomenschema der Induktion.
Was muß man für Axiome hinzufügen, um von Formeln und Formelmengen sprechen zu können.
Leider habe ich immer noch keine Spur von Ahnung, wo man da ansetzen muß.

mfg
cx



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 02.12.2013
Mitteilungen: 247
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, eingetragen 2021-03-10


2021-03-09 08:30 - carlox in Beitrag No. 4 schreibt:
Was ist das Induktionsaxiom?
Ich kenne nur das Axiomenschema der Induktion.
Das ist das Gleiche.


2021-03-09 08:30 - carlox in Beitrag No. 4 schreibt:
Was muß man für Axiome hinzufügen, um von Formeln und Formelmengen sprechen zu können.

So wie in jedem Lehrbuch Formeln definiert sind, das sind dann die Axiome. Da diese induktiv definiert sind, erhält man aus der Definition sofort ein Induktionsprinzip.



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
metabole
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 15.08.2016
Mitteilungen: 53
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, eingetragen 2021-03-10


Offtopic, aber: Warum reicht PL1 nicht aus, um das 5. Peano Axiom zu formalisieren? Wie geht man stattdessen vor?

Viele Grüße
μεταβολή



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1197
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, vom Themenstarter, eingetragen 2021-03-10


Die folgende Formel (abgekürzt mit $\lambda$) muß also in PL1 + Induktion formuliert werden:
$\lambda :=$  $\forall \Sigma \forall \Sigma' (\Sigma \supset \Sigma' \rightarrow \forall \alpha (\Sigma \vdash \alpha \rightarrow \Sigma' \vdash \alpha)) $  
Ich gehe davon aus, daß mit "PL1 + Induktion" eine Menge $\Psi$ von Formeln ("Axiomen") gemeint ist, so daß gilt:
$\Psi \vdash \lambda$

Aus welchen Formeln besteht nun $\Psi$ ?
Sind das dann, die Formeln, die man braucht um Formeln zu definieren ?
Hast du das gemeint mit:
---------------------------------------------------------------
So wie in jedem Lehrbuch Formeln definiert sind, das sind dann die
Axiome. Da diese induktiv definiert sind, erhält man aus der Definition sofort ein Induktionsprinzip.
---------------------------------------------------------------
also gehört intuitiv so etwas wie die folgende Formel zu $\Psi$:
$\forall t_1 \forall t_2 (Tt_1 \land Tt_2) \rightarrow F(t_1=t_2)$
(mit der Bedeutung, daß $t_1=t_2$ eine Formel ist, wobei $t_1$ und $t_2$ beliebige Terme aus der Menge der Terme T sind)
und genauso:
$\forall f_1 \forall f_2 (Ff_1 \land Ff_2) \rightarrow F(f_1 \land f_2)$
(mit der Bedeutung, daß $f_1 \land f_2$ zu der Menge aller Formeln F gehört)
wobei T und F dann Relationssymbole sind.

Zuerst müßte man aber noch die Definition der Terme bringen:
Also gehört Folgendes auch zu $\Psi$:
$\forall x Tx$
und
$\forall t_1 \forall t_2 T(ft_1t_2)$, falls f ein2-stelliges Funktionssymbol ist.
bei unendlich vielen Funktionssymbolen mit entsprechenden Stelligkeiten wären das dann unendlich viele Elemente in $\Psi$

Allerdings werden hier in PL1 über verschiedene Dinge quantifiziert:
Variablen, Funktionen, Relationen. Wie z.B:
$\forall x ... \forall t_1 ... \forall f_1$
Kann das sein ?

Wenn das vollkommen falsch sein sollte (was ich vermute), was ich da denke, bitte ich dich mir mal ein Konkreteres Beispiel zu geben.

mfg
cx






Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 02.12.2013
Mitteilungen: 247
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, eingetragen 2021-03-10


2021-03-10 11:06 - metabole in Beitrag No. 6 schreibt:
Offtopic, aber: Warum reicht PL1 nicht aus, um das 5. Peano Axiom zu formalisieren?

Es wird über alle Teilmengen von N quantifiziert, und davon gibt es überabzählbar viele.

Es gibt aber nur abzählbar viele Instanzen der PL1-Version des Induktionssxioms.

2021-03-10 11:06 - metabole in Beitrag No. 6 schreibt:
Wie geht man stattdessen vor?

Man bleibt bei PL1 + Induktion. Die Schwäche dieses Ansatzes macht sich "im täglichen Leben" nicht bemerkbar. Anders gesagt, wenn man ein Beispiel findet, für das "PL1 + Induktion" nicht reicht, dann wird man berühmt => en.wikipedia.org/wiki/Goodstein%27s_theorem  




Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: im letzten Quartal
Dabei seit: 02.12.2013
Mitteilungen: 247
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, eingetragen 2021-03-10


2021-03-10 13:02 - carlox in Beitrag No. 7 schreibt:
Wenn das vollkommen falsch sein sollte (was ich vermute), was ich da denke, bitte ich dich mir mal ein Konkreteres Beispiel zu geben.

Nein, Du bist schon auf dem richtigen Weg.

2021-03-10 13:02 - carlox in Beitrag No. 7 schreibt:
Allerdings werden hier in PL1 über verschiedene Dinge quantifiziert:
Variablen, Funktionen, Relationen. Wie z.B:
$\forall x ... \forall t_1 ... \forall f_1$
Kann das sein ?

Nicht "Funktionen, Relationen" (das verwendet man in der Semantik), sondern "Funktionssymbole, Relationssymbole", denn hier geht es um die Syntax.

Das Problem mit den "verschiedene Dingen" kann man mittels weiterer Funktions- und Prädikatsymbole lösen. Beispiel:

all f, t1, t2. is-functionsymbol(f) & arity(f) = 2 & is-term(t1) & is-term(t2) -> is-term(ft1t2).



Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1197
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, vom Themenstarter, eingetragen 2021-03-12


(2021-03-10 22:35 - Zwerg_Allwissend in <a
Das Problem mit den "verschiedene Dingen" kann man mittels weiterer Funktions- und Prädikatsymbole lösen. Beispiel:

all f, t1, t2. is-functionsymbol(f) & arity(f) = 2 & is-term(t1) & is-term(t2) -> is-term(ft1t2).
Vielen Dank für diese Hilfe.
Ich werde in den nächsten Tagen ein konkretes Beispiel bringen.

mfg
cx




Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox 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-2021 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]