京都大学理学部特色入試[3](2)

もう一問,解いてみました.

 設問の各条件は $f$ を $-f$ に変えても等価なので,${\rm lc}(f)>0$ としてよく,${f}({x})\to+\infty\ ({x\to+\infty})$,$f$ は連続なので $\exists x\in\mathbb{R} \left({{f}({x})\in\mathbb{Z}}\right)$ であり,設問の仮定により $\exists x\in\mathbb{R} \left({{g}({x})\in\mathbb{Z}}\right)$ となるから,${\rm deg}(g)>0$ として矛盾を導く.このとき,同様に ${\rm lc}(g)>0$ としてよく

【方法0】 ${\rm deg}(f)>{\rm deg}(g)$ ならば,区間 $({a,\ +\infty})$ において $f,\ g,\ f-g$ が狭義増加で,$f(c)=f(b)+1,\ g(b),\ g(c)\in \mathbb{Z},\ a<$ $b<$ $c$ となる $a,\ b,\ c$ があり
$$f(b)-g(b)\,{<}\,f(c)-g(c)$$ したがって $$1\le g(c)-g(b)\,{<}\, f(c)-f(b)=1$$ なので矛盾.

あるいは

 $f,\ g$ が狭義増加となる区間 $I=({a_0,\ +\infty})$ があり,$({{f}({a_i})\in\mathbb{Z}})_{i=1}^{\infty}$ が公差 $1$ の等差数列で,$a_i\to+\infty\ ({i\to\infty})$ となる狭義増加な $({a_i\in I})_{i=1}^{\infty}$ がある.よって

【方法1】 $({{g}({a_i})\in\mathbb{Z}})_{i=1}^{\infty}$ の階差はつねに $1$ 以上だから,$i=1,2,\ldots$ のとき
$${f}({a_i})-{f}({a_1})=i-1\le{g}({a_i})-{g}({a_1})$$
つまり
$${f}({a_i})-{g}({a_i})\le {f}({a_1})-{g}({a_1})$$
となるが,${\rm deg}\,f>{\rm deg}\,g$ ならば ${f}({a_i})-{g}({a_i})\to+\infty\ ({i\to\infty})$ なので矛盾.

【方法2】 $n>d={\rm deg}(g)$ として,$1\le x<$ $y$ のとき
$$
{g}({x})=\sum_{j=0}^{d}{ A_j x^j },\quad
{f}({x})=\sum_{j=0}^{n}{ B_j x^j },\quad
{G}({x,\ y})=\frac{{g}({x})-{g}({y})}{x^n-y^n},\quad
{F}({x,\ y})=\frac{{f}({x})-{f}({y})}{x^n-y^n}-B_n
$$
とおくと,(1) により
$$|{{G}({x,\ y})}|\le\sum_{j=0}^{d}{ |{A_j}|\cdot \left|{\frac{x^j-y^j}{x^n-y^n}} \right| }{<}\frac{1}{x} \sum_{j=0}^{d}{ |{A_j}| },\quad |{{F}({x,\ y})}|\le\sum_{j=0}^{n-1}{ |{B_j}|\cdot \left|{\frac{x^j-y^j}{x^n-y^n}}\right| }{<}\frac{1}{x} \sum_{j=0}^{n-1}{ |{B_j}| }$$
なので,$i\to\infty$ のとき,${G}({a_i,\ a_{i+1}}),\ {F}({a_i,\ a_{i+1}})\to0$,したがって
\begin{equation*}
1\le\left|{{g}({a_i})-{g}({a_{i+1}})}\right|
=\left|{\frac{{g}({a_i})-{g}({a_{i+1}})}{{f}({a_i})-{f}({a_{i+1}})}}\right|
=\left|{\frac{ {G}({a_i,\ a_{i+1}}) }{ {F}({a_i,\ a_{i+1}})+B_n }}\right|
\to\left|{\frac{0}{B_n}}\right|=0
\end{equation*}
となり矛盾.


京都大学理学部特色入試[4]

