ディオファントス方程式が整数解を持つことは任意の自然数nについてmod nの解を持つことと同値かどうか

整数係数多項式f(x_1, \dots, x_n)を使って書けるx_1, \dots, x_nの方程式

f(x_1, \dots, x_n) = 0

ディオファントス方程式という。

ディオファントス方程式の例は x^2 + y^2 = 25 とか x^3 + y^3 = z^3 などがあげられる。

さて、ディオファントス方程式が整数解を持つならば、当然それを\bmod nで射影すれば\bmod nの解が得られる。 逆に任意の正整数nについて\bmod nの解をもつならば整数解を持つだろうか?

これの答えはNoである。ディオファントス方程式であって任意の正整数nについて\bmod nの解をもつが、整数解を持たないものが存在する。

これの証明がいろいろあり、面白かったので紹介する。

解答5を除いてはnt.number theory - Diophantine equation with no integer solutions, but with solutions modulo every integer - MathOverflowによる。

解答1

3x^3+4y^3+5z^3=0が反例。

これは\mathbb{Q}上に解を持たないが、\mathbb{R}と任意の\mathbb{Q}_pに解を持つ3次形式として知られている。しかしその証明はあまり簡単ではないようだ。

解答2

x^2+y^2+z^2+w^2=−1が反例。

まず、整数解を持たないのは明らか(任意の整数について左辺は0以上なので)。 一方で任意のnについて4平方和定理よりx^2+y^2+z^2+w^2=n-1となるx, y, z, wが存在する。よって両辺\bmod nをとって方程式の\bmod n解を得る。

解答3

(x^2-2)(x^2-17)(x^2-34)=0が反例。

まず整数解を持たないのは、この実数解がx = \pm \sqrt{2}, \pm \sqrt{17}, \pm \sqrt{34}有理数でないことからわかる。

次に任意の素数pについて\bmod pで解を持つこと。 これは平方剰余の理論からわかる。

p2でも17でもないとき。ルジャンドル記号の性質

\displaystyle{\left(\frac{2}{p}\right)  \left(\frac{17}{p}\right) =  \left(\frac{34}{p}\right)}

より217がともに平方非剰余なら34が平方剰余となる。 よって2, 17, 34のどれか一つは平方剰余なので(x^2-2)(x^2-17)(x^2-34)\equiv 0 \pmod pは解を持つ。

p=2の場合はx=1が解。 p=17の場合は方程式はx^2=2となるが、これは第二補充法則より\left(\frac{2}{17}\right)=1なので解あり。

次に任意の素数べきp^eについて\bmod p^eで解を持つこと。 これはヘンゼルの定理よりわかる。 ただし、p=2のときはf(x) = x^2-17微分f'(x) = 2x \equiv 0 \pmod 2となってしまうので、x=1x^2-17 \equiv 0 \pmod 4の解であるところから始めなければいけない。

最後に一般のnについては中国剰余定理から\bmod nの解の存在が分かる。

解答4

x^2+23y^2=41が反例。

整数解を持たないことはx^2 \ge 0よりy = 0, \pm 1とならないといけないことからわかる。

有理数解として(x, y) = (1/3, 4/3)があるので3以外の素数べきの法について解が得られる。 また、(x, y) = (9/4, 5/4)も解なので2以外の素数べきの法についても解が得られる。 したがって任意の素数べきの法について解が得られるので中国剰余定理より任意のnについて\bmod nの解が得られる。

解答5 (基礎論的解答)

 A = \{ f(x_1, \dots, x_k) \in \bigcup_{n \in \mathbb{N}} \mathbb{Z}[x_1, \dots, x_n] : \text{$f$は整数解を持つ} \}

は計算可能でない集合であることが知られている(MRDP定理)。 Aは明らかに\Sigma_1なため、\Pi_1でない。

一方で、任意のディオファントス方程式について整数解を持つこととすべてのnに対して\bmod n解を持つことが同値だったら

 A = \{ f(x_1, \dots, x_k) \in \bigcup_{n \in \mathbb{N}} \mathbb{Z}[x_1, \dots, x_n] : \forall n\in\mathbb{N}, \exists a\in(\mathbb{Z}/n\mathbb{Z})^k, f(a) = 0 \pmod n \}

