###### tags: `数学` `基礎論`
# 数理論理学
## Russelのパラドックス
$R= \{ x|x \notin x \}$ について $R \in \{ x|x \notin x \}$ 、 $R \notin \{ x|x \notin x \}$ となり矛盾. このパラドックスを解消するには

1. 全体集合を定める
2. 公理的集合論に従う
3. 型理論に従う

などの手段が考えられる.
## 形式系
形式系 $Q$ を例にとる.

1. **記号** $0$ 、 $s$ 、 $=$ 、 $\lor$ 、 $\forall$ 、 $\perp$
2. **公理** $0=0$ 、 $sn=sn$
3. **推論規則** $x \lor y \rightarrow x$ 、 $x \lor y \rightarrow y$ 、 $x, y \rightarrow x \lor y$

を合わせて**形式系**という. 公理は、0個の前提から結論を導ける推論規則とみなせる.

#### 推論規則の例(導入規則 $i$、除去規則 $e$)
- $t=t$
- $([A] \rightarrow .. \rightarrow B) \rightarrow A \Rightarrow B$
- $[A]$は仮定を**閉じる**という. 以降Aを仮定とみなさない.
- **Modus Ponens** $(A \Rightarrow B, A) \rightarrow B$

#### [原子再帰法](https://hackmd.io/jEzSfpEdSp-YZE1nQjhndA?both#%E5%86%8D%E5%B8%B0%E3%81%A8%E8%A1%A8%E7%8F%BE%E5%AE%9A%E7%90%86)による $+$ と $*$ の定義
- $t+\underline{0}=t$
- $t+\underline{S(u)}=S(t+u)$
- $t*\underline{0}=0$
- $t*\underline{S(u)}=t*u+t$
### 束縛と自由
量化子 $\forall,\exists$ の対象になっている変数を**束縛変数**、そうでないものを**自由変数**という.
すべての束縛変数について

