定義の定義は何ですか？
数理論理学または他の形式的システムでは、形式的に定義の定義は何ですか？
「A」が「B」として定義されている場合、「A」の定義はどのようなものですか？「A」と「B」の両方（「A：= B」など）が含まれますか、それとも「B」のみが含まれますか？
たとえば、§3のp126 。エビングハウスの数理論理学におけるVIII構文解釈と正規形の定義による拡張は、次のように仮定します。$S$ （非論理）記号セットであり、
3.1定義。しましょう$\Phi$ のセットである $S$-文。
（a） $P \notin S$ は $n$-関係記号と $\phi_P(v_0, ... , v_{n-1})$ AN $S$-式。それから私達はそれを言う$$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $$ は $S$-の定義 $P$ に $\Phi$。
どちらと呼ぼうか $S$-の定義 $P$ に $\Phi$：
$ \forall v_0, .... \forall v_{n-1} (P v_0 ... n_{n-1} \leftrightarrow \phi_P(v_0, ... , v_{n-1})) $？
定義するのは循環的ですか $P$ それ自体の観点から？
です $𝑆$-の定義 $𝑃$ に $Φ$ シンボルの解釈 $P$ として $S'$-文？（の一部として構文解釈の$S'$ に $S'$ 自体？）
の外観です $P$ 独自の定義で $∀ 𝑣_0,....∀ 𝑣_{𝑛−1}(𝑃𝑣_0...v_{𝑛−1}↔𝜙_𝑃(𝑣_0,...,𝑣_{𝑛−1}))$、の外観と同じ意味で $A$ に $𝐴:=𝐵$？
$\phi_P(v_0, ... , v_{n-1})) $？（私はそれを推測します$P$ と定義されている $\phi_P(v_0, ... , v_{n-1})) $ に $\Phi$。）
$\phi_P$？（それを2番目と比較してください：$P$ それ自体は変数を含みません）
この定義がシンボルをどのように定義するかを参照してください$P$ シンボルセットの外側 $S$ として $S$-文？
ありがとう。
回答
署名があります $S$ そしてそれを拡張します $S':=S\cup\{P\}$。
ザ・ $S$-の定義 $P$ それは $S'$-式 $$\forall v_0\dots v_{n-1}: Pv_0\dots v_{n-1}\leftrightarrow \phi_P(v_0,\dots,v_{n-1})$$これは、与えられたものに対する追加の公理として正式に扱うことができます$S$-私たちが取り組んでいる理論、したがって同等のものを生み出す $S'$-理論、そのシンボル $P$式の略語として使用できます$\phi_P$。
たとえば、次の式は通常の順序関係の定義です。 $\le$ 言語における非負の整数の $(0,+)$： $$\forall x,y:\ x\le y\,\leftrightarrow\,\exists z: x+z=y$$
以下では、最初にプロセスをより直感的な方法で説明し、次に循環性に関する懸念に対処します。後者の点が実際にはもっと役立つのではないかと思うので、最初に2番目のセクションを読んでください。特に、そこで強調されているモットーは非常に役立つと思います。
（Re：あなたの最後のコメント、定義は $(1)$-すでに持っていて理解している古いシンボルの観点から、新しいシンボルがどのように動作するかを示すもの。）
ここでのキーワードは「定義による拡張」です。
直感的に、次のプロセスを念頭に置いています。
署名から始める $S$ といくつかのセット $\Phi$ の $S$-文章、私たちは非効率性に少し悩まされます：私たちが使用することについて話すことができるいくつかのことがあります$S$-数式ですが、回り道のみです。たとえば、集合論の言語について考えてみてください。$\{\in\}$：「$x$ のデカルト積です $y$ そして $z$「この言語では、しかし厄介な長い数式を介してのみです。（たとえば、クラトフスキペアを使用して、前の例を処理するのは良い練習です。）
だから私たちの本当に複雑な式を考えると $\varphi(x_0,...,x_{n-1})$、基本的には同じである新しい理論を作り上げたい $\Phi$ ただし、追加で「略語」があります。 $\varphi$。
まず、これは私たちが言語を拡大したいということを意味します。 $S$ 一緒に働きたい $S\cup\{R\}$ いくつかのための $n$-関係記号 $R\not\in S$ の略語として使用する予定です $\varphi$。
ここで、このより大きな言語で理論を定義する必要があります。この理論は、私たちがすでに持っているもの（つまり、$\Phi$）、の動作を正しく指示する必要があります $R$ （つまり、それはの略語だと言う $\varphi$）、他に何もするべきではありません。これは私たちに新しい理論を考えるように導きます$$\Phi':=\Phi\cup\{\forall x_0,...,x_{n-1}(R(x_0,...,x_{n-1})\leftrightarrow \varphi(x_0,...,x_{n-1})\}.$$
からの通路 $S,\Phi$、および $\varphi$ に $S\cup\{R\}$ そして $\Phi'$で定義することによって拡張。ここには深刻な冗長性があります。正確には、$\Phi'$ 本当に良いです $\Phi$。（正式には、$\Phi'$の保守的な拡張です$\Phi$ 可能な限り強い意味で：のすべてのモデル $\Phi$ のモデルへの拡張が1つだけあります $\Phi'$。）これは驚くべきことではありません。我々はすでに知っていた私たちが経て気に事を表現できます$\varphi$、もっと早くできるようにしたかっただけです。
ちなみに、これは理論の自然な「最大効率」バージョンを示唆していることに注意してください。すべての数式に新しい記号を追加するだけです。これはMorleyizationと呼ばれ、場合によっては便利です（ただし、通常はばかげています）。
さて、あなたが心配している真円度はどうですか？
まず、「$R$「それ自体は単なる記号です。追加する新しい文は、実際には次の定義ではありません。 $R$、むしろの意味の定義 $R$、またはの動作を管理するルールを好む場合$R$。
さらに深刻なことに、FOLでは循環性が問題になることはありません。重要なアイデアは次のとおりです。これは、プログラミングからもたらされる可能性のある直感からの重要な逸脱であると思います。
一次文のセットは物を作成するのではなく、物を説明します。
具体的には、一次文のセット $\Phi$特定のクラスの構造を切り分けます。これは正確な説明です。たとえば、危険に見える可能性のあるセット$$\{\forall x(P(x)\leftrightarrow P(x))\}$$ そして $$\{\forall x(Q(x)\leftrightarrow \neg Q(x))\}$$完全に円がありません。それらはそれぞれ空虚（=すべての構造の保持）と矛盾（=構造の保持）ではありません。