ちょっとした経緯があり,解いてみました.

 $O$ を原点とする $xyz$ 空間内の任意の点 $X=(x,\ y,\ z)$ に対して,$X'=(0,\ y,\ z)$ とし,$X$ と $x$ 軸との距離を ${d}({X})$ で表すと,${d}({X})=\sqrt{y^2+z^2}=\left|\overrightarrow{OX'}\right|$ だから,$4$ 点 $V_i\ (i=1,2,3,4)$ と和が $1$ である非負の $4$ 数 $t_i\ (i=1,2,3,4)$ に対して,$T_1=\sum_{i=1}^{4}{ t_i V_i }$ とおくと

$${d}({T_1})=\left|\sum_{i=1}^{4}{ t_i \overrightarrow{O{V_i}'} }\right| \le \sum_{i=1}^{4}{ t_i \left|{\overrightarrow{O{V_i}'}}\right| }
=\sum_{i=1}^{4}{ t_i {d}({V_i}) }\le\max\{{d}({V_i}):i=1,2,3,4\}$$

さらに,$x$ 軸上の $2$ 点 $T_2,\ T_3$ に対して,$3$ 角形 $XT_2T_3$ の面積を ${m}({X})$ で表すと,${m}({X})=\left|{\overrightarrow{T_2T_3}}\right|\times{d}({X})/2$ だから

$${m}({T_1})\le\max\{{m}({V_i}):i=1,2,3,4\}$$

したがって,設問の $\mathrm{P,\ Q,\ R}$ を逐次 $T_1$ とし,この不等式の右辺を与える $4$ 面体 $\mathrm{ABCD}$ の頂点に移せば,面積が減少しない $3$ 角形の列が得られ,$4$ 面体 $\mathrm{ABCD}$ の面に至る.


√素数が有理数でないこと(その3)

同じ内容をどこかに書いた気もするのですが,等号の話が出た流れで.かなり以前の「√素数有理数でないこと」http://ehito.hatenablog.com/entry/20130419/1366333894 の続編です.

定数記号c,2項関数記号f,gをもつ言語に,前回のように等号の公理を導入して,理論

{∀x(fcx=x),∀x(gxx=x),∀x∀y∀z(g(fxy)z=c \leftrightarrow gxz=c∧gyz=c)}

をTとおくと,domain が自然数全体,c,f,gの解釈がそれぞれ1,乗算,最大公約数を与える関数である任意の構造Mは,Tのモデルですが,論理式

∀p(p≠c∧∀x∀y(fxy=p→x=c∨y=c)→ ¬(∃x∃y(gxy=c∧fxx=f(fyy)p)))

は,Tから証明可能なので,(健全性により)Mにおいて valid です.

# (UNDISCH_ALL o SPEC_ALL) (METIS [] 
`!f g:a->a->a. (!x. f c x = x) ==> (!x. g x x = x) 
==> (!x y z. g (f x y) z = z <=> g x z = c /\ g y z = c) 
==> (!p. ~(p = c) /\ (!x y. f x y = p ==> x = c \/ y = c) ==> ~(?x y. g x y = c /\ f x x = f (f y y) p))`
);;
val it : thm = !x y z. g (f x y) z = z <=> g x z = c /\ g y z = c,
  !x. f c x = x, !x. g x x = x
  |- !p. ~(p = c) /\ (!x y. f x y = p ==> x = c \/ y = c)
         ==> ~(?x y. g x y = c /\ f x x = f (f y y) p)

数理論理4:等号

今回は
・等号の公理

・理論と構造の濃度との関係
について述べます.

以下,2項述語記号=を等号と呼び,これを元にもつ言語を固定,t1,t2がその項ならば
 =(t1,t2)をt1=t2
 ¬(=(t1,t2))をt1≠t2
とそれぞれ略記します.

まず,等号の公理を導入します.

(定義4-1)適当な変数記号xによって
  ∀x(x=x)
