まえがき

小野勝次先生が 2001 年 8 月 18 日に永眠されてから２年以上の年月が経ってしまいました．ようやく昨年５月から６月にかけて静岡で開催された「小野勝次先生追悼シンポジウム」の講演記録集が完成しました．この記録集は講演者が書いたものと記録係が L^{A}TEX 化したノートに講演者が手を入れたものとがあります．シンポジウム終了後に田中尚夫先生から送っていただいた追悼文も収録してあります．

全ての講演者が小野勝次先生との思い出を語り，講演内容も何らかの意味で先生の仕事と関連のあるものが多くありました．シンポジウムを有意義なものにしてくださった講演者および参加者の皆さんに感謝いたします．また，記録係の長新人さん (千葉大学自然科学研究科大学院生) と本記録集作成の最終段階でお世話になった鈴木信行さん (静岡大学) に感謝いたします．

この記録集を手にとり小野先生と追悼シンポジウムのことを思い出していただければ幸いです．

2003 年 10 月

「小野勝次先生追悼シンポジウム」世話人梅沢敏郎，太田稔，古森雄一，佐藤雅彦，白井古希男

小野勝次先生追悼シンポジウム

日時: 2002 年 5 月 31 日 (金) ・ 6 月 1 日 (土) 場所: 静岡大学大学会館研修室

                             http://www.shizuoka.ac.jp/campus1.html

プログラム

5 月 31 日 (金) 14:00〜17:45

14:00〜14:30 太田稔小野先生の業績と私 14:30〜15:00 小野寛晰 An algebraic proof of cut elimination theorem 15:00〜15:30 河原康雄 Tarski’s fixed point theorem in Dedekind categories

15:30〜15:45 休憩

15:45〜16:15 高橋正子論理学の歴史とコンピュータ 16:15〜16:45 村田全数学的連続性から哲学的連続性へ 16:45〜17:15 古森雄一古典論理の自然推論 17:15〜17:45 佐藤雅彦概念と対象の理論について

18:00〜懇親会場所：静岡大学大学会館食堂

6 月 1 日 (土) 10 ： 00〜12:00

10:00〜10:30 八杉満利子実効的収束について 10:30〜11:00 大芝猛 multi-modal logics の Shannon type 標準形展開による特性化 11:00〜12:00 角田譲抽象設計論

参加者

大西正男松本和夫角田譲田中義人古森雄一
白井古希男佐藤雅彦長新人近藤通朗青山究
鈴木康人村上祐子永島孝鈴木信行桜井貴文
小方一郎中戸川孝治廣川佐千男河原康雄橋本安司
小野寛晰大芝猛田中尚夫春藤修二塩谷賢
竹内外史三浦聰大濱茂生太田稔村田全
久馬栄道鹿島亮高橋正子下田守河田賢二
千谷慧子渕野昌五十嵐真奈八杉満利子志村立矢

梅沢敏郎以上 (敬称略)

目次

小野先生の業績と私 1 太田稔

An algebraic proof of cut elimination theorem (oultine) 3 小野寛晰

Tarski’s Fixed Point Theorem in Dedekind Categories 9 河原康雄

論理学の歴史とコンピュータ 15 高橋正子

数学的連続性から哲学的連続性へ 27 村田全

古典論理の自然推論 35 古森雄一

概念と対象の理論について 37 佐藤雅彦

Effective Convergence 51 八杉満利子

Multi-modal logics の Shannon type 標準形展開による特性化 55 大芝猛

小野勝次先生へのオマージュ 65 田中尚夫

小野先生の業績と私

太田稔 (愛知教育大学名誉教授)

あいさつ • 小野先生の業績の広さ

小野勝次先生との出会い • 教養学部数学コンクール

• 転学部・編入試験

• 大学院教育

• 情報・教育の世界

• 20 世紀の巨人 B. Russell, K. Ono

• 21 世紀を見た人, 3 千年紀の情報世界, 教育・後継育成

Russell-Type Paradoxes • ¬(∃p)(∀x)(x ∈ p ↔ R(x))

• 弱い論理体系

• Primitive Logic エピソード

• 数学振興会主催シンポジューム, 日本数学会

• アメリカにおける集合論シンポジューム

• Abstraction Principle と集合論

論理の実用的記述法 • Ono の PD

• 論理教育, カッコ付き演繹

• 辞書式順序と記述法

• LK との構造的思考的考察

小野先生からの影響 • 慈父の教育, 学校数学発展研究会, 日本数学コンクール • 自由

• スポーツ, 肉体運動の大切さ, 環境活動

• 創造

An algebraic proof of cut elimination theorem (oultine)

To the memory of my father, Katuzi Ono

Hiroakira Ono Japan Advanced Institute of Science and Technology, Japan

                          e-mail ono@jaist.ac.jp

We will give here a purely algebraic proof of cut elimination theorem, based on the idea by Maehara [M91] and Okada [Okada96]. The author has been inspired by discussions on this subject with P. Jipsen, whom and whose joint paper with Tsinakis [JT] he owe much.

Here, we will give a proof of cut elimination theorem for FL_{ew} as an example, but our idea seems to work also for most of sequent systems, including LK and LJ, for which we have syntactic proofs of the cut elimination theorem.^{1}

1 Semi-residuated lattices

In the rest of this paper, by a residuated lattice we mean a commutative, integral residuated lattice with the least element 0 and the greatest 1, except Lemma 2. By RL, we mean the class of all residuated lattices. An algebra A = ⟨A, ⪯, ∧, ∨, ·, →, 0, 1⟩ is a semi-residuated lattice^{2} if it satisfies the following conditions;

1. ⟨A, ·, 1⟩ is a commutative monoid with the unit 1 (in the following we will write xy instead of x · y),

2. ⪯ is a reflexive relation on A satisfying the following SRL conditions:

• 0y ⪯ x, and x ⪯ 1,

• x ⪯ y ⇒ xz ⪯ y,

• x ⪯ y and u ⪯ w ⇒ xu ⪯ yw,

• x ⪯ y and zu ⪯ w ⇒ (y → z)xu ⪯ w,

• xy ⪯ z ⇒ x ⪯ y → z,

• xu ⪯ w and yu ⪯ w ⇒ (x ∨ y)u ⪯ w,

• x ⪯ y ⇒ x ⪯ y ∨ z,

• x ⪯ z ⇒ x ⪯ y ∨ z,

• xu ⪯ w ⇒ (x ∧ y)u ⪯ w,

• yu ⪯ w ⇒ (x ∧ y)u ⪯ w,

• x ⪯ y and x ⪯ z ⇒ x ⪯ y ∧ z.

Let SRL be the class of all semi-residuated lattices. It is clear that any residuated lattice with the lattice order ≤ is a semi-residuated lattice. Conversely, if ⪯ is a partial order in a semi-residuated lattice A, then A is a residuated lattice with the lattice order ⪯. A key point of this proof lies in the fact that we need the transitivity in proving x ⪯ y → z ⇒ xy ⪯ z.

1For the details, see the draft [BJO] by F. Belardinelli, P. Jipsen and the present author.

2We need to find a better prefix, e.g. transitivity-free(?), instead of “semi”.

2 Cut elimination theorem

The above remark implies that for all terms s and t, if an “inequality” s ⪯ t holds in every A ∈ SRL then s ≤ t holds in every B ∈ RL. Our main theorem, Theorem 2.3, says that the converse holds also. This is an algebraic expression of cut elimination theorem for FL_{ew}.

We will first give a general way of constructing a residuated lattice from a given commutative monoid. Let M = ⟨M, ·, 1⟩ be any commutative monoid. A unary function C on ℘(M) is a closure operator if it satisfies 1) X ⊆ C(X), 2) CC(X) ⊆ C(X), 3) X ⊆ Y implies C(X) ⊆ C(Y), and moreover 4) C(X) ∗ C(Y) ⊆ C(X ∗ Y), for all X, Y ∈ ℘(M). Here, W ∗ Z = {wz : w ∈ W, z ∈ Z}. A subset X of M is C-closed if C(X) = X. Let C(℘(M)) denote the set of all C-closed subsets. Define operations ∪_{C}, ∗_{C} and ⇒ on C(℘(M)) as follows. For all C-closed sets X and Y;

• X ∪_{C} Y = C(X ∪ Y),

• X ∗_{C} Y = C(X ∗ Y),

• X ⇒ Y = {z : X ∗ {z} ⊆ Y }.

Then we have the following (see e.g. Lemma 7.2 in [JT] and [Ono01]).

Lemma 2.1 The algebra C_{M} = ⟨C(℘(M)), ∩, ∪_{C}, ∗_{C}, ⇒, C(Ø), C({1}), M⟩ forms a commutative residuated lattice with the lattice order ⊆ and with the unit element C({1}). Hence, it is a commutative integral residuated lattice, if C({1}) = M.

As a special case, let us take a semi-residuated lattice A for a commutative monoid M. Following the notations in [JT] by Jipsen and Tsinakis, for each x, y ∈ A, define

[x; y] = {w ∈ A : xw ⪯ y}.

The set B of all subsets of A of the above form makes a closed base. We note that the closed base B depends on the relation ⪯. So, sometimes we call B, the closed base determined by A or simply the closed base determined by ⪯. By using B we can define a closure operator C (in the usual sense) on ℘(A) by

C(X) = ⋂{[x; y] : X ⊆ [x; y] for x, y ∈ A} for each subset X of A.

We can show moreover that C satisfies the fourth condition in the definition of closure operators (in our sense). Since C({1}) = A holds for our C, C_{A} becomes a commutative, integral residuated lattice. This residuated lattice C_{A} is uniquely determined by A, and is called the quasi-completion of A. In fact, the following Theorem 2.2 will explain why we call it in this way.

Let us define a map k : A → C(℘(A)) by k(u) = [u], where [u] = [1; u], i.e. [u] = {w ∈ A : w ⪯ u}. The following theorem can be shown essentially in the same way as the proof of Lemma 7.3 in [JT] (see also Maehara [M91] and Okada [Okada96]).

Theorem 2.2 Suppose that u, v ∈ A and that U and V are arbitrary C-closed subsets of A such that u ∈ U ⊆ k(u) and v ∈ V ⊆ k(v). Then for each ⋆ ∈ {∧, ∨, ·, →}, u ⋆ v ∈ U ⋆_{C} V ⊆ k(u ⋆ v), where ⋆_{C} denotes ∩, ∪_{C}, ∗_{C} and ⇒, respectively. Thus, in particular u ⋆ v ∈ k(u) ⋆_{C} k(v) ⊆ k(u ⋆ v).

Now we will show our main theorem.

Theorem 2.3 For all terms s and t, if s ≤ t holds in every B ∈ RL, then s ⪯ t holds in every A ∈ SRL.

This theorem follows immediately from the next lemma.

Lemma 2.4 For given terms s and t, if s ⪯ t doesn’t hold in a semi-residuated lattice then s ≤ t doesn’t hold in its quasi-completion.

We will give a proof of the above lemma. Suppose that s ⪯ t doesn’t hold in a semi-residuated lattice A. Then, there exists a valuation f on A such that f(s) ⪯ f(t) is not true in A. We take the quasi-completion C_{A} of A which is a commutative, integral residuated lattice. We define a valuation g on C(℘(A)) as follows. For each variable q appearing either in a term s or t, g(q) = k(f(q)). (For constants 0, 1 we suppose that f(0) = 0 and f(1) = 1 for f, and define that g(0) = CØ(⊆ k(0)) and g(1) = k(1)(= A).) Then, using Theorem 2.2, we can prove the following by induction on the length of the term r.

Lemma 2.5 For any subterm r of s or t, f(r) ∈ g(r) ⊆ k(f(r)).

Suppose that s ≤ t holds in C_{A}. Then g(s) ⊆ g(t). Using Lemma 2.5, we have f(s) ∈ g(s) ⊆ g(t) ⊆ k(f(t)). Thus, f(s) ⪯ f(t). But this contradicts our assumption. Therefore, the inequality s ≤ t doesn’t hold in the residuated lattice C_{A}. This completes the proof.

Corollary 2.6 For all terms s and t, s ≤ t holds in every B ∈ RL iff s ⪯ t follows from the system of “inequalities” described in the definition of semi-residuated lattices ( with the “axiom” x ⪯ x), i.e. s ⪯ t is “cut-free” provable in FL_{ew}.

3 Dedekind-MacNeille completion

Let us consider the case where ⪯ is moreover transitive. Then, each [x; y] is downward closed, i.e., if w ∈ [x; y] and z ⪯ w then z ∈ [x; y]. Therefore, each C-closed set is also downward closed. Then, u⋆v ∈ k(u)⋆_{C} k(v) in Theorem 2.2 implies k(u⋆v) ⊆ k(u)⋆_{C} k(v). Hence, we have k(u⋆v) = k(u)⋆_{C} k(v). Also, it is clear that k is injective. Thus, we have the following.

Corollary 3.1 When A is a residuated lattice, the map k defined by k(u) = [u] for each u ∈ A is an embedding of A into C_{A}.

In any residuated lattice, [x; y] = [1; x → y] = [x → y] holds. Therefore, the closure operator C defined before can be expressed as

C(X) = ⋂{[u] : X ⊆ [u] for an element u ∈ A} for each subset X of A.

In other words, C(X) = ((X)^{→})^{←}, where (Y)^{→} = the set of all upper bounds of Y, and (Y)^{←} = the set of all lower bounds of Y, for any subset Y of A. Thus the above corollary is a well-known result, which says that any residuated lattice A is embedded into its Dedekind-MacNeille completion C_{A}. (See e.g.

[Ono01] for complete embeddings.) Thus, we have the following.

Corollary 3.2 The quasi-completion of a residuated lattice is its Dedekind-MacNeille completion.

4 Finite model property

Along the line of the present paper, we will give a proof of the finite model property of FL_{ew}, which is obtained by modifying slightly the proof given by Okada-Terui in [OT99] (see also [L97]).

Since the set of all C-closed subsets is finite whenever the closed base is finite, we have the following lemma, by observing the way of construction of C_{A} in Section 2.

Lemma 4.1 Suppose that A = ⟨A, ⪯, ∧, ∨, ·, →, 0, 1⟩ is a semi-residuated lattice such that the closed base determined by ⪯ is finite. Then the quasi-completion C_{A} of A is also finite.

Let A = ⟨A, ⪯, ∧, ∨, ·, →, 0, 1⟩ be a semi-residuated lattice. For a given pair ⟨u, v⟩ of elements of A, predecessors of ⟨u, v⟩ are defined inductively as follows.

1. The pair ⟨u, v⟩ itself is a predecessor of ⟨u, v⟩.

2. Suppose that ⟨w_{1}, w_{2}⟩ is a predecessor of ⟨u, v⟩ and that for some u_{1}, u_{2}, v_{1}, v_{2} “u_{1} ⪯ u_{2} (and v_{1} ⪯ v_{2}) ⇒ w_{1} ⪯ w_{2}” is one of SRL conditions (for ⪯). Then every predecessor of ⟨u_{1}, u_{2}⟩ (and ⟨v_{1}, v_{2}⟩) is a predecessor of ⟨u, v⟩.

A finite subset S of pairs of elements in A is finitely based, if the set of all predecessors of some elements in S is finite.

Lemma 4.2 Let A = ⟨A, ⪯, ∧, ∨, ·, →, 0, 1⟩ be a semi-residuated lattice. For any finitely based subset S of pairs of elements in A, there exists a binary relation ⪯^{∗} on A such that

1. if ⟨u, v⟩ ∈ S then u⪯^{∗}v iff u ⪯ v,

2. the structure A^{∗} = ⟨A, ⪯^{∗}, ∧, ∨, ·, →, 0, 1⟩ forms a semi-residuated lattice,

3. the closed base determined by ⪯^{∗} of A^{∗} is finite.

This lemma says that any finitely based subset of A can be embedded into a semi-residuated lattice with a finite the closed base. Here we will show a proof. Let S^{†} be the set of all predecessors of S, which is finite by our assumption. We define a binary relation ⪯^{∗} on the set A as follows. For u, v ∈ A, if ⟨u, v⟩ ∈ S^{†} then u⪯^{∗}v iff u ⪯ v, and otherwise u⪯^{∗}v holds always. Clearly, this relation ⪯^{∗} satisfies the first condition of Lemma 4.2.

Next, we show that ⪯^{∗} satisfies all the SRL conditions. Suppose that a given SRL condition (∗) (for ⪯^{∗}) is of the form “u_{1}⪯^{∗}u_{2} and v_{1}⪯^{∗}v_{2} ⇒ w_{1}⪯^{∗}w_{2}”. To show that this holds, we suppose that w_{1}⪯^{∗}w_{2} does not hold. By the definition of ⪯^{∗}, this happens when ⟨w_{1}, w_{2}⟩ ∈ S^{†} but w_{1} ⪯ w_{2} does not hold. In this case, both ⟨u_{1}, u_{2}⟩ and ⟨v_{1}, v_{2}⟩ must belong to S^{†}. Since “u_{1} ⪯ u_{2} and v_{1} ⪯ v_{2} ⇒ w_{1} ⪯ w_{2}” is the SRL condition (∗) for ⪯ and hence it must be true, at least one of u_{1} ⪯ u_{2} and v_{1} ⪯ v_{2} does not hold. Therefore, at least one of u_{1}⪯^{∗}u_{2} and v_{1}⪯^{∗}v_{2} does not hold either. Thus, this condition (∗) is satisfied. Similarly, we can see that SRL conditions of other forms holds for ⪯^{∗}. Hence A^{∗} is a semi-residuated lattice.

The closed base determined by ⪯^{∗} consists of all sets of the following form, where x, y ∈ A ;

[x; y]^{∗} = {w ∈ A : xw⪯^{∗}y}.

Then, [x; y]^{∗} = A holds for all but finitely many pairs (x, y). In fact, if ⟨x, y⟩ ∉ S^{†} then ⟨xw, y⟩ ∉ S^{†} for any w, and hence xw⪯^{∗}y holds for any w. Thus, [x; y]^{∗} = A holds for any x, y such that ⟨x, y⟩ ∉ S^{†}. Thus, the closed base is finite.

Theorem 4.3 The logic FL_{ew} has the finite model property.

To show the theorem, suppose that s ≤ t is not provable in FL_{ew}. Then, s ⪯ t doesn’t hold in a semi-residuated lattice A. For such A, we can take in particular the free semi-residuated lattice whose universe is the set of all terms. Then, we show that the singleton set {⟨s, t⟩} is finitely based. To see this, define the “length” of a pair ⟨u_{1}, u_{2}⟩ to be the sum of lengths of terms u_{1} and u_{2}. Then, it is easily shown that for any given pair of terms, the length of any of its predecessor is shorter than its length. Using this, we have that {⟨s, t⟩} is finitely based. Then by Lemma 4.2, {⟨s, t⟩} is embedded into a semi-residuated lattice A^{∗} with a finite closed base (determined by ⪯^{∗}). Then by Lemma 4.1, the quasi-completion C_{A^{∗}} is finite. Moreover, since s⪯^{∗}t doesn’t hold in A^{∗}, s ≤ t doesn’t hold either in C_{A^{∗}} by Lemma 2.4. This completes the proof.

Remark. The essential part of the proof of Theorem 4.3 is to show that for any given pair of terms s and t, the set {⟨s, t⟩} is finitely based in the free semi-residuated lattice. In a syntactic term, this can be rephrased as: for any given sequent its proof-search tree is finite in the cut-free FL_{ew}. This will suggest how far our argument can be applied to other cut-free systems, in order to show their finite model property.

The above syntactic condition obviously implies the decidability of FL_{ew}. Thus, in the present case the decidability implies the finite model property, while usually the finite model property is proved in order to show the decidability.^{3}

References

[BJO] F. Belardinelli, P. Jipsen and H. Ono, Algebraic aspects of cut elimination theorem, draft, 2003.

[JT02] P. Jipsen and C. Tsinakis, A survey of residuated lattices preprint, 2002.

[L97] Y. Lafont, The finite model property for various fragments of linear logic, Journal of Symbolic Logic 62 (1997), pp.1202-1208.

[M91] S. Maehara, Lattice-valued representation of the cut-elimination theorem, Tsukuba Journal of Mathematics 15 (1991), pp.509-521.

[MOM97] R.K. Meyer, H. Ono and G.J. Massey, When decidability implies the finite model property: Inexpensive converses to Harrop’s theorem, note, 1997.

[Okada96] M. Okada, Phase semantics for higher order completeness, cut-elimination and normalization proofs (extended abstract), Electronic Notes in Theoretical Computer Science 3 (1996).

[OT99] M. Okada and K. Terui, The finite model property for various fragments of intuitionistic linear logic, Journal of Symbolic Logic 64 (1999), pp.790-802.

[Ono01] H. Ono, Closure operations and Complete embeddings, to appear in Studia Logica, 2003.

3This twisted situation was discussed already in [MOM97].

Tarski’s Fixed Point Theorem in Dedekind Categories

Yasuo Kawahara ^{4}

Tarski’s fixed point theorem for complete lattices is a fundamental theorem in lattice theory and very useful for computer science applications. This paper will show a general result in Dedekind categories, which extends the Tarski’s theorem.

1 Dedekind Categories

In this section we recall the definition of a kind of relation category which we will call Dedekind categories following Olivier and Serrato [3]. Dedekind categories are equivalent to locally complete division allegories introduced in [1].

Throughout this paper, a morphism α from an object X into an object Y in a Dedekind category (which will be defined below) will be denoted by a half arrow α : X ⇁ Y, and the composite of a morphism α : X ⇁ Y followed by a morphism β : Y ⇁ Z will be written as αβ : X ⇁ Z. Also we will denote the identity morphism on X as id_{X}.

