Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Logik, Mengen & Beweistechnik » Prädikatenlogik » Formel aus der Prädikatenlogik für ZFC verwenden
Autor
Universität/Hochschule Formel aus der Prädikatenlogik für ZFC verwenden
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1492
  Themenstart: 2023-01-23 17:41

Hallo allerseits, A sei eine Formel in der Prädikatenlogik 1. Stufe (PL1) bei der y eine freie Variable in A ist, f sei ein Funktionssymbol und x eine Variable. Ist meine folgende Behauptung richtig? Behauptung: $\vdash (\forall x \exists y \; y = fx) \land A(s)_s^{fx} \quad .\leftrightarrow. \quad \forall x \exists y \; (y = fx \land A(y))$ Bem: 1) Mein Beweis über die Wahrheit ist informal. 2) Ich verwende diese Behauptung, um durch definitorische Erweiterung (Buch Ebbinghaus über ZFC) generierten Operationssymbole (Funktionssymbole) zu eliminieren, so dass nur noch die Symbole von ZFC vorhanden sind. Dazu aber irgendwann später mehr. mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2686
  Beitrag No.1, eingetragen 2023-01-24 00:22

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}} \newcommand{\monus}{\mathbin {∸}}\) * Ist $y$ die einzige freie Variable in $A$? * Was soll $A(s)_s^{fx}$ sein? * (und $A(y)$, for that matter) * $\forall x \exists y \; y = fx$ stimmt eh immer. ----- Ich vermute ja jedenfalls mal, dass $y$ eine ausgewählte freie Variable in $A$ sein soll, und die Notation am Ende von Punkt 2 einfach 'ne Substitution ist, und "$A(t)$" für Terme $t$ auch. Also: $A(s)_s^{fx}$ ist derselbe Term wie $A(fx)$, und wie $A(y)_y^{fx}$; in etwas eindeutigerer Notation $A[fx/y]$. Und $A(y)$ ist $A$. Es geht also um $$ A[fx/y] \quad .\leftrightarrow. \quad \forall x \exists y \; (y = fx \land A), $$ bzw., wenn $x$ frei in $A$ vorkommt, um $$ A[fx/y] \quad .\leftrightarrow. \quad \forall x' \exists y \; (y = fx' \land A[x'/x]). $$ (Hier habe ich die gebundenen $x$ mal umbenannt, damit sie nicht in die Quere der freien Variable namens $x$ kommen.) \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1492
  Beitrag No.2, vom Themenstarter, eingetragen 2023-01-24 17:08

\quoteon(2023-01-24 00:22 - tactac in Beitrag No. 1) * Ist $y$ die einzige freie Variable in $A$? * Was soll $A(s)_s^{fx}$ sein? * (und $A(y)$, for that matter) * $\forall x \exists y \; y = fx$ stimmt eh immer. ----- Ich vermute ja jedenfalls mal, dass $y$ eine ausgewählte freie Variable in $A$ sein soll, und die Notation am Ende von Punkt 2 einfach 'ne Substitution ist, und "$A(t)$" für Terme $t$ auch. Also: $A(s)_s^{fx}$ ist derselbe Term wie $A(fx)$, und wie $A(y)_y^{fx}$; in etwas eindeutigerer Notation $A[fx/y]$. Und $A(y)$ ist $A$. \quoteoff Danke für deine kritische Durchsicht. Das hat mir sehr geholfen. Vermutlich wird deine Behauptung stimmen. Ich habe meine Behauptung abgeändert und die neue Version in PL1 bewiesen: Behauptung (modifiziert): $\vdash \forall x A[fx/y] \quad .\leftrightarrow. \quad \forall x \exists y \; (y = fx \land A)$ Beweis: 1) $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; (y = fx \land A)$ $\quad$ (Ph) $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; \exists y \; (y = fx \land A)$ $\quad$ [fx/y] $\vdash (fx = fx \land A[fx/y]) \quad .\rightarrow. \quad \; \exists y \; (y = fx \land A)$ $\quad$ [Aussagenlogik] $\vdash A[fx/y] \quad .\rightarrow. \quad \; \exists y \; (y = fx \land A)$ $\quad$ Gv $\vdash \forall x A[fx/y] \quad .\rightarrow. \quad \; \exists y \; (y = fx \land A)$ $\quad$ Gh und x nicht frei im Antezedenz $\vdash \forall x A[fx/y] \quad .\rightarrow. \quad \; \forall x \exists y \; (y = fx \land A)$ 2)\\ $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; (y = fx \land A) $ $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; (A[y/y] \leftrightarrow A[fx/y]) \land A $ $\quad$ Leibnitzsches Ersetzbarkeitstheorem $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; (A \leftrightarrow A[fx/y]) \land A $ $\quad$ Aussagenlogik $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; (A \rightarrow A[fx/y]) \land A $ $\quad$ Aussagenlogik $\vdash (y = fx \land A) \quad .\rightarrow. \quad \; A[fx/y])$ $\quad$ Pv und y nicht frei im Sukzedenz $\vdash \exists y \; (y = fx \land A) \quad .\rightarrow. \quad \; A[fx/y])$ $\quad$ Gv $\vdash \forall x \exists y \; (y = fx \land A) \quad .\rightarrow. \quad \; A[fx/y])$ $\quad$ Gh und x nicht frei im Antezedenz $\vdash \forall x \exists y \; (y = fx \land A) \quad .\rightarrow. \quad \; \forall x \; A[fx/y])$ Beweis Ende Ist das so korrekt? Gv: vordere Generalisierung Ph: hintere Partikularisierung mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2686
  Beitrag No.3, eingetragen 2023-01-25 02:15

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}} \newcommand{\monus}{\mathbin {∸}}\) Aus den jeweiligen Zeilen folgt jedenfalls die nächste. Die letzten beiden Schritte sind jeweils nicht nötig (und ich würde sagen, auch nicht wesentlich für den Kern der Frage), wenn man das Problem um $$\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (y = fx \land A)$$ kreisen lässt.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1492
  Beitrag No.4, vom Themenstarter, eingetragen 2023-01-25 10:41

\quoteon(2023-01-25 02:15 - tactac in Beitrag No. 3) Aus den jeweiligen Zeilen folgt jedenfalls die nächste. Die letzten beiden Schritte sind jeweils nicht nötig (und ich würde sagen, auch nicht wesentlich für den Kern der Frage), wenn man das Problem um $$\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (y = fx \land A)$$ kreisen lässt. \quoteoff Du hast vollkommen Recht! Behauptung (Auflösungslemma) $\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (A \land y=fx)$ Beweis: $\vdash A[fx/y] \quad .\leftrightarrow. \quad A[fx/y] \land \exists y \; y=fx$ $\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (A[fx/y] \land y=fx)$ y nicht frei in A[fx/y] $\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (A[fx/y] \land y=fx \land (y=fx \rightarrow (A[y/y] \leftrightarrow A[fx(y])$ Leibn. Ersetzbarkeitstheorem $\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (A[fx/y] \land y=fx \land (y=fx \rightarrow (A \leftrightarrow A[fx(y])$ $\vdash A[fx/y] \quad .\leftrightarrow. \quad \exists y \; (A \land y=fx)$ Aussagenlogik Ist der Beweis korrekt? mfg cx


   Profil
carlox hat die Antworten auf ihre/seine Frage gesehen.

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-2023 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]