或いは,t,t’がAのxに代入可能である(つまり,新たな束縛が生じない)適当な項t,t’,変数記号x,論理式Aによって
  t=t’→(A [ t / x ] A [ t' / x ] )の全称閉包
と表せる論理式を等号の公理と呼びます.

ここで,A[t/x]A[t'/x] はA内のxの全ての自由出現をぞれぞれt,t’に置き換えたものです.

また,次のような流儀もあります.

(定義4-2)適当な変数記号x,y,zによって
  ∀x(x=x)
  ∀x∀y(x=y→y=x)
  ∀x∀y∀z(x=y→(y=z→x=z))
或いは,適当なn(>0)項関数記号f,適当な項t1,...,tn,t1’,...,tn’によって
  t1=t1’∧...∧tn=tn’→f(t1,...,tn)=f(t1’,...,tn’)の全称閉包
或いは,適当なn(>0)項述語記号p,適当な項t1,...,tn,t1’,...,tn’によって
  t1=t1’∧...∧tn=tn’→(p(t1,...,tn)→p(t1’,...,tn’))の全称閉包
と表せる論理式を等号の公理と呼びます.

このとき

・ (定義4-2)の各公理は(定義4-1)の公理全体の集合から証明可能
・ (定義4-1)の各公理は(定義4-2)の公理全体の集合から証明可能

であり,(定義2-1)に

 とくに
 I(=)はD上の相等関係,つまり,任意の(a,b)∈D^2に対して,a=b(この=はD上の等号)ならば1,そうでないならば0となる写像

を追加すると

・ (定義4-1),(定義4-2)の各公理は valid

です.

以下,(定義2-1)に上記を,(定義3-1)に

Kが(定義4-1)の等号の公理ならば
0.{}\longrightarrow{K}

をそれぞれ追加し,理論と構造の濃度との関係を見て行きます.

まず
  ∀x∀y(x=y) ⇔ ∃x∀y(x=y)
であり,2つの理論{∀x∀y(x=y)},{∃x∀y(x=y)}はどちらも濃度が1の任意の構造のみをモデルにもちます(domain が空である構造を許す流儀では,∀から始まる任意の論理式はその構造において valid なので,前者は濃度が2より小の任意の構造のみをモデルにもちます).

同様に,2つの理論
  {∃x1∃x2(x1≠x2)∧∀x1∀x2∀x3(x1=x2∨x1=x3∨x2=x3))}
  {∃x1∃x2(x1≠x2∧∀y(x1=y∨x2=y))}
はどちらも濃度が2の任意の構造のみをモデルにもちます.

そして,2以上の任意の整数nに対して,φnを
  ∀x1...∀xn(1≦i<j≦nを満たす各整数の対(i,j)に対するxi=xjを∨で結んだもの)
とおくと,それぞれ
  {φn}は濃度がnより小
  {¬φn} は濃度がn以上
  {¬φn,φ(n+1)} は濃度がn
の任意の構造のみをモデルにもちます.

このように任意の正の整数nに対して,理論Tnが存在して
  任意の構造Sに対して,Sの濃度がnとS|=Tnとは等価
ですが
  任意の構造Sに対して,Sの濃度が有限とS|=Tとは等価
となる理論Tは存在しません(そのようなTがあるとT’=T∪{¬φj:j≧2}の任意の有限部分集合がモデルをもつのでコンパクト性定理( https://en.wikipedia.org/wiki/Compactness_theorem )によりT’もモデルをもちますが、その濃度は有限かつ無限となり不合理です).

これと双対的に,無限濃度については,上記のφにより
  任意の構造Sに対して,Sの濃度が無限とS|={¬φj:j≧2}とは等価
ですが,任意の無限濃度mに対して,濃度mの任意の構造のみをモデルにもつ理論は存在しません(無限濃度の任意の構造M,Mをモデルにもつ任意の理論T,言語の濃度以上の任意の濃度kに対して,Tは濃度kの(Mと初等的同値な)モデルをもつことが,レーベンハイム-スコーレムの定理( https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem )として知られています).

最近の話題から

HOList with HOL Light
https://sites.google.com/view/holist/home

TacticToe with HOL4
https://www.thibaultgauthier.fr/tactictoe.html

さらに
http://aitp-conference.org/2019/
http://arg.ciirc.cvut.cz/teaching/mlr19/index.html
http://ai4reason.org/demos.html

CoqGym with Coq
https://github.com/princeton-vl/CoqGym

MetaGen with MetaMath
https://openreview.net/pdf?id=BJxiqxSYPB


PVS は...
https://github.com/nasa/vscode-pvs

数理論理3:構文論

今回は
・言語に対して,その言語の定理式の全体が定まること
をLKと呼ばれる流儀で述べます.

以下,言語,その言語の論理式の集合Σを任意に固定します.

(定義3-1)論理式の任意の集合の対(Ψ,Ω)をシーケントと呼び,Σから導出可能なシーケントの全体は,次の1.から16.(3.から16.を推論規則と呼びます)を満たす最小の集合です.以下,この集合に(Ψ,Ω)が属することを Ψ \longrightarrow Ω で表します.

xが変数記号,tが項,A,Bが論理式,CがΣの元,X,Yが論理式の(空でもよい)有限列ならば

1.{}\longrightarrow{C}
2.{A}\longrightarrow{A}

3.{X}\longrightarrow{Y}ならば{X}\longrightarrow{A,Y}かつ{A,X}\longrightarrow{Y}
4.{X}\longrightarrow{A,Y}かつ{A,X}\longrightarrow{Y}ならば{X}\longrightarrow{Y}

5.{A,X}\longrightarrow{Y}ならば{X}\longrightarrow{¬A,Y}
6.{X}\longrightarrow{A,Y}ならば{¬A,X}\longrightarrow{Y}

7.{A,B,X}\longrightarrow{Y}ならば{A∧B,X}\longrightarrow{Y}
8.{X}\longrightarrow{A,Y}かつ{X}\longrightarrow{B,Y}ならば{X}\longrightarrow{A∧B,Y}

9.{X}\longrightarrow{A,B,Y}ならば{X}\longrightarrow{A∨B,Y}
10.{A,X}\longrightarrow{Y}かつ{B,X}\longrightarrow{Y}ならば{A∨B,X}\longrightarrow{Y}

11.{A,X}\longrightarrow{B,Y}ならば{X}\longrightarrow{A→B,Y}
12.{X}\longrightarrow{A,Y}かつ{B,X}\longrightarrow{Y}ならば{A→B,X}\longrightarrow{Y}

13.{X}\longrightarrow{A,Y}ならば{X}\longrightarrow{∀xA,Y}
  ただし,X,Yの各論理式にxの自由出現はないとします(これを固有変数条件と呼びます).
14.{A内のxの全ての自由出現をtに置き換えたもの,X}\longrightarrow{Y}ならば{∀xA,X}\longrightarrow{Y}
  ただし,置き換えにより新たな束縛は生じないとします(これを代入可能条件と呼びます).

15.{A,X}\longrightarrow{Y}ならば{∃xA,X}\longrightarrow{Y}
  ただし,固有変数条件は満たされているとします.
16.{X}\longrightarrow{A内のxの全ての自由出現をtに置き換えたもの,Y}ならば{X}\longrightarrow{∃xA,Y}
  ただし,代入可能条件は満たされているとします.

なお,(定義3-1)も(定義1-2)のように「適当な・・・によって・・・と表せるもの」という表現も可能です.そして

・ {X}\longrightarrow{Y}を X \longrightarrow Y 或いは Σ \vdash\longrightarrow Y と書きます.また,とくに Σ \vdash \longrightarrow A を Σ \vdash A(Σが空集合ならば \vdash A)と書き,これを「AはΣの構文論的帰結」或いは「AはΣの定理式」或いは「AはΣから証明可能」(Σ が空集合ならば「Aは定理式」或いは「Aは証明可能」)と読みます.
・ (定義3-1)の集合は帰納的に定義されているので,1.または2.から{X}\longrightarrow{Y}に至る過程に現れるΣの元は有限個です.従って,Σ \vdash\longrightarrow Yならば,Σの有限部分集合Σ’が存在して Σ’ \vdash\longrightarrow Y となります.
・ 固有変数条件を満たさない代入を許すと,例えば,xが変数記号,pが1項述語記号ならば,px→∀xpx が定理式になってしまいます.
・ 代入可能条件を満たさない代入を許すと,例えば,xが変数記号,pが1項述語記号ならば,∀xpxx→∃x∀ypxy が定理式になってしまいます.

(例3-1)x,yが異なる変数記号,pが1項述語記号ならば
 \longrightarrow(¬(∀xpx))→∃x(¬px)
となるには,11. により
 ¬(∀xpx)\longrightarrow∃x(¬px)
となればよく,それには,6. により
 \longrightarrow∀xpx,∃x(¬px)
となればよく,それには,13. により
 \longrightarrowpy,∃x(¬px)
となればよく,それには,16. により
 \longrightarrowpy,¬py
となればよく,それには,5. により
 py\longrightarrowpy
となればよく,2. により,(¬(∀xpx))→∃x(¬px)は定理式です.

(例3-2 https://en.wikipedia.org/wiki/Drinker_paradox )シーケントは集合の対なので,その集合の要素を複製することが可能です.したがって,x,yが異なる変数記号,pが1項述語記号ならば
 \longrightarrow∃x(px→∀xpx)
となるには
 \longrightarrow∃x(px→∀xpx),∃x(px→∀xpx)
となればよく,それには
 \longrightarrowpx→∀xpx,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrow∀xpx,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrowpy,∃x(px→∀xpx)
となればよく,それには
 px\longrightarrowpy,py→∀xpx
となればよく,それには
 px,py\longrightarrowpy,∀xpx
となればよく,それには
 py\longrightarrowpy,∀xpx
となればよく,それには
 py\longrightarrowpy
となればよいので,∃x(px→∀xpx)は定理式です.

こうした手続きを上下を逆にして次のツールが生成するような図で表したものをその定理式の証明図と呼びます.http://bach.istc.kobe-u.ac.jp/seqprover/

(参考)
https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK

数理論理2:意味論

今回は
・言語,構造,割り当てに対して,その言語の項,論理式の値が定まること
そして
・言語に対して,その言語の valid な論理式の全体が定まること
を述べます.

以下,言語を固定します.

(定義2-1)構造は空でない集合D(domainと呼びます)と次のような写像I(解釈と呼びます)の対です.
 fがn項関数記号ならば
  n>0ならば,I(f)はD^nからDへの写像
  n=0ならば,I(f)∈D
 pがn項述語記号ならば
  n>0ならば,I(p)はD^nから{0,1}への写像
  n=0ならば,I(p)∈{0,1}
また,Dの濃度#Dを構造の濃度と呼びます.

なお,構造のことを解釈,或いは,モデルと呼ぶ流儀もあります.

次に,構造(D,I)を固定します.

(定義2-2)割り当てsは変数記号全体からDへの写像です.x,y,...が変数記号,d,e,...∈Dならば,sのx,y,...の像をそれぞれd,e,...に改めた割り当てをs[x→d,y→e,...]で表します.

(定義2-3)付値は(関数,述語,論理記号の出現の個数に関する帰納法により定義される)次のような写像||です.
 sが割り当て,xが変数記号ならば,|x|=s(x)
 gがn項関数または述語記号,t1,...,tnが項ならば
  n>0ならば,|g(t1,...,tn)|=I(g)(|t1|,...,|tn|)
  n=0ならば,|g|=I(g)
 A,Bが論理式ならば
  |¬A|=1-|A|
  |A∧B|=|A|×|B|
  |A∨B|=1-(1-|A|)×(1-|B|)
  |A→B|=1-|A|×(1-|B|)
 sが割り当て,xが変数記号,Aが論理式ならば
  |∀xA|={s[x→d]に対して定義された||による|A|:d∈D}の元の積
  |∃xA|={s[x→d]に対して定義された||による|A|:d∈D}の元の和

この定義において,付値による各元の像を元の値と呼びます.各項の値はDに属し,各論理式の値は{0,1}に属します.また,各割り当てに対して,付値は項と論理式全体の集合からD∪{0,1}への準同型写像になっています.

以下,言語のみを固定します.

(例2-1)A,Bが論理式ならば,任意のS,sに対して
  |((A→B)→A)→A|
 =1-|(A→B)→A|×(1-|A|)
 =1-(1-|A→B|×(1-|A|))×(1-|A|)
 =1-(1-(1-|A|×(1-|B|))×(1-|A|))×(1-|A|)
であり,|A|∈{0,1}により,この値は1です.

(例2-2)xが変数記号,Aが論理式ならば,任意のS,sに対して
  |¬(∀xA)|
 =1-|∀xA|
 =1-({s[x→d]に対して定義された||による|A|:d∈D}の元の積)
 ={1-(s[x→d]に対して定義された||による|A|):d∈D}の元の和
 ={s[x→d]に対して定義された||による|¬A|:d∈D}の元の和
 =|∃x(¬A)|
となります.

(定義2-4)Sが構造,sが割り当て,||が付値,A,Bが論理式,Σが論理式の(有限とは限らない)集合ならば
1.|A|=1を(S,s)|=Aと書き,「S,sはAを充足」と読み,そうしたS,sが存在するようなAを「充足可能」と呼びます.
2.任意のsに対して(S,s)|=AをS|=Aと書き,「AはSにおいてvalid」或いは「SはAのモデル」と読みます.
3.任意のBに対して,B∈ΣならばS|=BをS|=Σと書き,「SはΣのモデル」と読みます.
4.任意のSに対して,S|=ΣならばS|=AをΣ|=Aと書き,「AはΣの意味論的帰結」と読みます.
5.任意のS,sに対して,|A|=|B|をA≡Bと書き,「A,Bは同値」と読みます.

(定義2-4)において

・ Aが閉論理式ならば,|A|は割り当てによらないので,|A|=1はS|=Aであり(単に「SはAを充足」と読みます),Aが充足可能とAがモデルを持つは等価です.
・ Σが有限集合ならば
   {A1,...,An}|=AはA1,...,An|=A
   {}|=Aは|=A
のように{ }を略して書くことがあり
   |=Aを「Aは valid」と読みます.
   A|=Bは|=(A→B)と等価であり,これをA⇒Bと書きます.
   A|=BかつB|=Aは|=(A→B)∧(B→A)と等価であり,これをA⇔Bと書きます.
   A⇔BはA≡Bと等価です.
・  |=Aは,任意のS,sに対して,(S,s)|=Aつまり|A|=1つまり|¬A|=0と書けるので,入力されたAにおいて束縛されない全ての変数記号を定数記号とみなし,それがvalidであることを確かめよう,或いは,|¬A|=1となるS(これをAのカウンターモデルと呼びます)を見付けてvalidでないことを確かめようとする https://www.umsu.de/trees/ のようなツールがあります.
・ 論理式全体は,適当なS,sに充足される(充足可能といいます)論理式全体と,そうでない(充足不可能といいます)論理式全体に分割され,前者の部分集合として適当なSにおいて valid な論理式全体があり,さらにその部分集合として valid な論理式全体があります.

(例2-1)により
 |=((A→B)→A)→A つまり (A→B)→A|=A つまり (A→B)→A⇒A
(例2-2)により
 ¬(∀xA)≡∃x(¬A) つまり ¬(∀xA)⇔∃x(¬A)
となります.

なお,(定義2-4)において,より強く

4.任意のS,sに対して,「任意のBに対して,B∈Σならば(S,s)|=B」ならば(S,s)|=AをΣ|=Aと書き,「AはΣの意味論的帰結」と読みます.

とする流儀もあります.この場合,Σ∪{A}|=B ならば Σ|=A→B(意味論的な演繹定理 )がAが閉論理式でなくても成り立つ(つまり,pが1項述語記号,x,yが変数記号であっても{p x}|=p yとならない)など,構文論との対応が失われますが,閉論理式に限定するなら差異はありません.