Definition 1.1 A Dedekind category D is a category satisfying the following:

D1. [Complete Heyting Algebra] For all pairs of objects X and Y the hom-set D(X, Y) consisting of all morphisms of X into Y is a complete Heyting algebra (namely, a complete distributive lattice) with the least morphism 0_{XY} and the greatest morphism ∇_{XY}. Its algebraic structure will be denoted by

D(X, Y) = (D(X, Y), ⊑, ⊔, ⊓, 0_{XY} , ∇_{XY}).

D2. [Converse] There is given a converse operation ^{♯} : D(X, Y) → D(Y, X). That is, for all morphisms α, α′ : X ⇁ Y, β : Y ⇁ Z, the following converse laws hold: (a) (αβ)^{♯} = β^{♯}α^{♯}, (b) (α^{♯})^{♯} = α, (c) If α ⊑ α′, then α^{♯} ⊑ α^{′♯}. D3. [Dedekind Formula] For all morphisms α : X ⇁ Y, β : Y ⇁ Z and γ : X ⇁ Z the Dedekind formula αβ ⊓ γ ⊑ α(β ⊓ α^{♯}γ) holds. D4. [Residue] For all morphisms β : Y ⇁ Z and γ : X ⇁ Z the residue (or division, weakest precondition) γ ÷ β : X ⇁ Y is a morphism such that αβ ⊑ γ if and only if α ⊑ γ ÷ β for all morphisms α : X ⇁ Y. □

A morphism f : X ⇁ Y such that f^{♯}f ⊑ id_{Y} (univalent) and id_{X} ⊑ ff^{♯} (total) is called a total function and may be introduced as f : X → Y. In what follows the word relation is a synonym for morphism of a Dedekind category.

An object I of a Dedekind category D is called a unit if 0_{II} ≠ id_{I} = ∇_{II}. An I-point x of X is a total function x : I → X, and denoted by x ∈ X.

In this paper we assume that a Dedekind category D has a unit I.

4Department of Informatics, Kyushu University 33, Fukuoka 812-8581, Japan. {kawahara@i.kyushu-u.ac.jp}

2 Upper and Lower Bounds

In this section we will review upper and lower bound operators for the Dedekind-MacNeille completion in Dedekind categories.

Let α : X ⇁ Y be a relation in D called a (formal) context. For relations ρ : I ⇁ X and μ : I ⇁ Y define relations ρ^{↑} : I ⇁ Y and μ^{↓} : I ⇁ X by

ρ^{↑} = (α^{♯} ÷ ρ)^{♯} and μ^{↓} = (α ÷ μ)^{♯},

respectively.

[figure: X; α; Y; I; ρ; μ]

The following is the fundamental property of the pair (^{↑},^{↓}) of operations defined above:

Lemma 2.1 (Galois Connection) Let ρ : I ⇁ X and μ : I ⇁ Y be relations in D. Then ρ ⊑ μ^{↓} if and only if μ ⊑ ρ^{↑}.

Proof. It follows at once from

ρ ⊑ (α ÷ μ)^{♯} ⇔ ρ^{♯} ⊑ α ÷ μ  { Converse }
⇔ ρ^{♯}μ ⊑ α  { Residue }
⇔ μ^{♯}ρ ⊑ α^{♯}  { Converse }
⇔ μ^{♯} ⊑ α^{♯} ÷ ρ  { Residue }
⇔ μ ⊑ (α^{♯} ÷ ρ)^{♯}. { Converse }
□

The Galois connection deduces the following well-known properties.

Proposition 2.2 Let ρ : I ⇁ X and μ : I ⇁ Y be relations in D. Then the following hold:

1. ρ ⊑ ρ^{↑↓} and μ ⊑ μ^{↓↑},

2. ρ_{0} ⊑ ρ_{1} ⇒ ρ_{1}^{↑} ⊑ ρ_{0}^{↑} and μ_{0} ⊑ μ_{1} ⇒ μ_{1}^{↓} ⊑ μ_{0}^{↓},

3. ρ^{↑↓↑} = ρ^{↑} and μ^{↓↑↓} = μ^{↓},

4. (⊔_{j∈J}ρ_{j})^{↑} = ⊓_{j∈J}ρ_{j}^{↑} and (⊔_{j∈J}μ_{j})^{↓} = ⊓_{j∈J}μ_{j}^{↓},

5. ρ = ρ^{↑↓} ⇔ ρ = μ^{↓} for some μ.

Proof. (a) As ρ^{↑} ⊑ ρ^{↑} is always true it follows from 2.1 that ρ ⊑ ρ^{↑↓}. Also, as μ^{↓} ⊑ μ^{↓} is always true it follows from 2.1 that μ ⊑ μ^{↓↑}.

(b) If ρ_{0} ⊑ ρ_{1}, then we have ρ_{0} ⊑ ρ_{1}^{↑↓}, since ρ_{1} ⊑ ρ_{1}^{↑↓} by (a), and so ρ_{1}^{↑} ⊑ ρ_{0}^{↑} using 2.1 again. Another implication is similar.

(c) First note that ρ ⊑ ρ^{↑↓} and ρ^{↑} ⊑ (ρ^{↑})^{↓↑} hold by (a). The first inequality ρ ⊑ ρ^{↑↓} implies ρ^{↑↓↑} ⊑ ρ^{↑} by (b). Hence we have ρ^{↑↓↑} = ρ^{↑}, and similarly μ^{↓↑↓} = μ^{↓}.

(d) It is immediate from

μ ⊑ (⊔_{j∈J}ρ_{j})^{↑} ⇔ ⊔_{j∈J}ρ_{j} ⊑ μ^{↓}  { 2.1 }
⇔ ∀ j ∈ J : ρ_{j} ⊑ μ^{↓}
⇔ ∀ j ∈ J : μ ⊑ ρ_{j}^{↑} { 2.1 }
⇔ μ ⊑ ⊓_{j∈J}ρ_{j}^{↑}

and

ρ ⊑ (⊔_{j∈J}μ_{j})^{↓} ⇔ ⊔_{j∈J}μ_{j} ⊑ ρ^{↑}  { 2.1 }
⇔ ∀ j ∈ J : μ_{j} ⊑ ρ^{↑}
⇔ ∀ j ∈ J : ρ ⊑ μ_{j}^{↓} { 2.1 }
⇔ ρ ⊑ ⊓_{j∈J}μ_{j}^{↓}.

(e) If ρ = μ^{↓}, then ρ^{↑↓} = μ^{↓↑↓} = μ^{↓} = ρ by (c). □

3 Tarski’s Fixed Point Theorem

A relation α : X ⇁ X is called a preorder if it is reflexive (id_{X} ⊑ α) and transitive (αα ⊑ α). Note that α is a preorder iff α ÷ α = α. (αα ⊑ α ⇔ α ⊑ α ÷ α, and id_{X} ⊑ α ⇔ α ÷ α ⊑ α.) A relation α : X ⇁ X is an order if it is a preorder and antisymmetric (α ⊓ α^{♯} ⊑ id_{X}).

For a relation μ : I ⇁ X define min μ = μ ⊓ μ^{↓} = μ ⊓ (α ÷ μ)^{♯}, max μ = μ ⊓ μ^{↑} = μ ⊓ (α^{♯} ÷ μ)^{♯}, sup μ = min μ^{↑} = μ^{↑} ⊓ μ^{↑↓}, and inf μ = max μ^{↓} = μ^{↓} ⊓ μ^{↓↑}. It is trivial that min μ ⊑ inf μ and max μ ⊑ sup μ. These four relations are always univalent as long as α is antisymmetric. For example, min μ is univalent since

(min μ)^{♯}(min μ) = {μ^{♯} ⊓ (α ÷ μ)}{μ ⊓ (α ÷ μ)^{♯}}
⊑ (α ÷ μ)μ ⊓ μ^{♯}(α ÷ μ)^{♯}
⊑ α ⊓ α^{♯}  { (α ÷ μ)μ ⊑ α }
⊑ id_{X}.  { α ⊓ α^{♯} ⊑ id_{X} }

Hence, if α is anitsymmetric and min μ (max μ, inf μ, or sup μ) is total, then min μ (max μ, inf μ, or sup μ) is an I-point of X, respectively.

A relation ξ : X ⇁ X preserves α if it satisfies a condition ξ^{♯}αξ ⊑ α.

Lemma 3.1 If α : X ⇁ X is transitive and ξ : X ⇁ X preserves α, then μ^{↓}ξ ⊑ (μξα)^{↓} holds for all relations μ : I ⇁ X.

Proof. An inclusion (α ÷ μ)^{♯}ξ ⊑ (α ÷ μξα)^{♯} simply follows from

ξ^{♯}(α ÷ μ)μξα ⊑ ξ^{♯}αξα { (α ÷ μ)μ ⊑ α }
⊑ αα  { ξ^{♯}αξ ⊑ α }
⊑ α.  { αα ⊑ α }
□

Then we can state the main result of the paper, which extends the Tarski’s fixed point theorem [5] for complete lattices.

Theorem 3.2 If α : X ⇁ X is transitive and ξ : X ⇁ X is a total relation preserving α, then a relation τ = ∇_{IX}(ξα ⊓ id_{X}) : I ⇁ X satisfies the following inclusion:

(inf τ)ξ ⊑ min τ.

Proof. First note that αξ ⊑ ξα follows from ξ^{♯}αξ ⊑ α and the totality of ξ, and that τ ⊑ τξα holds since

τ = ∇_{IX}(ξα ⊓ id_{X})(ξα ⊓ id_{X}) ⊑ τξα.

Set τ_{0} = inf τ. It suffices to show τ_{0}ξ ⊑ τ and τ_{0}ξ ⊑ τ^{↓}. The second inclusion τ_{0}ξ ⊑ τ^{↓} can be proved from a computation

τ_{0}ξ ⊑ τ^{↓}ξ  { inf τ = τ^{↓} ⊓ τ^{↓↑} }
⊑ (τξα)^{↓} { Lemma 5.2 }
⊑ τ^{↓}.  { τ ⊑ τξα }

On the other hand, as τ_{0} ⊑ τ^{↓↑} by the definition of τ_{0}, we have τ^{↓} ⊑ τ_{0}^{↓} making use of the Galois connection. Combining this with the second inclusion we have τ_{0}ξ ⊑ τ_{0}^{↓}. Therefore the first inclusion τ_{0}ξ ⊑ τ can be seen as follows:

τ_{0}ξ = τ_{0}^{↓} ⊓ τ_{0}ξ  { τ_{0}ξ ⊑ τ_{0}^{↓} }
⊑ τ_{0}ξ(ξ^{♯}τ_{0}^{♯}τ_{0}^{↓} ⊓ id_{X}) { Dedekind Formula }
⊑ ∇_{IX}(ξ^{♯}α^{♯} ⊓ id_{X}) { τ_{0}ξ ⊑ ∇_{IX}, τ_{0}^{♯}τ_{0}^{↓} ⊑ α^{♯} }
= ∇_{IX}(αξ ⊓ id_{X})  { αξ ⊓ id_{X} ⊑ id_{X} }
⊑ ∇_{IX}(ξα ⊓ id_{X})  { αξ ⊑ ξα }
= τ.
□

A relation α : X ⇁ X is inf-complete if for every relation μ : I ⇁ X its infimum inf μ : I ⇁ X is total.

Corollary 3.3 If α : X ⇁ X is an inf-complete order and ξ : X ⇁ X is a total relation preserving α, then a pair of relations τ = ∇_{IX}(ξα ⊓ id_{X}) and τ_{1} = ∇_{IX}(ξ ⊓ id_{X}) satisfies the following equalities:

(inf τ)ξ = min τ = inf τ = min τ_{1} = inf τ_{1}.

Proof. Set τ_{0} = inf τ as in the proof of the last theorem. First we recall that inclusions τ_{0}ξ ⊑ min τ ⊑ τ_{0} holds by the virtue of the last theorem. The inf-completeness of α and the totality of ξ guarantee the totality of the composite τ_{0}ξ. Also τ_{0} is univalent by the antisymmetry of α. Hence we have

τ_{0}ξ = min τ = τ_{0}

by the basic property of Dedekind categories. It follows from the reflexivity of α that τ_{1} ⊑ τ and so τ_{0} ⊑ τ^{↓} ⊑ τ_{1}^{↓}. On the other hand we have

τ_{0} = τ_{0}ξ ⊓ τ_{0}  { τ_{0} = τ_{0}ξ }
⊑ τ_{0}(τ_{0}^{♯}τ_{0}ξ ⊓ id_{X}) { Dedekind Formula }
⊑ ∇_{IX}(ξ ⊓ id_{X}) { α : antisymmetric}
= τ_{1},

which means τ_{0} ⊑ min τ_{1} ⊑ inf τ_{1}. Again the functionality of τ_{0} and inf τ_{1} implies equlities

τ_{0} = min τ_{1} = inf τ_{1},

which completes the proof. □

References

[1] P. Freyd and A. Scedrov, Categories, allegories, North-Holland, Amsterdam, 1990.

[2] B. Ganter and R. Wille, Formal Concept Analysis, Springer-Verlag, Berlin-Heidelberg, 1999.

[3] Jean-Pierre Olivier and Dany Serrato, Catégories de Dedekind. Morphismes dans les Catégories de Schröder, C. R. Acad. Sci. Paris 260 (1980) 939-941.

[4] A. Tarski, On the calculus of relations, J. Symbolic Logic 6 (1941) 73–89.

[5] A. Tarski, A lattice theoretical fixpoint theorem and its applications, Pacific J. Math. 5 (1955) 285–309.

Theorem 3.4 (Tarski’s Fixed Point Theorem (original)) Let ⟨X, ≤⟩ be an inf-complete lattice. Every monotone function f : X → X has the least fixed point. Proof. Consider a subset T = {x ∈ X | f(x) ≤ x} of X and set t = inf T, which exists since X is inf-complete.

x, y ∈ X : x ≤ y ⇒ f(x) ≤ f(y) (f: monotone) x ∈ T ⇔ f(x) ≤ x (Def. of T) (∀x ∈ T : t ≤ x) (∧-1) (∀x ∈ T : y ≤ x) ⇒ y ≤ t (∧-2) (∀x ∈ T : y ≤ x) ⇔ y ≤ t (∧)

∀x ∈ T : t ≤ x ⇒ ∀x ∈ T : f(t) ≤ f(x) { f : monotone }
⇒ ∀x ∈ T : f(t) ≤ x  { Def. of T }
⇒ f(t) ≤ t  { (∧-2) }
( ⇒ t ∈ T ) { Def. of T }
⇒ f(f(t)) ≤ f(t)  { f : monotone }
⇒ f(t) ∈ T  { Def. of T }
⇒ t ≤ f(t)  { (∧-1) }
⇒ f(t) = t
f(x) = x ⇒ f(x) ≤ x
⇒ x ∈ T  { Def. of T }
⇒ t ≤ x  { (∧-1) }
□

論理学の歴史とコンピュータ

高橋正子 (国際基督教大学)^{5}

現在のコンピュータの原型と見られる万能コンピュータが 20 世紀半ばに誕生してから半世紀余りが過ぎた. その間に, 機械の性能や, 利用形態, 応用分野の広がりなどの面で著しい進展が見られる一方で, コンピュータの基本設計そのものには大きな変化はないという. 本稿では, コンピュータより半世紀余り前に芽を出し, やがて急速に花開いた論理学^{6}が, 現代のコンピュータの誕生にどのような影響を与えたかについて, 既存の資料^{7}をもとに考察を行う.

1 節では, 万能コンピュータが誕生するまでの 1 世紀余りの間に自動計算機械作成のためにどのような試みが行われたかを概観する. 2 節では, 万能コンピュータとは何か, それまでに作られた道具や機械と比べて万能コンピュータは基本的にどこが違うのかなどの問題を現代の視点で整理する. 次の 3 節では, 万能コンピュータに対する Babbage と Turing の試みを比較し, 二人がそれぞれ生きた 19 世紀と 20 世紀の間に何が決定的に変化したのかについて論じる. 続く 4 節では, von Neumann が Turing の成果を現実の (万能) コンピュータの誕生に繋ぐ上で実際にどんな役割を演じたのかについて考察する. 最後の 5 節では, コンピュータの歴史に関する研究についての期待などを述べる.

1 コンピュータ小史 (Babbage から万能コンピュータの誕生まで)

この節では, 次節以降の準備として, 万能コンピュータの誕生に関連する主な出来事を簡単な注と共に列挙する.

1.1 ケンブリッジ大学の数学の教授だった C. Babbage(1791-1871) は 1822 年に英国政府の予算を得て, 数表作成の自動化を目指す歯車式計算機 difference engine の開発を始めた. しかし, 試作機の作成を終え実用機の完成を目指していた 1834 年頃, より高性能の新しい計算機の着想を得たためこの計画を断念した. Analytical engine とよばれるその新しい機械は, 計画によると「あらゆる種類の数値計算」を行うためのもので, ある種の「プログラム」を鑽孔カードを読みながら, そこに指定された演算を, 歯車で表現されたデータに対して次々に適用していく手動の計算機である. そして, そのプログラムの中に条件分岐や繰り返し計算の機能も含み得るとされた [16]. しかし, 彼の多年の努力にも拘らず, この構想も実現には至らなかった.

1.2 それから約 1 世紀後の 1944 年, ハーバード大学と IBM が共同でリレー式計算機 Harvard-IBM Mark I を完成した. これは Babbage の analytical engine の構想の縮小版を 20 世紀前半の電磁気のテクノロジーを用いて実現したもので, (条件分岐を含まない) 基本演算の列を紙テープから読み込み, そこに示された演算をメモリー中のデータに順次適用する自動計算機械である. なお, これ以前に作られたリレー式計算機として, 2 進法を採用したベルリン工科大学の Z1(1938 年) や Z3(1941 年) がある.

1.3 話が前後するが, 1936 年に英国の若い数学者 A. Turing(1912-1954) は以下の内容の論文 [25] を発表した.

5Masako Takahashi, Department of Information Science, International Christian University, Tokyo 181-8585 Japan.

E-mail:mth@icu.ac.jp

6記号論理学, 数理論理学, 数学基礎論などの名で呼ばれる数学的な論理学をここでは簡単のため単に論理学とよぶ.

7コンピュータの歴史とその主な登場人物に関する一般的な事項については [1, 5, 7, 10, 11, 13, 15, 17, 21] を本文中のあちこちで参考にした. それ以外の事項についてはその都度引用文献を示す.

(1) コンピュータの概念を今日「チューリング機械」とよばれる形で数学的に定式化した上で,

(2) 次に述べる意味で万能なチューリング機械が存在することを示した: 任意のチューリング機械 M の記述とそのための入力データを万能チューリング機械 U に与えると, U は, それらを必要に応じて参照したり書き換えたりしながら, 本来 M が行う筈の仕事を M に代わって行う.

(3) 更に, この万能チューリング機械を使って, その当時 D. Hilbert が提起していた論理学上の決定問題を否定的に解いた.

ここで, (1) の「コンピュータ」として現在我々の身の回りにあるコンピュータを考えてもよいが, 1930 年代にこのことばは計算する人を意味した. 要するに人や機械が行う「計算」とよぶに相応しい一連の行為に共通でしかも本質的な部分を体系化して作られたのかチューリング機械である. 実際, 彼の定式化は, 計算ということばで我々が理解する内容を的確に表現したものとして, 現実のコンピュータが登場する前もそれ以後も, この種の問題に関心をもつ人々の間で広く支持されている.

(2) の「チューリング機械の記述」は計算の内容を記号列で表現したものであり, 今日のことばでいうとプログラムに相当する. (1) と (2) をこのことばを使って言い換えると次のようになる:

計算の手順は記号列の形で (プログラムとして) 正確に記述することができ, そのようなプログラムをデータと共に記憶し必要に応じて随時参照したり書き換えたりできるという状況のもとで, そのプログラムに書かれた通りのことを実行する万能コンピュータがある.

彼は, このように一台ですべてのアルゴリズム (計算手順) を実行することのできる万能チューリング機械の存在を単に証明しただけでなく, その具体的な記述を論文の中で与えている.

1.4 第二次世界大戦中に, 軍事上の特殊目的のための電子計算機がいくつか開発された. その代表的なものとして, ペンシルバニア大学と米国陸軍が主に弾道計算用に開発し, 1946 年に完成した ENIAC(Electronic Numerical Integrator and Calculator) がある.

この機械はその名が示す通り, アナログ計算機 (積分機) の仕組みを膨大な数の真空管を使ってデジタル計算機の形で実現した 10 進法による自動計算機である. そのため, プログラムの一部はハードウェアに組み込まれ, それ以外の (データによって変化する) 部分は配電盤上の結線やスイッチで指示する方式が採用された. この機械の演算速度は電子化によりそれまでのリレー式機械に比べて千倍程度向上したが, デジタル計算機としては無駄の多い構造であること, プログラムの組み換えに手作業を要すること, プログラムの再利用が困難なことなどの欠点があった.

ENIAC の他に, 戦時中に軍事目的のために作られ実際に活躍した電子式計算機械として, 英国がドイツの暗号解読のために開発した COLOSSUS(1943 年) および Mark-II COLOSSUS(1944 年) がある. また, アイオワ州立大学で, 連立一次方程式を解くための 2 進法による電子式計算機 ABC(Atanasoff-Berry Computer) の開発が 1942 年まで進められたが, 戦争のため未完に終わった.

1.5 ENIAC の開発グループは設計が終わると, 機械の製作と平行してこの機械の問題点について議論を重ね, 次の目標として, 新しく開発した大容量の (遅延線による) メモリに入力データと共にプログラムも記憶して計算を行う汎用電子計算機 EDVAC(Electronic Discrete Variable Computer) の構想をまとめつつあった.

