夜も眠れなくなることをここにまとめておく．
定期的に気になって，そのたびに考えて納得して，しばらく経ってまた気なって，をずっと繰り返している． そろそろ専門家に教えを請いに行かねばならない．
完全性定理と循環論法と超数学
Quoraにおける渕野昌さんの回答集
- 述語論理の完全性定理の証明などに集合論を使うのは循環しているのではありませんか？自己回答の形で質問を補足します．
- 論理学を議論するとき、それはメタ言語を使うということですか？
- 完全性定理の対象となる理論はモデルを持ちますが、逆にモデルを持つ理論で「不」完全性定理の対象となる理論はありますか？
- 仮にヒルベルトプログラムが正しければ、すべての理論にはモデルが存在することになるのでしょうか？言い換えると、不完全性定理はモデルが存在しない理論の存在を示した定理ということなのでしょうか？
- 数学の論理って真理値を使う方法と推論規則を使う方法があると思いますが、どっちでもいいんですか？
渕野昌さんによる説明
述語論理の完全性定理では，理論のモデルを考えなくてはいけなくなるわけですが，一般には，無限の（つまり underlying set が無限の）モデルを考えなくてはならなくなるので，何らかの「集合論」の枠組みの中で議論せざるを得なくなります． そのため，循環を完全に避けることは，いずれにしても不可能です． だから，ここでの問題は，循環を完全に避けることではなく，どのくらい軽微な循環で，後で集合論をその上に展開することになる，metamathematicsでの論理に対する完全性定理（と，その帰結，特に，一階の述語論理での証明の体系が「完全」なものになっていて，新たに推論規則や論理公理を付け加える必要がないこと – 付け加えて証明の効率は変わる可能性があるとしても，論理的に証明できるかできないか，ということに関しては何も付け加わらないこと）が証明できるか，ということになります．
逆数学と呼ばれる分野での研究から，$\mathrm{WKL}_0$と呼ばれる二階の算術の体系で，この意味での完全性定理が証明できることが知られています． $\mathrm{WKL}_0$は，無限二分木に無限枝が存在することに対応する公理を持つ弱い二階算術の体系ですが，Henkinの完全性定理の証明での，証明木を遡ってその無限枝からモデルを構成する証明法が遂行できることが，この公理によって保証されることから，無矛盾な理論のモデルに対応する二階のobjectの存在証明が，この体系でできることになります．
$\mathrm{WKL}_0$はconsistency strengthに関しては，弱い体系です． 例えば，Peano arithmeticが無矛盾なら，この公理系は無矛盾であることが示せます． Peano arithmeticには，Gentzenの無矛盾証明など，有限の立場の自然で妥当と言える拡張での無矛盾性証明が存在するので，この理論体系で証明できたことの帰結のうち methamathematics で解釈できることについては，methamathematics での立場でも「正しい」ことの保証が十分にされていると考えて問題なさそうに思えます． その意味で，この$\mathrm{WKL}_0$で完全性定理が証明できることは，この後，完全性定理の知見を足がかりにして一階の論理の上に集合論の公理系をベースとした数学の体系を構築することの妥当性の保証になっていると，ぎりぎりで解釈できる状況を作っている，と考えられます．
一方，一般的な（例えば非可算な公理系も対象として含めた）完全性定理が，モデル理論でのような完全性定理の応用で必要になるわけですが，この一般化された完全性定理は，集合論の中で展開されているもので，例えば，そこで「すべての論理式」と言った時には，これは，metamathematicsでの具体的に与えられた表現としての論理式の一つ一つという意味ではなく，集合論の中で（例えば$\omega$の部分集合として定義された）論理式（のコード）の全体からなる集合の全ての要素に対して，という意味です．
上で書いたことから数学の基礎づけを，次のように捉えることができるようになります： Metamathematicsから出発して，とりあえず（既存の一階の述語論理の論理体系を使って）$\mathrm{WKL}_0$で議論をする． 上で述べた説明から，$\mathrm{WKL}_0$で （そこで記述できる分の）一階の述語論理の完全性定理が得られるが，この，$\mathrm{WKL}_0$の無矛盾性が有限の立場に準ずる立場で証明できることから，そこでの完全性定理（命題が公理系から証明できなかったときには，そのことの反例となるモデルが構成できる）は，metamathematics での厳密な解釈でも「正しい」定理となっている，と考えてよいものになっている． ただし，この「命題が公理系から証明できなかったときには，そのことの反例となるモデルが構成できる」自身は，$\mathrm{WKL}_0$での定理だとしても，上で議論したように，metamathematicsで記述できる主張ではない． そこで，この定理の帰結の一つである，「一階の述語論理の証明の体系に，新しい論理公理や推論規則を更に付加する必要がない」，というmetamathematicsでも表明することのできる知見を，methamathematicsに持ち帰る． この知見を議論の支えとして，数学を展開するために十分な理論体系（ZFC集合論，その何らかのfragmentあるいは逆にその何らかの拡張）を固定して，この数学理論で証明できることは，この固定された公理系から，一階の述語論理の証明の体系を使って証明のできることのことである，として，数学をそこで展開する，あるいは，そのような体系についての metamathematicalな考察をする．
証明の体系が固定されて，それが，この，「一階の述語論理の証明の体系が，新しい論理公理や推論規則を更に付加する必要がない」ものになっているということから，このmetamathematicalな考察で，ある命題の数学の体系からの独立性が証明されたときには，それは，一階の述語論理の証明の体系の不備に起因するものでなく，その命題や数学の体系に起因するものであることが帰結できる
参考文献
- Cori-LascarのMathematical Logicの序文での説明は腑に落ちる．
So there is no vicious circle. Rather than a circle, imagine a helix (nothing vicious there!), a kind of spiral staircase: we are on the landing of the $n$th floor, where our mathematical universe is located; call this the ‘intuitive level’. Our work takes us down a level, to the $(n-1)$st floor, where we find the prototype, the reduced model; we will then be at the ‘formal’ level and our passage from one level to the other will be called ‘formalization’. What is the value of $n$? This makes absolutely no difference; there is no first nor last level. Indeed, if our model is well constructed, if in reproducing the mathematical universe it has not omitted any detail, then it will also contain the counterpart of our very own work on formalization; this requires us to consider level $n-2$, and so on. At the beginning of this book, we find ourselves at the intuitive level. The souls that inhabit it will also be called intuitive objects; we will distinguish these from their formal replica by attaching the prefix ‘meta’ to their names (meta-integers, meta-relations, even meta-universe since the word ‘universe’ will be given a precise technical meaning in Chapter 7). We will go so far as to say that for any value of $n$, the $n$th level in our staircase is intuitive relative to level $(n-1)$ and is formal relative to level $(n+1)$. As we descend, i.e. as we progress in our formalization, we could stop for a rest at any moment, and take the opportunity to verify that the formal model, or at least what we can see of it, agrees with the intuitive original. This rest period concerns the meta-intuitive, i.e. level $(n+1)$.
- CohenのSet theory and the continuum hypothesisには次のように書かれている．
(p.3) By a formal system we shall mean a finite collection of symbols and perfectly precise rules for manipulating these symbols to form for manipulating these symbols to form certain combinations called “theorems”. Of course, these rules must be given in informal mathematical language. However, we shall demand that they be completely explicit rules requiring no infinite processes to check and that in principle they can be coded into a computing machine. In this way questions concerning infinite sets are replaced by questions concerning the combinatorial possibilities of a certain formal game. Then we will be able to say that certain statements are not decidable within given formal systems.
(p.3) If we examine Peano’s axioms for the integers, we find that they are not capable of being transcribed in a form acceptable to a computing machine. This is because the crucial axiom of induction speaks about “sets” of integers but the axioms do not give rules for forming sets nor other basic properties of sets. Here is an example of the difficulty in satisfying the stringent requirements for a formal system outlined above. When we do construct a formal system corresponding to Peano’s axioms we shall find that the result can not quite live up to all our expectations. This difficulty is associated with any attempt at formalization.
(p.4) In any given discussion one may need arbitrarily many variables so that we shall use $x, x’, x’’, \dots$ as symbols for variables. In practice we will use the letters $x_1, x_2, x_3, \dots$ or $x, y, z$ although in theory these should be replaced by $x, x’, x’’, \dots$. In this way we need only a finite set of symbols.
(p.5) To each $R_i$ is assigned an integer $n_i \ge 1$, $n_i$ intuitively indicating that the relation represented by $R_i$ is a relation between $n_i$ objects.
(p.8) The object of mathematics is to discover “true” theorems. We shall use the term “valid” to describe statements formed according to certain rules and then shall discuss how this notion compares with the intuitive idea of “true”.
(p.11) Having now given rules for forming valid statements we come to the problem of identifying these statements with the intuitively “true” statements. This discussion will be carried out in the spirit of traditional mathematics, that is to say, outside of any formal language. We shall use some elementary notions of set theory. After we have formalized set theory itself, then of course this discussion can be expressed in that formal system. In our original discussion, we had a finite number of symbols. This was important for foundational purposes, in order to reduce mathematics to a formal game playable by a computing machine. However, for some purposes it is of interest to allow arbitrarily many constant and relation symbols. We write the proofs of Sections 4 and 5 for this more general case.
(p.13) The proof uses the axiom of choice (unless the set $S$ is already well-ordered). Given $S$ we shall explicitly show how to construct a model for $S$. The proof however is non-constructive in the sense that the construction of the model for $S$ may depend upon examining an infinite number of possibilities. Nevertheless, if $S$ is finite, the model can be taken as the set of integers and the resulting relations will be arithmetically definable (i.e, definable by formulas using only addition and multiplication). This will follow from the form of the proof although we shall not go into the matter.
(p.17) This corollary shows that no system of axioms can have a unique model (up to isomorphism) unless this unique model is finite. So one sees that the usual systems of mathematics such as the integers and real numbers, which presumably have only one model, cannot be described completely by any formal system of axioms. As mentioned, if one looks at the classical axioms for these systems, one sees that they are not formal systems in our sense, since they speak informally about the set concept. Later the incompleteness theorem will show us that in an even more modest sense of the word, the axioms for mathematics cannot be complete.