1. 限界 $<$ が定められている式を**有界式**という. 停止する.
2. 量化子が $\exists$ の式を **$\Sigma _1$ 式**という. 真のとき停止する.
3. 量化子が $\forall$ の式を **$\Pi _1$ 式**という. 偽のとき停止する.
- [停止する](https://hackmd.io/DkSR1zk3T6CoCZBRaq66NA#%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C)
- [**$\Sigma _n$ 式** と **$\Pi _n$ 式**](#Sigma-_n-%E5%BC%8F-%E3%81%A8-Pi-_n-%E5%BC%8F)

$A$ が $\Sigma _1$ 式のとき $\lnot A$ は $\Pi _1$ 式. これを**De=Morgan則**という.

### 関数と述語
$f:A \to B$ について $A,B$ が数の集合のとき**関数**、 $A$ が 数 $B$ が真偽値の集合のとき**述語**、 $B$ が真偽値の集合のとき**式**という. 自由変数 $x$ を持つとき $f(x)$ と表す. 自由変数がない述語を**命題**、式を**文**という. 述語1つ( $=$ )からなる式を**原始式**という.
### Peano算術
1. $0 \in \mathbb{N}$
2. $\forall n \in \mathbb{N}(sn \in \mathbb{N})$
3. $\forall n \in \mathbb{N}(sn \neq 0)$
4. $\forall m,n \in \mathbb{N}(sm=sn \Rightarrow m=n)$
5. $f(0) \land \forall n \in \mathbb{N}(f(n) \Rightarrow f(sn)) \Rightarrow \forall n \in \mathbb{N}(f(n))$

を公理とする形式系を**Peano算術**という. 公理1を認めないとき1-5の $0$ を $1$ で置き換えたものを用いる場合がある.

3. $S(t)=0 \rightarrow \perp$, $x \ne 0 \rightarrow \exists y(x=S(y))$
4. $S(t)=S(u) \rightarrow t=u$

### 述語論理と拡大
形式系から数論の記号、公理、推論規則を除いたものを**述語論理**という.
形式系 $Y$ について $\forall L(X \vdash L \Rightarrow Y \vdash L)$ を満たすとき $X$ の**拡大** $\forall L(X \vdash L \Leftrightarrow Y \vdash L)$ を満たすとき $X$ の **保存拡大**という. $Y$ が $X$ の保存拡大のとき $Y$ と $X$ の述語論理は一致する
### 濃度と連続体仮説
$|A|$ について有限のとき**個数**、そうでないとき**濃度**という. $A$ について $| \mathbb{N} |=|A|$ のとき**可算集合** 、 $| \mathbb{R} |=|A|$ のとき**連続体**という. $A$ のとき $\forall A(|A| \leqq | \mathbb{N} | \lor | \mathbb{R} | \leqq |A|)$ を満たす. これを**連続体仮説**という. 連続体仮説とZFC集合論と独立である.
### Cantorの対角線論法
濃度を調べるために**対角線論法**を用いる場合がある. 以下 $\mathbb{R}$ が可算集合でないことを示す例.
> $\mathbb{R}$が加算集合と仮定すると $n \in \mathbb{N}$ を添字に用いて元の列 $\{ A_n \}$ を考えることができる. $a_n$ を $A_n$ をbinary表示したときの $n$ 桁目の値、 $b_n$ を $a_n$ のbit反転とする.
> このとき $\forall n(a_n \neq b_n) \cdots 1^ \circ$
> $b_n$ を $B$ をbinary表示したときの $n$ 桁目の値とみなすと $B \in \mathbb{R}$ より $\exists m \in \mathbb{N}(B=A_m)$ なので $a_m=b_m \cdots 2^ \circ$
> $1^ \circ$ と $2^ \circ$ は矛盾. よって背理法より $\mathbb{R}$ は可算集合でない $(Q.E.D)$
### 矛盾と完全
形式系 $F$ について $F \vdash A \land \lnot A$ のとき**矛盾**、 $F \vdash A \lor \lnot A$ のとき**完全**という. **Hilbert計画**では無矛盾完全な形式系を考えた.
### 再帰と表現定理
$f(0),\forall n(f(n) \Rightarrow f(sn)) \backslash \forall n(f(n))$ を**数学的帰納法**という. 形式系 $Q$ の推論規則に数学的帰納法を加えた拡張は $\Sigma _1$ 式について完全である.
$a$ が定数のとき $f(0)=a \land f(sx)=g(f(x))$ による定義を $f: \mathbb{N} \to A$ を**原子再帰法**という. 原子再帰法の繰り返しによる定義を**原子再帰的である**という.
形式系 $F$ の原始再帰的述語 $R$ について $R(a,b, \cdots) \Rightarrow F \vdash r(\overline{m},\overline{n})$ 、 $\lnot R(a,b, \cdots) \Rightarrow F \vdash \lnot r(\overline{m},\overline{n})$ を満たす. これを**表現定理**という.
### Gödel数と対角化
$S$ を形式系に含まれる記号の集合とする. このとき全単射 $f:S^n \to \mathbb{N}$について $f((A_0, \cdots ,A_n))$ を長さ $n$ の記号列 $\{ A_n \}$ の**Gödel数**という. 全単射 $g:S \to \mathbb{N}$ を定め $g(A_n)$ を $n$ 番目の素数の指数とみなした素因数分解が表す自然数を $f$ として用いる場合がある.
記号列 $l$ のGödel数を $\overline{l}$ と表すとき $l( \overline{l} )$ を $l(x)$ の**対角化**という.以下は自己言及を導く例である.
> 形式系 $F$ について $y(x) \equiv F \not \vdash x(\overline{x})$ の対角化 $z$ は $y(\overline{y}) \equiv F \not \vdash y(\overline{y})$ より $F \not \vdash z$
### Gödelの不完全性定理
無矛盾なPeano算術の拡大 $F$ について

1. $F$ は不完全
2. $A$ は無矛盾、を表す論理式 $A$ について $F \not \vdash A$

を**Gödelの不完全性定理**という.

---
### 真理述語の定義可能性
$A$ を文とすると
- $\forall A (\mathbb{N} \vDash A \Leftrightarrow \mathbb{N} \vDash true(\overline{A}))$

を満たす $true$ は存在しない. しかし有限の $n>0$ において $A$ を $\Sigma _n$ 文とすると
- $\forall A (\mathbb{N} \vDash A \Leftrightarrow \mathbb{N} \vDash true(\overline{A}))$

を満たす $\Sigma _n$ 論理式 $true$ は存在する.
### 包括原理 $CA$
- $\exists X \forall x(x \in X \Leftrightarrow A(x))$
## 不動点
$f:X \rightarrow X$ について $f(x_0)=x_0$ となる $x_0 \in X$ を**不動点**という.
### Brouwerの不動点定理
$X$ を任意の $n$ 次元閉球体、$f:X \rightarrow X$ を連続関数とすると、$f$ は不動点を持つ.
## 型理論
### **$\Sigma _n$ 式** と **$\Pi _n$ 式**
###