その過程で, この開発グループに 1944 年から加わっていたプリンストン高等研究所の J. von Neumann(1903-1957) が, 1945 年にそれまでの議論の結果を彼の視点で「EDVAC に関するレポートの初稿」 (以降, 「EDVAC レポート」と略す) [28] としてまとめた. 彼の単独名で書かれたこの未完の草稿は, 電子計算機の開発に関心をもつ人々の間に「プログラム内蔵方式」とか「ノイマン型」コンピュータの名で広く知られるようになり, その後のコンピュータを方向付ける結果となった.

1.6 ENIAC が完成した 1946 年にこのグループは意見の食い違いのため解散したが, ケンブリッジ大学のグループが 1949 年に EDVAC レポートに基づく汎用電子計算機 EDSAC(Electronic Delay Stored Automatic Calculator) を完成した.

一方, 戦時中に暗号解読やレーダー技術の開発を行っていた英国の研究者達のグループが, 戦後マンチェスター大学で新しく (陰極管による) 大容量のメモリを開発し, EDSAC とは独立に, 「プログラム内蔵方式」 (2.4 参照) による汎用電子計算機の実験機 Manchester Baby Mark-I と実用機 Manchester Mark-I をそれぞれ 1948 年と 1949 年に完成した.

これら 3 台の機械は次節に述べるように, いずれも万能コンピュータとよぶに相応しい機械である.

2 万能コンピュータとそうでないもの

この節では, 前節に登場した万能コンピュータについて, そもそも万能コンピュータとは何か, それまでに作られた道具や機械と比べて万能コンピュータは基本的にどこが違うのか, 現代のコンピュータは果たして万能なのか, などの問題について整理する.

2.1 簡単にいうと, 万能コンピュータとは「万能チューリング機械と同等の計算能力を持つ機械またはその仕組み」をさす^{8}. ただし, この説明は万能チューリング機械の定義を述べなければ無意味だが, それは適当な教科書 (例えば [3, 12, 23]) に任せることにして, 代わりにそれが行う仕事をアルゴリズム (計算手順) の形で述ｋ u 椌 C 襪伴， (1)〜(3) のようになる.

(1) [入力] 任意のプログラム P とそれに対応する入力データをメモリに記憶する.

(2) [初期設定] P の実行に必要なデータの初期値を設定する. 特に, プログラム P で最初に実行する命令の位置をプログラム・カウンタ^{9}にセットする.

(3) [命令の実行とプログラム・カウンタの値の更新] プログラム・カウンタの示す命令 S が終了命令ならこのプログラムの処理を終える. そうでなければ S を実行し, 次いで, プログラム P の中で S の次に実行すべき命令の位置をプログラム・カウンタにセットして (3) に戻る.

2.2 ここで肝心なのは, プログラム P としてあらゆるアルゴリズム (をこのコンピュータ用の書式で記述したもの) を万能コンピュータは処理できることで, その性質を持たないものは仮令上の (1)〜(3) の流れに従って作業を行うものでも万能コンピュータではない. ところで, そうするとプログラム P として想定されるものは無限にあるから, 従って P の長さはどれほどにも長くなり得る. そのため万能コンピュータのメモリ (記憶装置) は有限ではあり得ない. しかし, 現実のコンピュータが無限に多くのメモリを持つことはないから, 万能コンピュータの実現という場合には, 「必要に応じてメモリをどれだけでも拡張できるという理想化された状況のもとで万能チューリング機械と同等の働きをするコンピュータ」^{10}を万能コンピュw) 沁燭箸い.

8Turing が論文を書いた当時は, 彼が構成し我々が現在「万能チューリング機械」とよんでいるものが, 上で述べた意味の万能コンピュータとして知られる唯一の者だった. そして彼はそれを「万能コンピュータ」とよんだ. 今日ではそれと同等の能力をもつものが沢山知られているが, 我々は M. Davis[7] に従い, それらを万能コンピュータとよぶ. なお蛇足ながら, 万能コンピュータは宇宙の森羅万象を計算するものではない. 実際, 計算では解けない問題があることを Turing の論文 [25] は具体的に示しているが, それらはもちろん万能コンピュータでも計算できない.

9プログラムの実行中に, 次に実行すべき命令 (の位置, またはアドレス) を記憶するための変数をこのようによぶ.

2.3 上で述べた万能コンピュータの記述は Turing の論文に記されているものと比べると見かけ上大きく異なる. その理由は, チューリング機械の基本設計や命令体系が今日のコンピュータのそれとは異なるためである. 特に, チューリング機械のメモリ (彼はこれをテープとよんだ) にはアドレスがなく, 従ってプログラム・カウンタもない. そのため, チューリング機械の場合には, はじめに読み込んだプログラムやデータを途中で参照するだけでなく何度も書き換えることによって上の (1)〜(3) に相当する作業を行っている.

2.4 万能コンピュータの「万能性」とは, すべてのアルゴリズムが実行できることだと述べたが, その性質を保証するのが, プログラムと入力データをまずメモリに読み込み実行時に必要な箇所を随時参照するという意味での「プログラム内蔵方式」である^{11}. その際, 万能チューリング機械の場合のように, 記憶したプログラム (やその他のデータ) を実行時に書き換えてもよいが, そのことは本質的ではない. 実際, ある種の基本的な機能が備わっているコンピュータであれば, 実行時にプログラムを書き換える必要はない. 具体的にいうと, 次の三つの機能をもつコンピュータの場合, プログラムを実行時に書き換えることなしに万能コンピュータのアルゴリズムを実装できることが知られている^{12}: (1) メモリにアドレスの機能がある. (2) メモリの指定された位置に整数 0 を書き込んだり 1 を足したりする機能がある. (3) メモリを指定された位置に記憶されている値に従って条件分岐を行う機能がある.

ところで, 1.6 で述べた 1940 年代末に完成した 3 台のコンピュータは, いずれも上の機能をもっているから, その 3 台とも万能コンピュータである.

2.5 一方, プログラムをメモリに読み込まずに, 端から順に 1 文字ずつ読みながら処理していくコンピュータを考えると, 上で述べた意味での「プログラム内蔵方式」に比べて計算能力に決定的な違いがある. 実際, データを読みながら (それらを書き換えたり, 新たにデータを書き込んだりせずに) 処理を行うコンピュータの数学的なモデルは「有限オートマトン」とよばれ, その計算能力はチューリング機械に比べて著しく小さいことが知られている^{13}.

2.6 現代のコンピュータは, 半世紀前にその原型が誕生して以来, 例えばインターネットやマルチメディアなどの新しい応用分野を次々に開拓しつつあるが, こうしたコンピュータの多様な活躍ぶりは, 「あらゆるアルゴリズムを実行できる」という万能コンピュータの万能性の現れと見ることができよう. そう考えると, コンピュータの応用分野が新しく開拓されると, その度に新しい入出力機器やアルゴリズムを開発する必要はあっても, コンピュータの基本設計を変える必要がないのは当然だといえる. この点が, 特定の目的のために作られる従来の道具や機械と比べて現代の (万能) コンピュータが決定的に異なる点である.

10このコンピュータはあくまでも有限の現実的な機械であり, 無限に大きい仮想機械を考えているわけではない. 一方, チューリング機械は無限のメモリをもつ仮想機械である.

11プログラム内蔵方式 (stored-program) ということばは二つの異なる意味で使われることがあるので注意を要する. その一つは上で述べた意味で, もう一つは単にプログラムを実行前にメモリに読み込むという意味である. 本稿では専ら前者の意味で用いるが, 念のためカッコをつけて「プログラム内蔵方式」と書くことにする.

12これらの機能をもつコンピュータはしばしば Random Access Machine(略して RAM) とよばれる. RAM の概念は, 1950 年代末に複数の研究者により独立に見出され, それが万能コンピュータの条件を満たすことが文献に登場したのは 1961 年 [14, 18] といわれる.(例えばを [3] を見よ.)

13例えば [12] を見よ.

3 Babbage の時代に不足していたもの

3.1 Babbage は analytical engine(1.1 参照) を開発しながら, その構想についてヨーロッパ各地で講演を行った. その中の一つであるイタリアでの講演をまとめた文献 [16] が analytical engine に関する比較的詳しい解説とされるが, その中にこの機械で何ができるかについて次のような説明がある: すべての数値計算は四則演算に還元することができ, 四則演算はこの機械の基本演算として装備されるから, この機械であらゆる種類の数値計算を行うことができる. Analytical engine に関する記述にはこうした大胆な (しかし必ずしも意味が明確でない) 文章と, 具体的な数値計算の例について計算のステップを詳しく解説したものが多く見受けられるが, 残念ながら機械の全体の輪郭が掴み難い. その一つの理由は, この機械ではプログラムをどのように書くのかについての記述が見当たらないことである. (例えば [13] にもそのことが指摘されている.)

3.2 ところで, ある分野の計算 (またはその他の人間の行動) の手順を機械に伝えて代行させるとなると, ふだん人間がやっていることを曖昧さのない形で詳細に書き下し, それを機械が認識できるような形に記号化して与える必要がある. そしてそのためには, 機械化しようとする事柄について人間が行っていることのすべてを正確に表現することのできる一種の人工言語をまず設計する必要がある. ただし, もし機械に実行させようとする仕事が (例えば自動販売機にように) ごく限られた種類のものであれば, 予め機械に必要な手順を組み込んでおき, 外側に押しボタン等を用意すれば済む^{14}. しかし, もっと多様な種類の計算を機械に代行させようとする場合はそのような方法では済まない. 実際, Babbage は analytical engine で初めて計算手順の指定が実行時に必要なことに気付き, そのために「オペレータ・カード」や「オペランド・カード」とよばれる鑽孔カードを使ってそれらを読み込むアイディアをジャカール織機^{15}から得たという. しかし, 上で指摘したように, それらのカードでどのように (条件判定を含む) 計算手順を指定するのかを彼が明確にしなかったということは, 彼がその問題の重要性を認識していなかったか, あるいは納得のいく結論が得られないままに終わったことを示唆するように思われる.

3.3 しかし考えてみると, Babbage に限らず当時の人々に, 「ふだん人間が半ば無意識に行っていることを, 完全に曖昧さのない形で書き下し, それを機械が認識できるように記号化して表現する」ことを期待することは果たして妥当だろうか. 今でこそ, コンピュータは人間のように融通が利かないことや, 従ってコンピュータに何か仕事をさせるにはプログラミング言語という一種の人工言語を使って逐一その内容を指示しなければならないことが常識になっているものの, 当時, それに類するものはまだ全く姿を見せていなかったのではないだろうか.

3.4 歴史上これに近い考え方が初めて登場したのは, 近代科学としての (数学的な) 論理学が誕生した 19 世紀後半から 20 世紀はじめにかけてではないかと思われる. というのは, 論理学はそもそも数理科学的なものの考え方の原理やその性質を数学的な厳密さをもって研究しようとする学問であるから, 数理科学の諸分野でふだん人々が伝統的に何気なく使っているいろいろな表現を例えば「論理式」や「証明」 (の形と意味) として定式化し, それらの間に見られる規則性 (その多くはやはり直感的に人々が理解しているもの) を明示的かつ網羅的に体系としてまとめる作業が必要だった筈である. しかし, 皮肉なことに Babbage が analytical engine の実現のために奮闘していた 19 世紀中頃という時代は, (数学的な) 論理学がまさにこれから生まれようとする時代だった^{16}.

14実際, Babbage が最初に手掛けた difference engine の場合は, 計算の内容が, 階差法に基づき多項式 (で近似される関数) の数表を作成するというごく限られたものだったため, 機械の中に組み込まれた計算機構に外から必要なパラメタを入力データと共に与えればよかった. また, 後の ENIAC の場合も, プログラムが w) ヽ�冒箸濆�泙譴晋把衂瑤噺紊�薀好ぅ奪舛覆匹濃慊蠅垢覯鎚冑瑤�蘋 �襪箸いΠ嫐�, 同様の考え方に基づいて限られた種類の数値計算を行う機械と見ることができる.

1519 世紀初頭にフランスで発明され当時広く使われていた折込模様入りの織物を織る機械.

3.5 それに対して, Babbage より約 120 年後に生まれた Turing の時代には状況が一変していた. 彼が万能コンピュータに関する研究を行った経緯は概略次の通りである.

1934 年 6 月にケンブリッジ大学数学科を卒業した後, 大学に残って研究を続けることを希望した彼は, 翌年 3 月に大学のフェローの資格を得て一人前の研究者としての道を歩き始めた. またそれと同じ頃 (1935 年春学期), 彼は M. H. A. Newman による「数学基礎論」の講義を聴き, その数年前に発表されたばかりの K. Gödel の不完全性定理とその証明を学んだ. 更に彼はその講義で, 論理体系が満たすべき条件として Hilbert が提唱した「完全性」 , 「無矛盾性」 , 「決定可能性」の三つの条件のうち, はじめの二つは Göidel の結果により (ある厳密な意味で) 達成不可能であることが示されたが最後の条件は未解決のままであることを知った. そして彼は述語論理の体系が決定不能であることの証明を考え始めた.

3.6 そのため彼はまず, 「計算」という直感的な概念をチューリング機械という新しい体系を用いて的確に定式化し, その上で, Gödel によるゲーデル数化や G. W. Cantor による対角線論法などの既知の手法と彼自身の新しい証明のアイディアを用いて, 万能チューリング機械の構成と Hilbert の決定問題に対する否定的な解を得ることに 1936 年 4 月に成功した^{17}. その際, 彼自身が見出した新しい証明のアイディアのうち特に重要なのは, 2.1 に述べた万能コンピュータのアルゴリズムの考え方で, これは後に (1945 年以降に) 「プログラム内蔵方式」として, また (1950 年代以降に) コンパイラの基本原理として知られる考え方に繋がるものである. 彼は, 現実の自動計算機がまだ一台も作られていなかった 1936 年という早い時機にそのアイディアに到達し, それを使って世界で最初の万能コンピュータである万能チューリング機械を構築した.

3.7 Turing の場合にはこのように, (1) 直感的な概念を定式化および記号化するという考え方が論理学の新しい伝統の中で既に始まっていたこと, また, (2) Gödel の不完全性定理のような深い結果がその上に築かれ, 論理学にそれまでとは異なる新たな展望が開かれると同時に, そのために必要な新しい証明の手法が開発されつつあったこと, そして (3) 彼自身が是非解明したいと思う魅力的な論理学上の問題が目の前にあったこと, などの好条件があった.

Babbage と Turing の時代の間に, こうした論理学の誕生と目覚しい発展があったことに注目する視点は, 現代のコンピュータと論理学の関係を正当に評価する上で重要であると思う.

4 万能コンピュータの実現に対する von Neumann の貢献

本節では, 一般の書物でよく見かける「コンピュータの生みの親は von Neumann である」という説の妥当性について検討する.

16古代ギリシャに始まる広義の (哲学や弁論の術などを含む) 論理学の歴史を振り返ると, アリストテレスの推論体系 syllogism が紀元前 4 遂 u 桙�坊狙�気, それがすべての正しい推論を網羅するものとして 2000 年以上に亘って本質的な変化のないまま継承された後, 1850 年前後になってようやく数学的視点に基づく論理学の芽生えが G. Boole, D. S. Peirce らによって研究され始めた. そして 1879 年に, 本格的な述語論理の体系が G. Frege により初めて構築された. ただしその Frege の体系も, 表記法 (つまり, 上で述べた人工言語の形式の部分) の問題点などのために, 20 世紀初頭に B. Russell が有名なパラドックスを指摘するまで誰も注意を向けなかったといわれる [4, 8].

17なお, その論文の初稿完成とほぼ同時期に, プリンストン大学の A. Church により λ 計算に関する関連研究が発表されたことを Newman から知らされた Turing は, 直ちにチューリング機械と λ 計算が同等の能力をもつことの証明を論文に附録として書き加えた. 更に彼は翌 1937 年に, チューリング機械, λ 計算, 帰納的関数など, その時点で知られていた計算モデルの間の関係をより詳しく研究した [26]. その結果, 当時の論理学者達の間でこれらを計算の妥当な定式化とみなすことについての実質的な合意が得られるようになった [8, 9].

4.1 これまでに 2 節で, von Neumann の書いた「EDVAC レポート」の中心的なアイディアである「プログラム内蔵方式」と万能コンピュータの関係について, 前者は後者を実現するための方法であることを述べ, 3 節では, 後者が Turing の論文に由来するものであることを述べた. 時間的に見ると Turing の論文は EDVAC レポートより 9 年前に発表されたから, 万能コンピュータのアイディアの発見 (あるいは発明?) 者は明らかに Turing である. しかし, 学問の世界でよくあるように, von Neumann が Turing の論文とは独立に「プログラム内蔵方式」のアイディアを考えたということも可能性としてはあり得る. あるいはそうでないとしても, von Neumann がコンピュータの生みの親とよばれるに相応しい何か別の理由があるかも知れない. もしそうだとすると, それはどんな役割だろうか.

4.2 上の疑問に答えるため, 以下にまず関連する事柄を列挙する. それらを見比べると互いに矛盾しているような印象を受けるものもあるが, 時間差などを考慮すると必ずしもそうではなく, 全体を矛盾なく説明する一貫したストーリーが見えてくるように思われる.

(1) Von Neumann は, 論理学, 量子力学, 連続幾何学, リー群論, ゲーム理論, コンピュータの開発と応用などの広範な分野で活躍した著名な数学者である. 論理学の分野では, Russell のパラドックスを回避する目的で, 「集合」より大きい「クラス」の概念を導入した公理的集合論 (NBG 集合論とよばれるものの前身) を構築・研究した博士論文 [24] が有名である. しかし彼は 1930 年, Gödel の不完全性定理によりそれまで Hilbert 学派の仲間達と共に目指していた目標が打ち砕かれたことを知って論理学を離れた. 1933 年に彼はプリンストン高等研究所に最年少の教授として着任し, その後次第に応用数学, 特にコンピュータを利用したいわゆるビッグ・サイエンスの方向に舵を切り替え, 研究所内外のグループを率いて精力的に活動した. (Von Neumann の生涯, 業績, 思想などについて詳しくは [1, 10, 15, 21] を見よ.)

(2) Turing は 1936 年, チューリング機械の論文 [25] を書き終えたのち, その年の夏から 2 年間プリンストン大学の博士課程に留学し Church のもとで λ 計算, 群論, 相対的計算可能性などの研究を行った. 帰国後は, 暗号解読機 (COLOSSUS およびその前身) の論理設計に従事した後, 国立物理学研究所やマンチェスター大学のコンピュータ・グループに加わり, コンピュータの開発と応用に参加するかたわら, 初期の人工知能論や数理生物学などの研究を行った. (Turing の生涯, 業績, 思想などについて詳しくは [7, 11, 17] を見よ.)

(3) Turing が渡米する前年の 1935 年, von Neumann はケンブリッジ大学を訪れ, 概周期関数に関する講義を行った. 一方, 予て von Neumann の著書「量子力学の数学的基礎」 [27] を勉強していた Turing はそこに記されていた著者の概周期関数に関する結果を拡張した論文を数週間前に書き, 学会誌に投稿していた [11].

(4) Turing がプリンストンで 1937 年夏に奨学金を申請した際, 彼のために von Neumann が書いた推薦書が残されている. その中で von Neumann は, 自分が興味を持った Turing の仕事として, 純粋数学の論文二篇^{18}を挙げているが, 既に出版済みだったチューリング機械の論文 [25] には触れていない [7, 11].

(5) 1938 年春, 帰国を数ヵ月後に控えた Turing に von Neumann はプリンストン高等研究所における助手のポストを申し出た. しかし Turing はそれを断わり, 予定通りケンブリッジ大学に戻った [7, 10, 11].

(6) 1939 年に von Neumann は高等研究所の同僚 S. Ulam に何度も Turing の論文 [25] の素晴らしさについて語った [10, 11].

18その一つは (3) で述べた Turing の最初の論文で, もう一つは彼がプリンストンに来てから von Neumann の薦めで取り組んだ群論に関する論文である.

(7) Von Neumann は, 1930 年代末に弾道計算と関わりをもつようになってからコンピュータに本格的に関心を寄せるようになり, 1943 年前半の英国滞在が彼のコンピュータへの興味を更に駆り立てた [1, 10, 21].

(8) 1943 年頃 von Neumann は, ロスアラモス科学研究所の物理学者 S. Frankel に, コンピュータの基本的なアイディアは他の誰でもなく Turing に負うと強調して語り, Turing の論文を読むことを強く薦めた [11, 20].

(9) 1944 年 1 月に ENIAC グループのメンバーにより大容量のメモリが開発された. そして, このメモリを使ってプログラムとデータを記憶して計算を行う ENIAC の後継機の計画が話し合われた [13, 17].

(10) Von Neumann は, ENIAC グループの数学系のメンバーである H. H. Goldstine の誘いで 1944 年 9 月から ENIAC グループに加わり, 翌年 6 月に EDVAC レポートを書いた. 彼自身はこのレポートを公開する意志はなかったという [10].

(11) 1946 年に von Neumann は高等研究所の彼のコンピュータ・プロジェクトのメンバー達に, 計算理論に関する教育の一環として Turing の論文 [25] を読ませた.

(12) 1946 年 von Neumann は N. Wiener に宛てた手紙の中で, 彼の EDVAC レポートの内容は, Turing の万能コンピュータと (神経回路網に対する)McCulloch-Pitts モデルという二つの偉大な研究成果を合体させたものであるとのコメントを述べている [11].

