算術におけるメタ数学

$ \mathscr L_\mathrm{A} \supseteq \mathscr L_\mathrm{OR}

メタ論理

対象論理：項・論理式で記述される

注意

また原始項をアリティ0の演算子として扱う

対象論理ではわかりやすさのために束縛変数を通常のように記号で書くが

以下の略記を用いる

自由代数

は以下を満たすとする

$ \mathrm{Op}^\bullet(x) \to (\exists! y)\mathrm{ar}^\bullet(x,y)

$ (\forall i < \mathrm{lh}(v))[\mathrm{Expr}^\bullet((v)_i)] \to \mathrm{Expr}^\bullet(\mathrm{appl}^\bullet(o,v))

$ \mathrm{appl}^\bullet(o,v, y) \coloneqq o \in \mathrm{Op}^\bullet \land v \in \mathrm{Seq}^\bullet \land \mathrm{ar}^\bullet(o) = \mathrm{lh}(v) \land y = \braket{o}^\frown v

$ (\forall o,v,y)[\mathrm{appl}^\bullet(o,v) = y \land (\forall i < \mathrm{lh}(v))[\mathrm{Expr}^\bullet((v)_i) \land \varphi((v)_i)] \to \varphi(y)] \to (\forall x)[\mathrm{Expr}^\bullet(x) \to \varphi(x)]

Proof.

$ \mathrm{Deriv}(w) \coloneqq \mathrm{Seq}(w) \land (\forall i < \mathrm{lh}(w))(\exists o,v < w)[\mathrm{appl}(o,v) = (w)_i \land (\forall j < \mathrm{ar}(o))[(v)_j \in \mathrm{rng}(w)]]

$ \mathrm{Expr}^\bullet(x) \coloneqq (\exists w)[\mathrm{Deriv}(w) \land x \in \mathrm{rng}(w)]]

$ \mathrm{Expr}^\bullet(x) \leftrightarrow (\exists y)[H(x) < y \to (\exists w < y)[\mathrm{Deriv}(w) \land x \in \mathrm{rng}(w)]]

$ \mathrm{Expr}^\bullet(x) \leftrightarrow (\forall y)[H(x) < y \to (\exists w < y)[\mathrm{Deriv}(w) \land x \in \mathrm{rng}(w)]]

$ H(x) \coloneqq x2^{\braket{x,x}} \ge \sum_{i < x} 2^{\braket{i,x}} = \braket{\underbrace{x,...,x}_{x}} \ge \braket{\scriptsize \text{$x$に登場しうるすべての部分項の列}}

帰納法

項・論理式

以下の略記を用いる

$ v^\bullet_x \equiv \mathrm{applTerm}^\bullet(v_x^\bullet, \braket{})

$ 0^\bullet \equiv \mathrm{applTerm}^\bullet(0^\bullet, \braket{})

$ 1^\bullet \equiv \mathrm{applTerm}^\bullet(1^\bullet, \braket{})

$ x +^\bullet y \equiv \mathrm{applTerm}^\bullet(+^\bullet, \braket{x,y})

$ x \cdot^\bullet y \equiv \mathrm{applTerm}^\bullet(\cdot^\bullet, \braket{x,y})

以下の略記を用いる

$ x =^\bullet y \equiv \braket{=^\bullet,x,y}

$ x <^\bullet y \equiv \braket{<^\bullet,x,y}

$ \top^\bullet \equiv \mathrm{applForm}^\bullet(\top^\bullet, \braket{})

$ \bot^\bullet \equiv \mathrm{applForm}^\bullet(\bot^\bullet, \braket{})

$ x \land^\bullet y \equiv \mathrm{applForm}^\bullet(\land^\bullet, \braket{x,y})

$ x \lor^\bullet y \equiv \mathrm{applForm}^\bullet(\lor^\bullet, \braket{x,y})

$ \forall^\bullet x \equiv \mathrm{applForm}^\bullet(\forall^\bullet, \braket{x})

$ \exists^\bullet x \equiv \mathrm{applForm}^\bullet(\exists^\bullet, \braket{x})

$ (0)^\bullet \coloneqq 0^\bullet

$ (1)^\bullet \coloneqq 1^\bullet

$ (t + u)^\bullet \coloneqq t^\bullet +^\bullet u^\bullet

$ (t \cdot u)^\bullet \coloneqq t^\bullet \cdot^\bullet u^\bullet

$ (\top)^\bullet \coloneqq \top^\bullet

$ (\bot)^\bullet \coloneqq \bot^\bullet

