戸田山和久 著 論理学をつくる 名古屋大学出版会 について、私が気が付いた、たいしたことない誤植です。２０１６年１１月発行の、１０刷を対象とします。
これ、本当に良い本でした。
説明がていねい。全ての練習問題に完全な回答がついている。用語が英語でも示されている。
８７ページ Subcase 3
誤
AがB ∧ C という形のとき
正
AがB ∨ C
162ページ
誤
存在指定アリ
正
存在措定
２９５ページ
誤
(a) の図の、 Q -> P Rest
正
Reit
４１６ページ
誤
問題８７の（２） ２５３ページですでにやってある
正
２３５
４１９ページ
誤
(iv) aRx となるすべての x に対し、それぞれ何らかの z が存在して、VM(z, P) = 0
正
(iv) aRx となる何らかの x に対し、それぞれ存在する z すべてに対して、VM(z, P) = 1 であることはない
説明
右図のモデルでは、 a にとって、 x は w1 だけです。そこから到達可能な w2 では、 P = 0, w3 では、P = 1 なので、VM(z, P) = 0 の世界があります。
(iii) の方は、 w1 から P = 1 である w3 へ到達可能なので、なんらかの y の条件が満たされます。
◇□というのは、こういう理解でよいのですよね。
ページの後半は、
Computability and Logic を読んだときのメモ
Computability and Logic Unofficial Errata 別ページにしました。
以下は、主に、ポエムです。
私は Kindle 版を読みましたが、違法コピーっぽい pdf ファイルを見たら、私が誤植としたところが、正しい記述でした。紙の本でも、きっと、そうなのでしょう。Kindle 版固有の誤植がたくさんあるようです。
戸田山先生の本を読んで、次に読む本に選んだのが、これです。戸田山先生も、推薦しておられたので。
買っちゃったあ。iPad Kindle アプリで英語の本を読むのはとても快適。単語をタップするだけで辞書が引ける。オフラインでもよし。
Fifth Edition の公式 errata は、ここです。１７章までの奇数番号の演習問題のヒントもあります。
https://www.princeton.edu/~jburgess/addenda.htm
数式とか証明に、致命的な誤植がたくさんあります。
ギリシア文字ガンマ Γ が欠落していることが多いです。Kindle 版固有らしいです。
p.29 3-4 Example
空白から始めると、q1S0Rq2 の規則で、右に行ってしまうから、１を０にする論理が動かない。そもそも、最初が１を指してないと３１ページで言う、標準形式でない。
p.43
(1) p(n+2j) >= p(p(n))
私が理解できなかったので、覚え書きです。これを読んだら、わかりました。
https://plato.stanford.edu/entries/turing-machine/#5.1
p(n) が出力するのは、ｎ 状態のマシンの最大可能な生産性です。これをさらに、p に与えて p(p(n)) を作るのがわかりませんでした。
説明
図４．３の三つのマシンの真ん中の BB マシンを考える。この入力は、状態数だが、例えば n=3 とするためには、１を３つ並べたものを作る必要があって、そのために左の３状態のマシンが必要。真ん中の BB マシンの出力が１０になるか１００になるか知らないけど、その出力を、右の BB マシンは、状態数として、生産性を計算する。
その結果が、p(p(n))
一方、この三つのマシンをくっつけたマシンの状態数は、数えれば、 n+2j とわかる。
p の定義から、p(n+2j) は、最大可能な生産性を出すはずなので、右の BB マシンが出力した p(p(n)) より大きいはず。
４章
正の整数から正の整数への関数は非可算無限個ある。
一変数のチューリングマシンは、状態と遷移を４つの整数の組で表したもののシーケンスで表せる。全体を一つの整数でも表せる。これは加算無限である。なので、チューリング計算不可能な関数がある。
定理４．１ 対角化関数 d はチューリング計算不可能。
チューリング計算可能な一変数の関数を、 f1, f2 と全て列挙して、fn(n) が定義されかつ値が１ならば、２を取る関数を、 d(n) と定義する。矛盾が生じる。
定理４．２ halting 関数はチューリング計算不可能。
チューリングマシン m に、入力 n を与えた時に、停止するなら１を返す halting マシンと定義する。
copying マシン、 halting マシン、 dithering マシンを直列にしたマシンに、自身のマシン番号を与えると、停まるか停まらないかで矛盾が生じる。
９章 問題
9.1 ケンタウロスは投票できない。タブローを書いても閉じない。変だ。
存在措定が無いからだ。戸田山 159ページ。ヒントで、9.１節の9と10式を見ろというのはそういうこと？
１１章 よくわからなかった。
PPLが決定不可能なことと、チューリングマシンが止まるか不明なことが同じだという、初等論理学の一つのクライマックスなのですよね。
MPLは決定可能ですね。それを判定するチューリングマシンは、必ず止まるものが作れますね。１１章の証明で、どこが違ってくるのでしょう。
再帰関数の方の証明は、もっと、わからなかった。
定理１１．２ 論理的含意は決定不可能。
チューリングマシンが停まる、ということは、Γ |= D という論理式に、きっちり翻訳できる。Γ は、マシンが時刻 t に、状態 i、位置 x にいて、マーク e を読んだら、どうしなさい、という規則と、現在の状態を持つ。D は、次の状態が無い、という状態の全ての OR である。これまでの議論で、停止問題は解けないことがわかっているので、含意問題も解けない。
１３章
コンパクト性定理
戸田山 ８３ページ。
１２．１５ コンパクト性定理
文の集合の全ての有限部分集合が充足可能（＝モデルを持つ）ならば、元の集合も充足可能。
１３．１ satisfaction 属性補題
充足可能な文の集合Γの集合Sは、S0からS8のsatisfaction 属性を持つ。
元の集合の有限部分集合は、それを持つ。Sに属する。元の集合がSに属することを言いたい。
全ての有限部分集合がSに属する文の集合の集合を、S*と呼ぶ。元の集合はここに含まれる。
実は、S*は、satisfaction 属性を持つ。定理１３．２
１３．３ モデル存在補題
S*を、文の集合の集合で、satisfaction 属性を持つとする。
S*に含まれる文の集合は、モデルを持つ。
なので、元の集合は充足可能。コンパクト性定理の結論。
１３．３は、なぜならば。
１３．６ closure 補題
S*を、文の集合の集合で、satisfaction 属性を持つとする。
S*に含まれる文の集合Γを拡張して、closure 属性C1からC8を持つΓ*にできる。
証明は、１３．４節。
Γに、文Bあるいは~B を加えて、Γ*を構成する。closure 属性を持つようにする。
１３．５ term models 補題
Γ*は、文の集合でclosure 属性を持つ。
ならば、モデルを持つ。Γ*のすべての文を真にする解釈Mがある。
証明は、１３．２と３節。
原子文を真とするように述語を決めればいい。否定やORを含む文も、closure 属性があるから、矛盾したものはできない。
13.5節 非可算言語
closure 補題の証明では、Γに、文を一つづつ増やして、Γ* を作った。非可算の場合、これはできないので、集合論の有限性と極大元のしかけを使う。
14章
{A, B} => {C, D} は、(A and B) |- (C or D) と読む。
健全性定理 soundness theorem の用語のまとめ
１４８ページ。戸田山２６５ページの表も参照。
論理式の集合Γと論理式Dについて、
Γ|-D ならば Γ|=D
シンタックスの世界
Γ|-D
演繹可能 deducible from
Dは公理であるか、Γの要素であるか、前記２つから推論規則によって引き出された式である。
セマンティクスの世界
Γ|=D
ΓからDが論理的に帰結する、導かれる。consequence of
Γに含まれるすべての式を真にするモデルのもとで常にDも真になる。
Γを充足する任意の真理値割り当てのもとでDも真になる。
完全性定理１４．２ secure な文は derivable である。
if Γ secures Δ, then is Γ => Δ is derivable
戸田山 定理４２ Γ|=D ならば Γ|-D
１４．１４ Γ => Δ iff Γ ∪~ Δ が inconsistent
戸田山 定理４０
Γ secures Δ iff is Γ ∪~Δ is unsatisfiable
戸田山 定理４３
なので、完全性定理１４．２の証明は、
consistent set is satisfiable 戸田山 定理４４ヘンキンの定理 無矛盾なら充足可能
を証明すればいいことになる。
S を、無矛盾な文の集合とする。それが、satisfaction 属性を持つことを言いたい。そうすれば、１３．３ モデル存在補題により、Sに属する全ての文はモデルを持つ、つまり充足可能。
戸田山で行った、極大化は、この本では、１３．６ closure 補題 で終わっているので、無矛盾な文の集合が、S0からS8 を満たすことを示せば終わり。
Γ is in S 無矛盾とは、Γ=>∅ でないこと。
１４．１８カット除去定理
Γ=>{(A -> B)} ∪ Δと、Γ=>{A} ∪ Δ が成り立つならば、(R0)–(R9)を使って、 Γ=>{B} ∪ Δ が導出できる。R10のカット規則を使わなくても。
用語のまとめ
formula: 論理式
sentence: closed formula を文と呼ぶことがある。戸田山１２５ページ。
Closed formulas, which are also called sentences, have truth values p.105
recursive set とは。７３ページ。
set is called recursively decidable, or simply recursive for short, if its characteristic function is recursive
要素が含まれるかどうかの判定が再帰関数のもの。
対偶：contraposition
complement: 補集合
再帰的な集合の部分集合は、再帰的とは限らない。部分集合の特性関数を、再帰関数で示せるかが問題となる。全ての文の集合が再帰的でも、真である文の集合は、 semirecursive であることしか言えない。これが、決定不可能ということ。
で、１５章、算術化、のところで、しばらく挫折。
照井先生の再帰的関数論
http://www.kurims.kyoto-u.ac.jp/~cs/cs2011_terui.pdf
を読んで、再帰関数とか最小化が、わかりました。
誤植
１６ページ
P0^n1+1 でなく、P0^n0+1
２８ページ 定理４．５の２
得られる関数は再帰的’ である でなく 部分再帰的’ である
再帰的関数論の誤植 以上
p.102
logical symbol: 個体変項、論理定項 logical connective、補助記号、等号。x, ∧、∀、, () , =
non logical symbol: 個体定項(constant, individual symbol)と述語記号(predicate, relation)、関数。c, A, f
non logical symbol の集まりを、language と言う。色がついている方ね。
p.103 example 9.1 language of arithmetic L*
0, <, ', +,*
p.103 言語Lの解釈Mとは、|M| domain と、denotation からなる。集合の要素に、言語の non logical symbol をマップする。述語は関係であり、すなわち subset
p.104 例９．２ 算術言語の標準解釈 N*
自然数の０，<, ＋１、加算、乗算。
15章
定理１５．２ 論理式は再帰である。
当たり前でしょ。例えば、 0=0 のコード番号は、１９３ページに示してあるし、それらを ∧ や かっこでつなげたら、例７．２０の concatenation をほどこした結果になる。conc 関数は、再帰であることが示されている。だいたい、論理式全体を、 UTF-8 エンコードして、巨大な１６進数としてコードにする、という手続きは、有限ステップで終わるのは自明ですよね。
いや、論理式であるという集合の特性関数、つまり、そうであるかないかの判定が、有限ステップでできることがここで問題としていること。
コードが与えられた時に、それが論理式として正しいか。 コード a が述語であるかは、１９４ページに示すように、2^2*3^n*5^i == a である n, i があるかによる。上限なしの ∃n は、semirecursive になってしまうが、幸い、コードの長さが上限にできる。文法的に正しい論理式、という判定も、７章で例をあげた各種の再帰関数でできる。これが、１５．２節の議論。
deducible な文の集合が、recursive でなくて、semirecursive なのは、演繹可能かどうかは、決定不可能だから。
p.191
theorem: Γから演繹可能な文
theory: set of sentences that contains all the sentences of its language that are provable from it.
それから演繹可能な全ての文を含む、文の集合
theory が complete：language の全ての文について、Bか！Bのどちらかを必ず含む。
文の集合 Γ が decidable: Γから演繹可能な文の集合が、再帰。つまり、要素が所属するしないが有限ステップで判定できる。
theory がdecidable:集合として、再帰。
language は、non logical symbol つまり、述語と定数。
= を含むか、関数を含むかは、 language にはかかわらない。どういう演繹規則を採用するかは、language にはかかわらない。
theory は、language の一部だけで閉じていていい。
例
language は、述語 P と定数 a, b, c からなる。
Γ = { Pa, Pb } とする。Pa ∨ Pb は、Γ の theorem. T := { Pa, Pb, Pa ∨ Pb , ~~Pa, ... } は theory。これは complete でない。c を含まないから。
Γ は、再帰で有限なので、Tは有限公理化可能。T は、無矛盾。T は再帰。
定理１５．７ 公理化可能な theory Tが完全ならば、決定可能。
Tが決定可能とは。Tから演繹可能な文の集合が、再帰。今、Tは theory としているので、T自身がそれ。
T*を、Tの theorem の集合とする。実は、T。それは１５．４より、 semirecursive.
Tがそもそも矛盾しているなら、全ての文が入っているはずで、ならば１５．２から再帰。
そうでないなら、完全という前提から、Dあるいは～Dのいずれかが、T* に入っている。
ここで、T*の補集合を考える。それは、X ∪ Y で、前者は文として不適格なコードで再帰、後者は、 theorem の集合に否定をつけたもので、semirecursive.
T*とその補集合が semirecursive なので、クリーネの定理７．１６により、T* は再帰。
問題１５．３を解こうとしてわからなかった。
定理１２．１７ １４７ページ。同型の非可算モデルが一つしか無いなら、complete.
定理１５．７ complete なら決定可能。
問題の前提より、Tは complete でないので、T ∪ {Pc}, T ∪ {~Pc} のいずれも充足可能。なんで？T が２つの同型のモデルを持つことから、なんやら場合がわけられて、再帰。
p.200
pair(s, t) を、(1, 1), (1, 2) を並べる話か、と思うと、わけがわからない。
p.12 example 1.8 を参照。これは、（コードつまり自然数のシーケンス、ベース例えば、１０進数）の対のこと。
Fent(x1, x2, x3, y) も、２０２ページの３つの論理式も、Fent(i:何番目か、s: コード、t: ベース、結果）と思うと理解できる。
１６章
p.199
correct の定義。‘true in the standard interpretation’
arithmetically define:
We say a formula F(x) of the language of arithmetic arithmetically defines a set S of natural numbers if and only if for all natural numbers a we have Sa if and only if F(a) is correct.
論理式 F が、関係 S を決められる時。
関数は、そのグラフ関係が算術的である時、算術的であるとする。
p.204
rudimentary formula：原子論理式から、! and or ∀x<t ∃x<t で構成される論理式
∃ rudimentary：自由な ∃x があるもの
p.206
rudimentary function: rudimentary formula によって、arithmetically definable な関数。
p.207
a set S is defined in T by D(x)：要素 n が 集合 S に含まれるなら、論理式 D(x) は、theory T の theorem である。含まれないなら、！D(x)が、theorem である。
S is definable in T：集合を定義するなんらかの論理式がある。要素が所属するしないに対応して真か偽になる論理式がある。
Arithmetical definability は、theory T が、true arithmetic の場合。
p.207
関数 f is representable in T：f(a)=b なら、論理式 F があって、∀y(F(a, y) <-> y=b) は、theorem である。つまり、F(a, b) かつ ∀y(y != b->∼F(a, y))
それに対して、definability は、F(a, b) を要求するが、c!=b の 全ての c に対して、∼F(a, c) を要求するだけ。∀y ではない。
ただし、true arithmetic の場合、representability と definability は同じ。
１７章
p.221
対角化補題、具体的な例がないとすっきりしない。例えば、B(y) として、 y=0 に対して、G を書き下すことはできるの？
ゲーデル数はゼロにならないから、⌜G⌝=0 <-> 0=1 とすれば、成り立つ。G は =(0, 1) のゲーデル数。
あるいは、1=1 という G <-> B(⌜G⌝) なる B は決まるか？ y=⌜1=1⌝ とすれば、両辺とも、恒真。
G に、 B がエンコードされてないと、意味ないんじゃない？
p.224
undecidable な文：真とも偽とも prove できない文。
p.273
補題２１．９の証明で挫折していたら、Monadic Predicate Logic is Decidable -
http://homepages.abdn.ac.uk/k.vdeemter/pages/teaching/CS3518/abdn.only/MonadicFOPL.pdf
を読んで、わかった。
述語２つが and 他で組み合わさっている論理式なら、 2^2==4 の要素を持つ集合が、モデルになることができる。４カラムの真理値表を書けば、真になるか有限ステップで判断できる。当たり前。
今まで、決定不可能、と結論したいくつかの証明の、どこかのステップが、１つしか引数を取らない述語だと変わってくるはずですよね。チューリングマシン、再帰関数、あと、まだ何かあったな。
as, bs, us, vs は、サブスクリプトでなくて、複数形。as は、 a1, a2, のこと。
a1, ...,as, R(u1, ..., us) なんて、説明なしに使われてもわからない。 s は、R の自由変数の数。a, b は、R に代入する定数。S は文だけど、その断片の自由変数を含む論理式 R でまず、証明をする。 s=0 は、自由変数なしなので文になる。それには、R が S 自身である場合も含む。
補題２１．９ 簡単な例を考える。
P(x) := x % 2 == 0, Q(x) := x % 3 == 0, S := Pa & Qb k=2, r=0, M は自然数。a=2, b=3 はモデル。a=100, b=33 でもよい。
signature σ(1)=={0, 0} σ(2)=={1, 0} σ(3)=={0, 1} σ(4)=={1, 0} σ(6)=={1, 1}, 2 is similar to 4
N := {1, 2, 3, 6} とする。2^2 の要素で、十分。N is a model of S.
変数がない時、 R(u1, .. us) はどうするの？ExEy P(x) & a=x & Q(y) & b=y なのか。
We claim (a1, a2) in M satisfy R iff (b1, b2) in N satisfy R. なお、 a1, a2 matche b1, b2.
(100, 33) は、(2, 3) in N にマッチする。
あれ、変数がなくて、k 個の命題だけならば、 2^k 要素の equivalent class がモデルになることは自明なのか。
まあいいや。
２１．１０の例
等式しか無い文。 ExEy x=y, ExEy x!=y, ExEyEz x!=y & y!=z & z!=x, AxAy x=y なるほど。３変数なら、最大３つの要素があれば、モデルになる。
ExEy x!=y を考える。シグネチャは、() だけで、全ての数は similar。M は自然数。{100, 33} はモデル。equivalent class は１つだけで、M の全部が入る。N := {1, 2} とする。
subformula R(u1, u2) := u1!=u2
We claim (a1, a2) in M matches (b1, b2) in N => as satisfy R iff bs satisfy R.
(100, 33) と (1, 2) はマッチして、どちらも R を充足する。(100, 100) はマッチしないし充足しない。そりゃそうだ。
ExEy x!=y の subformula は、自身と、x!=y、Ey x!=y
x!=y の場合は (a1, a2) match (b1, b2) の時だけ、充足する。 ~Q の説明。
Ey x!=y の場合は Ey a1!=y iff Ey b1!=y を示す必要がある。
if direction の証明。
if (b1, b2) satisfy Ey b1!=y for all b2 in N, then (a1, a2) satisfy Ey a1!=y for all a2 in M.
Therefore, a1, b1 がマッチする場合（シグネチャが無くて、シーケンスが１つだから、必ず、マッチする）、for any a2 in M, there is a b2 in N such that (a1, a2) match (b1, b2) を示せば十分。帰納法の仮定によりマッチしていれば、充足するから。
重複がある場合つまり、 a2==a1 なら、 b2==b1 にすればいい。
ない場合 a2 は今は一つしか無い同値類に属し、 a1!=a2 で t=1. マッチする b2 を探したい。b2!=b1 である必要がある。N には r 個の要素があるから、b2 は存在する。
証明終わり。
何をやってたんだっけ。等号だけを含む３変数の一階述語論理は、３要素のモデルを持つ。
p.285
problem 22.2
official errata にもあるが、かっこが抜けている。
R*ab := ∀X[(Xa &∀x∀y((Xx & Rxy)→Xy))→Xb]
(a), (b) は、機械的な式の変形で、 P or !P が出て、 valid とわかる。22.3, 22.4 は、まるでわからん。
２３章
23.1 Theorem. For each n, Vn is arithmetically definable.
わからん。ので、整理。
arithmetically definable：自然数の関係や部分集合と、対応する、Q の論理式がある。
と、何が嬉しいの？
p.222
17.3 Theorem (Tarski’s theorem).
Q で真である文のゲーデル数の集合は、算術的に定義可能でない。
なぜ？
17.2 Lemma.
Q の theorem のゲーデル数の集合は、定義可能でない。
なぜ？
対角化補題によって、こういう、G があり、G は theorem であるとしてもないとしても矛盾になる。
対角化補題ってなんだっけ。
p.221
17.1 Lemma (Diagonal lemma).
どんな論理式 B(y) でも、 |-G <-> B(⌜G⌝) となる文 G がある。
で、p.287 に戻ると、複雑さが有限なら、算術的に定義可能。
23.1 Theorem. For each n, Vn is arithmetically definable.
Vn とは
By Vn we mean the set of code numbers of first-order sentences of L of complexity ≤n that are true in N.
(1) L の文のコード番号の集合 S は再帰的だ。
(2) n の論理演算子を持つ文のコード番号の集合 Sn は再帰的だ。
(1) の証明は、
p.189
15.2 Proposition. The sets of formulas and of sentences are recursive.
ent, neg, disj などの、再帰関数を使って、任意の文をエンコードできるから。
p.287
The sets above all being recursive, they are definable in arithmetic and indeed in Q, and the functions are representable.
再帰関数だから、算術的に定義可能である。そして、representable である。
再帰は、算術的？
p.201
16.4 Lemma. Every recursive function f is ↑-arithmetical.
p.203
16.6 Lemma (a) Every recursive function f is arithmetical.
なんで？
再帰関数の基本、ゼロとか、サクセサは、論理式で書くことができるのを、例で示した。
あと、合成や g, h を使う再帰定義も、論理式で書き下した。
そして、representable？
関数 f が representable とは
p.207
f is representable in T if there is a formula F(x, y) such that whenever f (a) = b, the following is a theorem of T
∀y (F(a, y) <-> y=b)
論理式に置き換えられる。
By contrast, definability would only require that we have the positive assertion
representable の方が、対応が強い。
否定を表す再帰関数νに対して、論理式 Nu(x, y) がある。
あれ、全ての文は、再帰関数で表現可能だから、算術的に定義可能でない？
p.189
15.5 Corollary (Gödel completeness theorem, abstract form). The set of valid sentences is semirecursive.
いいえ。文は算術的に定義可能だが、正しい文は、semirecursive なだけ。
正しい文は、タルスキの定理によって、算術的に定義可能でないけれど、論理式の数が有限なら、原子論理式と論理式 Nu(x, y) などから算術的に定義可能なままで構成できるというのが、ここのテーマ？
semirecursive と recursive の違いは、大きい。前者は決定不可能。
(7)が、決定的に重要。atomic sentence は、正しいけれど、再帰であると言っている。なぜ、semirecursive から一歩ジャンプできたかというと、否定も semirecursive と言えるから。
なんで？
atomic sentence とは？
p.114 述語と定数からだけなる文。
その後は、複雑さに関する帰納法。
forcing, 強制法の話は、あきらめた。いずれ、きちんと集合論の本を読むことにして、先に進む。
https://www.amazon.co.jp/%E9%9B%86%E5%90%88%E8%AB%96%E2%80%95%E7%8B%AC%E7%AB%8B%E6%80%A7%E8%A8%BC%E6%98%8E%E3%81%B8%E3%81%AE%E6%A1%88%E5%86%85-%E3%82%B1%E3%83%8D%E3%82%B9-%E3%82%AD%E3%83%A5%E3%83%BC%E3%83%8D%E3%83%B3/dp/4535783829 - 集合論―独立性証明への案内 ケネス キューネン。定番だそうな。
Forcing 入門 渕野 昌
http://fuchino.ddo.jp/kobe/forcing-LN-2015.pdf
これ、いい。行間が狭くて、独習者にやさしい。演習問題もたくさんある。解答はない。現時点では未完成で、forcing はまだ、出てこない。けど、集合論の教科書として、とてもありがたい。
Forcing 入門 渕野 昌 errata 誤植 2017 年03 月20 日(08:46) 版
演習問題1.2 (3) exerc-1
read ϕ(b, a1 for
ϕ(b, a0, ..., an) となるような
演習問題1.8 ( i ) exerc-2-0
read ω \ ∅ for
すべてのn ∈ ω \ {∅}
演習問題1.11 exerc-3
read (4) for
(3) すべてのf, x に対し，f ′′x
p.10
read range(f) = y for
あるx, y に対してf : x → y のとき，dom(f) = y となるとき，f はx からy への上射である
read x for capital X
n-組の全体からなる集合xn はn からX への関数の全体nx と同じ集合
pair-1
read ω<X for
これをω>X とも表わすことにする．
p.17 和集合の公理
read u ε x ∧ z ε u
for u ε x ∧ y ε u
冪集合公理
read ε for u ε z → u ∈ y
ここは、∈ と書かないで、ギリシア文字のイプシロン、ε なのですよね。
p.18
∃!xϕ は「ϕ を満たす対象x がちょうど一つ」の説明の、∀x∀y (ϕ(x, ...) ∧ ϕ(y/x, ...)) の部分、なんか変ですよね。一つしか無いことをあらわすなら、~ ∃y(ϕ(y/x) & x!=y) でしょうか。
read 関係記号 for L にこの関数記号を加えて
Forcing 入門 渕野 昌 errata 誤植 終り
こっちは、定理１の証明で、１０箇所以上、追えないところがあって速攻で挫折した。
http://fuchino.ddo.jp/shizuoka/forcing2010.p
２７章、様相論理と証明可能性について。
数学基礎論サマースクール 2015 証明可能性論理１ 倉橋 太志 http://www2.kobe-u.ac.jp/~mkikuchi/ss2015kurahashi1.pdf
いちおう読了。うーん。このくらいのレベルかもうちょっとやさしい、日本語の本を探してみよう。
と、思ったのだが、手近に適当なものが無いので、もう一回り、読むことにした。今回は、きちんと、奇数番号の問題をやる。できるだけ。
独習するのに困るでしょ。インストラクターズマニュアルB、売ってくださいよ。＞ Burgess 先生
と、思ったら、近所の図書館で、野矢茂樹 論理学と、内井惣七 真理・証明・計算 が手に入った。パラパラ見た。うーん。もう一回り、を続けよう。つまり、これらは、戸田山本と、 computability 本の間を埋めるものではない。
以下、お世話になりました。
https://ja.wikipedia.org - 論理学の記事が異様に詳しくない？
照井一成先生、渕野昌先生、インターネット上の講義ノート、ありがとうございました。論理学、集合論の教科書を書かれたら、必ず、購入して勉強させていただきます。
以上