(13) ENIAC グループおよびプリンストン高等研究所のコンピュータ・グループで von Neumann と行動を共にした Goldstine は, von Neumann の死後, 彼のコンピュータに関する業績を中心にコンピュータの歴史を著した [10] が, その中で彼は Turing の論文 [25] に言及する際, チューリング機械とよく似た方法で計算を定式化した E. L. Post の論文^{19}[19] と対にして, 常に Post-Turing work とよんでいる.

4.3 これらの証言を読むと, 二人は 1935 年 (当時 von Neumann は 32 歳, Turing は 23 歳) 数学者として知り合い, 少なくとも Turing の渡米 1 年後の 1937 年夏までは二人の間の話題は純粋数学に関するものに限定されていたようである. 特に, 当時出版されたばかりのチューリング機械の論文に対して von Neumann は関心を示さなかった. しかし, その後 von Neumann はコンピュータに興味をもつようになると共に Turing の論文 [25] を読み, 高く評価するようになったと思われる.

一方, ENIAC グループでは ENIAC の後継機として, 新たに開発された大容量メモリにプログラムとデータを記憶する案が検討されていたところに von Neumann が加わり, 翌年 6 月に彼は「EDVAC レポート」を書いた. その時点で von Neumann は Turing の論文を理解していたが, 実際のコンピュータでそれが実現可能かどうかについては必ずしも確信をもっていなかったかも知れない. 一方, グループの他のメンバーが Turing の論文の特に万能チューリング機械について理解していた可能性は極めて低いと思われる.

4.4 そのような状況の下で von Neumann は,

(a) 万能コンピュータを実現するためにはどのようなアーキテクチャ^{20}であればよいかを考えてみることに彼自身興味をもち, また

(b) もしそれが上手くいけば, グループのメンバーにそのアーキテクチャを提案して賛同を得たいと考え, グループ内の討議資料として彼は EDVAC レポートを書いたのではないだろうか. しかし, 予想に反して彼のレポートはグループのメンバーの反感を買い, ENIAC グループは解散した. そして, 更に予想外の展開として, 彼がグループのメンバーに伝えたかったことは, このグループの代わりに世界のコンピュータ関係者に彼の名前と共に伝えられる結果となった^{21}.

19Post は Turing とは独立に研究を行い, Turing の論文よりやや遅れてこの論文が発表された. ただし, この論文には万能コンピュータに類するものは全く登場しない.

20コンピュータを構成する個々のハードウェアについて語るのではなく, それらが全体の中でどのような論理的役割を担っているかに注目してコンピュータの構造を述べたもの.

4.5 上のように考えると, 彼が何故個人名でこのレポートを書いたか理解できるような気がする. つまり, 彼はこのレポートをグループを代表して外に発表するために書いたのではなく, 万能コンピュータが現実に可能かどうか彼自身で確かめるために書き, その結果が良好と思われた段階でそれをグループのメンバーに自分からの提案として渡したのだとすると, 彼が (提案者として) 自分の名前を書くことは至極当然である. また, このレポートにはグループでの話し合いで出された様々なアイディアが誰のものか説明なしに書かれているという非難があったというが, それもこのレポートの意図を上のように考えれば不自然なことではない.

なお, そのことに関連して, 実はこのレポートには Turing の名前や万能コンピュータについての言及もないという事実がある. そのこと事態は上と同じ理由で説明がつくと思うが, しかし, そのことのために「コンピュータは大天才 von Neumann がごく短期間で発明した」というような子供じみた俗説が広まったとすると, それは将来を担う (大天才でない) 子供達にとって不幸なことだと思う.

4.6 Von Neumann が現代のコンピュータにどんな貢献をしたかについては, 様々なことが語られている^{22}が, その中で, 物理学者 Frankel による次の証言 [20] が私には最も的を得たものに思われる.

多くの人が von Neumann をコンピュータの父だと主張するが, 彼自身は決してそうは思っていなかった. むしろ彼は助産婦とよぶ方が相応しい. 彼はよく私や他の人々に向かって, 基本的な考え方は Turing に負っているのだと強くいっていた. 私の考えでは, von Neumann が行った本質的なことは, Turing によって明らかにされた基本的な考え方と ENIAC グル−プやその他の人々が行ったコンピュータの開発の仕事を世界中に知らせることだったと思う.

4.7 最後に一言上のことばに付け加えて, ここでの助産婦役は決して誰にでもできる簡単な仕事ではなかったことを指摘したい. というのは, Turing の (論理学上の) 論文の本質を読み解き, その背後にあるアルゴリズムを正しく把握した上で, それを現実のコンピュータ上で実現するにはどういう基本設計や命令体系があればよいかを (そもそもコンピュータの基本設計という考え方がなかった時代にそれを導入して) 考えるという仕事は, 当時の電子計算機の実情に十分詳しく, しかも論理学に造詣の深い研究者にして初めて可能な仕事だと思われるからである.

5 おわりに

はじめに述べたように本稿のねらいは, 現代のコンピュータの原型と見られる万能コンピュータが 1940 年代末に誕生するに当たって (数学的な) 論理学がどのような役割を果たしたかについて, 既存の資料に基づいて考察することだった. そのため前半の 1, 2 節で準備を行い, 後半の 3 節と 4 節で試論を展開した.

21当時のコンピュータ関係者の間でこのレポートが如何に好感をもって迎えられたかを示す証言として例えば [22] がある.

22例えば [13] にそれらがまとめて紹介されている.

5.1 まず 3 節では, Turing が万能コンピュータの概念に到達するに当たって論理学からの寄与がどのようなものであったかについて考察し, Babbage の時代との違いを指摘した. なおその際, 機械で実行する事柄を詳細に記述するための人工言語の問題に触れたが, その点を重要視し過ぎていると感じられた向きもあろうかと思う. 実際, 私がこの問題を考え始めた時点でこのことは全く念頭になかった. しかし, Babbage がプログラムの書き方を説明していないことに気付き, 不審に思って色々考えながら, ふと (数学的な) 論理学の場合に共通な問題があることに気付いて調べるうちに, 19 世紀半ばに「数学における論理」に注意が向けられ始めてから, Boole, Peirce, Frege, Peano らの仕事を経て Whitehead-Russell の “Principia Mathematica” に至る実に半世紀という歳月をかけて, ようやく論理学のための (人工) 言語の土台が一応固まったという意外な事実^{23}に遭遇し, この問題 w) 陵動廚覆蕕兇襪海箸傍ど佞�気譴深‖茲任△. 論理学の場合もコンピュータの場合も, 一旦そのための人工言語に慣れてしまえば, 表現の手段としても思考の道具としても何ら問題なく, あたかも水や空気のように自然に感じられるが, その必要性に気付き, 無からそれを実際に作り上げる仕事は, 決して過小評価すべきではないだろうと思う.

5.2 ところで近年, 大学のあり方が様々に問われ, その中で教育や研究においてもとかく即戦力が問題にされる傾向が強まっているが, この 3 節の内容は, その時流に逆らい, 即戦力とは対極にある息の長い理論的な学問のもつ底力について改めて私自身考えるよい機会となった.

5.3 次いで 4 節では, Turing の結果を現実の万能コンピュータに繋ぐ重要な橋渡しの役を von Neumann がどのような形で果たしたかについて考察した. これまで私自身, von Neumann が ENIAC グループの議論をまとめるに当たって, 何故グループの人々に断りなく彼一人の名前でそれを書いたのか, また, このレポートで Turing について一言も触れていないのは何故かという疑問を感じていた. しかし, 今回 4 節のテーマについて考えているうちに, Turing の仕事を von Neumann が現実的なコンピュータのアーキテクチャというレベルで表現したからこそ, それが多くの人々に伝わり, 結果として, 不自然なものではなく望ましい構造をもった万能コンピュータが世の中に広まったことを好運に感じた. なおこの件に関連して, 英国のマンチェスター大学と国立物理学研究所のコンピュータ開発計画に Turing と彼の論理学上の師である von Neumann が関わった由であるが, 彼らの果たした役割についても時間があれば調べてみたい.

5.4 私はこれまで理系の立場からコンピュータ・サイエンスの基礎理論とその関連分野の研究・教育を行ってきたが, 最近, 教育上の必要からコンピュータの歴史を調べ始めてみて, まだ謎につつまれた部分が多く, 自分であれこれ想像を巡らす余地が沢山あり面白い分野だと思うようになった. その面白さの一つは, 近年コンピュータを巡る状況が次第に総合科学的な様相を呈しつつあるが, コンピュータの歴史も従来より幅広い視点から見直すことに意味がありそうだと気付いたことである. その幅広い視点の一つとして, ここに理学的な視点からコンピュータの歴史を考える試みを行った次第である. ただし, 私自身は歴史にもコンピュータ技術 (特にハードウェア) にも昏く, 従って本稿にも多くの間違いや無理解があるのではないかと懸念する. 読者諸賢の忌憚のないご批判を頂ければ幸いである.

参考文献

[1] W. Aspray: John von Neumann and the Origins of Modern Computing, MIT Press, 1990.

23例えば [4] を見よ.

[2] W. Aspray and A. Burks (eds.): Papers of John von Neumann on Computing and Computer Science, MIT Press, 1987.

[3] J. Bell and M. Machover: A Course in Mathematical Logic, North-Holland, 1977.

[4] N. Bourbaki: Éléments d’Histoire des Mathématiques, Hermann, 1969. 村田全他訳「ブルバキ数学史」東京図書, 1970.

[5] M. Campbell-Kelly and W. Aspray: Computer: A History of the Information Machine, BasicBooks, 1996.

[6] M. Davis (ed.): The Undecidable - Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Raven Press, 1965.

[7] M. Davis:The Universal Computer - The Road from Leibniz to Turing, W. W. Norton & Company, 2000.

[8] J. W. Dawson: Logical Dilemmas, A. K. Peters, 1997.

[9] K. Gödel: On undecidable propositions of formal mathematical systems, Lecture notes by S. C. Kleene and J. B. Rosser, Inst. for Advanced Study, Princeton. (Reprinted with corrections in [6, pp. 39–74].)

[10] H. H. Goldstine: The Computer - From Pascal to von Neumann, Princeton University Press, 1972.

[11] A. Hodges: Alan Turing: The Enigama, Walker & Campany, 2000.

[12] J. E. Hopcroft, R. Hotwani and J. D. Ullman: Introduction to Automata Theory, Languages, and Computation, Second Edition, Addison Wesley, 2001.

[13] 星野力「誰がどうやってコンピュータを創ったのか?」共立出版, 1995.

[14] J. Lambek: How to program an infinite abacus, Can. Math. Bull., Vol. 4, pp. 295–302(1961).

[15] N. Macrae: John von Neumann, Pantheon Bools, 1992. 渡辺正他訳「フォン・ノイマンの生涯」朝日選書 610, 1998.

[16] L. F. Menabrea and A. A. Lovelace: Sketch of the analytical engine invented by Charles Babbage,

http://www.fourmilab.ch/babbage/sketch.html

[17] N. Metropolis et al. (ed.): A History of Computing in the Twentieth Century, Academic Press, 1980.

[18] M. L. Minsky: Recursive unsolvability of Post’s problem of “tag” and other topics in the theory of Turing machines, Ann. Math. Bull., Vol. 34, pp. 437–455(1961).

[19] E. L. Post: Finite combinatory processes - formulation 1, J. Symbolic Logic, Vol. 1,pp. 103–105(1936). (Reprinted in [6, pp. 289–291].)

[20] B. Randell: The COLOSSUS, in [17, pp. 47–92(1980)].

[21] 佐々木力「二十世紀数学思想」みすず書房, 2001.

[22] 高橋秀俊「電子計算機の誕生」中公新書 273, 1972.

[23] 高橋正子「計算論 - 計算可能性とラムダ計算」近代科学社, 1991.

[24] A. H. Taub (ed.): John von Neumann: Collected Workes, Macmillan, Vol. 1, pp. 339–422(1960).

[25] A. Turing: On computable numbers with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, ser. 2, vol. 42(1936), pp.230–267. Correction: vol. 43(1937), pp. 544–546. (Reprinted in [6, pp. 116–154].)

[26] A. Turing: Computability and λ-definability, J. Symbolic Logic, vol. 2, pp. 153–163(1937).

[27] J. von Neumann: Mathematishce Grundlagen der Quantenmechanik, Springer, 1932.

[28] J. von Neumann: First Draft of a Report on the EDVAC, Moore School of Electrical Engineering, University of Pennsylvania, 1945. (Reprinted in [2, pp. 17–82].)

数学的連続性から哲学的連続性へ

村田全

この問題についての報告の内, 次のものを発表順に番号付きで引用する.

[1] 連続性の問題, 第 1 報; 2001, 4 月, 北大; “Hokudai ronri”(on line journal) 既刊.

[2] 私論「連続性の問題」の梗概; 2001, 8 月, 京大数理研『数学史の研究』 (in printing).

[3] 数学的連続と形而上学的連続; 2001, 10 月, 津田塾大 (in printing).

[1] の第 2 報は現在執筆中で, 今回の話はその一部になるが, これは [3] の小修正である.

§1. 一般的注意

(1) 数学: 数学は言葉の一種で, 仮定から導かれる結果に関する形式的記号体系である. しかしこれは「出来上がった数学」のことで, 形成期の数学は純形式的なものではなく, 経験科学に近い面を持つ. 論理も同様で, それらの形成には人類の長い経験が働いている. 私はこの意味で, 数学を経験的要素をもつ学問と考え, 自然科学のみでなく, 人文科学や社会科学の「文法」として寄与しうる基本的な学問と考えている.

(2) 連続: ここではその意味を数学あるいは自然科学に限定せず, それらの「連続性」の根底には「時の流れ」のような混沌たる形而上学的な契機が隠れていると見る. この流れは普通, 実数で表現される例が多いので, 先ず数学的実数論の連続性を検討するが (§2), これを論ずるのがこの主題ではない. 私は後にこの流れの中の「今」を自分の哲学の中心に置き, これを「根元的連続」と呼んで, そこから「時間」 , 「空間」 , あるいは数学その他の学問における「連続性」などを根拠づけようとしている. 「今」はいわば形而上学的で超越的な連続である.

(3) 言語: 学問的言語は矛盾律によって諸概念を峻別し, それらを論理的推論によって段階的に展開するという意味で離散的である. 私はこの離散的な言語も「根元的連続」から導こうとしているが, これはなかなか離しい. ここにはベルグソンの生の哲学から, 『荘子』や禅の不立文字などにつながる思想の歴史があり, それらも簡単には無視できない. しかし, 特に荘子や禅哲学などは理論的学問になりにくいので, その芳ば意識しつつも, 最終的にはそこからの離脱の道を考える.

§2. 数学的連続; デデキントの実数論

(4) デデキントの実数論は, 連続や運動の概念を前置せずに集合 (多者) の概念だけを用いて組立られた卓抜なもので, 解析学や物理学での運動の理論はその実数論を基にして得られている. しかし上記の立場から見ると, 個々の「集合」は変化や運動をしないから (だからこそ言語として使える!), 運動そのものを表してはおらず, 運動を表現するには別の工夫が要る・むしろ「運動」を「多者・集合」で置き換えたのがデデキントの優れた創意であり, そこに現代数学の卓越性があるのだが, 彼が「連続性」の背後に, 理論以前の想念と理論との関係について考えいたことは, 『連続と無理数』 §2 に見られる.

「“直線を左右に「切断」するとき, 分点は一つ且つ唯一つだけ存在する”という原理を誰もが自明と思い, 自分の直線の表象と一致すると思うならば幸いである. その原理の正しさは私にも証明できず, また誰にもできないから… 直線にこの性質を認めるのは公理であり, それによって初めて我々は連続性を直線の中に持ちこんで考えうる… もし空間が現実的存在性を持つとしても, その空間は必ずしも連続とは限らない… 仮に空間が不連続だと分かったとしても, 望むならば, 思考の中でその隙間を満たすことによって一つの連続者を作るのに何の支障もない. それは点個体を新たに創造することであり, 上の原理によって実行できることが分かっているからである. 」

デデキントは数を ‘人間精神の自由な創造物’ とする立場だが, 上の引用文からは, 彼の創造的精神と形式的な実数の連続性との底に, その潜在的原型としての直線の連続性, ひいては直線を引く運動体験などの原始的体験を感じ取る. 「精神の自由な創造」を調う彼にしてなおこの言のあることを注意する.

これを私流にいうと, 連続の根元的な形は, 視覚や聴覚に基づくノッペラボウなイメージと, 体や心の持つ流れるような運動感覚 (感性的) で, デデキントの理論は前者はともかく後者は捨象している, あるいは表面には出さない. 一般に, 理論は感性よりは悟性の産物で, 事実, デデキントの理論に現れる有理数, 点, 直線, 集合などの概念は正に一悟性的対象である. ここに感性と悟性の関係, 悟性的存在の存在性の問題が生ずる.

要するに, デデキントの理論は時間, 空間の連続性に一つの確かな足がかりを与え, 連続的変化, 運動の表現に「場」を与えるが, 変化, 運動そのものを直接に表現はしていない. 連続的変化を与えるのは, 変数 (variable) なる記号の導入と「任意の点」を固定する論理的手法との工夫である. 例えば区間での連続関数は, 区間の任意の点で連続な関数として原子論的, 論理的に定義されている.

この工夫は極めて卓抜だが, 点の走り具合までを直接的に集合で表現するものではなく, 点が走るのは思考の中に止まっている. またそれでこそ論理が使えるのである.

実数論, 解析学ないしその物理学等への応用は, 論理的整合性よりもその現実的成果によって受け容れられるもので, 私が数学を経験科学的側面をもつとした一つの理由はこのようなところにもある.

上記, 感性と悟性の関係と悟性的対象の存在性との問題が今後の課題である. 前者については, 数学の実際において, デデキントの実数論などは, あたかも目に見える感性的対象に近くなり, その線を何処に引くかが問題になるし, 後者については, 連続的実数は何処に, どのように存在するかという種類のことが問題になる.

(5) ゼノンの逆理: これは上記, 変数の動きを論理的に把握しようとするとき, 先ず遭遇する蹟きの石である. 今回の議論はゼノン解釈を目的とするものではないが, 第 2 部では, この線上で一つの新しい解釈が得られることを期待しつつ考えている. 感性的対象と悟性的対象の差は, その一つの鍵だと私は考えている.

§3. 物理学等の経験科学における連続性

(6) 物理学における連続・不連続: (4) 項を受けて, 自然科学における連続性の所在を問う. 自然科学的連続性における認識主観と客観との関係は, 数学的連続とはひと味違った微妙な問題である.

ニュートン力学は古典解析学の形で書かれているが, これは自然に対する一つの理想化された数学モデルである. 理想が現実とかなり良く合うのは科学哲学の最大の不思議だが, 一方, その乖離は理想論に対する修正として理論の継子のように処理される. その大きな原因として摩擦があるが, これはまた自然解釈の連続性を破る元凶でもある.

一例は運動の発進, 停止である. ニユートン・モデルでは発進停止の説明は困難で, 摩擦を以って説明される. 粘性 v = 0 の (摩擦のない) 完全流体では渦が永久運動をすることになるのに, v (> 0) の流体に関する方程式 (Navier-Stokes) で v → 0 の極限値としても v = O の方程式にならないのも別の例である. これは関数の収束に関連し (関数空間における) 「連続性」の問題になる. これは摩擦と無関係だが, 過冷却や突沸のような状態変化も似ている (cf. 角田和雄『摩擦の世界』岩波新書). ともかく摩擦などの非保存的現象は本来のニュートンカ学では異分子で, これをニュートンの体系に繰り込むのは極めて難しい. 粘性体力学や粉体力学についてもいえる (cf. 田口善弘『砂時計の七不思議』 , 名著!).

量子力学では粒子と波動, 離散性と連続性の「矛盾」の問題が有名である. この矛盾には一応の説明が付いているが (Heisenberg, Schrodinger, Born), その理解にはヒルベルト空間での線形代数や, この波動の場が多数者に関する確率場であるとの理解が要る. そういえば, ニュートンカ学の場も単純なユークリッド空間でなく, 重力場であり輻射を伝達する物理空間である. このような「空間」の導入は解釈としては優れているにせよ, 悟性の産物であるこれらの空間の「実在性」には違和感を持つ. 時間についてはまだ別の面がある. その不可逆性はむしろ人間の実存的時間の本質と思うのに, それを支える事実が今度は熱力学の方にある. しかも面白いのはそこにも摩擦や熱放散を始め熱現象が絡むことである. 別に, 観測問題も「実在」の認識に伴う深刻な曲題を抱えている.

こうした次第で, 私はカントの空間論, 時間論に疑問を感じ, 特に自然の中に連続性が客観的に存在するという考えには懐疑的である.

(7) 前項では人間の認識と独立な「連続性」が人間の外的自然に内在するかを問うたが, 今度は内的自然について同じことを吟味する. ところがここでは連続性と走対の離散性が顕著に見られるのである.

視神経, 聴神経等の働きとそれらの信号の (ドミノ倒し的) 伝達が離散的であることはよく知られている. ところが我々は連続運動を見, 連続な音を聞くと思っている. そう思わせる働きは何か. それも神経の働きなのか. しかも最近の脳生理学ないし分子生物学では, 脳の働きを離れて「精神」あるいは「心」は存在しないとの考えが強く, 生命現象の一切を機械論的, 原子論的に説明できるとする物理還元主義が主流であるらしい.

してみると, 我々が連続運動を「見る」ことを説明するには, 物理的還元の中に超越的な何者かが要るのではないか. 前節では人間外の自然に連続性が内在することを疑ったが, 私はここで, 「精神」には, 内的自然か外的自然かは知らないが, その認識に「連続性」を付与する超越的契機があるとの考えをとる.

§4. 私の哲学的立場