A\Pi_1で書けてしまう。矛盾。

この解答だとMRDP定理という大道具を使うし、具体的な方程式が与えられない。

参考文献

  1. nt.number theory - Diophantine equation with no integer solutions, but with solutions modulo every integer - MathOverflow
  2. y., Hilbert の第 10 問題 http://iso.2022.jp/math/undecidable-problems/files/hilberts-tenth-problem.pdf
  3. 雪江明彦 『整数論1 初等整数論からp進数へ』 日本評論社

上にも述べたが解答5以外は[1]によるものである。 MRDP定理については[2]を参照せよ。 平方剰余の理論やヘンゼルの補題は[3]を参照。

集合論の言語の有限構造がZFCの各公理を満たすか判定するプログラム

この記事はMathematical Logic Advent Calendar 2019の8日目の記事です。 もともと「C[0,1]の中の微分可能関数全体がΠ^1_1完全なこと」という記事を書く予定でしたが、予定変更です。

adventar.org

集合論の言語の有限構造がZFCの各公理を満たすか判定するプログラムをOCamlで書きました。 ただし、分出公理図式と置換公理図式はそれぞれ無限個公理があるわけですが、それらについてはそのすべてのインスタンスを満たすことを判定します。

たとえば、Kunenの"The Foundations of Mathematics"に載っている7つの有限モデルについて各公理を確かめてみます。

f:id:fujidig:20191209174332j:plain

図は邦訳『キューネン数学基礎論講義』(訳: 藤田博司)より抜粋です。 ノードxからノードyに辺が貼ってあったら、x∈yの意味です。

ついでに次のモデルも追加しておきます。

f:id:fujidig:20191209192639p:plain

外延 基礎 分出 置換 無限 べき 選択
モデル1 1 1 1 0 1 1 0 0 1
モデル2 1 0 0 1 1 1 0 1 1
モデル3 1 1 0 0 1 1 0 1 1
モデル4 1 0 0 0 1 0 0 0 1
モデル5 0 1 1 0 1 0 0 0 1
モデル6 1 1 0 0 1 0 0 0 1
モデル7 1 1 1 0 1 0 0 0 1
モデル8 0 1 0 0 0 0 0 0 0

0がfalse、1がtrueを意味しています。

なお、確かめるのがナンセンスなものも含まれていることに注意してください。たとえば、無限公理は後続者の一意存在、選択公理は二つの集合の共通部分の一意存在がないと意味があるとはいいづらいです。

分出公理と置換公理をどう確かめているか

分出公理と置換公理はそれぞれ無限個の公理からなるので素朴に考えたら有限時間で判定できるか怪しいです。 ですが、できます。 まず、分出公理 \begin{align} \forall Z \forall \vec{p} \exists Y \forall x (x \in Y \iff x \in Z \land \varphi(x, z, \vec{p})) \end{align} はパラメータ$\vec{p}$を使えることを考えれば、どんなオブジェクト$Z$についてもその部分集合の候補というのは論理式で定義可能になっています。 たとえば、$Z$の子供が$x_1, \dots, x_n$ならば$x = x_1 \lor x = x_3$によって$\{ x_1, x_3 \}$が定義可能になっています。 したがって、どんなノード$Z$についてもその子供たちの任意の選び方$y_1, \dots, y_i$について子供がぴったり$y_1, \dots, y_i$なノードがあるか探せば分出公理が成り立っているか確かめられます。

置換公理は、これもパラメータが使えるので、任意のマッピングが定義可能になっています。 よって、すべてのノード$x$にわたる$x$の子供の数の最大値$n$をとり、ノードの$n$個の任意の集まりについて、それらをすべて子供にするノードの存在を確かめればよいのです。

以上より分出公理も置換公理も有限時間で判定できます。

なお、この方法は数学基礎論若手の会2019にてyさんとkさんの助言により得られることができました。

ソースコード

type variable = string

type formula =
   Equal of variable * variable
 | Epsilon of variable * variable
 | Imply of formula * formula
 | Not of formula
 | And of formula * formula
 | Or of formula * formula
 | Forall of variable * formula
 | Exists of variable * formula