$ (\varphi \land \psi)^\bullet \coloneqq \varphi^\bullet \land \psi^\bullet

$ (\varphi \lor \psi)^\bullet \coloneqq \varphi^\bullet \lor \psi^\bullet

$ (\forall\varphi)^\bullet \coloneqq \forall^\bullet \varphi^\bullet

$ (\exists\varphi)^\bullet \coloneqq \exists^\bullet \varphi^\bullet

$ \mathrm{val}^\bullet(v^\bullet_x,z) = {(z)_x}

$ \mathrm{val}^\bullet(0^\bullet,z) = 0

$ \mathrm{val}^\bullet(1^\bullet,z) = 1

$ \mathrm{val}^\bullet(x +^\bullet y,z) = \mathrm{val}^\bullet(x,z) + \mathrm{val}^\bullet(y,z)

$ \mathrm{val}^\bullet(x \cdot^\bullet y,z) = \mathrm{val}^\bullet(x,z) \cdot \mathrm{val}^\bullet(y,z)

Proof.

定理

$ T \vdash (\forall \vec x, z)\left[\mathrm{Seq}(z) \land \mathrm{lh}(z) = \overline n \land \left(\bigwedge_{i < \overline n}z(i) = x_i \right) \to t = \mathrm{val}^\bullet(t^\bullet, z)\right]

Proof.

$ \mathrm{PSat}_0(q,p,r) \coloneqq

$ \text{$q$ is a mapping from $(\le p) \times (\le r)$ to $\{0,1\}$}

$ {}\land (\forall z \le p)(\forall e \le r)(\forall u,v \le z)

$ [z = \top^\bullet \to q(z, e) = 1 \\

$ {} \land z = \bot^\bullet \to q(z, e) = 0

$ {} \land z = u \land^\bullet v \to [q(z, e) = 1 \leftrightarrow q(u,e) = 1 \land q(v,e) = 1]

$ {} \land z = u \lor^\bullet v \to [q(z, e) = 1 \leftrightarrow q(u,e) = 1 \lor q(v,e) = 1] \\

$ {} \land z = (\forall^\bullet <^\bullet w)[u] \to [q(z, e) = 1 \leftrightarrow (\forall x < \mathrm{val}^\bullet(w,e))[q(u,\braket{x}^\frown e) = 1]]

$ {} \land z = (\exists^\bullet <^\bullet w)[u] \to [q(z, e) = 1 \leftrightarrow (\exists x < \mathrm{val}^\bullet(w,e))[q(u,\braket{x}^\frown e) = 1]]]]

$ \mathrm{Sat}_0(z, e) \coloneqq (\exists q,p,r)[\mathrm{PSat_0}(q,p,r) \land q(z, e) = 1]

定理

$ T \vdash (\forall p, r)(\exists q)[\mathrm{PSat}_0(q,p,r)]

$ T \vdash (\forall q_1,p_1,r_1, q_2,p_2,r_2)[\mathrm{PSat}_0(q_1,p_1,r_1) \land \mathrm{PSat}_0(q_2,p_2,r_2) \to (\forall z \le p_1 \sqcap p_2)(\forall e \le r_1 \sqcap r_2)[q_1(z,e) = q_2(z,e)]]

Proof.

定理

注意

論理式

を以下を満たすように定義する

$ \Pi^\bullet_0(u) \leftrightarrow \Sigma^\bullet_0(u)

$ \Pi^\bullet_{x+1}(z) \leftrightarrow (\exists u \le z)[z = \forall^\bullet u \land \Pi^\bullet_x(u)]

$ \Sigma^\bullet_{x+1}(z) \leftrightarrow (\exists u \le z)[z = \exists^\bullet u \land \Sigma^\bullet_x(u)]

定理

$ \mathrm{Sat}_{\Sigma,0}(z,e), \mathrm{Sat}_{\Pi,0}(z,e) \coloneqq \mathrm{Sat}_0(z,e)

$ \mathrm{Sat}_{\Pi,n+1}(z,e) \coloneqq \Pi^\bullet_{n+1}(z) \land(\forall x_n)(\exists u)[z = \forall^\bullet u \land \mathrm{Sat}_{\Sigma,n}(u,\braket{x_n}^\frown e)]

$ \mathrm{Sat}_{\Sigma,n+1}(z,e) \coloneqq \Sigma^\bullet_{n+1}(z) \land(\exists x_n)(\forall u)[z = \exists^\bullet u \to \mathrm{Sat}_{\Pi,n}(u,\braket{x_n}^\frown e)]

補題