(8) 私は自分の哲学の出発点を「永遠の今」 ( 「今」と略) という混沌たる現実存に置く. (2) 項でも述べたように, これは学問的分析には馴染まない, 学問を進めるには, 曰く言い難い「今」から脱出し, それをできるだけ客観化せねばならない.

私は「今」の中に「原記憶」 , 「原分別」 , 「原表現」の三つの契機を認める. 原記憶は「今」のもつ, のっぺらぼうな (通常の意味の) 連続が認識される契機, 原分別はそこに不連続な刻みを入れて異同の分別や分類を導かせる契機, 原表現は原記憶や原分別の結果を表出, 再現 (‘expressio’, ‘repraesentatio’; ライプニッツ) される契機で, 言語などの表現, 象徴の作用の母胎である. 文献 [5] ではこれを嬰児が知恵に目覚める状況を用いて具体化した. 「根元的連続」の中に (連続の契機である) 原記億と共に (非連続の契機である) 原分別を含めたのは, 「連続」は「非連続」がなければ意識されず, 逆も同じたからである.

私のここでの所論にはライプニッツの単子論の思想が影響している.

(9) 「今」からの脱出の分析は, 上記三つの潜在能力の吟味を含めて現在進行中で, 以下は希望的見通しを込めた将来の見取り図である. 私の考えでは「時間」 , 「空間」の問題に加えて「実体」の扱いにもカントと少し違いがある. それは窮極的にカントの「感性」と「悟性」の区別に由来する一実際の人間の思考においては, 悟性 (思考) の産物 (例えばユークリッド空間, ヒルベルト空間など) が, より進んだ段階の研究では, いわば高次の感性として機能している. これを勘定に入れてそれらの問題を考えようとしているが, その考えの芽はカントの統覚の中にも見出される. これらについては後節で触れる.

§5. カントの『純粋理性批判』覚え書き

(10) カント『純粋理性批判』の主題: それは真理性の根拠, 即ち人間は如何にして普遍妥当な真理に到達できるかの問いである. 感覚的知覚に頼るのみでは真理は得られないが, 論理一本で貫くには出発点である定義, 公理の真理性の保証を欠く. カントは大陸の合理論と英国 6 経験論の調停者であろうとし, 数学, 自然学の真理が普遍妥当と認められるために人間の理性が満たすべき要件を吟味した. これが彼の批判の方法である.

人間が自分の外界また内界を知るのは結局は感覚器官によるので, それ以外は「概念」によって「考え」られるだけである. 例えば現に眼で見ている物に対してその「物自体」の実在を知ろうとしても, 触覚や聴覚によるのでは所詮感覚から離れていない. より抽象的な概念に対する「物自体」の存在など分かりようがない. そこには一部の知識からの「綜合」という飛躍がある. その飛躍を避け通せば, 最も確実なはずの数学や物理学も取れない. そこをどう切り抜けるか, ここにカント哲学の大きな課題がある.

(11) 感性と悟性: 前項の問題を彼は克明に分析する. 大づかみにいうと「感性」は感覚器官に触発されて直観する働き, 「悟性」は直観に触発されて概念を作り, 概念について思考し判断する働きである. 感性と悟性は裁然と切り離される. 「認会載」は対象の直観に始まり, そこに悟性が働いて成立するが, 数学や物理学の真理性は認識でき, 「物自体」を認識すること許さないようにと, 「認識」の議論を組み立てねばならない.

感性は, 感覚の触発する直観の内容を時間, 空間の枠に整理して捉える. 時間, 空間は直観の「内容」を欠いた純粋の「形式」で, 感性に先だって人間に天与であるとする. 直観は対象を直接捉えるが, 時間, 空間は, その捉え方に関する「超越論的 (transzendental) 形式」で, 人間の精神が時間, 空間という天与の形式を共通に持つことが, 直観的認識の普通的妥当性の根拠とされる. 彼のこの後の議論には, この種の「超越論的」な, 現代流に言えばメタの道具立てが頻出し, “苦しい時の ‘超越論的’ 頼み”の感さえある. しかし物自体には手が届かぬまま, それの代替物について議論しようとすればこの種の議論は避けがたく, それでこそ数学や物理学の真理性も救えるのである. カントはその間の煩雑な論理的吟味を極めて克明に行っている. 私が「今」にまつわる議論を導入したのも同様の動機だが, その議論の整理はまだ不十分である.

一方, 悟性は直観に触発されて概念を生み, それについて思考し判断する精神能力だが, 感性の場合と同様, 悟性は, 思考内容を取り去った天与の「基本形式 ( 「カテゴリー」 )) に従って働くとされる. それは次の四組 (各組

三個, 計十二個) である. 「量」 (単一性, 多者性, 全体性), 「質」 (実在性, 否定性, 制限性), 「関係」 (実体と属性の関係, 原因と結果の関係, 能動者と受動者の相互関係), 「様相」 (可能性と不可能性, 現実的存在と非存在, 必然性と偶然性).

詳細は略すが, 人間が経験に即して客観的な判断ができるのは, 判断の枠組みであるこれらの形式が, 人間に共通かつ天下りに備わっていて判断を整理するからだとされる.

カテゴリーの種別は, 論理的判断における「量」 (単称, 特称, 全称), 「質」 (肯定, 否定, 無限定), 「関係」 (定言, 仮言, 選言), 「様相」 (蓋然, 突然, 必然) の各判断に対応する. 当時の論理学の状況に応じた, いささか人工的な感じさえするもので再吟味の余地はあるが, 下で見るように, 統覚の議論を予期して巧みに配慮されている.

(12) 統覚: 感性は対象を時空の枠に沿って把握し, 悟性は対象をカテゴリーに分けて把握するから, それらの知見の断片を綜合, 統一する働き, 「統覚」が必要である. その手近な例は眼や耳の受け取る無統一な感覚から一個の「物」を想像し, 各感覚をその物の属性として綜合することだが, 一般的に言うと, 人間の認識は感性的直観に始まり, 悟性がそれを概念化して考察するが, 最終的には感覚器官を介さなければ何も捉えられないとするのだから, 概念化以後の動きも結局は感性に捉えられるようにせねばならない. このことをカントは, 各カテゴリーの示す思考過程を, いわばそれの形として「時間」の中に投影することによって行う. この一連の議論は「図式論 (Schematismus)」と呼ばれ, カントの思索の中核で難解な部分である.

先ず, 統覚についてなお二三注意をしておく. 第 1 に, 統覚は感性でもなく悟性でもなく, 超越論的に両者の橋渡し役である. カントはこれを, 超越論的に考えられた「自己意識 (Selbstbewusstsein)」なるものに備わった「想像力 [構想カの率もある](Einbildungskraft)」のもつ「超越論的機能 (transzendental Funktion)」だとする. つまりその「想像力」が統一の源であり, そのカは “我考う (Ich debke)”の「我 (Ich)」に天下っているとするのである. 経験に足をおいたここまでの吟味を「我」の意識で集約するところが, 経験論と合理論の調停者としてのカントの思索の鍵である. 尤も, この前後はカント哲学の機微に当たる難しいところで, カント自身も第 1 版と第 2 版の間でその記述は揺れているほどである. ともかくこの「想像力」は万人に均しく備わっているとするので, 数学と経験科学との真理の普遍妥当性などは, 最終的にこうして保証されることになる.

統覚が感性と悟性, あるいは経験と理論, またあるいは帰納と演緯, を結ぶ鍵になっていることも注意すべきである. 実際, 統覚作用は経験からの帰納的知識を, 経験を超えた一般原理に飛躍させ, その原理を改めて経験界に引き戻すことに似ているが, 違うのは, その飛躍を「物自体」までにはさせぬようにする点である. 即ち, 感性的認識が悟性の思考の範囲以上には拡大できないと制約するのである. これまで「現象 (Erscheinung)」という言葉は説明なしに用いてきたが, これはカテゴリーを経験に支えられた範囲で用いる対象を意味し, 経験の及ぶ範囲外にまでカテゴリーを流用した仮象 (Schein) と区別する. 後者からは二律背反の生ずることが示されるので, 統覚作用の適用は現象に限るとするのである. 尤も, 私はこの辺の議論を十分理解している自信がないので詳細は成書に譲り, 次に「量」と「実体」のカテゴリーが時間の中に反映されるとはどんなことかについてだけ簡単に触れる (例えばカッシーラ: 『カントの生涯と学問 w) 沱 C 澆垢砂駛).

(13) 図式論: カテゴリーは元来, 概念を生む能力で直観に触発されて働くが, 図式論ではそれを逆に経験に適用しようとする. それは, 妥当性が (超越論的に) 確かめられる四つの「原則 (Grundsatz)」に沿って行われる. 例えば第 1 の原則「直観の公理: あらゆる現象は直観に関して外延量 (つまり部分から全体が分かるような量) をもつ」は, 時間, 空間における直観に関する限り, 妥当するために, 第 1 のカテゴリー「量」 (単一性, 多者性, 全体性) を時間の系列に反映させる. 即ち一つの時刻, 反復された時刻, 反復の完了の三つである. (カントの場合, 無限の全体までは考えなくて良いであろう. 尤もデデキントの自然数論を認め, 従って数学的帰納法を許すならば, 自然数の全体性までは採り入れられるが, いずれにせよ, これは現代数学の基礎付けの問題に属する.)

「実体」のカテゴリーは, 第 3 のカテゴリー「関係」 (実体と属栓, 原因と結果, 能動者と受動者の相互関係) に属するが, 「関係」は時間の順序に反映させられる. ここでは第 3 の原則「経験の類推: 経験 (的認識) は知覚の必然的結合の表象によってのみ可能である」が用いられ, 「原因」と「結果」は時間の前後関係, 「相互関係」は両者の同時的共存, そして「実体」は時間において持続するもの, 「属性」はそこにおいて変化するもの, にそれぞれ反映させられる.

第 2 の原則「知覚の先取的認識」は第 2 のカテゴリー「質」 (実在性, 否定性, 制限性) に関係し, 第 4 の原則「経験的思惟一般の公準」は第 4 のカテゴリー「様相」 (可能性と不可能性, 現実的存在と非存在, 必然性と偶然性) に関係するが, ここでは省略する. きちんとした説明ではないが, カントが, 概念を生む能力としてのカテゴリーを経験に適用する, と言った意味の示唆ぐらいにはなったであろうか.

彼はこの間, 経験的な「現象」と経験の裏付けを欠いた「仮象」とを分かち, 仮象からは純粋理性の二律背反が生ずることを示して, 純粋理性批判の真の対象範囲を現象界であるとし, 超越論的自我の想像力の及ぶ範囲をそこに制限するわけである. 彼は最後に「第 3 部超越論的方法論」として純粋理性の訓練や基準を説くが, 自分の議論構成のための私的覚え書きとしてはこれで止めてよいであろう.

しかしそれと共に, 彼の議論を, 無限集合を用いる現代数学をそのまま適用できないのもこの点にある. 早い話が, 現象と仮象を峻別しては, 本来, 経験にうったえる訳にいかない無限集合は仮象の議論になりかねない. 他方, その間の彼の分析の精緻巧妙さの故に, ここに手を着けて現代数学にまで及ぼうというのは泡に難しい.

なお「連続」の意味についてカントは特に注意していないように見える. 『純粋理性批判』で連続, 連続量 (Kontinuitat, kontinuierlich, quantum continuum) あるいは持続性 (Beharrlichkeit, beharrlich) などの言葉が現れるのは, 主として上記の第 2,3,4 の原則の部分 (岩波文庫版, 上巻 p.241-251; p.251-294, p.294-313) と, 二律背反を扱う「第 2 部超越論的弁証論」の「付録」 (中巻 p.305-367; 特に p.318-322) に集まっており, 他にはこの第 2 部に散見する程度である ( 「超越論的」は現行の文庫版では「先験的」 ).

§6. 「実体」についてこの試論の発端は時間, 空間, 実体の連続性に関する考え方の成立だが, それは「連続」を相似た事象が引き続き現れる状態とし, 現れ方を自然数や実数で並べて考えることと解しても良い. 勿論, この自然数, 実数は感覚的なもので理論的対象ではない. ところがその変化が理想的なディジタル時計のように真に離散的な形で進むか, アナログ型のように実数型になるか, あるいは中間的に有理数型になるかによって, ここで言う「実体」の様相は大きく変わり, しかも三者それぞれに問題がある. 即ち実数型では「実体」の「連続性」は保たれるが, その移りゆきの様子が見えにくい. 自然数型だと瞬間ごとに「実体」の発生, 生滅が繰り返されることになって, 「実体」の連続性または恒常性 (Beharrlichkeit) が失われる. 有理数型となると実体の連続性も保たれず, 無理数に当たる「孔」においてはどうなっているか, 見当もつかない. 少なくとも私はそう思う.

この瞬間的消失-発生 (あるいは滅亡-創造) は, インド哲学では「刹那滅」と呼ばれるが, これは理論としては奇怪に見える. 同様のことをライプニッツも. 「連続的創造 (creation continuee)」としているが, 同じように苦しい. いずれにせよ, この種の問題には連続性の保持は避けがたく見えるから, 私も「実体の連続性」を超越論的に認める.

「実体」の恒常性の下で, 物事の変化, 運動に関して動一不動が言えるために不動の「空間」が要請され, これで物の位置決定が可能になる. 但し実は, 真に直観的なのは身の回りの感性的な空間で, 数学的空間や物理空間ではない筈である. ヒルベルト空間等はもとより, 無限に広がるユークリッド空間なども既に悟性の産物である. 超越論的空間が, カントの示唆したような力学的空間だというのでは, 人は戸惑いを避けられないだろう.

私は彼のように感性と悟性を峻別するのでなく, 身の回りの感性的空間が悟性的構成を経て, (一段高い) 感性的空間になり, さらにそこから事の悟性化が進むというように, 感性界と悟性界の間には回り階段のような構造があると考えたい. カント流の感性と悟性の峻別を私が疑うのはこの理由によるが, 彼の統覚の議論はここで何らかの示唆を与えてくれるように思われる.

続いて空間と共に時間を要請する問題だが, とりあえずカントに従って, それは, (一瞬にもせよ) 空間に固定された (と考えられる) 対象が変わり行く状況を示すための「形式」として要請することにする. 但し勿論, これで時間論が片づいたわけではなく, この辺は大変むずかしい.

このようにして私は「空間」 , 「時間」の連続性の根を, 「実体」の連続性を経て「根元的連続性」にたどれると考えている. しかしこれとは別に, 「実体」や「空間」の連続性の根を「時間」の方におくとして議論を立てる余地は残っていると思う.

§7. 感性と悟性の関係以下は目下考慮中の, 全くの未定稿である. 目標は「連続」とは何かに一つの答えを与えることだが, 併せて現代数学の, カント的意味での批判的救済 (Save) も念頭にある.

カントは感性と悟性を峻別し ( 「感性は思考せず, 悟性は直観しない」 ), 但しその両者を, 「我」のもつ「想像力」の超越論的な機能である「統覚」を持ちだすことによって橋渡しした. これに対して, §6 でほのめかした「感性」と「悟性」の回り階段構造というのは, 直接的な第 1 次的感性に触発されて得た概念を第 1 次的悟性の仕事とし, それらの概念を第 2 次的感性での直観に繰り入れる; また第 1 次, 第 2 次的感性の触発した概念を第 2 次的悟性の仕事とし, それらを第 3 次的感性での直観に繰り入れる, … というように, 感性と悟性の意味を (峻別のまま) 初めは狭く取り, 順次それぞれを拡大して行く階層のつもりである. 上昇階段を上る動きを引き起こし, 次いでその結果を高次の感性に繰り入れる力には, 「統覚作用」の意味を少し変えて使おうとしている. 即ちそれは感性, 悟性に対しては超越論的だが, 本来の統覚ほど超越論的でないところの, 時間, 空間, あるｋ u 桙魯�謄乾蝓爾里茲Δ米��任△, むしろそれらの動き全体を生み, 支配するのが本来の超越論的働きとしたいのである.

言葉の問題もこの脈絡で考えたいテーマである.

勿論, 以上は目下の見込みで, 今後変更もあり得るし, そもそも夢物語に終わるかもしれない. 直ぐ分かるように, これの原型はラッセルの「型の理論」や記述集合論の「階層の理論」にあって, そこからは知恵が借りられるかもしれない. しかし最初で最大の難関は, その出発点, 例えば primitive recursive のような論理的に明確確定的な段階の議論がここに作りうるかが怪しいことである. 特に私のいわゆる混沌の「今」からことを始めようとすれば, 困難は倍加する. 仮にそれが切り抜けられても, その先も難しい. この記述では, 感性と悟性の階層構造をラッセルの「単純型理論 (simple type theory)」と決めているかに見えるかもしれないが, 事柄の性格上, とてもそれは期待できないでだろうと思っている. これらの吟味を進める上でも, 先に良く分かっていないと書いたカントの図式論は, もう少し勉強しないといけない. 文献 [1] の第 2 部では, これらの全面的な解明は望むべくもないが, 小さいこと w) 任發い�蕕�棲里癖鷙陲鬚靴燭い發里任△.

(28/II/’02; 加筆 30/V/’02)

古典論理の自然推論

古森雄一

Gentzen の直観主義論理の自然演繹体系 NJ の implicational fragmant は

k α ; Π ; β ; α ⊃ β k(⊃ i), \begin{matrix}α ⊃ β & α \\ β \end{matrix} (⊃ e),

という規則で構成されている. これは見事な体系であるが, 古典論理にするためには二重否定の除去などの自然演繹体系には相応しくない規則を付け加えなければならなかった. その古典論理の体系 NK が気に入らないから LK が考え出された. NJ, LJ, LK は非常に良い体系である.

NJ を拡大解釈して結論が複数 (0 個も含む) あることを認め規則 (⊃ i) において証明図 Π に結論 β が 0 個であることを認めることを考えると古典論理の体系になる. この体系は Prigot[1] の体系と本質的には同じものであると考えている. 例えば, Peirce の論理式 ((α ⊃ β) ⊃ α) ⊃ α の証明図は (L^{A}TEX では書きづらいのであるが, あえて書くと) 次のようになる:

\begin{matrix}\begin{matrix}{2 \atop (α ⊃ β) ⊃ α} & α ⊃ β 1 \\ α \end{matrix} & 1 α \\ ((α ⊃ β) ⊃ α) ⊃ α \end{matrix} 2.

この体系の reduction の一つは, 次の一回の (⊃ e) を二回の (⊃ e) の適用に変えるものである.

\begin{matrix}{Π_{1} \atop α ⊃ β α ⊃ β} & {Π_{2} \atop α} \\ β \end{matrix} (⊃ e)

二回の (⊃ e) の適用に変えたものは L^{A}TEX では非常に書きづらい. このように結論が複数個であるのは扱いにくい. そこで結論は 1 つしかない (⊃ e) と次の (Case) と (w) を持つ古典論理の体系が考えられた:

\begin{aligned}k α ; Π_{1} ; γ & {k \atop α ⊃ β} ; Π_{2} ; γ \\ & γ \end{aligned} ; k(Case),

Π β ; α ⊃ β (w).

適当に reduction を決めてやると, この体系の normal form は上から (⊃ e), (w), (Case) となる証明図になる. この体系は鹿島氏 (東工大) の作った体系を古森が改変したものであるが, normal な証明図があることが証明できる. この体系の部分論理式特性を示すのに, NJ(の {⊃, ⊥}-fragment) の証明図からこの体系の証明図への写像を利用し, NJ の正規化定理を用いた. NJ の {⊃, ⊥}-fragment には

⊥ α

という rule があるが, ⊥ を任意の fromula として

{β \atop α}

という rule に変えると古典論理になることに気付いた.

新しい体系として NJ に

Π α ; β a, Π α ; α ρa

を加える. 結果的にはこの体系は Parigot の体系と似ているが微妙に異なっている. この体系の方が Parigot の体系より証明図がコンパクトになる. この体系の normalization theorem の証明は意外に難しいが, βreduction の strong normalization theorem を使って示すことができる. この体系については [3] に書かれているが, ほぼ同じ内容が http://www.math.s.chiba-u.ac.jp/˜ komori/gakkai02-04/lambdar3.dvi にある.

参考文献

[1] Michel Parigot. λμ-CALCULUS: AN ALGORITHMIC INTERPRETATION OF CLASSICAL NAT-URAL DEDUCTION, Lecture Notes in Computer Science 624, pp. 190–201, 1992.

[2] Yuichi Komori. A natural deduction for classical logic, in which there exists a proof with the subformula property. In Proc. 33rd MLG meeting, pp. 3–6, Echigo Yuzawa, 2000.

[3] Yuichi Komori. λρ-Calculus: A Natural Deduction for Classical Logic, BULLETIN OF THE SEC-TION OF LOGIC, VOL. 31, No. 2, pp. 65–70, 2002.

概念と対象の理論について

佐藤雅彦 (京都大学大学院情報学研究科)

1 はじめに

われわれの数学的思考は，決して，個々の数学的理論の展開だけに向けられるものではない．現実に，われわれは，それらの諸理論間の相互関係などについても数学的思考を重ねている．このように，重層的な構造をもつ数学的思考を無理なく自然に理解するためには，私としては，在来の形式言語からも一歩踏み出して，その源泉へ遡ろうとしてみるほかなかった．

— 『概念対象理論の構想とその哲学的背景』 (小野勝次著, 1989 年) —

上で引用した小野勝次先生の著書は「個々の数学的理論の形式化は見事になされている」という観察のもとで「個々の数学的理論だけでなく，それらの相互の関係を形式化したい」という目標を持って書かれている．そのために，著者は数学的判断を表現する文の基本形：

S は P である

