Was ist die Definition einer Definition?
Was ist in der mathematischen Logik oder anderen formalen Systemen die formale Definition einer Definition?
Wenn "A" als "B" definiert ist, wie ist die Definition von "A"? Handelt es sich sowohl um "A" als auch um "B" (z. B. "A: = B") oder nur um "B"?
Zum Beispiel auf S. 126 in §3. Nehmen wir an, dass Erweiterungen durch Definitionen in VIII Syntaktische Interpretationen und Normalformen in Ebbinghaus ' mathematischer Logik$S$ ist ein (nicht logischer) Symbolsatz,
3.1 Definition. Lassen$\Phi$ eine Reihe von sein $S$-Sätze.
(a) Angenommen $P \notin S$ ist ein $n$-ary Beziehungssymbol und $\phi_P(v_0, ... , v_{n-1})$ ein $S$-Formel. Dann sagen wir das$$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ ist ein $S$-Definition von $P$ im $\Phi$.
Welches soll ich als ein nennen $S$-Definition von $P$ im $\Phi$::
$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $?
Ist es kreisförmig zu definieren $P$ in Bezug auf sich selbst?
Ist ein $𝑆$-Definition von $𝑃$ im $Φ$ eine Interpretation des Symbols $P$ als $S'$-Satz? (als Teil einer syntaktischen Interpretation von$S'$ im $S'$ selbst?)
Ist das Aussehen von $P$ in seiner eigenen Definition $∀ 𝑣_0,....∀ 𝑣_{𝑛−1}(𝑃𝑣_0...v_{𝑛−1}↔𝜙_𝑃(𝑣_0,...,𝑣_{𝑛−1}))$im gleichen Sinne wie das Erscheinen von $A$ im $𝐴:=𝐵$?
$\phi_P(v_0, ... , v_{n-1})) $? (Ich vermute, dass$P$ ist definiert als $\phi_P(v_0, ... , v_{n-1})) $ im $\Phi$.)
$\phi_P$? (Vergleichen Sie das mit dem zweiten:$P$ selbst beinhaltet keine Variablen)
Siehe Wie definiert diese Definition ein Symbol?$P$ außerhalb des Symbolsatzes $S$ Als ein $S$-Satz?
Vielen Dank.
Antworten
Wir haben eine Unterschrift $S$ und wir erweitern es auf $S':=S\cup\{P\}$.
Das $S$-Definition von $P$ ist der $S'$-Formel $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$was formal als zusätzliches Axiom zum Gegebenen behandelt werden kann$S$-Theorie, mit der wir arbeiten, und damit ein Äquivalent produzieren $S'$-Theorie, in der das Symbol $P$kann als Abkürzung für die Formel verwendet werden$\phi_P$.
Zum Beispiel ist die folgende Formel die Definition der üblichen Ordnungsbeziehung $\le$ von nichtnegativen ganzen Zahlen in der Sprache $(0,+)$:: $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
Im Folgenden werde ich zunächst versuchen, den Prozess intuitiver zu beschreiben, und dann Ihre Sorgen um die Zirkularität ansprechen. Ich vermute, dass der letztere Punkt tatsächlich hilfreicher ist. Lesen Sie also zuerst den zweiten Abschnitt - und insbesondere das dort hervorgehobene Motto wird meiner Meinung nach sehr hilfreich sein.
(Betreff: Ihr letzter Kommentar, die Definition ist $(1)$- die Sache, die Ihnen sagt, wie sich das neue Symbol in Bezug auf die alten Symbole verhält, die Sie bereits haben und verstehen.)
Der Schlüsselbegriff hier ist " Erweiterung durch Definitionen ".
Intuitiv denken wir an folgenden Prozess:
Beginnend mit einer Unterschrift $S$ und einige setzen $\Phi$ von $S$-Sätze, wir ärgern uns ein wenig über Ineffizienzen : Es gibt einige Dinge, über die wir sprechen können$S$-Formeln, aber nur auf Umwegen. Denken Sie zum Beispiel an die Sprache der Mengenlehre,$\{\in\}$: wir können Dinge ausdrücken wie "$x$ ist das kartesische Produkt von $y$ und $z$"In dieser Sprache, aber nur über ärgerlich lange Formeln. (Es ist eine gute Übung, mit dem vorherigen Beispiel umzugehen - beispielsweise mit Kuratowski-Paaren.)
Also angesichts unserer wirklich komplizierten Formel $\varphi(x_0,...,x_{n-1})$Wir wollen eine neue Theorie aufstellen, die im Grunde die gleiche ist wie $\Phi$ außer dass es zusätzlich eine "Abkürzung" für hat $\varphi$.
Erstens bedeutet dies, dass wir unsere Sprache erweitern wollen: anstatt damit zu arbeiten $S$ wir wollen mit arbeiten $S\cup\{R\}$ für einige $n$-ary Beziehungssymbol $R\not\in S$ was wir als Abkürzung für dienen wollen $\varphi$.
Jetzt müssen wir eine Theorie in dieser größeren Sprache definieren. Diese Theorie sollte zusammenfassen, was wir bereits haben (das heißt,$\Phi$), sollte das Verhalten von richtig diktieren $R$ (das heißt, sagen Sie, dass es eine Abkürzung für ist $\varphi$) und sollte nichts anderes tun. Dies führt uns dazu, die neue Theorie zu betrachten$$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
Die Passage von $S,\Phi$, und $\varphi$ zu $S\cup\{R\}$ und $\Phi'$ist eine Erweiterung durch Definitionen . Wir haben hier eine ernsthafte Redundanz : im genauen Sinne,$\Phi'$ ist wirklich nicht besser als $\Phi$. (Formal,$\Phi'$ist eine konservative Erweiterung von$\Phi$ im stärksten Sinne: jedes Modell von $\Phi$ hat genau eine Erweiterung zu einem Modell von $\Phi'$.) Das ist nicht überraschend. Wir wussten bereits, dass wir das ausdrücken können, was uns wichtig ist$\varphi$Wir wollten das nur schneller können.
Beachten Sie im Übrigen, dass dies eine natürliche "maximal effiziente" Version jeder Theorie nahe legt: Fügen Sie einfach neue Symbole für jede Formel hinzu! Dies nennt man Morleyisierung und ist gelegentlich nützlich (obwohl normalerweise irgendwie albern ).
OK, was ist nun mit der Zirkularität, über die Sie sich Sorgen machen?
Beachten Sie zunächst, dass "$R$"selbst ist nur ein Symbol. Der neue Satz, den wir hinzufügen, ist nicht wirklich eine Definition von $R$, sondern eine Definition der Bedeutung von $R$, oder wenn Sie eine Regel bevorzugen, die das Verhalten von regelt$R$.
Im Ernst, Zirkularität ist in FOL nie ein Thema! Die Schlüsselidee ist die folgende, die meiner Meinung nach eine wichtige Abweichung von den Intuitionen darstellt, die man aus der Programmierung einbringen könnte:
Eine Reihe von erster Ordnung Sätzen nicht schaffen Dinge, es beschreibt Dinge.
Insbesondere eine Reihe von Sätzen erster Ordnung $\Phi$schnitzt eine bestimmte Klasse von Strukturen heraus, über die es sich um eine genaue Beschreibung handelt. Zum Beispiel die möglicherweise gefährlich aussehenden Sets$$\{\forall x(P(x)\leftrightarrow P(x))\}$$ und $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$sind vollkommen kreisfrei; Sie sind nur leer (= Halten jeder Struktur) bzw. widersprüchlich (= Halten keiner Struktur).