Computer Mathematician
『コンピュータは数学者になれるのか？』 照井一成
# 数学者をつくろう
## Basics
### symbols
numeric symbols
- $ = $ (eqauls)
- $ 0 $ (zero)
- $ S $ (successor)
- $ + $ (plus)
- $ \cdot $ (multiplier)
logical symbols
- $ \land $ (logical and)
- $ \lor $ (logical or)
- $ \to $ (so)
- $ \bot $ (inconsequence)
- $ \forall $ (forall)
- $ \exists $ (exists)
### term
- $ x,y,z, ... $ : numeric term
- $ A,B,C, ... $ : propositional term
### derivatively defined symbols
- $ \lnot A $ := $ \lnot A \iff A \to \bot $
- $ x \neq y $ := $ (x = y) \to \bot $
- $ A \leftrightarrow B $ := $ (A \to B) \land (B \to A) $
- $ x \le y $ := $ \exists s . (s + x = y) $
### derivatively defined propositions
- $ \forall x \le y . A(x) $ := $ \forall x . (x \le y \to A(x)) $
- $ \exists x \le y . A(x) $ := $ \exists x . (x \le y \land A(x)) $
- $ div(x,y) $ := $ \exists z \le y . ( x \cdot z = y ) $
- $ even(x) $ := $ div(2,x) $
- $ prime(x) $ := $ 2 \le x \land \forall z \le x. (div(z,x) \to (z = 1 \lor z = x)) $
### variables
$$ \forall x . \exists y . x = S(y) + z $$
- bounded variables : $ x $ , $ y $
- free variable(s) : $ z $
### models
$$ \mathbb{N} \models A $$
- we read this " $ A $ is True "
- $ \mathbb{N} $ is called "標準モデル"
### Bounded Logical Expression
BLE : Bounded Logical Expression (有界論理式) ;
expression composed of
- $ \land $
- $ \lor $
- $ \to $
- $ \forall x \le t . $
- $ \exists x \le t . $
BLS : Bounded Statemente (有界文);
BLE which contains NO free variable
#### NOTE
( BLS is true or not ) is computationally proved
## 論理式
### $ \sum _ 1 $ 論理式 , $ \prod _ 1 $ 論理式
$ \sum _ 1 $ logical expr
- $ \exists x . \exists y .\ ...\ . A $
$ \prod _ 1 $ logical expr
- $ \forall x . \forall y .\ ...\ . A $
### more
e.g.
- $ \exists x . \forall y . \forall z . \exists w . A $
this is $ \sum _ 3 $ logical expr
- $ \forall x . \forall y . \exists z . \exists w . \forall v . \exists u . A $
this is $ \prod _ 4 $ logical expr
## prop 1.1
$ \exists P . $
$$ \mathbb{N} \models A \quad \Rightarrow \quad P(A) = yes $$
$$ \mathbb{N} \not\models A \quad \Rightarrow \quad P(A) = no $$
- $ P $ is a program judge the truth of a proposition
- $ A $ is bounded statement
## prop 1.2
$ \exists Q . $
$$ \mathbb{N} \models A \quad \iff \quad Q(A) = yes $$
- $ Q $ is a program which outputs `yes` iff A is True.
- $ A $ is BS
## De Morgan's law
$$ \mathbb{N} \models \forall x . A(X) \leftrightarrow \exists x . \lnot A(x) $$
$$ \mathbb{N} \models \exists x . A(X) \leftrightarrow \forall x . \lnot A(x) $$
## 推論規則
# 一階算術
## prop 1.3
def mathematician $ \mathbf{Q} $
$ A \in \sum _ 1 \Rightarrow $
$$ \mathbb{N} \models A \iff \mathbf{Q} \vdash A $$
- $ \mathbf{Q} $ は 小学生並みの数学者
# prop