type model = int * ((bool list) list)

type assignment = (variable, int) Hashtbl.t

let subst asgn var value =
  (let asgn' = Hashtbl.copy asgn in
    Hashtbl.add asgn' var value; asgn');;

let rec forall n fn = 
  if n = 0 then true
  else (fn (n-1)) && (forall (n-1) fn);;

let rec exists n fn = 
  if n = 0 then false
  else (fn (n-1)) || (exists (n-1) fn);;

(* モデルmdlが論理式fmlを割り当てasgnで満たすかどうか *)
let rec satisfies mdl fml asgn =
  let (numelems, graph) = mdl in
  match fml with
   Equal (var1, var2) -> (Hashtbl.find asgn var1) = (Hashtbl.find asgn var2)
 | Epsilon (var1, var2) ->
      let a = (Hashtbl.find asgn var1) in
      let b = (Hashtbl.find asgn var2) in
      List.nth (List.nth graph b) a
 | Imply (fml1, fml2) -> (not (satisfies mdl fml1 asgn)) || (satisfies mdl fml2 asgn)
 | Not fml -> not (satisfies mdl fml asgn)
 | And (fml1, fml2) -> (satisfies mdl fml1 asgn) && (satisfies mdl fml2 asgn)
 | Or (fml1, fml2) -> (satisfies mdl fml1 asgn) || (satisfies mdl fml2 asgn)
 | Forall (var, fml) -> 
      forall numelems (fun x -> satisfies mdl fml (subst asgn var x))
 | Exists (var, fml) -> 
      exists numelems (fun x -> satisfies mdl fml (subst asgn var x));;

(* リスト [0; 1; 2; …; n - 1]を返す *)
let range n = List.init n (fun x -> x);;

(* range nとrange mの直積を返す *)
let range2 n m = List.init (n*m) (fun x -> (x / m, x mod m));;

(* モデルmdlの元xに対してy∈xとなっているy全体のリストを返す *)
let children mdl x = 
  let (numelems, graph) = mdl in
  List.filter (fun y -> List.nth (List.nth graph x) y) (range numelems);;

(* リストlistのすべての部分リストのリストを返す *)
let rec all_subsets list =
  match list with
  [] -> [[]]
| x :: tail -> all_subsets tail @ List.map (fun y -> x :: y) (all_subsets tail);;

(* リストlistの部分リストで大きさkのもの全体のリストを返す *)
let rec all_combinations list n = 
  match list with
  [] -> (if n = 0 then [[]] else [])
| x :: tail -> (all_combinations tail n) @ List.map (fun y -> x :: y) (all_combinations tail (n - 1));;

(* 昇順に並んだ二つのリストx, yについてxがyの部分リストか判定する *)
let rec is_sublist x y =
  match x with
  [] -> true
