| |
| Autor |
 Formel aus der Prädikatenlogik für ZFC verwenden |
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1504
 |  Themenstart: 2023-01-23
|
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 
Dabei seit: 15.10.2014
Mitteilungen: 2710
 | Beitrag No.1, eingetragen 2023-01-24
|
\(\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
Dabei seit: 22.02.2007
Mitteilungen: 1504
| Beitrag No.2, vom Themenstarter, eingetragen 2023-01-24
|
\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
Dabei seit: 15.10.2014
Mitteilungen: 2710
| Beitrag No.3, eingetragen 2023-01-25
|
\(\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
Dabei seit: 22.02.2007
Mitteilungen: 1504
| Beitrag No.4, vom Themenstarter, eingetragen 2023-01-25
|
\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. |
|
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]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