を概念対象理論構築の基礎に置いた．これは, 対象 S は概念 P にあてはまるということである．この P も数学的対象と考えて，小野勝次先生はこれを概念対象とよんだ．

1.1 私なりの小野哲学の解釈

• 数学の形式化は自然でないといけない．

• 自然な形式化をおこなう前に日常の数学をよく観察する必要がある．

• 超数学だけでなく，超超数学も考えよ．

1.2 小野先生の言葉

友よ，たとえ落ちこぼれようとも，あくまで理を追おうではないか．

1.3 目標

全数学の形式化 ⇒ コンピュータの発達で可能になる (はずの/べき) こと ⇒ 形式化は徹底的に!

2 私の概念と対象の理論

私の概念と対象の理論は，小野先生の上記著書の影響を強く受けている．現時点では，その基礎となる，判断と導出の理論がほぼできているので，以下にその概要を示す．

2.1 背景

• 「計算と論理」教育用計算機システム CAL の経験

• McCarthy の S 式の理論

• Martin Löf の式の理論

• Smullyan の Elementary Formal System

• 操作的意味論

• Martin Löf の型理論

• Edinburgh Logical Framework

• Gentzen の自然演繹

• 小野勝次の哲学 ( 「概念対象理論」 , 「思考の枠組」 )

2.2 CAL: Computation and Logic

• 京大学部 3 年生講義「計算と論理」

• 1998, 1999, 2000 後期 (工学部), 2001 前期 (理学部), 2001 後期 (工学部)

• 講義資料原案 (竹内), User Interface と Parser(佐藤), 導出検証系 (亀山)

• Emacs Lisp で実装

⇒ 講義で扱う体系をすべて実装し, CAL システムで実習する ⇒ 講義内容, CAL システムについての感想をレポートとして課している ⇒ 受講学生の批判を受けて改良

2.3 CAL の思想

• あらゆる数学的思考 = 判断行為

• 導出 = 判断行為の言語表現

• 判断 = 導出の結論 = 判断行為の結論の言語表現 = 判断内容

⇒ 導出 (= 証明) の対象は判断である. ⇒ 定理は, 導出可能な判断のこと!

判断の例

2 + 3 × 4 = 14

2.4 「計算と論理」講義内容

• 直観主義命題論理

• 単純型付 λ 計算

• 単純型付 λ 計算の項の簡約と直観主義命題論理の導出の簡約, Curry-Howard Isomorphism

• 算術 (Heyting Arithmetic)

• 定義と定理

• 算術の証明項

• 算術の証明項の簡約と算術の導出の簡約, Curry-Howard Isomorphism

• 構成的プログラミング

• 構成的意味論，非構成的意味論

3 問題と解答の例

3.1 例 1

Q[57]

以下の仮定付判断の PropProof における証明をつくれ．

A : Prop ├¬¬ (A ∨¬ A)
---------------------------------------------------------------------------
A[57]
[A : Prop ├¬¬ (A ∨¬ A) in PropProof since
¬¬ (A ∨¬ A) by imp_intro {
    (x:¬ (A ∨¬ A))[
        ⊥ by imp_elim {
            ¬¬ A by imp_intro {
                (y:¬ A)[
                    ⊥ by imp_elim {
                        x;
                        A ∨¬ A by or_intro_right {
                            y
                        }
                    }
                ]
            };
            ¬ A by imp_intro {
                (z:A)[
                    ⊥ by imp_elim {
                        x;
                        A ∨¬ A by or_intro_left {
                            z
                        }
                    }
                ]
            }
        }
    ]
}]

3.2 例 2

Q[96]

Ｍを適当に選び，以下の仮定付判断の LambdaTerm における証明をつくれ.

A : Prop ├Ｍ : ¬¬ (A ∨¬ A)
---------------------------------------------------------------------------
A[96]
[A : Prop ├
λ (x:¬ (A ∨¬ A))[λ (y:¬ A)[x(inr(A,y))](λ (z:A)[x(inl(¬ A,z))])] : ¬¬ (A ∨¬ A)
in LambdaTerm since
λ (x:¬ (A ∨¬ A))[
λ (y:¬ A)[x(inr(A,y))](λ (z:A)[x(inl(¬ A,z))])] : ¬¬ (A ∨¬ A) by imp_intro {
    (x:¬ (A ∨¬ A))[
        λ (y:¬ A)[x(inr(A,y))](λ (z:A)[x(inl(¬ A,z))]) : ⊥ by imp_elim {
            λ (y:¬ A)[x(inr(A,y))] : ¬¬ A by imp_intro {
                (y:¬ A)[
                    x(inr(A,y)) : ⊥ by imp_elim {
                        x;
                        inr(A,y) : A ∨¬ A by or_intro_right {
                            y
                        }
                    }
                ]
            };
            λ (z:A)[x(inl(¬ A,z))] : ¬ A by imp_intro {
                (z:A)[
                    x(inl(¬ A,z)) : ⊥ by imp_elim {
                        x;
                        inl(¬ A,z) :  A ∨¬ A by or_intro_left {
                            z
                        }
                    }
                ]
            }
        }
    ]
}]

3.3 例 3

Q[146]
Γ≡ A:Prop, B:Prop とするとき
        Ｄ←→λ (x:A ∨ B)[case(x, (y)[inr(B, y)], (z)[inl(A, z)])] under Γ

となる命題論理の証明Ｄを求めよ．

---------------------------------------------------------------------------
A[146]
[A ∨ B ⊃ B ∨ A by imp_intro {
    (x:A ∨ B)[
        B ∨ A by or_elim {
            x;
            (y:A)[
                B ∨ A by or_intro_right {y}
            ];
            (z:B)[
                B ∨ A by or_intro_left {z}
            ]
        }
    ]
}]

3.4 例 4

Q[147]
Γ≡ A:Prop, B:Prop, u:A, v:B とするとき
    A by imp_elim {
      A ∧ B ⊃ A by imp_intro {
        (x:A ∧ B)[A by and_elim_left {x}]
      };
      A ∧ B by and_intro {u; v}
    }
    ←→Ｍ under Γ

となるλ項Ｍを求めよ．

---------------------------------------------------------------------------
A[147]
[λ (x:A ∧ B)[left(x)]([u, v])]

3.5 例 5

Q[181]

以下の仮定付判断の ArithProof における証明をつくれ. (Hint. 数学的帰納法を使う. 前問を定理として登録すると利用できるかもしれない.)

├∀ (x,y)[x+y = y+x]
---------------------------------------------------------------------------
A[181]
[├∀ (x,y)[x+y = y+x] in ArithProof since
∀ (x,y)[x+y = y+x] by univ_intro {
    (x:Nat)[
        ∀ (y)[x+y = y+x] by univ_intro {
            (y:Nat)[
                x+y = y+x by comm_plus {}
            ]
        }
    ]
}]

3.6 例 6

加法の可換性の証明．

Theorem[comm_plus]
[x:Nat, y:Nat ├ x+y = y+x in ArithProof since
x+y = y+x by univ_elim {
    ∀ (y)[x+y=y+x] by ind {
        x+0 = 0+x by repl {
            x+0 = x by plus_0 {};
            x = 0+x by sym_of_eq {
                0+x = x by lemma2_zero_plus {}
            }
        };
        (y:Nat, Y:x+y=y+x)[
            x+s(y) = s(y)+x by repl {
                x+s(y) = s(y+x) by repl {
                    x+s(y) = s(x+y) by plus_s {};
                    Y
                };
                s(y+x) = s(y)+x by repl {
                    (y+s(0))+x = s(y)+x by repl {

(y+s(0))+x = (y+s(0))+x by refl {};
y+s(0) = s(y) by repl {
    y+s(0) = s(y+0) by plus_s {};
    y+0 = y by plus_0 {}
}
};
(y+s(0))+x = s(y+x) by repl {
(y+s(0))+x = y+s(x) by repl {
    (y+s(0))+x = y+(s(0)+x) by asso_plus {};
    s(0)+x = s(x) by lemma1_one_plus_is_succ {}
};
y+s(x) = s(y+x) by plus_s {}
}
}
}
]
}
}]

3.7 例 7

Q[195]

以下の仮定付判断の ArithProof における証明をつくれ.

├∀ (x)[Even(x) ∨ Odd(x)]
---------------------------------------------------------------------------
A[195]
[├∀ (x)[Even(x) ∨ Odd(x)] in ArithProof since
∀ (x)[Even(x) ∨ Odd(x)] by ind {
Even(0) ∨ Odd(0) by or_intro_left {
Even(0) by def_intro {
∃ (z)[0=s(s(0))*z] by exist_intro {
0 = s(s(0))*0 by sym_of_eq {
s(s(0))*0 = 0 by times_0 {}
}
}
}
};
(x:Nat, X:Even(x) ∨ Odd(x))[
Even(s(x)) ∨ Odd(s(x)) by or_elim {
X;
(Y:Even(x))[
Even(s(x)) ∨ Odd(s(x)) by or_intro_right {
Odd(s(x)) by def_intro {
∃ (z)[s(x)=s(s(0))*z+s(0)] by exist_elim {
    ∃ (z)[x=s(s(0))*z] by def_elim {
        Y
    };
    (y:Nat, Y:x=s(s(0))*y)[
        ∃ (z)[s(x)=s(s(0))*z+s(0)] by exist_intro {
            s(x)=s(s(0))*y+s(0) by repl {
                s(x)=x+s(0) by sym_of_eq {
                    x+s(0)=s(x) by repl {
                        x+s(0)=s(x+0) by plus_s {};
                        x+0=x by plus_0 {}
                    }
                };
                Y
            }
        }
    ]
}
}

                }
            ];
            (Z:Odd(x))[
                Even(s(x)) ∨ Odd(s(x)) by or_intro_left {
                    Even(s(x)) by def_intro {
                        ∃ (z)[s(x)=s(s(0))*z] by exist_elim {
                            ∃ (z)[x=s(s(0))*z+s(0)] by def_elim {
                                Z
                            };
                            (y:Nat, Y:x=s(s(0))*y+s(0))[
                                ∃ (z)[s(x)=s(s(0))*z] by exist_intro {
                                    s(x)=s(s(0))*s(y) by repl {
                                        s(x)=s(s(s(0))*y+s(0)) by repl {
                                             s(x)=s(x) by refl {};
                                             Y
                                        };
                                        s(s(s(0))*y+s(0))=s(s(0))*s(y) by sym_of_eq {
                                             s(s(0))*s(y) = s(s(s(0))*y+s(0)) by repl {
                                                 s(s(0))*s(y) = s(s(0))*y+s(s(0)) by times_s {};
                                                 s(s(0))*y+s(s(0)) = s(s(s(0))*y+s(0)) by plus_s {}
                                             }
                                        }
                                    }
                                }
                            ]
                        }
                    }
                }
            ]
        }
    ]
}]

3.8 例 8

Q[210]

以下の仮定付判断の ArithProof における証明をつくれ. 証明方針をよく考えて，必要な補助定理をあらかじめ登録してからこの判断の証明をつくれ.

├∀ (m,n)[n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)]]
---------------------------------------------------------------------------
A[210]
[├∀ (m,n)[n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)]] in ArithProof since
∀ (m,n)[n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)]] by univ_intro {
  (m:Nat)[
    ∀ (n)[n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)]] by univ_intro {
      (n:Nat)[
        n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)] by univ_elim {
          ∀ (m)[n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)]] by ind {
             n=0 ∨∃ (q,r)[0=n*q+r ∧ LT(r, n)] by or_elim {...};
             (m:Nat, X:n=0 ∨∃ (q,r)[m=n*q+r ∧ LT(r, n)])[
                n=0 ∨∃ (q,r)[s(m)=n*q+r ∧ LT(r, n)] by or_elim {...}
                        ]
                    }
                }
            ]
        }
    ]
}]

4 CAL の進化

• 1998, 1999 版では判断の文脈 (仮定列) をつねに明示した.

\begin{matrix}Γ ⊢ A & Γ ⊢ B \\ Γ ⊢ A ∧ B \end{matrix}

• 2000, 2001 版では導出ゲームの概念を導入し, 推論の前後で変化する文脈だけを記述するようにした.

• 2002 版では, 自然な枠組 (Natural Framework) を導入し, 導出ゲームごとに検証系を実装しないですむようにする.

4.1 Natural Framework の階層

数学 = 概念と対象の理論という思想. 例：数の概念自然数, 整数, 有理数, 実数, 複素数.

Semantics 概念と対象の理論判断と導出の理論式とスキーマの理論 S 式の理論 Syntax

4.2 Natural Framework は何故 natural か?

Natural Framework = Gentzen の Natural Deduction の芯を取り出したもの.

4.3 論理教育の難所

• 変数と代入

• 仮定の概念

• 仮定のもとでの推論

• 仮定の除去

• 固有変数 (eigen variable) Edinburgh LF では型理論の上に framework を実装.

⇒ 上記の難所は, judgement-as-types の原理と高階の型で処理. ⇒ 問題の本質的解決になっていない.

(論理をはじめて学習する人に最初に (!) Edinburgh LF を教えないといけない!) ⇒ 問題の本質的解決には哲学が必要．

5 式の理論

• 可算無限個の対象変数 (x, y, z).

• 可算無限個の定数 (c).

対象変数は可算無限個の一般変数と可算無限個の導出変数 (X, Y, Z) に分類される. 異る対象変数の列 x_{1}, …, x_{n} を文脈 (context) という.

5.1 式 (expression) の定義

{x ∈ Γ \atop Γ式 x} 対象変数{c 定数 \atop Γ式 c} 定数

\begin{matrix}Γ式 e & Γ式 f \\ Γ式 ⟨e|f⟩ \end{matrix} 対{Γ, x 式 e \atop Γ式 (x)[e]} 抽象

α 同値な式は区別しない. ⟨e_{1}, e_{2}, …, e_{n}⟩ は ⟨e_{1}|⟨e_{2}| ⋯ ⟨e_{n}|nil⟩ ⋯⟩⟩ のこと.

5.2 規則はスキーマだ

                                A : Prop B : Prop

                                   A ∧ B : Prop ∧F

は規則のスキーマ. A を 0 = 1, B を 1 = 2 とすれば, 具体的な規則

                            0 = 1 : Prop 1 = 2 : Prop

0 = 1 ∧ 1 = 2 : Prop ∧ F

が得られる.

A, B は規則のパラメータ. A, B の動く範囲は? A, B は式であれば何でもよい!

                                0 : Prop 1 : Prop

                                   0 ∧ 1 : Prop ∧ F

も規則．

5.3 スキーマの理論

式の理論を拡大するために可算無限個のスキーマ変数 (z, X) を追加する．

{z スキーマ変数 \atop Γスキーマz} スキーマ変数

{x ∈ Γ \atop Γスキーマx} 対象変数{c 定数 \atop Γスキーマc} 定数
\begin{matrix}ΓスキーマS & ΓスキーマT \\ Γスキーマ⟨S|T ⟩ \end{matrix} 対{Γ, x スキーマS \atop Γスキーマ(x)[S]} 抽象
\begin{matrix}ΓスキーマS & ΓスキーマT \\ ΓスキーマS[[T]] \end{matrix} 適用

5.4 スキーマの評価

ρ : V_{s} → E

は, 有限個の z を除いて, ρ(z) ≡ nil となるとき環境であるという. 1. [[z]]_{ρ} :≡ ρ(z).

2. [[x]]_{ρ} :≡ x.

3. [[c]]_{ρ} :≡ c.

4. [[⟨S|T ⟩]]_{ρ} :≡ ⟨[[S]]_{ρ}|[[T]]_{ρ}⟩.

5. [[(x)[S]]]_{ρ} :≡ (x)[[[S]]_{ρ}]. (We assume, without loss of generality, that for any z occurring in S, x is not free in ρ(z).)