| a :: tail -> (match y with
    [] -> false
  | b :: tail' -> (if (a = b) then (is_sublist tail tail') else (if (b < a) then (is_sublist (a::tail) tail') else false)));;

(* 分出公理をすべて満たすか *)
let sat_all_comprehension mdl =
  let (numelems, graph) = mdl in
  forall numelems (fun x -> 
    List.for_all (fun subset -> 
      exists numelems (fun y -> children mdl y = subset)
    ) (all_subsets (children mdl x)));;

(* 置換公理をすべて満たすか *)
let sat_all_replacement mdl =
  let (numelems, graph) = mdl in
  let maxchildren = List.fold_left max 0 (List.map (fun x -> List.length (children mdl x)) (range numelems)) in
  let combinations = all_combinations (range numelems) maxchildren in
  List.for_all (fun subset ->
    exists numelems (fun y -> is_sublist subset (children mdl y))
  ) combinations;;

let model_to_pairs mdl =
  let (numelems, graph) = mdl in
  List.filter (fun (x, y) -> List.nth (List.nth graph y) x) (range2 numelems numelems);;

let model_to_string mdl =
  "{" ^ (String.concat ", " (List.map (fun (x, y) -> "(" ^ (string_of_int x) ^ ", " ^ (string_of_int y) ^ ")") (model_to_pairs mdl))) ^ "}";;

let iff fml1 fml2 = And (Imply (fml1, fml2), Imply (fml2, fml1));;
let bforall x y fml = Forall (x, Imply (Epsilon (x, y), fml));;
let bexists x y fml = Exists (x, And (Epsilon (x, y), fml));;

(* x=∅ (using z as a bounded variable) *)
let emptyset x z = Forall (z, Not (Epsilon (z, x)));;

(* ∅∈x (using y, z as bounded variables) *)
let containsempty x y z = Exists (y, And (Epsilon (y, x), emptyset y z));;

(* x⊆y (using z as a bounded variable) *)
let contains x y z = bforall z x (Epsilon (z, y));;

(* y=x∪{x} using z as a bounded variable *)
let successor x y z = Forall (z, (iff (Epsilon (z, y)) (Or (Epsilon (z, x), (Equal (z, x))))));;

(* w=x∩y using z as a bounded variable *)
let intersection x y w z = Forall (z, iff (Epsilon (z, w)) (And (Epsilon (z, x), Epsilon (z, y))));;

(* x∩y=∅ *)
let disjoint x y z = bforall z x (Not (Epsilon (z, y)));;

(* xが一点集合 using y, z as bounded variables *)
let singleton x y z = bexists y x (bforall z x (Equal (z, y)));;

(* 外延性公理 *)
let extensionality = Forall ("x", Forall ("y",
  Imply (Forall ("z", iff (Epsilon ("z", "x")) (Epsilon ("z", "y"))), Equal ("x", "y"))));;

(* 基礎の公理 *)
let foundation = Forall ("x", Imply (Exists ("y", Epsilon ("y", "x")),
                                     Exists ("y", And (Epsilon ("y", "x"), Not (Exists ("z", And (Epsilon ("z", "x"), Epsilon ("z", "y"))))))));;

(* 対の公理 *)
let pairing = Forall ("x", Forall ("y", Exists ("z", (And (Epsilon ("x", "z"), Epsilon ("y", "z"))))));;

(* 和集合公理 *)
let union = Forall ("F", Exists ("A", Forall ("Y", Forall ("x",
  Imply (And (Epsilon ("x", "Y"), Epsilon ("Y", "F")), Epsilon ("x", "A"))))));;

(* 無限公理 *)
let infinity = Exists ("x", (And (containsempty "x" "y" "z", bforall "y" "x" (bexists "z" "x" (successor "z" "y" "w")))));;

(* べき集合公理 *)
let powerset = Forall ("x", Exists ("y", Forall ("z", Imply (contains "z" "x" "w", Epsilon ("z", "y")))));;

(* 選択公理 *)
let choice = Forall ("F", Imply (
  And (Not (containsempty "F" "y" "z"), bforall "x" "F" (bforall "y" "F" (Or (Equal ("x", "y"), disjoint "x" "y" "z")))),
  Exists ("c", bforall "x" "F" (Exists ("d", And (intersection "c" "x" "d" "y", singleton "d" "y" "z"))))));;

let models = [
  (1, [[false]]);
  (1, [[true]]);
  (2, [[false; true]; [true; false]]);
  (3, [[false; true; false]; [true; false; false]; [true; true; false]]);
  (3, [[false; false; false]; [true; false; false]; [true; false; false]]);
  (4, [[false; false; false; false]; [true; false; false; false]; [true; true; false; false]; [true; true; true; false]]);
  (3, [[false; false; false]; [true; false; false]; [false; true; false]]);
  (5, [[false; true; false; false; false]; [true; false; false; false; false]; [true; false; false; false; false]; [false; true; false; false; false]; [false; false; true; true; false]])
];;

List.iter (fun mdl -> 
  let (numelems, graph) = mdl in
  let asgn = Hashtbl.create 0 in
  print_endline ("In the model=(" ^ string_of_int numelems ^ ", " ^ (model_to_string mdl) ^ ")");
  print_endline (String.concat " " (List.map (fun x -> (if x then "1" else "0")) [
    satisfies mdl extensionality asgn;
    satisfies mdl foundation asgn;
    sat_all_comprehension mdl;
    satisfies mdl pairing asgn;
    satisfies mdl union asgn;
    sat_all_replacement mdl;
    satisfies mdl infinity asgn;
    satisfies mdl powerset asgn;
    satisfies mdl choice asgn;
  ]));
) models;;

Davisのゲーム

Mathematical Logic Advent Calender 2019 5日目の記事です。

adventar.org

閉集合から決まる無限ゲームには先手か後手のどちらかに必ず必勝法が存在する」という事実を使い、非可算な解析集合はすべて完全集合を含むことを示します。

PDF:

f:id:fujidig:20191204210952p:plain:w500

今回Davisのゲームという無限ゲームを扱いましたが、Mathematical Logic Advent Calender 2019にはまだ無限ゲームの寄稿があります。ちょうど1週間後にy.さんがBanach-Mazurゲームの話を、2週間後にYasudaくんが決定性公理のもとでの無限組み合わせ論の話を書いてくれるそうです。楽しみですね。

6日目はp進大好きbot (@non_archimedean)さんの担当です!

院試体験期

W大

英語で足切りされた。TOEICで550点必要だったところが、530点だった。 TOEICはもう間に合うのはなくてIELTSなども受けたが、これもだめ。

N大

合格。 学部の成績がよかったため、面接だけの試験を受けることができた。(これに落ちれば通常の筆記+面接の試験をもう一度受ける仕組み)。

その面接では大失敗した。 Y先生から「無限組み合わせ論で印象に残っている定理」を聞かれた。僕は「Delta System Lemma」と答えた。 定理の主張と証明をホワイトボードに書かされるのだが、主張は書けたが証明はほとんど書けなかった…。これでよく通ったなあ。

あとはM先生から基数に関するちょっとした問題を出される。だいぶヒントをもらいながらだったけれどなんとか解くことができた。

T大

一般入試で合格。 筆記試験は微積と線形を解かずに、「集合」「位相」「代数」「集合論」を解いた。

  • 集合: 全射単射の問題
  • 位相: 弧状連結性と連結性の問題
  • 代数: F_2[x]/(x3+x+1)の問題
  • 集合論: カントール空間のコンパクト性を示す問題 (位相の用語は使わずに出題されているが実質的にはそういう問題)

面接は7分くらいであっさり終わった。 指導教官にDescriptive Set Theoryではどんなことをやっているのか聞かれて、MoschovakisのDSTの第6章の話をしたのだが、自分で読んだわけではない部分だったので (人のゼミを聞いただけ)突っ込まれるとやばかった。突っ込まれずに済んだが。

入学先

N大にします。

2019年1月~7月振り返り

2018年度秋学期の時間割

1
2 多様体入門演習 トポロジーB 応用体育水泳(秋) 代数学IB
3 計算機数学II 関数解析入門 確率論II
4 多様体入門 関数解析入門演習 数理論理学II
5 卒研(秋BC) 代数学IIB
6 数学外書輪講(秋A) 卒研(秋BC)
  • 多様体入門演習: 長い直線について発表したら大変受けが悪かった
  • 関数解析入門: 相対評価なのでA+取るためにはかなり問題を解かないといけなくて大変
  • トポロジーB: 「この問題解いたらA+あげる」というのを解いて無事A+をもらった
  • 代数学IB: 群論をしっかりやってくれてありがたかった。位数75の群の分類が印象に残っている。あとは、初回の小テストで上級者向けを選んだらTorとExtを計算する問題を出されて撃沈したりとか

2019年度秋学期の時間割

1 論理回路(春AB)
2 論理回路(春AB)
3
4
5 卒研
6 卒研

2月

25日~28日: 数物セミナー合宿で静岡に行った。Riehlの"Category Theory in Context"でセミナーした。

組み合わせ論の本を読み始めた

f:id:fujidig:20190808182718j:plain:w400

"Combinatorial Enumeration" (Ian P. Goulden & David M. Jackson)という本を借りました。所属大学の図書館になかったので別の大学から取り寄せて借用。

Random Mapping Statisticsという論文を読みたいのですが、この本に書いてあるようなことは前提知識としているようで、読むことを決定。

この読みたい論文には次のような内容が書かれています: nを自然数としてn元集合から自分自身への写像fがランダムに与えられたとき、そこから決まるグラフに関する量のn→∞の漸近挙動を見る。たとえば、不動点が存在する確率だとか、ランダムな初期値に対する周期の期待値だとか。

グラフに存在するサイクルの最小の長さの期待値については論文に書かれていないので、いつか自分で考察してみたいなあ。 そのためにはまずは、この"Combinatorial Enumeration"を読まねば。

この本と論文がある程度読めたら都数のTSとかで発表できたらいいな。

線形代数の最重要定理「基底のサイズ(次元)の一意性」を復習した

線形代数最重要定理:基底のサイズ(次元)の一意性

今日は線形代数の最重要定理といわれる「基底のサイズ(次元)の一意性」の証明を復習しました。

定理1: $V$を有限次元ベクトル空間とする。このとき$V$の基底のサイズは一意的である。

これは行列の階数標準形を使えばそんなに難しい話ではないですが、行列を使わずに証明するとなると結構やっかいです。齋藤正彦『線型代数入門』p.104に行列を使わない証明が載っています。

f:id:fujidig:20190525212131j:plain:w400

行列を使う証明はせいぜいPID上の加群までしか一般化できないですが、この齋藤に載っている証明なら任意の可換環上の自由加群に対して同様の議論で証明ができるのがメリットかもしれません。

そういえば、一般の可換環上の自由加群についても階数の一意性が言えたはずでどうやって証明しているのだろうと気になり調べました。 雪江明彦『代数学2 環と体とガロア理論』を参照すると次のような証明。

f:id:fujidig:20190525205718j:plain

極大イデアルで割り、ベクトル空間の話に帰着されています。これは賢い。

ところで、こういう話をTwitterでしていたら「ジョルダン・ヘルダーの定理はベクトル空間の次元の一意性の一般化と思える」という話をある方から教えてもらいました。確かにそうですね。

線形代数2番目に重要な定理:線形独立な集合は基底に延長できる

次元の一意性が最重要定理なら、二番目に重要なのは基底の存在、もっと一般には「線形独立な集合は基底に延長できる」ことなんじゃないかと思いました。

定理2: $V$をベクトル空間とする。$S$を線形独立な$V$の部分集合とする。このとき$S \subseteq S'$となる$V$の基底$S'$が存在する

この定理、一般の可換環上の自由加群には一般化できません。例は$\mathbb{Z}$加群$\mathbb{Z}$で$S=\{2\}$です。 さて、では定理の証明のどこで体であることを使っているんでしょうか。

この定理の証明は次の2ステップに分かれます:

  1. 線形独立な集合$S$はそれを含む極大な線形独立な集合に拡大できる
  2. 極大な線形独立な集合は基底である

1つ目はいつも通りZorn補題を使えば示すことができ、一般の加群でも言えます。 2番目が体であることを本質的に使います。

2番目の証明を追ってみましょう。

ベクトル空間$V$において極大な線形独立な集合$S$は基底である

$S$が$V$を生成しないと仮定し、$x \in V \setminus \langle S \rangle$をとります (ここに$\langle S \rangle$は$S$の生成する空間)。 $S' = S \cup \{x\}$とおく。

主張: $S'$はまた線形独立である。

∵) 線形関係 $\sum_{i=1}^n a_i x_i + b x = 0 (a_i, b \in k, x_i \in S)$ を仮定する。$b=0$なら$S$の線形独立性よりこの線形関係は自明である。 $b \ne 0$なら両辺$b$で割り整理すると \[ x = \sum_{i=1}^n \left(-\frac{a_i}{b}\right) x_i \] となる。これは$x \not \in \langle S \rangle$に矛盾。よって主張が言えた。 //

よって、$S'$は$S$より真に大きい線形独立な集合。これは極大性に反する。 □

線形関係の$x$にかかっている係数$b$で割ったところがポイントです。ここで体であることを使っています。

まとめ

復習をしてみて、線形代数の理解が深まりました。