√素数が有理数でないこと(その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とならない)など,構文論との対応が失われますが,閉論理式に限定するなら差異はありません.

nfsplitting(*,,2);

私が案出した Galois 群の計算方法を PARI の開発メンバーの方にお伝えしたところ,それに基づいた nfsplitting さらに galoisinit の改良版を作成してくださいました. 試用方法は
https://pari.math.u-bordeaux.fr/cgi-bin/gitweb.cgi?p=pari.git;a=tree;h=refs/heads/bill-nfsplitting;hb=refs/heads/bill-nfsplitting
の snapshot のリンクをクリック,保存,展開して

./Configure;make all;./gp

で,PARI が起動します.以下,実行例です.

? #
   timer = 1 (on)
? galoisinit(nfsplitting(x^17-2)); \\ 従来の方法
  *** galoisinit: Warning: increasing stack size to 16000000.
  *** galoisinit: Warning: increasing stack size to 32000000.
  *** galoisinit: Warning: increasing stack size to 64000000.
time = 1h, 3min, 8,876 ms.
? galoissplittinginit(x^17-2); \\ 新作
  *** galoissplittinginit: Warning: increasing stack size to 16000000.
  *** galoissplittinginit: Warning: increasing stack size to 32000000.
  *** galoissplittinginit: Warning: increasing stack size to 64000000.
time = 20,935 ms.
? g=nfsplitting(f=x^17-2);nfisincl(f,g); \\ 従来の方法
  *** nfisincl: Warning: increasing stack size to 16000000.
  *** nfisincl: Warning: increasing stack size to 32000000.
time = 20,210 ms.
? nfsplitting(x^17-2,,1); \\ 処理の共通部分をまとめたもの.出力は分解体の定義多項式と入力の全ての根の分解体上での表示です.
  *** nfsplitting: Warning: increasing stack size to 16000000.
  *** nfsplitting: Warning: increasing stack size to 32000000.
time = 16,544 ms.
? nfsplitting(x^17-2,,2); \\ 出力は分解体の定義多項式とその Galois 群の写像表示です.
  *** nfsplitting: Warning: increasing stack size to 16000000.
  *** nfsplitting: Warning: increasing stack size to 32000000.
time = 16,846 ms.

数理論理1:言語

ちょっとした経緯があり,数理論理(古典一階論理)の基本事項を少し書きます.

今回は
・言語に対して,その言語の項,論理式の全体が定まること
を述べます.

(定義1-1)言語は,次のような互いに区別できる記号の集合です.
 n項関数記号 (各nは非負整数)
 n項述語記号 (1個以上,各nは非負整数)
 変数記号 x1 x2  … (可算個)
 論理記号 ¬ ∨ ∧ → (結合子とも呼びます) ∀ ∃ (量化子とも呼びます)
 補助記号 ( , )

ここで,関数記号,述語記号は言語を特徴付けるもので
・それぞれの全体(と各記号に上記のnを対応させる関数)の組をその言語のシグネチャーと呼びます.
なお
・関数記号,述語記号を非論理記号,その他(つまり,全ての言語に共通するもの)を論理記号と呼ぶ流儀,また,等号=を論理記号に含める流儀もあります.

言語を固定すると,その言語の項,論理式が以下のように定まります.

(定義1-2)項は
 0項関数記号 (定数記号とも呼びます)
 変数記号
 適当なn(>0)項関数記号f,n個の適当な項t1,...,tn,補助記号によってf(t1,...,tn)と表せるもの
のいずれかです.

(例1-1)xが変数記号,cが定数記号,fが2項関数記号ならば,f(x,c)は項です.

なお,(定義1-2)では「逆にこれらはいずれも項です.」を略しており,正確には,現れる定数記号でない関数記号の個数に関する帰納法により

 T(0)=変数記号の全体と定数記号の全体との和集合
 任意の非負の整数jに対して
  T(j+1)=∪_{n≧1}{f(t1,...,tn):fはn項関数記号,t1,...,tnはそれぞれT(m_1),...,T(m_n)の元.ただし,m_1,...,m_nは和がjである非負の整数.}
と定め,項全体を
 ∪_{j≧0}T(j)
と定めます.

そして,f(t1,...,tn)は,項の個数に関する帰納法により

 f(t1,...,t1)=f(t1)
 任意の正の整数jに対して
  f(t1,...,t(j+1))=f(t1,...,tj)の最後の ")" を ",t(j+1))" に置き換えたもの
と定めます.

同様に(定義1-3),(定義2-3)は関数,述語,論理記号の出現の個数,(定義3-1)は推論規則を適用した回数に関する帰納法による定義です.

(定義1-3)論理式は
 0項述語記号 (命題記号とも呼びます)
 適当なn(>0)項述語記号f,n個の適当な項t1,...,tn,補助記号によってp(t1,...,tn)と表せるもの
のどちらか(これらを原子論理式と呼びます),或いは,適当な変数記号x,論理式A,Bおよび論理記号,補助記号によって
 ¬(A)
 (A)∧(B)
 (A)∨(B)
 (A)→(B)
 (∀x)(A) (この∀xのx,および,A内の各xをxの(全称)束縛出現といいます)
 (∃x)(A) (この∃xのx,および,A内の各xをxの(特称)束縛出現といいます)
のいずれかと表せるものです.

ここで
・論理式に現れる個々の変数記号をその変数記号の出現
・束縛出現でない変数記号の出現を自由出現
・各変数記号の出現がすべて束縛出現である論理式を閉(じた)論理式,そうでない論理式を開(いた)論理式
そして
・閉論理式以外の元をもたない集合を理論
と呼びます.

なお,A,Bが論理式ならな
 (A)\leftrightarrow(B)は((A)→(B))∧((B)→(A))
の略記とします.

また,言語の定義において,論理記号は,例えば ¬ ∧ ∃ のみとして
 (A)∨(B)は ¬((¬(A))∧(¬(B)))
 (A)→(B)は ¬(A∧(¬(B)))
 (∀x)(A)は ¬((∃x)(¬(A)))
それぞれの略記と定義する流儀もあります.

(例1-2)x,yが変数記号,fが1項関数記号,pが1項述語記号,rが2項述語記号ならば
 r(f(x),y)
 ((∀x)(p(x)))→(p(x))
はどちらも論理式,そして
 (∃x)((p(x))→((∀x)(p(x))))
は閉論理式です.

(例1-2)の論理式をそれぞれ
 rfxy
 (∀xpx)→px 或いは (∀x(p(x)))→p(x)
 ∃x(px→∀xpx) 或いは ∃x(p(x)→∀x(p(x)))
などのように記すこともあり,本稿もその作法に従います.

(定義1-4)Aが論理式,x,y,..がAに現れる束縛されていない全ての変数記号ならば,Aの全称閉包は閉論理式∀x∀y...(A)です.

論理式を"閉じる"方法としては,各変数の自由出現を各変数ごとに新たな定数記号に置き換えるというものもあり,本稿のメタ論理でも暗にそれを採用しています.

(参考)
https://www.encyclopediaofmath.org/index.php/Formalized_language