6. [[S[[T]]]]_{ρ} ≡ [x := [[T]]_{ρ}(e), where ρ(S) ≡ (x)[e]. ρ(S) が抽象でないときには, [[S[[T]]]]_{ρ} ≡ nil と定める．

6 導出ゲーム

判断を導出するための個々の形式体系を「導出ゲーム」として一様な形式で与えることができる．

6.1 判断の形式

• Categorical Judgment: s : P. 対象 s は概念 P にあてはまる.

• Hypothetical Judgmnent: H ⇒ J.

• Universal Judgment: (x)[J]. 判断は式により表現される. s : P は ⟨:, s, P ⟩ の略記. H ⇒ J は ⟨⇒, H, J⟩ の略記. 判断は文脈のもとで定められる.(Γ判断J)

6.2 規則のスキーマ

以下の形の閉じたスキーマを規則のスキーマという．

⟨RS, J, ⟨c, z_{1}, …, z_{m}⟩, ⟨H_{1}, …, H_{n}⟩⟩

このスキーマを以下のようにも表記する．

\begin{aligned}H_{1} & ⋯ & H_{n} \\ & J \end{aligned} c(z_{1}, …, z_{m})
J : −_{c(z_{1},...,z_{n})} H_{1}, …, H_{n}.

R_{1}, …, R_{n} が規則のスキーマのとき,

⟨R_{1}, …, R_{n}⟩

のことを導出ゲームという.

6.3 導出文脈 Γ とその一般変数部分 GV(Γ)

1. 空文脈. 空リスト ⟨⟩ は導出文脈で GV(⟨⟩) ≡ ⟨⟩.

2. 一般変数宣言. Γ が導出文脈, x が Γ で宣言されていない一般変数ならば, Γ ⊕ ⟨x⟩ は導出文脈でその一般変数部分は GV(Γ) ⊕ ⟨x⟩.

3. 導出変数宣言. Γ が導出文脈, J が GV(Γ) のもとでの判断で X が Γ で宣言されていない導出変数ならば, Γ ⊕ ⟨X :: J^{24}⟩ は導出文脈でその一般変数部分は GV(Γ).

Γ が導出文脈のとき, Γ-環境とは任意のスキーマ変数 z に対して, ρ(z) が GV(Γ) のもとでの式であるような環境のこと．

6.4 G-導出とその結論

1. 導出変数. X が導出変数で X :: H が Γ の要素ならば，

X

は Γ のもとでの G-導出でその結論は H である.

2. 合成. D_{1}, …, D_{n} が Γ のもとでの G-導出で, これらの結論が H_{1}, …, H_{n} であり,

\begin{aligned}H_{1} & ⋯ & H_{n} \\ & J \end{aligned} R(e_{1}, …, e_{m})

が G の規則のスキーマをある Γ 環境で評価したもので, さらに J が GV(Γ) のもとでの基本判断 (categorical judgment) ならば,

\begin{aligned}D_{1} & ⋯ & D_{n} \\ & J \end{aligned} R(e_{1}, …, e_{m})

は Γ のもとでの G-導出でその結論は J である.

24X :: J is an abbreviation of ⟨::, X, J⟩.

3. Hypothetical derivation. D が Γ ⊕ ⟨X :: H⟩ のもとでの G-導出でその結論が J ならば,

(X :: H)[D]

は Γ のもとでの G-導出でその結論は H ⇒ J である．

4. Universal derivation. D が Γ ⊕ ⟨x⟩ のもとでの G-導出でその結論が J ならば,

(x)[D]

は Γ のもとでの G-導出でその結論は (x)[J] である．

このことを以下のように表記する．

                              Γ ⊢ J in G since D

6.5 判断の形

• X •

\begin{aligned}D_{1} & ⋯ & D_{n} \\ & J \end{aligned} R(e_{1}, …, e_{m})

この判断は

J by R(e_{1}, …, e_{m}) {D_{1}; …; D_{n}}

とも書くことがある．

• (X :: H)[D]

• (x)[D]

6.6 Nat

                       0 : Nat zero()  {n : Nat \atop s(n) : Nat} succ(n)

⊢ (x)[x : Nat ⇒ s(s(x)) : Nat] in Nat since

(x)[(X :: x : Nat)[

  s(s(x)) : Nat by succ(s(x)){
        s(x) : Nat by succ(x){X}

} ]]

6.7 NJ

\begin{matrix}\begin{matrix}A ⊃ B^{Y} & A^{X} \\ B \end{matrix} & ^{⊃^{E}} \\ (A ⊃ B) ⊃ B \end{matrix} ; ⊃^{I}, Y ; A ⊃ (A ⊃ B) ⊃ B ; ⊃^{I}, X

{(X :: A)[ {(Y :: A ⊃ B)[\begin{aligned}Y & & X \\ & B \end{aligned} ^{⊃^{E}}] \atop (A ⊃ B) ⊃ B} ^{⊃^{I}}] \atop A ⊃ (A ⊃ B) ⊃ B} ^{⊃^{I}}

6.8 λ 計算

(x)[x : Term ⇒ M[[x]] : Term] λ(x)M[[x]] : Term λF    M : Term N : Term app(M, N) : Term appF

Y :: y : Term ⊢ λ(x)[app(x, y)] : Term in Term since

λ(x)[app(x, y)] : Term by λF{

(x)[(X :: x : Term)[

           app(x, y) : Term by appF{
                x : Term by triv{X};
                y : Term by triv{Y }

} ]]

}

参考文献

[1] 小野勝次, 「概念対象理論の構想とその哲学的背景」 , 1989.

[2] M. Sato, Y. Kameyama and I. Takeuti, CAL: A computer assisted learining system for computation and logic, in Moreno-Diaz, R., Buchberger, B. and Freire, J-L. eds., Computer Aided Systems Theory – EUROCAST 2001, Lecture Notes in Comupter Science, 2718, pp. 509 – 524, Springer 2001.

[3] Masahiko Sato, Theory of judgments and derivations, in Arikawa, S. and Shinohara, A. eds., Progress in Discovery Science, Lecture Notes in Artificial Intelligence 2281, pp. 78 – 122, Springer, 2002.

Effective Convergence

M.Yasugi,Y.Tsujii,M.Mori,M.Washihara

X is a non-empty set. T = ⟨X , {U_{\}}⟩: a uniform space.

Definition 0.1 {U_{n}} on X is an effective uniformity: there are recursive functions α_{3}, α_{4},α_{5}, U_{I}^{∗} x ∈ U_{n}(x).

U_{II}^{∗} ∩_{n∈N}U_{n}(x) = {x}. U_{III}^{∗} U_{α_{3}(n,m)}(x) ⊂ U_{n}(x) ∩ U_{m}(x). U_{IV}^{∗} x ∈ U_{α_{4}(n)}(y) ⇒ y ∈ U_{n}(x). U_{V}^{∗}

x ∈ U_{α_{5}(n)}(y), y ∈ U_{α_{5}(n)}(z) ⇒ x ∈ U_{n}(z).

(2) Two (effective) uniformities, say {U_{n}} and {V_{n}}, on a set X are effectively topologically equivalent if there are recursive functions μ_{1} and μ_{2}, x ∈ X, V_{μ_{1}(n)}(x) ⊂ U_{n}(x) and U_{μ_{2}(n)}(x) ⊂ V_{n}(x).

Proposition 0.2 There is a recursive function α_{6},

∀n∀x, y, z ∈ X(x ∈ U_{α_{6}(n)}(z) ∧ y ∈ U_{α_{6}(n)}(z) ⇒ y ∈ U_{n}(x))

Definition 0.3 (Effective convergence) (1) A sequence {x_{k}} ⊂ X effectively converge to x ∈ X if there is a recursive function γ, ∀n∀k ≥ γ(n)(x_{k} ∈ U_{n}(x)).

Can generalize to multiple sequences.

1 Refinement and uniform covering

Definition 1.1 (Refinement and expansion) Let U and V be coverings of X.

(1) U ≻ V (U is a refinement of V):

∀U ∈ U∃V ∈ V(U ⊂ V)

(2)

U ⋀ V := {U ∩ V : U ∈ U, V ∈ V}

(3)

S(x, U) := ∪{U : x ∈ U ∈ U}
S(E, U) := ∪{U : U ∈ U, E ∩ U ≠ ϕ} where E ⊂ X.
U^{Δ} := {S(x, U) : x ∈ X}
U^{∗} := {S(U, U) : U ∈ U}

Proposition 1.2 (1) For a uniformity {U_{n}}, each U_{n} is a covering (3) {S(·, U_{n})} is a uniformity.

Definition 1.3 {U_{n}}: a sequence of uniform coverings {U_{n}} is called effective if: V_{I}^{∗} For any covering U,

∀n ∈ N(U ≻ U_{n}) → U = Δ = {{x} : x ∈ X}.

V_{II}^{∗} There is a recursive function α_{II}

∀n, m(U_{α_{II}(n,m)} ≻ U_{n} ⋀ U_{m}).

V_{III}^{∗} There is a recursive function α_{III}

U_{α_{III}(n)}^{Δ} ≻ U_{n}.

(2) {U_{n}} is called a normal sequence of coverings if U_{n+1}^{∗} ≻ U_{n} holds.

Theorem 1.4 An effective uniformity {U_{n}} is an effective sequence of uniform coverings.

Proof V_{I}^{∗} ∼ V_{III}^{∗} for {U_{n}}?

V_{I}^{∗}: classical V_{II}^{∗}: α_{II} ≡ α_{3} V_{III}^{∗}: α_{III} ≡ α_{6}

Theorem 1.5 {U_{n}} ⟶ {V_{n}} an effective normal sequence of coverings, an effective uniformity, topologically effectively equivalent to {U_{n}}

Proof Define λ(0) = 0.

λ(n) = α_{6}α_{6}α_{3}(λ(n − 1), n).
μ_{1}(n) = n; μ_{2}(n) = λ(n)

U_{III}^{∗}: Put η_{3}(l, k) = α_{3}(λ(l), λ(k)). U_{IV}^{∗}: η_{4}(l) := α_{4}(λ(l)). U_{V}^{∗}: η_{5}(l) := α_{5}(λ(l)).

2 General construction of metric: review

Definition 2.1 We will define V (x, r) for arbitrary x ∈ X and arbitrary dyadic number r ∈ (0, 1].

V (x, 1) := S(x, V_{0})

V (x, \frac{1}{2^{n}}) := S(x, V_{n})

For r = \frac{1}{2^{n−1}} , \frac{2}{2^{n−1}} , ⋯, 1 − \frac{1}{2^{n−1}} (> \frac{1}{2^{n}}),

V (x, r + \frac{1}{2^{n}}) := S(V (x, r), V_{n})

Definition 2.2 f_{x}(y) := sup{r|y ∈ V (x, r)^{c}}

d_{x}^{∗}(y, z) := |f_{x}(y) − f_{x}(z)|

d^{∗}(y, z) := sup_{x} d_{x}^{∗}(y, z)

Proposition 2.3 (1) If x ∈ S(y, V_{n}), then d^{∗}(x, y) ≤ \frac{1}{2^{n−1}} .

(2) If d^{∗}(x, y) < \frac{1}{2^{n}}, then x ∈ S(y, V_{n}).

3 Effective convergence

Theorem 3.1 Let {x_{mk}} and {x_{m}} be sequences from X. Then the former effectively converges to the latter as k → ∞ in ⟨X, {U_{n}}⟩ if and only if it does in ⟨X, d^{∗}⟩.

Proof {U_{n}}, {V_{n}} and {S(∗, V_{n})} are topologically effectively equivalent Show the equivalence with respect to {S(·, V_{n})} and d^{∗} Suppose there is a recursive ν_{1},

∀k ≥ ν_{1}(m, n)(x_{mk} ∈ S(x_{m}, V_{n})).

Put ν′_{1}(m, n) = ν_{1}(m, n + 2). Then, (1) above,

∀k ≥ ν′_{1}(m, n), d^{∗}(x_{mk}, x_{m}) ≤ \frac{1}{2^{(n+2)−1}} < \frac{1}{2^{n}} .

Suppose there is a recursive ν_{2} such that

∀k ≥ ν_{2}(m, n)(d^{∗}(x_{mk}, x_{m}) < \frac{1}{2^{n}}).

By (2), x_{mk} ∈ S(x_{m}, V_{n}). Remark No computability property for {x_{mk}} or {x_{m}} is assumed.

4 Fréchet space and metrization

X: a Fréchet space with {p_{m}}, seminorms

Definition 4.1 (1) {x_{nk}} of X converges to {x_{n}} effectively: there exists a recursive function ϕ,

k ≥ ϕ(n, p) implies p_{m}(x_{nk} − x_{n}) ≤ 1/2^{p}.

(2) The definition of computability structure on a Fréchet space:

Axiom 1 (effective linear combinations)

Axiom 2 (effective limits)

Axiom 3′ (Seminorms). If {x_{n}} ∈ S, then {p_{m}(x_{n})} is a computable double sequence of reals.

Metrizations of (X, {p_{m}})

d_{1}(x, y) = ∑_{m=0}^{∞} p_{m}(x − y)/(2^{m}(1 + p_{m}(x − y))),

d_{2}(x, y) = max_{m}p_{m}(x − y)/(2^{m}(1 + p_{m}(x − y)))

d_{1} and d_{2} preserve computability U_{n} = {x : p_{n}(x) < 1/2^{n}} D =set of all finite binary fractions in the interval (0, 1) r ∈ D,

r = 1/2^{i_{1}} + 1/2^{i_{2}} + ... + 1/2^{i_{ℓ}} (1 ≤ i_{1} < i_{2} < ... < i_{ℓ}),
A(r) = U_{i_{1}} + U_{i_{2}} + ⋯ + U_{i_{ℓ}}

ϕ(x) = \{ \begin{matrix}inf\{r ∈ D : x ∈ A(r)\}, & if x ∈ A(r) for some r, \\ 1, & otherwise, \end{matrix}

U + V = {x + y : x ∈ U, y ∈ V }.

d_{3}(x, y) = ϕ(x − y).

Preserves computability? Effective convergence with respect to d_{1}, d_{2} or d_{3}: simlarly to real sequences They are all equivalent to effective convergence with respect to seminorms.

References

[1] Y.Tsujii, M.Yasugi,T.Mori, Some properties of the effective uniform topological space,LNCS 2064 (2001), Springer, 336-356.

[2] M. Yasugi, V. Brattka, M. Washihara, Computability aspects of some discontinuous functions, SCMJ Online, 5(2001),405-419.

[3] M.Yasugi, Y.Tujii and T.Mori, Metrization of the uniform space and effective convergence, to appear in MLQ.

[4] M.Yasugi and Y.Tsujii, Two notions of sequential computability of a function with jumps ENTCS 66 no.1 (2002): http://www.elsevier.nl/locate/entcs/volume66.html

[5] For more information: http://www.kyoto-su.ac.jp/ yasugi/Recent/

[6] M.Yasugi and M.Washihara, Sugaku Expositions (AMS), 13(2000), 215-235.

Multi-modal logics の Shannon type 標準形展開による特性化

大芝猛

[0] 標題のテーマは「命題論理における選言標準形展開と恒真性検証手続きを multi-modal logics の場合に拡張する内容」に関するものである.

命題論理 P L_{0} において,

(1) 高々m 変数を持つ論理式 A ∈ ^{(m)}L に対して, m 変数最小項の全集合 {p_{1}^{δ_{1}} ∧ ⋯ ∧ p_{m}^{δ_{m}}|δ_{1}, …, δ_{m} ∈

{0, 1}} = ^{(m)}W の部分集合^{(m)}W [A] = {f_{1}, …, f_{n}} ⊆ ^{(m)}W がきまり, その選言和について,

P L_{0} ⊢ A ≡ f_{1} ∨ ⋯ ∨ f_{d} (= ^{∗(m)}W [A] とかく: 命題論理の選言標準形)

となる. (ただし, p^{1} = p， p^{0} = ¬p.)

(2) またすべての m 変数最小項の選言和^{∗(m)}W について

P L_{0} ⊢ ^{∗(m)}W

が示される. 更に決定手続きについて, 次の性質が有効である.

(3) 任意の A ∈ ^{(m)}L に対し,

P L_{0} ⊢ A ⇔ ^{(m)}W [A] = ^{(m)}W (選言標準形の最小項全体が全集合^{(m)}W に一致) . (ここで展開の base として, 変数の個数 m = 1, 2, … に対応して, ^{(1)}W, ^{(2)}W, ^{(3)}W, … が必要.)

[1] multi-modal logics の modal 記号 K_{1}, …, K_{n}, (□_{1}, …, □_{n}) の n は固定するとして, (たとえば n = 3), A = (p_{1} ∧ p_{2}) ∨ K_{2}(K_{1}(p_{1} ∨ p_{3}) ∧ K_{3}(p_{2})) ∈ ^{(3)}L^{(2)} のように, 高々m 個の変数, 深さ k の論理式の全体を (m)L^{(k)} とかく (m = 1, 2, …; k = 0, 2, …), またこれらに対応して, 展開の base も^{(m)}W^{(k)} (m = 1, 2, …; k = 0, 2, …) が必要である. また^{(m)}W^{(k)} の要素を index m, degree k の拡張された最小項と呼ぶ.

[2] 標準形展開構造: ⟨^{(m)}W^{(k)}, ^{(m)}W, ∗⟩ on ^{(m)}L^{(k)} (m = 1, 2, …; k = 0, 2, …):

• 拡張された最小項集合の列^{(m)}W^{(k)} (m = 1, 2, …; k = 0, 2, …) および

• 論理式 A ∈ ^{(m)}L^{(k)} に対する最小項展開集合^{(m)}W [A] を対応させる mapping:

(m)W · : A ∈ ^{(m)}L^{(k)} → ^{(m)}W [A] ⊆ ^{(m)}W^{(k)}

と

• 最小項集合 U ⊆ ^{(m)}W^{(k)} に選言和型論理式を対応させる mapping:

∗ : U ⊆ ^{(m)}W^{(k)} → ^{∗}U ∈ ^{(m)}L^{(k)}

を適切に定義するならば, 多くの modal-logics L についても命題論理同様に, (1) 任意の論理式 A ∈ ^{(m)}L^{(k)} に対して,

L ⊢ A ≡ ^{∗(m)}W [A]

となる; また, m 変数, degree k のすべての最小項の選言和型論理式^{∗(m)}W^{(k)} について

(2) L ⊢ ^{∗(m)}W^{(k)} が示される; 更に決定手続きについて, 次の性質が有効となる.

(3) 任意の論理式 A ∈ ^{(m)}L^{(k)} に対して,

L ⊢ A ⇔ ^{(m)}W_{L}^{(k)} ⊆ ^{(m)}W [A]

ただし, ^{(m)}W_{L}^{(k)} = {f ∈ ^{(m)}W^{(k)}|L ⊬ ¬^{∗}f} ⊆ ^{(m)}W^{(k)};

が成立する.

(def.) 以上のような 2 重列^{(m)}W_{L}^{(k)} = {f ∈ ^{(m)}W^{(k)}|L ⊬ ¬^{∗}f} (m = 1, 2, …; k = 0, 2, …) を logic L を特性化する集合列 (basis) という. また，全最小項集合の列^{(m)}W^{(k)} (m = 1, 2, …; k = 0, 2, …) を multi-modal logics の展開全体の base-sequence(基底集合列) という.

有限集合^{(m)}W_{L}^{(k)}, ^{(m)}W [A] の要素が列挙可能なとき，条件 (3) は L での証明可能性の決定条件となる. (後述の構造の定義によれば, ^{(m)}W [A] の要素は列挙可能となる.)

(def.）条件 (1), (2) の成立する logic L を Shannon type logic とよぶ.

[3] ^{(m)}L^{(k)} 上の標準形展開構造 S: ⟨^{(m)}W^{(k)}, ^{(m)}W, ∗⟩ (m = 1, 2, …; k = 0, 1, …) を次のように定義することにより, 拡張された最小 normal 論理 K を含む様々な論理が Shannon type となる.

(def.） base sequence(基底集合列) の定義.

(m)W^{(0)} = {p_{1}^{δ_{1}} ∧ ⋯ ∧ p_{m}^{δ_{m}}|δ_{1}, ⋯, δ_{m} ∈ {0, 1}} = ^{(m)}W,
(m)W^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W^{(k)}, X_{1}, …, X_{n} ⊆ ^{(m)}W^{(k)}}
(k = 0, 2, …)
(m = 1, 2, …).

(def.) 最小項またはその集合 U ⊆ ^{(m)}W^{(k)} の論理式への mapping:

∗ : U ⊆ ^{(m)}W^{(k)} → ^{∗}U ∈ ^{(m)}L^{(k)}.

1. {f_{1}, …, f_{d}} ⊆ ^{(m)}W^{(k)} に対し, ^{∗}{f_{1}, …, f_{d}} = ^{∗}f_{1} ∨ ⋯ ∨ ^{∗}f_{d}. ∗∅ = ⊥.

2. f = p_{1}^{δ_{1}} ∧ ⋯ ∧ p_{m}^{δ_{m}} ∈ ^{(m)}W^{(0)} に対し, ^{∗}f = p_{1}^{δ_{1}} ∧ ⋯ ∧ p_{m}^{δ_{m}} ∈ ^{(m)}L^{(0)}.

3. f = ⟨g, ( K_{1}[U_{1}] ; ⋮ ; K_{n}[U_{n}] )⟩ ∈ ^{(m)}W^{(k+1)} に対し,

∗f = ^{∗}g ∧ ^{∗}(K_{1}[U_{1}])^{(m,k+1)} ∧ ⋯ ∧ ^{∗}(K_{n}[U_{n}])^{(m,k+1)} ∈ ^{(m)}L^{(k+1)}.

4. U ⊆ ^{(m)}W^{(k)} に対し,

∗(K_{i}[U])^{(m,k+1)} = K_{i}(^{∗}(U)^{(m,k)}) ∧ ⋀_{U⊈X⊆^{(m)}W^{(k)}} ¬K_{i}(^{∗}(X)^{(m,k)})

ただし Notation:

∗(U)^{(m,k)} = ^{∗}U(U ≠ ∅),^{∗} (∅)^{(m,k)} = ⊥ ∧ ^{∗(m)}W^{(k)},

いずれも degree= k の論理式を対応させる.

(註) ^{∗}(K_{i}[U])^{(m,k+1)} の意味について: unimodal, m = 2 の場合. 2 つの最小項 f = p ∧ q, g = p ∧ ¬q 等について, たとえば, K(f ∨ g) の選言展開を考えるとき, その degree= 1 の要素として K(f), K(g) は必要といえるが, 十分ではない. それは, K(f ∨ g) ⇐ K(f) ∨ K(g) なるも, K(f ∨ g) ⇏ K(f) ∨ K(g) となるからである. この同値へのギャップを埋めるために, (∗) K(f ∨g)∧¬K(f)∧¬K(g) = ^{∗}K[{f, g}] という定義を用いると, normal 論理 K で K ⊧ K(f ∨g) ≡ K(f)∨K(g)∨ ^{∗}K[{f, g}] と展開しうる. 4. の定義はこの (∗) の一般化である. また, notation ^{∗}(∅)^{(m,k)} = ⊥ ∧ ^{∗(m)}W^{(k)} などについては: 展開の根幹に必要な mapping ^{(m)}W [ ] が mapping ∗ の inverse になるという性質: Theorem 0 ：^{(m)}W [^{∗}U] = U のために必要である. w) 燭箸┐ n = 1, deg= 2 の場合, f = ⟨f_{0}, K[∅], K[∅]⟩, ∅ ⊆ ^{(m)}W^{(0)}, ∅ ⊆ ^{(m)}W^{(1)} について, ^{∗}(∅)^{(m,k)} = ⊥ を定義とするならば, ^{(m)}W [^{∗}{f}] = {⟨f_{0}, K[∅]⟩} ≠ {f} となり, 不都合をきたすからである. (deg = 1 deg = 2 の位置の ∅ を^{(m,k)} によって区別すると同時に, 論理式^{∗}(∅)^{(m,k)} に deg = k の情報を保持させる必要がある.)

(def.) 論理式の最小項集合への mapping

(m)W [ ] : A ∈ ^{(m)}L^{(k)} → ^{(m)}W [A] ⊆ ^{(m)}W^{(k)}

0. ^{(m)}W [⊥] = ∅;

1. ^{(m)}W [p_{i}] = {p_{1}^{δ_{1}} ∧ ⋯ ∧ p_{i−1}^{δ_{i−1}} ∧ p_{i} ∧ p_{i+1}^{δ_{i+1}} ∧ ⋯ ∧ p_{m}^{δ_{m}}|δ_{1}, …, δ_{i−1}, δ_{i+1}, …, δ_{m} ∈ {0, 1}};

2. A ∨ B ∈ ^{(m)}L^{(k)} ⇒ ^{(m)}W [A ∨ B] = ^{(m)}W [A]^{⟨k⟩} ∪ ^{(m)}W [B]^{⟨k⟩};

3. A ∧ B ∈ ^{(m)}L^{(k)} ⇒ ^{(m)}W [A ∧ B] = ^{(m)}W [A]^{⟨k⟩} ∩ ^{(m)}W [B]^{⟨k⟩};

4. ¬A ∈ ^{(m)}L^{(k)} ⇒ ^{(m)}W [¬A] = ^{(m)}W^{(k)} − ^{(m)}W [A];

5. A ⊃ B ∈ ^{(m)}L^{(k)} ⇒

(m)W [A ⊃ B] = (^{(m)}W^{(k)} − ^{(m)}W [A]^{⟨k⟩}) ∪ ^{(m)}W [B]^{⟨k⟩};

6. K_{i}(A) ∈ ^{(m)}L^{(k+1)} ⇒

(m)W [K_{i}(A)] = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W^{(k)}, X_{1}, …, X_{n} ⊆ ^{(m)}W^{(k)}, X_{i} ⊆ ^{(m)}W [A]}

(Notation) ただし, U ⊆ ^{(m)}W^{(d)}, d ≤ k に対して, U^{⟨k⟩} = U\overbrace{′ ⋯′}^{k − d}, V ⊆ ^{(m)}W^{(d)} に対して,

V′ = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ V, X_{1}, …, X_{n} ⊆ ^{(m)}W^{(d)}}.

Theorem 0 U ⊆ ^{(m)}W^{(k)} に対して, ^{(m)}W [^{∗}U] = U (^{(m)}W [ ] は ∗ の inverse mapping). 論理に無関係な mapping としての性質.

Theorem 1 L が Shannon type(条件 (1), (2) をみたす論理) なら, 「(3): 任意の A ∈ ^{(m)}W^{(k)} に対し, L ⊢ A ⇔ ^{(m)}W_{L}^{(k)} ⊆ ^{(m)}W [A]」も成立する. Theorem 2

◯^{1} L_{1} が Shannon type logic かつ L_{1} ≺ L_{2} ならば， L_{2} も Shannon type logic.

◯^{2} L_{1}, L_{2} が Shannon type logic ならば,

∘ L_{1} ⪯ L_{2} ⇔ ^{(m)}W_{L_{1}}^{(k)} ⊇ ^{(m)}W_{L_{2}}^{(k)} (for all m ≥ 1, k ≥ 0),
∘ L_{1} ≺ L_{2} ⇔ ^{(m)}W_{L_{1}}^{(k)} ⊇ ^{(m)}W_{L_{2}}^{(k)} (for all m ≥ 1, k ≥ 0)
& ^{(m)}W_{L_{1}}^{(k)} ⊃ ^{(m)}W_{L_{2}}^{(k)} (for some m ≥ 1, k ≥ 0).

