"Toward a forcing model construction of H"

今朝、メールが届き、9月にプラハで開かれる国際会議　"Logic Algebra and Truth Degrees 2010" にアクセプトされたとの通知を受けました。
これは、Lukasiewicz無限値述語論理　∀Ł 上、包括原理を持つ集合論 H について、モデルを強制法で構成する方法について予備的考察を加えるという話です。Hは、これまでもっぱら統辞論的に取り扱われてきましたが、モデルを柔軟に構成することが可能になれば、その研究が進むと期待されます。

以下、要旨の第一章に相当する文章を掲載します。お暇な方はどうぞご覧下さい。

The study of a logical theory of circularity is important not only in logic but also in computer science. For, one of the key concepts, recursion, has a circular nature since: to calculate the value of 4 + 3, we should calculate the value of 4 + 2. However, it is well-known that the full form of circularity implies a contradiction, e.g. Russell paradox: the comprehension principle, it guarantees the existence of term {x : P(x)} for any formula P(x), implies a contradiction (an infinite loop R ∈ R → ¬(R ∈ R) → R ∈ R → … ) in classical logic. Therefore we have to restrict the form of recursion to have a consistent theory if we keep classical logic.

It is known that the comprehension principle does not imply a contradiction in many non-classical logics by paying a cost of weakening logical rules. These theories allow a very strong form of circularity, namely a general form of the recursive definition: a term θ, such that θ =ext {u : P(u, θ)} for any formula P(x, y), can be defined in a set theory with the comprehension principle within Grisin Logic (classical logic minus the contraction rule) [Can03]. This allows us, for example, to define a set ! of natural numbers and to make any recursive function numerically representable, therefore we can develop arithmetic to some extent. Such form of circularity is not only interesting as itself, but also worth studying, for it is an ideal generalization of a recursion in classical recursion theory.
Generally speaking, it is very difficult to construct a model of a theory which allows a strong form of circularity is really difficult (remember, it takes time to construct a domain model of λ-calculus). H is a typical case: H is a set theory with the comprehension principle within Łukasiewicz infinite-valued predicate logic 　∀Ł. H is known as one of the strongest theory in which the comprehension principle does not imply a contradiction, therefore H shows the limit of the consistency of the general form of recursive definition, and as we remarked, this makes difficult to prove the consistency of H. In 1957 Skolem [Sko57] conjectured that the comprehension principle does not imply a contradiction within 　∀Ł. Skolem, Chang [Cha63] and Fenstad [Fen64] proved it when the principle restricted to formulae with quantifier in a few special forms. However they could not prove the whole consistency of H because they failed to construct a model of full H.

The aim of this paper is to try to introduce a method of constructing a natural model of the set theory H. Only known model of H is an infinite set of sentences whose truth value are 1 constructed by a proof theoretic way [Whi79]. Since 8Ł is defined by its models by one’s nature, treating H via models should be a more natural way. We review a new construction method, forcing in ZFC: we discuss how it can be applied to construct a model of Hqf , and a possibility to extend the result to construct a model of full H.