[4] 前記 [3] 項で定義した展開構造 S : ⟨^{(m)}W^{(k)}, ^{(m)}W, ∗⟩ (m = 1, 2, …; k = 0, 1, …) のもとで, Shannon type となるいくつかの拡張された modal logic をあげる.

• 拡張された最小 normal logic K:

Axiom (K): 1) tautologies.

2) K_{j}-axioms:

{K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))|ϕ, ψ ∈ L}_{(j=1,...,n)}

rule (K): 1) modus ponens.

2) K_{j}-rules:

\{\frac{ψ}{K_{j}(ψ)} | ψ ∈ L\}(j = 1, …, n).

ただし, (notation) L = ∪{^{(m)}L^{(k)}|m = 1, 2, …; k = 0, 1, …}.

• (minimum) Shannon type logic K^{∼}:

K の Axioms のうち 2) K_{j}-axioms を次のよう換えた論理. 2’) {K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))|ϕ, ψ ∈ L, degree(ϕ) = degree(ψ)} (j = 1, …, n).

• KΣ ⋯ Σ type 論理: K にさらにいくつかの公理を追加して得られる論理.

[5] 前述の^{(m)}L^{(k)} の上の標準形展開構造 S : ⟨^{(m)}W^{(k)}, ^{(m)}W, ∗⟩ (m = 1, 2, …; k = 0, 1, …) の上で, K^{∼} ,K さらに KΣ ⋯ Σ type 等の一連の論理の特性化を提示するために, まず, つぎの定理が重要である.

Theorm 3 U ⊆ ^{(m)}W^{(k)} に対し, K^{∼} ⊢ K_{i}(^{∗}(U)^{(m,k)}) ≡ ⋁_{X⊆U}(^{∗}(K_{i}[X])^{(m,k+1)}): ∗-mapping の中の定義

4）^{∗}K_{i}[U]^{(m,k+1)} = K_{i}(^{∗}(U)^{(m.k)}) ∧ ⋀_{U⊈X⊆^{(m)}W^{(k)}} ¬K_{i}(^{∗}(X)^{(m,k)}) の逆解に対応.

Theorm 4 K^{∼} は特性集合が^{(m)}W_{K^{∼}}^{(k)} = ^{(m)}W^{(k)} となる Shannon type logic であることが示される. (前

半の証明は次々項 [8] の定理による.)[後半: K^{∼} が Shannon type であることの証明.]

• Shannon type での条件 (2) K^{∼} ⊢ ^{∗(m)}W^{(k)} については, k に関する induction による:

• K^{∼} ⊢ ^{∗(m)}W^{(0)} については, K^{∼} が命題論理を含むので成立.

• K^{∼} ⊢ ^{∗(m)}W^{(k)} を仮定する,

(m)W^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W^{(k)}, X_{1}, …, X_{n} ⊆ ^{(m)}W^{(k)}}.

∗ の定義から,
∗(m)W^{(k+1)} = ⋁_{x∈^{(m)}W^{(k)}} ⋁_{X_{1}⊆^{(m)}W^{(k)}} ⋯

⋁_{X_{n}⊆^{(m)}W^{(k)}}(^{∗}x ∧ ^{∗}(K_{1}[X_{1}])^{(m,k+1)} ∧ ⋯ ∧ ^{∗}(K_{n}[X_{n}])^{(m,k+1)})

≡ ⋁_{x∈^{(m)}W^{(k)}} ^{∗}x ∧ ⋁_{X_{1}⊆^{(m)}W^{(k)}} ^{∗}(K_{1}[X_{1}])^{(m,k+1)} ∧ ⋯

∧ ⋁_{X_{n}⊆^{(m)}W^{(k)}} ^{∗}(K_{n}[X_{n}])^{(m,k+1)} ⋯ in PL0.

従って, 前定理と「∗ の定義の 4) の記法: ^{∗}(^{(m)}W^{(k)})^{(m,k)} = ^{∗}(^{(m)}W^{(k)}) (∵ ^{(m)}W^{(k)} ≠ ∅)」から,

∗(m)W^{(k+1)} ≡ ^{∗(m)}W^{(k)} ∧ K_{1}(^{∗}(^{(m)}W^{(k)})) ∧ ⋯ ∧ K_{n}(^{∗}(^{(m)}W^{(k)})) ⋯ in K^{∼}.

一方, 帰納法の仮定と K_{j}-推論によって, K^{∼} ⊢ K_{j}(^{∗}(^{(m)}W^{(k)})). 故に, K^{∼} ⊢ ^{∗}(^{(m)}W^{(k+1)}).

• Shannon type での条件 (1) も前定理と mapping ^{(m)}W [A] の定義を用いて類似に示される.

この定理から, K^{∼} はこのような展開構造 S において, 特性化される最も弱い logic となる. また,

(3) K^{∼} ⊢ A ⇔ ^{(m)}W [A] = ^{(m)}W^{(k)} が成立する. また， K^{∼} より強い logic として,

Theorm 5 拡張された最小 normal logic K さらに KΣ ⋯ Σ type 論理は Shannon type logic となる.

[6] 以上のような論理 L のいくつか (拡張された T, S5, … 等) について, L を特性化する展開の basis (m)W_{L}^{(k)} (m = 1, 2, …; k = 0, 1, …) を「‘要素である最小項の形を具体的に特定できる集合’」として表し、末尾の別表に与える.

[7] 論理 L に対応するその特性化集合列^{(m)}W_{L}^{(k)} (m = 1, 2, …; k = 0, 1, …) を得るための候補として, (def.) L のトートロジー以外の公理 (形) の集まり

Ax(L) = ∪_{1≤i≤d}{A_{i}(ψ_{1}, …, ψ_{r_{i}})|P i(ψ_{1}, …, ψ_{r_{i}})}

から導入される k-inductive な集合列:

(m)W_{Ax(L)}^{(0)} = ^{(m)}W^{(0)},
(m)W_{Ax(L)}^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W_{Ax(L)}^{(k)}, X_{1}, …, X_{n} ⊆ ^{(m)}W_{Ax(L)}^{(k)}}

∩ ⋂_{1≤i≤d} ⋂_{ψ_{1},...,ψ_{r_{i}} ∈^{(m)}L,P i(ψ_{1},...,ψ_{r_{i}}),deg(Ai(ψ_{1},...,ψ_{r_{i}}))=k+1} ^{(m)}W [Ai(ψ_{1}, …, ψ_{r_{i}})]

(k = 0, 2, …; m = 1, 2, …)

を選ぶ． (註) ただし (def.) k-inductive な集合列とは次の性質をもつ集合列をいう:

(m)S^{(0)} = ^{(m)}W ^{(0)},
(m)S^{(k+1)} ⊆ {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}S^{(k)}, X_{1}, …, X_{n} ⊆ ^{(m)}S^{(k)}}
(m = 1, 2, …; k = 0, 2, …).

Proposition トートロジー A ∈ ^{(m)}L^{(k)} について, ^{(m)}W [A] = ^{(m)}W^{(k)} が成立する.

そして, 次の定理が成り立つ.

Theorem 6 L の公理 (形) の集まりから導入される集合列について,

(m)W_{Ax(L)}^{(k)} = ^{(m)}W_{L}^{(k)}
⇔ ‘(^{(m)}W_{Ax(L)}^{(k+1)}) = ^{(m)}W_{Ax(L)}^{(k)}
(m = 1, 2, …; k = 0, 2, …).

(Notation) V ⊆ ^{(m)}W^{(k+1)} に対して,

‘V = {y ∈ ^{(m)}W^{(k)} | ∃X_{1}, …, ∃X_{n} ⊆ ^{(m)}W^{(k)}, ⟨y, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ ∈ V }.

[8]

Theorem 7 L = K^{∼} の場合, 特性化集合は^{(m)}W_{K^{∼}}^{(k)} = ^{(m)}W^{(k)} (m = 1, 2, …; k = 0, 2, …) (base sequence 自身) になる.

[証明] まず, 特性化の候補として^{(m)}W_{Ax(K^{∼})}^{(k)} を求める. K^{∼} の公理系は

Ax(K^{∼}) = ⋃_{1≤j≤n}{K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))|ϕ, ψ ∈ L, deg(ϕ) = deg(ψ)}.

ただし, 論理式 ϕ, ψ に対する条件 deg(ϕ) = deg(ψ), deg(K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))) = k + 1 のもとで, deg(ϕ) = deg(ψ) = k となる. さらに「(Proposition) この条件 deg(ϕ) = deg(ψ) = k の下での任意の論理式 ϕ, ψ に対し, 集合として^{(m)}W [K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))] = ^{(m)}W^{(k+1)}」を確かめうる. 従って, inductive な定義の^{(m)}W_{Ax(K^{∼})}^{(k+1)} の第 2 項も^{(m)}W^{(K+1)} となるので, 全体としても^{(m)}W_{Ax(K^{∼})}^{(k+1)} = ^{(m)}W^{(k+1)} (k = 0, 1, …) となる. 従って, ‘(^{(m)}W_{Ax(K^{∼})}^{(k+1)}) = ^{(m)}W_{Ax(K^{∼})}^{(k)} となり, 前 theorem 6 により, ^{(m)}W^{(k)} (k = 0, 1, …) 自身が K^{∼} の特性化集合を与える.

[9] L = K, T, S5, K_{I→J} などについても, 別表の公理から導入される候補集合がそのまま^{(m)}W_{Ax(L)}^{(k)} = (m)W_{L}^{(k)} (m = 1, 2, …; k = 0, 1, …) となり, 特性化集合列を与えることを確かめうる. [K_{I→j} は S5 に公理 {K_{I}(ϕ) ⊃ K_{J}(ϕ)|ϕ ∈ L} を付け加えた logic.] [10] 特性化集合列の 1 つの応用として，

Proposition K^{∼} ⊢ K_{j}(A) ⇒ K^{∼} ⊢ A (j = 1, …, n) を示してみる. J = 1 の場合: A ∈ ^{(m)}L^{(k)} のとき, Theorem 1 と前々項の結果 Theorem 7 から,

K^{∼} ⊢ K_{1}(A) ⇒ ^{(m)}W [K_{1}(A)] ⊇ ^{(m)}W_{K^{∼}}^{(k+1)} = ^{(m)}W^{(k+1)}.

従って,

(m)W [K_{1}(A)] ∋ ⟨x, ( K_{1}[^{(m)}W^{(k)}] ; ⋮ ; K_{n}[^{(m)}W^{(k)}] )⟩ for some x ∈ ^{(m)}W^{(k)}

一方,

(m)W [K_{1}(A)] = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W^{(k)}, X_{1}, …, X_{n} ⊆ ^{(m)}W^{(k)}, X_{1} ⊆ ^{(m)}W [A]}

故に, ^{(m)}W^{(k)} ⊆ ^{(m)}W [A]. K^{∼} は Shannon type 故, 再び Theorem 1 から, K^{∼} ⊢ A.

謝辞

このテーマについては, 様々な方々にお世話になりました. 標準形展開による S5 の拡張に対応する multimodal logic の検証のテーマを思いついた段階から, 佐藤雅彦先生, 古森雄一先生には最初フォーマライズする段階で, また小野寛晰先生には金沢の研究室で最初のまとまりを見た段階で, 静岡大学の白井古希男先生, 鈴木信行先生には, さらに一般化の段階で研究室にて話をし, コメントを伺うなどいたしました. その間勤め先でのコンピュータ管理に携わっていたため中断をしましたが, 最近ようやくこの問題の本質の一面がわかってきたように思っております. また, さらに他のモデルとの関係等を含めて調べていきたいと考えております.

おわりに, 小野勝次先生には, 発足のころから参加した MLG を通してロジックに対する取り組みについてご指導いただきましたこと, また当時は, 様相論理研究の松本和夫先生のおられた静岡大学工学部で数理言語の研究をしておりましたことから, 最近, 論理プロパーに近いテーマにアプローチし, この小野勝次先生を記念するシンポジュウムに参加できましたことを深く感謝いたします.

参考文献

[1] J.Hintikka: Knowledge and belief, Cornel University Press 1962.

[2] M.Sato: A study of Kripke-type Models for some Modal Logics by Gentzen’s Sequential Method, Publications Research Institute for Mathematical Science, Kyoto University, 1977.

[3] 笹尾勤: 論理設計, 近代科学社, 1995.

[4] 大芝猛, 小橋一秀: 知識命題の標準形を用いる妥当性検証, 数理解析研究所考究録, 906, pp132-137,1995.

[5] 大芝猛, 小橋一秀: 知識論理・様相論理の標準形展開基底による特性化, 数理解析研究所考究録, 950, pp189-192, 1996.

[6] 大芝猛: 最小 normal logic より小さい擬論理の標準形展開, 数理解析研究所考究禄, 1093, pp168-172, 1999.

別表論理 L の公理の集まり Ax(L) = ∪_{1≤i≤d}{A_{i}(ψ_{1}, …, ψ_{r_{i}})|P i(ψ_{1}, …, ψ_{r_{i}})} 対応の k-inductive な集合列^{(m)}W_{Ax(L)}^{(k)} により L を特性化する集合列^{(m)}W_{L}^{(k)} を次に与える.

((註) Ax(L) にトートロジーを含めないことについては, Theorem 6 の直前の Proposition 参照.)

[以下一般に, 最小項 f ∈ ^{(m)}W^{(k)} に対し, notation: F_{j}^{(d)}(⊆ ^{(m)}W^{(d−1)}) (k ≥ d ≥ 1) は次の位置の集合を表す.

f = ⟨f^{(0)}, ( K_{1}[F_{1}^{(1)}] ; ⋮ ; K_{n}[F_{n}^{(1)}] ) , …, ( K_{1}[F_{1}^{(k−1)}] ; ⋮ ; K_{n}[F_{n}^{(k−1)}] ) , ( K_{1}[F_{1}^{(k)}] ; ⋮ ; K_{n}[F_{n}^{(k)}] )⟩ ∈ ^{(m)W^{(k)}}

また, notation: f = ⟨f^{(0)}, f^{(1)}, …, f^{(k − 1)}, f^{(k)}⟩ もあわせて用いる.]

(0) K^{∼}: Ax(K^{∼}) = ⋃_{1≤j≤n}{K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))|ϕ, ψ ∈ L, deg(ϕ) = deg(ψ)}:

(m)W_{Ax(K^{∼})}^{(k)} = ^{(m)}W^{(k)}(m = 1, 2, …; k = 0, 1, …) ⋯ [Theorem 7].

(1) K: Ax(K) = ⋃_{1≤j≤n}{K_{j}(ϕ ⊃ ψ) ⊃ (K_{j}(ϕ) ⊃ K_{j}(ψ))|ϕ, ψ ∈ L}:

(m)W_{Ax(K)}^{(0)} = ^{(m)}W^{(0)},
(m)W_{Ax(K)}^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W_{Ax(K)}^{(k)}, X_{j} ⊆ ^{(m)}W_{Ax(K)}^{(k)}(j = 1, …, n),

k ≥ 1 ⇒ ‘X_{j} = X_{j}^{(k)}(j = 1, …, n)}
(k = 0, 2, …); (m = 1, 2, …).

(2) T: Ax(T) = Ax(K) ∪ ∪_{1≤j≤n}{(K_{j}(ϕ) ⊃ ϕ)|ϕ ∈ L}:

(m)W_{Ax(T)}^{(0)} = ^{(m)}W^{(0)},
(m)W_{Ax(T)}^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W_{Ax(T)}^{(k)}, X_{j} ⊆ ^{(m)}W_{Ax(T)}^{(k)}(j = 1, …, n),
k ≥ 1 ⇒ ‘X_{j} = X_{j}^{(k)}(j = 1, …, n),
x ∈ X_{j}(j = 1, …, n)}
(k ＝ 0, 2, …); (m ＝ 1, 2, …).

(3) S5: Ax(S5) = Ax(T)∪∪_{1≤j≤n}{(K_{j}(ϕ) ⊃ K_{j}(K_{j}(ϕ)))|ϕ ∈ L}∪∪_{1≤j≤n}{(¬K_{j}(ϕ) ⊃ K_{j}(¬K_{j}(ϕ)))|ϕ ∈ L|}:

(m)W_{Ax(S5)}^{(0)} = ^{(m)}W^{(0)},
(m)W_{Ax(S5)}^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W_{Ax(S5)}^{(k)}, X_{j} ⊆ ^{(m)}W_{Ax(S5)}^{(k)}(j = 1, …, n),

k ≥ 1 ⇒ ‘X_{j} = X_{j}^{(k)}(j = 1, …, n),

x ∈ X_{j}(j = 1, …, n),

∀h ∈ X_{j} ⇒ H_{j}^{(k)} = X_{j}^{(k)}(j = 1, …, n)}

(k = 0, 2, …); (m = 1, 2, …).

(4) K_{I→J}: Ax(K_{I→J}) ＝ Ax(S5) ∪ {K_{I}(ϕ) ⊃ K_{J}(ϕ)|ϕ ∈ L}:

(m)W_{Ax(K_{I→J})}^{(0)} = ^{(m)}W^{(0)},

(m)W_{Ax(K_{I→J})}^{(k+1)} = {⟨x, ( K_{1}[X_{1}] ; ⋮ ; K_{n}[X_{n}] )⟩ | x ∈ ^{(m)}W_{Ax(K_{I→J})}^{(k)},

X_{j} ⊆ ^{(m)}W_{Ax(K_{I→J})}^{(k)}(j = 1, …, n),

k ≥ 1 ⇒ ‘X_{j} = X_{j}^{(k)}(j = 1, …, n),

x ∈ X_{j}(j = 1, …, n),

∀h ∈ X_{j} ⇒ H_{j}^{(k)} = X_{j}^{(k)}(j = 1, …, n),

X_{J} ⊆ X_{I}}

(k = 0, 2, …); (m = 1, 2, …).

小野勝次先生へのオマージュ

田中尚夫

2002 年 5 月 31 日 (金)

小野先生のご逝去誠に残念でございます．ご家族の皆様に心からお悔やみ申し上げます．大きな支えを失った思いで一杯でございます．ご承知のように小野先生は名古屋大学に数学基礎論の大きな拠点を構築され，数学基礎論の発展に大きく貢献されました．本日ご追悼のシンポジウムが開催されましたことも，小野先生の偉大なご足跡を示すものの一端に他なりません．先生は多方面の学問に関心をお持ちになられそれらを専門的に研究されました．小野先生が数学基礎論以外の分野で学士院賞を受賞されたことがこれを如実に物語っています．

私が数学基礎論の世界へ足を踏み入れた頃，小野先生は 50 歳前後で活発な研究活動をなさっておられました． 60 年代初頭の頃のご講演で，定年まであと 10 年程あるから，自由な研究をしたい，とおっしゃって，先生独自の仕事：集合論の新しいシステム (一つの生成原理をもつ集合論， proto-type としての対象理論) を構築しておられました．

私は数年前に， 1930 年代の日本における数学基礎論がどのような状況であったか，を調べたことがあります (1920 年代には日本には数学基礎論はなかったようです)．その頃の邦語の解説は，高木貞治・末綱恕一・黒田成勝・今野武雄・平野次郎・哲学者田辺元の諸先生によって書かれていました．しかし，私が調べた限りにおいて，それらは殆どゲーデルに言及していないのです．さすが高木先生「過渡期の数学」という大阪大学での講演で，その中の一項“数学基礎論と集合論”に，ウィーンへ行ったときのこととして，数学基礎論の専門家ゲーデルの名前だけを挙げておられます．邦語でゲーデルの結果に触れた初めての記事は小野先生の論説だと思います．それは 1941 年の岩波「科学」における「学会展望：数学基礎論の問題」においてだと思います．その中で先生は，ゲーデルの第二不完全性定理に触れ，ゲンチェンは無矛盾性証明を立場を緩めて行ったが，自分が有限の立場を保った上で証明できる範囲を，ぎりぎりのところ迄求める，という方向をとった，と述べられました．ご承知のように，小野先生は 1938 年の学位論文“ Logische Untersuchungen über die Grundlagen der Mathematik ”において「自然数論の無矛盾性証明」を，数学的帰納法に或る制限を加えたシステムに対して，有限の立場で実行されました．それまでの Ackermann や von Neumann の「制限」は帰納法の論理式を quantifier-free なものに制限するというものでした．ところが小野先生の制限はそれよりもずっとゆるいもので，先生のご意見によれば，自然数論で実際に使用される殆どすべての数学的帰納法がこの制限の論理式で表せるということです．これは我が国における数学基礎論に関する本格的な研究の最初のものであると同時に大変高く評価された業績でございます．初めて本格的な数学基礎論の論文を書かれたという意味では，小野先生は我が国における数学基礎論のパイオニアと申し上げることができます．

1965 年 7 月東洋紡赤倉山荘で行われた数学基礎論シンポジウムでは，毎朝小野先生の散歩にご一緒させていただき，色々な興味深いお話を聞かせていただきました．その中には，ハンコの彫り方，刃物の研ぎ方や暴漢と元ボクサーのお話が含まれていました．先生はさすが競歩で鍛えられたご健脚で，私は同じ歩調でついていくのが大変でした．野尻湖畔で 10 人程で撮った写真があります．懐かしい思い出です．小野先生は私にとりましては，学位論文の主査をしていただいた格別な先生です．名古屋大学へ集中講義にも呼んで下さり，超ご多忙中にもかかわらず (当時先生は学生部長の重責を担っておられました)，小生の拙い講義を聞いて下さいました．弟子でもない私によくお目をかけて下さって，大変有り難く，感謝の気持ちで一杯です．つい数年前までは，達筆な年賀状を戴いていましたのに，お亡くなりになったという現実，本当に残念でなりません．今はただ小野先生の大きなご業績を讃え，ご冥福をお祈り申し上げるのみでございます．