一個(gè)關(guān)于有窮開放過程的類型論系統(tǒng)

梁曉龍 鞠實(shí)兒

1 引論

首先，有窮是人類知識(shí)中最為常見的概念之一，更是邏輯學(xué)的核心概念。如邏輯系統(tǒng)中的合式公式和定理的證明長度都是有窮的。在現(xiàn)實(shí)世界中，有窮體現(xiàn)為施加在對(duì)象及其發(fā)展過程的可量化特性上的限制：如個(gè)體獲得的知識(shí)總量、計(jì)算機(jī)儲(chǔ)存的數(shù)據(jù)量、計(jì)算機(jī)的計(jì)算能力、物體運(yùn)動(dòng)的速度等物理數(shù)值都是有窮的。而無窮可以看作是有窮的否定概念，常用來刻畫理想對(duì)象的數(shù)量特征：如圖靈機(jī)的紙帶長度、集合論中的自然數(shù)集等。

另一方面，數(shù)學(xué)和物理領(lǐng)域以及日常經(jīng)驗(yàn)生活中的事物，通常都具有可變性。我們將事物拓展的過程稱為開放過程。為了明確起見，本文主要研究可構(gòu)造的開放過程，如遞歸構(gòu)造自然數(shù)的過程。1將歸納構(gòu)造自然數(shù)看作自然數(shù)的構(gòu)建過程，這一觀點(diǎn)可以參考[1]。在該文中，布勞威爾（L.E.J.Brouwer）分析“two-oneness”的直觀時(shí)使用到“process”一詞。此外，在[2,3,5]等文獻(xiàn)中，也都用到“process”一詞來描述計(jì)數(shù)、論域擴(kuò)充（extending the domain）、樹和子樹等概念。而開放過程所產(chǎn)生的那些成員數(shù)可擴(kuò)展的類則被稱為開放類。例如，上述遞歸過程生成的自然數(shù)所構(gòu)成的類。反之，我們將那些成員數(shù)固定不變的類稱為封閉類。類中的成員稱作對(duì)象。

其次，有窮/無窮和開放/封閉這兩對(duì)概念之間有密切關(guān)系。事實(shí)上，對(duì)任一組對(duì)象組成的類，都可考慮它是否具有開放性。而當(dāng)對(duì)象類具有開放性，或?yàn)殚_放類時(shí)；就有必要探討相應(yīng)的開放過程是有窮的還是無窮的，以及是否存在確定的過程完成后不再變化的結(jié)果。因此，可以區(qū)分出四種不同的情況：有窮開放、有窮封閉、無窮開放、無窮封閉。其中，第二種情況是指有限步內(nèi)完成的過程，其生成的結(jié)果是確定的成員數(shù)有窮且不再擴(kuò)展的類；第三種指一個(gè)潛無窮過程，其生成的對(duì)象形成的類是一個(gè)成員數(shù)不斷增加，其增加過程無限制地進(jìn)行下去不會(huì)停止的類；第四種情況中，其生成的結(jié)果是一個(gè)確定的成員數(shù)無窮且不再擴(kuò)展的類，是一個(gè)實(shí)無窮；而有窮開放是指：開放過程不能無限制地進(jìn)行下去，開放過程會(huì)生成未完成的有窮類。例如：人類或機(jī)器從0 開始通過后繼函數(shù)構(gòu)造自然數(shù)的過程，和該過程生成的自然數(shù)所組成的類。如所周知，后三種情況已經(jīng)得到廣泛而深入的研究。本文主要探討有窮開放過程及其所生成的有窮開放類。

進(jìn)一步，根據(jù)開放過程生成對(duì)象的方式和時(shí)間節(jié)點(diǎn)的不同，開放過程可以被區(qū)分成不同的階段，而生成的對(duì)象也被相應(yīng)地劃歸為各個(gè)不同階段。如數(shù)域擴(kuò)張過程中，從自然數(shù)類到整數(shù)類、從整數(shù)類到有理數(shù)類、從有理數(shù)類到實(shí)數(shù)類等過程，均可看作數(shù)域擴(kuò)張過程的不同階段；又如自然數(shù)生成過程中，生成104以內(nèi)數(shù)、生成108以內(nèi)數(shù)、生成1012以內(nèi)數(shù)等過程，均可看作自然數(shù)生成過程的不同階段。各個(gè)階段可以按順序分別稱為第一階段、第二階段、等等。第一階段也稱初始階段。

再次，開放過程的實(shí)質(zhì)是通過已有的對(duì)象生成新對(duì)象；而生成新對(duì)象的各種方式可以看作不同的對(duì)象生成算子，又稱開放算子。不僅如此，算子本身也是對(duì)象，對(duì)于這些生成算子組成的類，存在進(jìn)一步的問題：這個(gè)類是否具有開放性。不難看到，如此這般關(guān)于開放類的分析過程，可以一層一層地持續(xù)下去。這就是說：在開放過程中生成的開放類具有分層結(jié)構(gòu)。值得一提的是：根據(jù)前文分析，不同分層上的開放過程也可以是分階段的，其成員歸屬于開放過程的不同階段。本文主要通過研究開放類的層次和階段，揭示有窮開放過程及其生成結(jié)果的形式結(jié)構(gòu)。

最后，在研究方法方面，考慮到：類型論語言中任意對(duì)象所在的類型均是唯一的。對(duì)象和對(duì)象所在類型分別屬于不同的類型，故一個(gè)用在對(duì)象上的謂詞使用在對(duì)象所在的類型上是不合語法的；同樣，將若干對(duì)象以及對(duì)象所在類型組合在一起作為一個(gè)新類型，這也是不合語法的。而集合論語言（一階語言）中，謂詞符并不會(huì)限定于特定的集合，如可用于自然數(shù)上的謂詞符同樣可用于自然數(shù)集上，此外也存在如{3,ω}這類既含有自然數(shù)又含有自然數(shù)集本身的集合。在這個(gè)區(qū)別下，類型論語言在描述不同層次的對(duì)象使用的不同謂詞時(shí)會(huì)更加直觀。故使用類型論語言更便于描述開放類的分層屬性。

此外，本文主要研究可構(gòu)造的開放過程，故符合構(gòu)造主義觀點(diǎn)的理論更適合作為本文構(gòu)建的系統(tǒng)的基礎(chǔ)理論。而柯里-霍華德對(duì)應(yīng)（Curry-Howard correspondence）理論認(rèn)為類型、程序以及公式之間有著對(duì)應(yīng)關(guān)系：命題對(duì)應(yīng)類型（propositions as types）；證明對(duì)應(yīng)程序（proofs as programs）；證明的化簡(jiǎn)對(duì)應(yīng)程序的評(píng)估（simplification of proofs as evaluation of programs）。2可參考[7]中引言部分。由于程序通常是由確定的算法給出的，具有可構(gòu)造性，故在這個(gè)對(duì)應(yīng)下類型論更符合構(gòu)造主義觀點(diǎn)、更便于描述符合構(gòu)造主義的哲學(xué)觀點(diǎn)。為此，本文將使用類型論語言作為對(duì)開放類及其分層和分階段屬性進(jìn)行形式化描述和分析的工具。

根據(jù)以上所述，本文將在第2 節(jié)介紹類型論語言。在第3 節(jié)中，本文將以自然數(shù)類為典型案例，分析有窮和開放的分層和分階段屬性，并使用類型論語言進(jìn)行形式化。第4 節(jié)中，本文將對(duì)第3 節(jié)的形式化系統(tǒng)進(jìn)行一般化推廣，使用類型論語言構(gòu)建關(guān)于有窮開放類的分層和分階段系統(tǒng)，給出有窮開放類型系統(tǒng)的形式化定義。

2 類型論語言的基本概念

為了簡(jiǎn)潔起見，本節(jié)主要介紹本文研究中涉及的部分類型論概念及其與公式之間的對(duì)應(yīng)關(guān)系，更為詳盡的相關(guān)內(nèi)容可以參考[4,6]等文獻(xiàn)。本文所采用的是馬丁洛夫類型論（Martin-L?f’s Type Theory）。3本文構(gòu)建的系統(tǒng)并沒有用到所有的馬丁洛夫類型論中的類型。在本文以外的后續(xù)工作中，本文所構(gòu)建的系統(tǒng)可通過增加關(guān)于算數(shù)的公理，以進(jìn)一步描述有窮開放觀點(diǎn)下的算數(shù)系統(tǒng)。在這個(gè)需求下，馬丁洛夫類型論提供的等同類型（identity type）具有重要作用。故出于后續(xù)工作需求的考慮，本文采用馬丁洛夫類型論作為基礎(chǔ)理論。

定義1.4定義1-16 可參見[6]中附錄部分。類型論語言中的項(xiàng)t形式如下：

其中x,x′,...為變?cè)?，c,c′,...為項(xiàng)原始常元符，f,f′,...為定義常元符。

其中，每個(gè)定義常元符f通常會(huì)給出若干形如f(x1,x2,··· .xn):≡t的定義等式，用以給出定義常元符在代入不同項(xiàng)時(shí)所得到的項(xiàng)的具體表達(dá)式。

定義2.類型論中基本斷定的形式為：a:A以及a ≡b:A，其中a,b,A為項(xiàng)。

將a:A稱為：a的類型為A；將a ≡b:A稱為：項(xiàng)a和項(xiàng)b在類型A上斷定相等。

定義3.若一基本斷定序列x1:A1,x2:A2,...,xn:An滿足：變?cè)獂1,x2,...,xn互不相同，則稱其為一個(gè)上下文（context）。空的上下文記為·。

上下文中的每個(gè)基本斷定可稱為一個(gè)假定（assumption）。

常用字符Γ,Δ 表示類型論中的上下文。

定義4.類型論中的斷定（judgement）的形式為：Γ ctx、Γ?a:A以及Γ?a ≡b:A，其中Γ 為上下文，a,b,A為項(xiàng)。

將Γ ctx 稱為：上下文Γ 是良形式的（well-formed）；將Γ?a:A稱為：在上下文Γ 的假定下，a的類型為A；將Γ?a ≡b:A稱為：在上下文Γ 的假定下，項(xiàng)a和項(xiàng)b在類型A上斷定相等。

當(dāng)上下文Γ 為空時(shí)，Γ?a:A和Γ?a ≡b:A可分別記為· ?a:A和·?a ≡b:A，或?a:A和?a ≡b:A。

定義5.類型論中的推理規(guī)則（inference rule）的形式為：

其中，NAME 為推理規(guī)則的名稱，J,J1,...,Jk為斷定。

推理規(guī)則中，橫線上方稱為推理規(guī)則的假設(shè)，橫線下方稱為推理規(guī)則的結(jié)論。

定義6.如果一個(gè)通過若干推理規(guī)則構(gòu)造的樹的根部的斷定為J，則稱該樹為斷定J的一個(gè)推演。5類型論中推演的示例可參見[6]中附錄部分。

定義7.6命題類型和謂詞的定義可參見[6]，第41-47 頁。若存在斷定Γ?a:A的一個(gè)推演，其中Γ 為上下文，a,A為項(xiàng)，則：稱斷定Γ?a:A可證；稱類型A在上下文Γ 中是可居留的（inhabited）；若A為命題類型，則稱命題A在上下文Γ 中可證。

若存在斷定Γ?d:(P a)的一個(gè)推演，其中Γ 為上下文，a,d,P為項(xiàng)，若P為一個(gè)謂詞，則稱在上下文Γ 中項(xiàng)a滿足謂詞P。

接下來本節(jié)將列出本文進(jìn)行形式化時(shí)所需要涉及到的部分馬丁洛夫類型論中的推理規(guī)則。

類型論語言中，類型所在的類型稱為類型宇宙（type universes)，通常用一序列常元U0、U1、U2、……來表示不同層次的類型宇宙。當(dāng)文中不需要表明所需討論的是哪一層的類型宇宙時(shí)，可以用Type 表示類型宇宙，也可用A:Type 表示A是一個(gè)類型。此外，也用Set 表示集合宇宙（set universes)，用A:Set 表示A是一個(gè)集合；用Prop 表示命題宇宙（proposition universes），用A:Prop 表示A是一個(gè)命題。

定義8.類型宇宙的推理規(guī)則為：

類型宇宙推理規(guī)則給出了類型論語言中各個(gè)類型所在的宇宙之間的關(guān)系。

定義9.良形式推理規(guī)則為：

定義10.空類型0 的規(guī)則包括形成規(guī)則和消去規(guī)則7B[a1,...,an/x1,...,xn] 是指將項(xiàng) B 中自由變?cè)?x1,...,xn 的自由出現(xiàn)依次分別代入替換成a1,...,an，且對(duì)任意1 ≤i ≤n，均有ai 對(duì)于xi 在B[a1,...,ai1/x1,...,xi-1]中替換自由。：

定義11.單元類型1 的規(guī)則包括形成規(guī)則、引入規(guī)則、消去規(guī)則和計(jì)算規(guī)則。

單元類型的引入規(guī)則和消去規(guī)則如下：

單元類型的形成規(guī)則和計(jì)算規(guī)則如下：

空類型和單元類型在柯里-霍華德對(duì)應(yīng)理論中對(duì)應(yīng)命題False和命題True，規(guī)則0-ELIM 對(duì)應(yīng)命題False能推出任意命題；規(guī)則1-INTRO 對(duì)應(yīng)命題True可被無條件推出。

定義12.依賴乘積類型（Dependent product types）也稱依賴函數(shù)類型（Dependent function types）或Π-類型（Π-types），依賴乘積類型的推理規(guī)則有五條，包含形成規(guī)則、引入規(guī)則、消去規(guī)則、計(jì)算規(guī)則和唯一性規(guī)則。依賴乘積類型的形成規(guī)則和引入規(guī)則為：

依賴乘積類型消去規(guī)則和計(jì)算規(guī)則為：

依賴乘積類型的唯一性規(guī)則為：

類型(Πx:A)B稱為依賴于類型A的到類型B的函數(shù)類型，也可記為Π(x:A)B、?x:A,B或(?x:A),B。若需要強(qiáng)調(diào)類型B根據(jù)變?cè)獂的取值變化，也可記為(Πx:A)B(x)、Π(x:A)B(x)、?x:A,B(x)以及(?x:A),B(x)。8多層的依賴乘積類型的符號(hào)可以進(jìn)行簡(jiǎn)寫，只保留最開始的Π 或?符號(hào)，如(Πx y: A)B、Π(x:A)(y:C)B、?(x: A)(y: C),B、(?x y: A),B 等等。在涉及類型宇宙的情況下(?A: Ui),B 可簡(jiǎn)寫為(?A),B，若根據(jù)表達(dá)式能得出(?x: A),B 形式的式子中的A 的表達(dá)式時(shí)，也可簡(jiǎn)寫為(?x),B。

Π-類型在柯里-霍華德對(duì)應(yīng)理論中對(duì)應(yīng)全稱命題，Π-類型的引入和消去規(guī)則分別對(duì)應(yīng)于一階邏輯的全稱引入和全稱消去規(guī)則。

定義13.在依賴乘積類型的規(guī)則中，若類型B不隨變?cè)獂的取值變化，則可稱為函數(shù)類型（function type），作為函數(shù)類型時(shí)，(Πx:A)B可以記為A →B。9多次使用符號(hào)→的情形下，符號(hào)→是右結(jié)合的，即A →B →C 表示A →(B →C)。

函數(shù)類型在柯里-霍華德對(duì)應(yīng)理論中對(duì)應(yīng)蘊(yùn)含命題，其引入規(guī)則對(duì)應(yīng)蘊(yùn)含引入規(guī)則；其消去規(guī)則對(duì)應(yīng)MP 規(guī)則。

除以上若干類型的推理規(guī)則外，馬丁洛夫類型論中還包括Σ-類型、等同類型、歸納類型（inductive type）等類型的推理規(guī)則；除上述良形式規(guī)則外，還包括變?cè)?guī)則（variables rule）、替換規(guī)則（substitution rule）、弱化規(guī)則（weakening rule）以及相等規(guī)則（equality rule）等結(jié)構(gòu)規(guī)則。詳細(xì)可參見[6]中附錄部分。

定義14.一個(gè)形如a:A的基本斷定可被稱為一個(gè)公理，其中a,A為項(xiàng)。

一組公理以及馬丁洛夫類型論的所有推理規(guī)則組成的整體，稱為一個(gè)基于馬丁洛夫類型論的公理系統(tǒng)，簡(jiǎn)稱一個(gè)公理系統(tǒng)。

不失一般性，由于任意項(xiàng)的所在類型是唯一的，故可用項(xiàng)a來表示公理a:A；由于不同公理系統(tǒng)的推理規(guī)則均為馬丁洛夫類型論的推理規(guī)則，故可用公理系統(tǒng)的公理集表示公理系統(tǒng)本身。進(jìn)一步，由于一組數(shù)量有窮的公理可以看作一個(gè)上下文，故也可用一個(gè)上下文表示一個(gè)公理系統(tǒng)。

定義15.對(duì)任意公理系統(tǒng)A，若存在A中部分公理組成的上下文Γ，且存在斷定Γ?a:A的一個(gè)推演，其中a,A為項(xiàng)，則：稱斷定a:A在A中可證；稱類型A在A中是可居留的；若A為命題類型，則稱命題A在A中可證。

若存在A中部分公理組成的上下文Γ，且存在斷定Γ?d:(P a)的一個(gè)推演，其中a,d,P為項(xiàng)，且P為一個(gè)謂詞，則稱A中項(xiàng)a滿足謂詞P。

定義16.對(duì)任意公理系統(tǒng)A，若對(duì)任意的A中部分公理組成的上下文Γ，以及任意項(xiàng)a，不存在斷定Γ?a:0 的使用公理系統(tǒng)中推理規(guī)則的推演，則稱公理系統(tǒng)A是一致的。

3 有窮開放的分層和分階段屬性

本節(jié)將給出有窮開放分層和分階段的直觀圖景，以及一個(gè)自然數(shù)開放類的具體的構(gòu)造過程；進(jìn)而分析自然數(shù)開放類的各層次各階段對(duì)象，以及各層次各階段的有窮謂詞之間的關(guān)系；并使用類型論語言對(duì)此進(jìn)行形式化，構(gòu)建一個(gè)關(guān)于自然數(shù)開放類的類型論系統(tǒng)。

為了實(shí)現(xiàn)目標(biāo)，本節(jié)先用類型論語言描述一個(gè)自然數(shù)的系統(tǒng)，它可以作為有窮開放過程以及由此生成的有窮開放類的典型案例。通過分析這一案例，可以展示有窮開放類構(gòu)建過程及其分層和分階段的一般結(jié)構(gòu)。

根據(jù)先前所述，對(duì)象和開放算子的分層和分階段的直觀圖景如下，稱為有窮開放層次圖景：

在上述圖景中，有窮開放類與它的生成算子的類分屬于不同的層次。其中，處在第0 層的是：關(guān)于類的成員的有窮開放類，簡(jiǎn)稱第0 層開放類；在第1 層的是：由從第0 層開放類生成其新成員的算子構(gòu)成的有窮開放類；在第2 層的是：由從第0 層或第1 層開放類的成員出發(fā)，生成第0 層或第1 層開放類的新成員的那些算子組成的有窮開放類；依次類推，在第n層的是：由從前n層中某一層開放類的成員出發(fā)、生成前n層中某一層開放類的新成員的算子構(gòu)成的有窮開放類。每個(gè)層次上的對(duì)象整體上構(gòu)成一個(gè)隨開放過程變化的開放類，而每個(gè)層次上的開放類又根據(jù)開放過程區(qū)分為不同的階段。其中，每個(gè)層次中的第一階段中的對(duì)象（若存在的話）均是給定的。

例如：在使用自然數(shù)0 和后繼函數(shù)fS遞歸生成自然數(shù)開放類的過程中10需要注意的是，是否將生成自然數(shù)的過程看作開放過程，這取決于數(shù)學(xué)哲學(xué)家的哲學(xué)觀點(diǎn)。若數(shù)學(xué)哲學(xué)家認(rèn)為：自然數(shù)集是事先給定的滿足某些公理的集合。那么，就不存在生成自然數(shù)的開放過程，其觀點(diǎn)中的自然數(shù)類也應(yīng)該是一個(gè)封閉的類。若數(shù)學(xué)哲學(xué)家認(rèn)為：自然數(shù)是通過各種運(yùn)算方式逐步生成，那么自然數(shù)類則是一個(gè)開放的類。進(jìn)一步，當(dāng)數(shù)學(xué)哲學(xué)家認(rèn)為自然數(shù)類為開放類時(shí)，需給出的初始階段的自然數(shù)和各層開放算子，取決于數(shù)學(xué)哲學(xué)家所認(rèn)為的自然數(shù)的生成方式。，自然數(shù)0 為第0 層的第一階段給定的對(duì)象，fS為第1 層的第一階段給定的開放算子。在任一開放類所在層次上，如果沒有給定的對(duì)象和生成算子，則無法形成這一層次上的開放類。

可見，上述從0 出發(fā)通過后繼函數(shù)生成自然數(shù)開放類的方式較為簡(jiǎn)單，僅涉及到自然數(shù)開放類所在層次，及其下一層算子所在類的層次。進(jìn)一步，為描述更復(fù)雜情形下有窮開放類的生成方式以及各階段之間的結(jié)構(gòu)關(guān)系，需要考慮涉及更多層次的情形。不失一般性，本文選擇了另一種自然數(shù)定義的方案，并基于此方案描述了一個(gè)作為有窮開放類的自然數(shù)類。在本節(jié)中，定義自然數(shù)類時(shí)給出的初始元素為：自然數(shù)0,1,2、后繼函數(shù)fS、+2 函數(shù)f+2、+3 函數(shù)f+3、加法函數(shù)f+、二次迭代函數(shù)f(-)2、值為0 的自然數(shù)上的常函數(shù)f0、值為0 的定義域?yàn)樽匀粩?shù)上一元函數(shù)的常函數(shù)自然數(shù)類定義為由上述各個(gè)初始對(duì)象和算子遞歸生成的對(duì)象類，后文將此自然數(shù)類記為N3。11由于初始元素包括了自然數(shù)0 及后繼函數(shù)fS，且涉及的其他自然數(shù)和算子均為皮亞諾算數(shù)系統(tǒng)中可定義的。所以可根據(jù)皮亞諾算數(shù)系統(tǒng)中的公理，以及根據(jù)各個(gè)初始元素在皮亞諾算數(shù)系統(tǒng)中的定義，給出相應(yīng)的關(guān)于各個(gè)初始元素的公理。此方式給出的公理均在皮亞諾公理系統(tǒng)中可證。反之，由于皮亞諾算數(shù)系統(tǒng)的公理集是此處所得的公理系統(tǒng)公理集的一個(gè)子集。故皮亞諾算數(shù)系統(tǒng)中的公理均在此系統(tǒng)中可證。故可通過此種更復(fù)雜的方式定義遞歸生成自然數(shù)開放類的過程，且此過程所描述的自然數(shù)類與前文更簡(jiǎn)單的生成方式所描述的自然數(shù)類相吻合。

本節(jié)中，基于類型論語言的描述上述方式生成的自然數(shù)類N3的公理系統(tǒng)，稱為基于N3的有窮開放分層系統(tǒng)，后文中記為OpenN3。系統(tǒng)OpenN3包含了兩部分公理：一部分是與上述自然數(shù)類中初始元素相關(guān)的公理；另一部分是與有窮開放分層圖景的前4 層的結(jié)構(gòu)相關(guān)的公理。OpenN3將描述這些層次上的各個(gè)階段有窮謂詞之間的關(guān)聯(lián)，并作為典型案例展示有窮開放分層圖景的前4 層的一般結(jié)構(gòu)。

在定義系統(tǒng)OpenN3時(shí)，本節(jié)將依次分階段給出有窮對(duì)象和分層次分階段給出開放算子。首先，引入論域類型：第0 層對(duì)象的論域記為Uopc:Type。

根據(jù)前文所述，給定的第0 層第一階段的對(duì)象為：0,1,2:Uopc。

對(duì)于每一個(gè)被認(rèn)為是第0 層第一階段有窮的對(duì)象，需要有一個(gè)關(guān)于“第0 層第一階段有窮”的謂詞，以及相應(yīng)的公理宣稱其有窮。

表示第0 層第一階段有窮的謂詞記為F1:Uopc →Prop，F(xiàn)1為類型Uopc上的一元謂詞。宣稱自然數(shù)0、1、2 是第0 層第一階段有窮的的公理分別為：

在第0 層第一階段有窮對(duì)象之后，下一層次為第1 層的開放算子，開放算子用于生成更多的對(duì)象。

第1 層開放算子所在的類型記為Uopc →Uopc。

表示第1 層開放算子的第一階段有窮謂詞記為FO1

1:(Uopc →Uopc)→Prop，為類型Uopc →Uopc上的一元謂詞。

此時(shí)的有窮謂詞與此前的第0 層第一階段有窮謂詞的論域并不相同。

根據(jù)前文所述，給定的三個(gè)第1 層第一階段的算子為：

fS、f+2、f+3分別為自然數(shù)上的后繼函數(shù)、+2 函數(shù)和+3 函數(shù)。

與第0 層第一階段有窮對(duì)象一樣，對(duì)于第1 層第一階段開放算子給出相應(yīng)的公理，以宣稱第1 層第一階段開放算子有窮：

給定第0 層第一階段對(duì)象和第1 層第一階段開放算子后，可以通過函數(shù)的應(yīng)用獲得更多的對(duì)象，如(fS0)、(f+21)、(f+32)等等。

數(shù)學(xué)哲學(xué)中，潛無窮和實(shí)無窮觀點(diǎn)會(huì)認(rèn)為：若一個(gè)數(shù)x有窮（如0），一個(gè)函數(shù)f滿足“作用在任意有窮數(shù)上得到的數(shù)仍然有窮”（如后繼函數(shù)fS），則x在函數(shù)f作用任意次的情況下得到的數(shù)仍然是有窮的。即是說，認(rèn)為函數(shù)迭代作用生成論域中的元素的過程是可以一直進(jìn)行下去的。

而在有窮開放觀點(diǎn)中，將避免接受“算子任意次迭代生成的對(duì)象‘同樣有窮’”。接下來將給出有窮開放觀點(diǎn)下的，關(guān)于第0 層第一階段有窮對(duì)象和第1 層第一階段有窮開放算子的公理。

為方便起見，首先引入一個(gè)三元謂詞符Pmap，該謂詞可用于簡(jiǎn)化公理的表達(dá)式，表示“保持滿足性”。Pmap及其所在的類型由如下斷定給出：

其中，由P1,P2,P3的類型可以得知A,B的形式，故不失一般性，可將A,B視為隱參數(shù)，用(Pmap P1P2P3)表示(Pmap A B P1P2P3)。項(xiàng)(Pmap P1P2P3)表示謂詞Pmap分別作用在關(guān)于A、關(guān)于A到B的函數(shù)所在類型、關(guān)于B的三個(gè)謂詞P1、P2、P3上可得：滿足謂詞P2的函數(shù)f，作用在滿足P1的項(xiàng)a上，所得的項(xiàng)滿足P3。

表示第0 層第二階段有窮謂詞記為F2:Uopc →Prop，F(xiàn)2為類型Uopc上的一元謂詞。且第0 層第二階段有窮謂詞應(yīng)滿足：對(duì)于任意第0 層第一階段有窮的對(duì)象n，使用第1 層第一階段有窮的開放算子f作用后，得到的項(xiàng)滿足第0 層第二階段有窮謂詞。即公理：

當(dāng)需要開放過程是擴(kuò)充過程的情形時(shí)，可得F1與F2之間的關(guān)系公理：

該關(guān)系公理也稱為擴(kuò)充公理。

定義17.若一個(gè)公理系統(tǒng)包括且僅包括以下公理：Uopc、0、1、2、F1、AF1,0、AF1,1、則稱該公理系統(tǒng)為前2 層的基于N3的有窮開放分層系統(tǒng)，記為Open2N3。

在這組公理中，第0 層第一階段有窮的對(duì)象使用第1 層開放算子獲得的對(duì)象是有窮的，但是對(duì)生成的對(duì)象使用的“有窮”謂詞和第0 層第一階段對(duì)象使用的“有窮”謂詞作出了區(qū)分。

可以注意到，若不對(duì)有窮謂詞作區(qū)分，認(rèn)為F1與F2相同，則上述公理可變形為：

若采用該變形公理替換掉系統(tǒng)Open2N3中的公理則可使用歸納法證明所得系統(tǒng)可以推出存在一組滿足謂詞F1的潛無窮長的對(duì)象序列：0、(fS0)、(fS(fS0))、(fS(fS(fS0)))、(fS(fS(fS(fS0))))、(fS(fS(fS(fS(fS0)))))……即在第0 層第一階段中，函數(shù)fS可以任意次迭代仍然保持所得對(duì)象滿足第0 層第一階段有窮謂詞。

本文在構(gòu)建各階段有窮和各層次開放的過程中將避免以上情形。在Open2N3中，不假定F1與F2相同，使用結(jié)構(gòu)歸納法可證明：不能得出形如(f+2(fS2))等對(duì)象滿足謂詞F2。

繼續(xù)上述構(gòu)建系統(tǒng)過程，當(dāng)已獲得若干第0 層第一、二階段有窮對(duì)象以及若干第1 層第一階段有窮的開放算子之后，會(huì)有下一層的開放算子。通過第0 層對(duì)象和第1 層開放中的對(duì)象，生成更多的對(duì)象，即為第2 層開放算子所產(chǎn)生的效果。

與第1 層開放算子只有一種類型的情形不同，第2 層開放的算子有四種不同形式，包括：作用在第0 層對(duì)象上獲得第1 層開放算子；作用在第1 層開放算子上獲得第1 層開放算子；作用在第0 層開放算子上獲得第0 層對(duì)象；作用在第1層開放算子上獲得第0 層對(duì)象。根據(jù)前文所述，在第2 層第一階段中各給定一個(gè)相應(yīng)的函數(shù)：

f+為自然數(shù)的二元加法函數(shù)；f(-)2為二次的迭代函數(shù)；f0和分別為定義域?yàn)樽匀粩?shù)和定義域?yàn)樽匀粩?shù)上一元函數(shù)的兩個(gè)常函數(shù)，其函數(shù)值均為自然數(shù)0。

故在給定關(guān)于第2 層開放算子的有窮謂詞時(shí)，需要根據(jù)對(duì)象的類型規(guī)定不同的有窮謂詞，故第2 層開放算子的有窮謂詞需要帶有類型參數(shù)。

不失一般性，當(dāng)類型A和B可以通過上下文確定的時(shí)候，可簡(jiǎn)寫為

對(duì)于上述四個(gè)不同類型的函數(shù)，分別用相應(yīng)公理宣稱其在第2 層中是第一階段有窮的。

第2 層開放算子可用于生成更多的（下一階段的）第0 層對(duì)象及第1 層開放算子，故對(duì)于這兩層的對(duì)象，需要有進(jìn)一步擴(kuò)展后的（下一階段的）有窮謂詞，用以宣稱生成的對(duì)象有窮。

第0 層第三階段有窮謂詞記為F3:Uopc →Prop；第1 層開放上的第二階段有窮謂詞記為:(Uopc →Uopc)→Prop。當(dāng)開放過程是擴(kuò)充過程時(shí)，二者已有謂詞之間的關(guān)系的公理如下，兩者均稱為擴(kuò)充公理：

謂詞F3和分別與謂詞F2和具有相同的類型。且F2和可看作F3和的子謂詞12P1 為P2 的子謂詞是指，任意滿足P1 的項(xiàng)a，均滿足P2。。

使用公理系統(tǒng)Open3N3，對(duì)證明結(jié)構(gòu)進(jìn)行歸納，可得出以下若干結(jié)果：(f+2 0)、(f+2(fS2))、(f(-)2fS(fS2))均滿足F3，即均是第0 層第三階段有窮的；(f+2(fS2))不滿足F2，不是第0 層第二階段有窮的；(f(-)2fS(f02))不滿足F3，不是第0 層第三階段有窮的。

至此，第2 層開放以及第2 層開放的有窮謂詞的定義示例已給出，同樣的步驟可以一步一步推廣到第3 層開放、第0 層第四階段有窮、第4 層開放等階段和層次。

對(duì)于第3 層開放的有窮謂詞，以及不同層的對(duì)象增加后對(duì)應(yīng)的范圍更廣的謂詞，給出方式與前述層次的情形類似。

當(dāng)開放過程是擴(kuò)充過程時(shí)，第三層開放的定義引入的謂詞，與之前已有謂詞之間的關(guān)系的公理如下：

第3 層開放的謂詞的“保持滿足性”的公理給出如下，共九條，此九條公理組成的公理系統(tǒng)記為K9N3：

已有層次中的對(duì)象在新謂詞下，可給出的關(guān)于“保持滿足性”的新公理如下，共五條，此五條公理組成的公理系統(tǒng)記為K5N3：

可以注意到，每一個(gè)新的層次中，增加的有窮謂詞和開放算子的形式都與已有的層次是相似的；同時(shí)，每個(gè)新的層次中的公理也與已有的公理具有相同的形式。故后續(xù)階段以及更高層的算子、謂詞、公理等，均可以通過繼續(xù)此步驟各開出。進(jìn)一步，可以從已有的示例中的層次出發(fā)，推理得出更高層次中對(duì)象、謂詞、公理的通項(xiàng)形式。本文將在下一節(jié)中給出這些形式的統(tǒng)一描述。

4 有窮開放類型系統(tǒng)

本節(jié)將對(duì)第三節(jié)中關(guān)于自然數(shù)開放類的類型論系統(tǒng)進(jìn)行一般化推廣；構(gòu)建描述有窮開放類的分層和分階段屬性的系統(tǒng)：開放類型系統(tǒng)；并構(gòu)建用于描述只涉及若干層開放算子的有窮開放類的系統(tǒng)：有窮開放分層系統(tǒng)。此外，本節(jié)將證明第三節(jié)中構(gòu)建的關(guān)于自然數(shù)開放類的系統(tǒng)是本節(jié)中的系統(tǒng)的子系統(tǒng)13系統(tǒng)A 是系統(tǒng)B 的子系統(tǒng)是指：系統(tǒng)A 中所有可證的斷定均是系統(tǒng)B 中可證的。；并證明第三節(jié)和本節(jié)中的各個(gè)關(guān)于開放類的系統(tǒng)的一致性。

第3 節(jié)中，關(guān)于自然數(shù)開放類的案例僅涉及了第0 層對(duì)象、第1、2、3 層開放算子。其中給出的關(guān)于不同階段不同層次的有窮謂詞、以及有窮謂詞之間關(guān)系的公理的角標(biāo)均只涉及0,1,2,3,4。對(duì)于更高層次和更后續(xù)的階段，有窮謂詞和有窮謂詞之間關(guān)系的公理可以通過前幾階段和前幾層次的公理推廣得到。本節(jié)將根據(jù)上文中的典型案例，整理構(gòu)建出關(guān)于有窮對(duì)象和開放算子的分階段和分層系統(tǒng)的一般結(jié)構(gòu)。14本節(jié)中的類型定義使用了自然數(shù)作為角標(biāo)，但使用自然數(shù)角標(biāo)不是“必須”的。在實(shí)際構(gòu)造過程中，可以用其他類型代替自然數(shù)作為角標(biāo)給出上述的各種定義。此處選用自然數(shù)的定義僅僅是因?yàn)槠溆浱?hào)較為方便，并且相關(guān)定義使用自然數(shù)作為參數(shù)更容易理解。

本節(jié)的系統(tǒng)中論域記號(hào)為Uopt:Type，為了闡述各階段和各層的有窮謂詞的使用范圍，引入以下一元謂詞系列及公理。

給定一組一元謂詞Di:Type→Prop，角標(biāo)i ∈N，N 為自然數(shù)集，謂詞Di:Type→Prop 稱為開放層次謂詞。

關(guān)于謂詞Di:Type→Prop 給出一組公理：

這些公理稱為層次函數(shù)公理，規(guī)定了開放層次謂詞與函數(shù)類型和類型Uopt之間的聯(lián)系。

第j層開放對(duì)象的第i階段有窮謂詞記為:(?A B:Type),(A →B)→Prop，角標(biāo)i,j ∈N+，其中N+為正整數(shù)集；第0 層第i階段有窮謂詞記為Fi:Uopt →Prop，角標(biāo)i ∈N+。合稱論域類公理。

公理Ai,j,cons稱為開放層次符合公理，該公理保證了不同層次的開放算子上的不同階段有窮謂詞必須使用在滿足對(duì)應(yīng)開放層次謂詞的類型上。

層次函數(shù)公理以及開放層次符合公理合稱為合理性公理。

該組公理表示：滿足某個(gè)階段有窮謂詞的項(xiàng)也會(huì)滿足更后續(xù)階段的有窮謂詞。

該組公理表示：階段相同的低層的開放算子是高一層的開放算子的特例。

該組公理描述了特定層次和階段的算子作用在特定層次和階段的對(duì)象上獲得的新對(duì)象會(huì)在何階段何層次。

論域類公理、合理性公理、階段擴(kuò)張公理、開放層次增加公理以及開放類型應(yīng)用公理合稱為開放類型公理；論域類公理、合理性公理、開放類型應(yīng)用公理合稱為非擴(kuò)張的開放類型公理。

定義20.一個(gè)公理系統(tǒng)被稱為（非擴(kuò)張的）有窮開放分層的基本公理系統(tǒng)，如果該系統(tǒng)包含且僅包含所有（非擴(kuò)張的）開放類型公理。有窮開放分層的基本公理系統(tǒng)記為BaseO；非擴(kuò)張的有窮開放分層的基本公理系統(tǒng)記為nexBaseO。

定理1.公理系統(tǒng)BaseO2、BaseO3、BaseO4為公理系統(tǒng)BaseO 的子系統(tǒng)。15需注意，BaseO2、BaseO3、BaseO4 中的謂詞，i ∈N+ 不帶類型參數(shù)，而BaseO 中的謂詞帶了類型參數(shù)，且參數(shù)值均為Uopt。另一方面，系統(tǒng)BaseO2、BaseO3、BaseO4 中對(duì)象類的論域?yàn)閁opc，而系統(tǒng)BaseO 中為Uopt。但是不失一般性，可將Uopc 替換為Uopt；將BaseO2、BaseO3、BaseO4 中的FO1i 替換為(Uopt Uopt)，并在替換后的意義下，稱BaseO2、BaseO3、BaseO4 為公理系統(tǒng)BaseO 的子系統(tǒng)。后文中出現(xiàn)Uopc 和Uopt 混用、和(Uopt Uopt)混用的情形時(shí)均按此處方式處理即可。

證明.對(duì)照可知，公理系統(tǒng)BaseO2、BaseO3、BaseO4中的各階段和各層次的有窮謂詞、及謂詞之間關(guān)系公理的角標(biāo)情形均為公理系統(tǒng)BaseO 中公理的特例。故定理得證。

定理2.公理系統(tǒng)BaseO 是一致的。

證明.當(dāng)不給定任意滿足謂詞、Fi，i,j ∈N+的項(xiàng)時(shí)，層次符合公理、有窮層次增加公理、開放層次增加公理以及開放類型應(yīng)用公理均無法推理得到更多結(jié)果。故公理系統(tǒng)BaseO 的一致性可以規(guī)約到僅由層次函數(shù)公理組成的公理系統(tǒng)的一致性。

遞歸定義包含三個(gè)引入規(guī)則的二元謂詞Dind:Type→nat→Prop，其中nat為類型論中遞歸定義的自然數(shù)類型：

對(duì)任意類型A及自然數(shù)類型中的自然數(shù)i，定義Di A為Dind A i。則根據(jù)Dind的引入規(guī)則，有公理AD0,Uopt、ADi,→、ADi,ex可證。由馬丁洛夫類型論的一致性16馬丁洛夫類型論的一致性可以參見[6]中附錄部分。可知，公理系統(tǒng)BaseO 是一致的。

推論1.公理系統(tǒng)nexBaseO 是一致的。

推論2.公理系統(tǒng)BaseO2、BaseO3、BaseO4是一致的。

在類型論語言中，可定義關(guān)于類型的（更高層類型宇宙中的）謂詞，用于指稱一個(gè)類型“有窮”或“無窮”。

定義21.記關(guān)于類型的“有窮”謂詞為FType，滿足FType的類型通過如下方式遞歸給出：

(1)空類型、單元類型滿足FType；

(2)對(duì)任意類型類型A、B，若類型A、B滿足FType，則sum A B滿足FType，其中sum A B為類型A和B的余積類型；17余積類型的定義可參見[6]中附錄部分。

(3)對(duì)任意類型A、B及函數(shù)f:A →B，若類型A滿足FType，且函數(shù)f為滿射18函數(shù)f 為滿射，指命題?x,?y,(f y= x)可證。其中，類型?y,(f y= x)為Σ-類型，類型(f y= x)是等同類型。Σ-類型的定義可參見[6]中附錄部分。，則類型B滿足FType。

引理1.對(duì)任意類型A、B，若類型A、B滿足FType，則prod A B滿足FType，其中prod A B為類型A和B的積類型。19積類型的定義可參見[6]中附錄部分。

證明.對(duì)類型A、B滿足FType的證明結(jié)構(gòu)進(jìn)行歸納即可證明prod A B滿足FType。

定義22.記關(guān)于類型的“無窮”謂詞為Inf，滿足Inf的類型通過如下方式遞歸給出：

(1)自然數(shù)類型nat 滿足Inf；

(2)對(duì)任意類型A及函數(shù)f:A →nat，若函數(shù)f為滿射，則類型A滿足Inf。

定義23.對(duì)任意類型A，若A滿足FType，則稱A有窮；若A滿足Inf，則稱A無窮。

定義24.對(duì)于任意類型A、B、任意A上的謂詞P:A →Prop，對(duì)于任意函數(shù)f:B →A，若?x,(P x →?y,(f y=x))可證，且類型B有窮，則稱謂詞P的外延有窮；

對(duì)于任意類型A、任意A上的謂詞P:A →Prop，對(duì)于任意函數(shù)f:A →nat，若?x,?y,(P y ∧(f y=x))可證，則稱謂詞P的外延無窮。

當(dāng)一個(gè)類型滿足謂詞Inf時(shí)，也稱該類型為一個(gè)潛無窮類型；外延無窮的謂詞，也稱為外延潛無窮的謂詞。

此外，在類型論中，可定義一個(gè)類型上的謂詞在何情況下被稱為外延確定。

定義25.對(duì)于任意類型A，任意A上的謂詞P:A →Prop，若?x,(P x ∨?(P x))可證，則稱謂詞P是外延確定的。

定義26.一個(gè)公理系統(tǒng)稱為基礎(chǔ)開放類型系統(tǒng)，若其包含：公理系統(tǒng)BaseO 中所有公理；用于給定每一層的初始階段中對(duì)象的公理，以及相應(yīng)的宣稱給定的對(duì)象滿足該層次初始階段有窮謂詞的公理。

如果一個(gè)基礎(chǔ)開放類型系統(tǒng)是一致的，則稱為開放類型系統(tǒng)。

定義27.一個(gè)公理系統(tǒng)稱為非擴(kuò)張的基礎(chǔ)開放類型系統(tǒng)，若其包含：公理系統(tǒng)nexBaseO 中所有公理；用于給定每一層的初始階段中對(duì)象的公理，以及相應(yīng)的宣稱給定的對(duì)象滿足該層次初始階段有窮謂詞的公理。

如果一個(gè)非擴(kuò)張的基礎(chǔ)開放類型系統(tǒng)是一致的，則稱為非擴(kuò)張的開放類型系統(tǒng)。

推論3.公理系統(tǒng)Open2N3∪BaseO、Open3N3∪BaseO、OpenN3∪BaseO 為開放類型系統(tǒng)。20此處A ∪B 指公理集為公理系統(tǒng)A 和B 中的公理集的并的公理系統(tǒng)。

進(jìn)一步，可以有如下定義：

定義28.對(duì)于自然數(shù)n和（非擴(kuò)張的）開放類型系統(tǒng)S。若S中的公理A滿足：公理涉及的所有謂詞Dk、、Fl中的角標(biāo)i,j,k,l均滿足命題l ≤n ∧(i+j)≤n ∧k ＜n，則稱公理A屬于S的前n層（非擴(kuò)張的）開放類型公理。

定義29.對(duì)任意自然數(shù)n，若（非擴(kuò)張的）開放類型系統(tǒng)S的一個(gè)子系統(tǒng)S′滿足：S′包含且僅包含S的所有前n層（非擴(kuò)張的）開放類型公理，則稱S′為S的前n層（非擴(kuò)張的）開放類型系統(tǒng)。

定義30.稱一個(gè)系統(tǒng)S′為（非擴(kuò)張的）有窮開放類型系統(tǒng)，如果S′滿足：存在自然數(shù)n和（非擴(kuò)張的）開放類型系統(tǒng)S使得，S′為系統(tǒng)S的前n層（非擴(kuò)張的）開放類型系統(tǒng)，且S′中每一層的初始階段有窮謂詞的外延有窮。

推論4.有窮開放類型系統(tǒng)是一致的。

定義31.一個(gè)開放類由一個(gè)作為論域的類型U和一個(gè)類型U上謂詞的有窮長的序列組成。一個(gè)開放類稱為有窮開放類，若組成該開放類的每個(gè)謂詞均外延有窮，且均不是外延確定的。

具體到一個(gè)自然數(shù)類型的（擴(kuò)張的）開放類，若該開放類的組成部分的其中一個(gè)謂詞P存在一個(gè)具體的自然數(shù)n作為上界21此處需注意，關(guān)于上界的描述需要預(yù)設(shè)有關(guān)于自然數(shù)上的序的定義。，那么根據(jù)定義25，可證出這個(gè)謂詞是外延確定的。故此情形下的自然數(shù)開放類不是一個(gè)有窮開放類。

定義32.若S為一個(gè)（非擴(kuò)張的）開放類型系統(tǒng)，則S中的論域類型Uopt和第0層的有窮謂詞Fi，i ∈N 組成了一個(gè)開放類，記該開放類為TS，稱開放類型系統(tǒng)S描述了開放類TS。

定義33.對(duì)于任意（非擴(kuò)張的）開放類型系統(tǒng)S，可用定義歸納類型的方式給出謂詞Fi以及，i,j ∈N+對(duì)應(yīng)的另一組謂詞Pi以及，i,j ∈N+。其中各個(gè)作為謂詞的歸納類型的形成規(guī)則可由如下方式表示。22由于篇幅原因，此處歸納類型所包含的推理規(guī)則不再詳細(xì)給出。具體的推理規(guī)則的方法可以參考[6]中附錄里的關(guān)于歸納類型的章節(jié)。

(1)歸納類型P1的形成規(guī)則為：對(duì)任意x:Uopt，由F1x形成P1x；

(3)歸納類型Pi，i ∈N+∧i ＞1 的形成規(guī)則為：對(duì)任意開放類型系統(tǒng)中以“→Fi x”結(jié)尾的公理，將公理中的謂詞Fx、對(duì)應(yīng)替換為Px、得到一個(gè)新公理，然后根據(jù)所得公理的形式給出Pi x的形成規(guī)則；23如根據(jù)公理AF10,+，可得形成規(guī)則包含：對(duì)任意x，通過P10 x 形成P11 x 的規(guī)則；如根據(jù)公理A4,7,F，可得形成規(guī)則包含：對(duì)任意x,f，通過P10 x 和f 形成P11 (fx)的規(guī)則。

S中的論域類型Uopt和謂詞Pi，i ∈N 也組成了一個(gè)開放類，記該開放類為稱開放類型系統(tǒng)S歸納地描述了開放類

引理2.對(duì)任意開放類型系統(tǒng)S，系統(tǒng)S歸納地描述了開放類在系統(tǒng)S中添加定義33中關(guān)于歸納類型Pi,，i,j ∈N+的規(guī)則后得到的公理系統(tǒng)記為S*。在系統(tǒng)S*中，對(duì)任意k,l ∈N+，有?x,Fk x →Pk x且?f,

證明.對(duì)k進(jìn)行歸納可證?x,Fk x →Pk x；依次對(duì)k和l進(jìn)行歸納可證?f,。其中：初始步的情形由定義33 中的(1)和(2)可得；歸納步的情形可通過定義33 中的(3)和(4)得到。

定理3.一個(gè)（非擴(kuò)張的）有窮開放類型系統(tǒng)歸納地描述了一個(gè)有窮開放類。

證明.若S為（非擴(kuò)張的）有窮開放類型系統(tǒng)，根據(jù)定義，S中每一層的初始階段有窮謂詞均是外延有窮的。故存在相應(yīng)的有窮類型及滿射函數(shù)。注意到，對(duì)于任意謂詞Pi或，i,j ∈N∧i ＞1，謂詞的生成規(guī)則的數(shù)量是有窮條的。故可對(duì)生成規(guī)則的結(jié)構(gòu)使用歸納法。根據(jù)歸納假設(shè)，生成規(guī)則中涉及到的謂詞均已證明是外延有窮的，即均存在各自對(duì)應(yīng)的有窮類型和滿射。進(jìn)而，根據(jù)生成規(guī)則的結(jié)構(gòu)，可以通過引理1 和定義21 構(gòu)造相應(yīng)的有窮類型和滿射，從而證明需證的謂詞外延有窮。即S歸納描述的開放類中的作為組成元素的謂詞是外延有窮的。

另外，對(duì)任意i ∈N，因系統(tǒng)S中不含有以“→?(Fi x)”形式結(jié)尾的公理，故系統(tǒng)得不出關(guān)于任意對(duì)象x的命題?(Fi x)的證明，所以根據(jù)引理2 可知S*得不出關(guān)于任意對(duì)象x的命題?(Pi x)的證明。又因?yàn)閷?duì)證明結(jié)構(gòu)使用歸納法可知，存在對(duì)象y的相關(guān)的命題Pi y不可證。故Pi y ∨?(Pi y)亦不可證。所以S歸納描述的開放類中的作為組成元素的謂詞均不是是外延確定的。

綜上，S歸納描述的開放類是一個(gè)有窮開放類。

需注意，我們可以根據(jù)是否滿足謂詞FType和Inf而確定是否稱一個(gè)類型是有窮的或者無窮的。但我們不能稱一個(gè)開放類是有窮的還是無窮的，因?yàn)殚_放類是由一個(gè)類型以及一序列的謂詞組成的，開放類本身不是類型。對(duì)于開放類，我們只能對(duì)它的論域和各個(gè)謂詞宣稱有窮或者無窮。而“有窮開放類”一詞是一個(gè)專有名詞，不能等同為“有窮的開放類”。

本節(jié)最后將給出兩個(gè)例子，說明開放類型系統(tǒng)的一些特點(diǎn)。

例1.考慮前2 層開放類型公理，可得到以下只涉及有窮對(duì)象和第一層開放算子的公理：

給定初始階段對(duì)象和算子及其相關(guān)公理如下：

對(duì)上述公理組成的公理系統(tǒng)中證明的證明結(jié)構(gòu)使用歸納法可知，可證的關(guān)于有窮對(duì)象和開放算子的相關(guān)命題有且僅有：

其次，使用歸納法可知：當(dāng)增加公理AF1,-:?x,F2x →F1x后，f迭代任意次作用在q上所得的項(xiàng)均滿足F1，即：(F2((f)i q))，i ∈N。

進(jìn)一步可知，若類型Uopt →Uopt中的f是非等同映射的單射25由于系統(tǒng)中沒有對(duì)于Uopt 作出限制的公理，f 是非等同映射的單射的情形是可以在保持系統(tǒng)一致的情形下成立的。，則可由自然數(shù)類型的推理規(guī)則證得謂詞F1的外延潛無窮。即是說，若接受前文所提到的潛無窮和實(shí)無窮觀點(diǎn)中所接受的“不區(qū)分有窮分層”的公理AF1,-，則可以生成潛無窮多的滿足有窮謂詞F1的對(duì)象，進(jìn)而可以得到潛無窮多個(gè)有窮對(duì)象。只有回避掉公理AF1,-，才能避免此情形。

從上述例子可以看出，對(duì)有窮和開放的分階段和分層的分析有助于澄清潛無窮觀點(diǎn)和有窮開放主義觀點(diǎn)之間的區(qū)別。該例子中系統(tǒng)作為有窮開放類型系統(tǒng)，根據(jù)定理3 可知其描述了一個(gè)關(guān)于自然數(shù)的有窮開放類。但若引入潛無窮觀點(diǎn)并對(duì)公理進(jìn)行改動(dòng)，則會(huì)導(dǎo)致不再能保證其描述了有窮開放類（這是因?yàn)榈? 層的各階段有窮謂詞不再能保證是外延有窮的）。

例2.考慮公理系統(tǒng)Fb，令公理系統(tǒng)Fb包含BaseO 中所有公理，以及如下關(guān)于初始階段對(duì)象和算子的公理：

其中，f0是值為0 的常函數(shù)；f1是值為1 的常函數(shù)；對(duì)任意項(xiàng)x:Uopt及任意函數(shù)f:Uopt →Uopt，((g f)x)的值為x+(f0)；對(duì)任意項(xiàng)x,y:Uopt，((h x)y)的值為x。26二元函數(shù)+僅用于解釋h 和g 所表示的函數(shù)，二元函數(shù)+本身不在系統(tǒng)F b 內(nèi)。

可知，函數(shù)h作用在數(shù)n上會(huì)得到值為n的常函數(shù)；函數(shù)g作用在值為n的常函數(shù)上，會(huì)得到+n函數(shù)；函數(shù)g作用在+n函數(shù)上，也會(huì)得到+n函數(shù)。

逐層分析可得到如下結(jié)論：

(1)滿足F1的數(shù)僅有0,1，滿足的函數(shù)僅有值為0,1 的常函數(shù)，進(jìn)而滿足F2的數(shù)僅有0,1；

(7)依次類推……

使用歸納法可以證明，滿足Fi的數(shù)的數(shù)量（i ∈N+），形成了一個(gè)斐波拉契數(shù)列（Fibonacci sequence）。

論域相同的類可以因不同的謂詞序列而組成不同的開放類。從上述例子可以看出，給出一些特別的初始階段對(duì)象，可以獲得具有特別的特點(diǎn)的自然數(shù)開放類。對(duì)于初始對(duì)象的給定方式和所得開放類的特點(diǎn)之間的關(guān)系研究，是未來工作推進(jìn)的一個(gè)重要方向。

5 結(jié)語

我們?cè)谟懈F開放過程及其產(chǎn)物有窮開放類的直觀圖景的基礎(chǔ)上，采用類型論方法構(gòu)建了描述有窮開放類的分階段和分層的系統(tǒng)。

首先，本文給出了該形式系統(tǒng)描述自然數(shù)開放類時(shí)的示例。在該系統(tǒng)中，描述了有窮對(duì)象和開放算子的分階段屬性和分層屬性，亦描述了開放類的各階段和各層次的對(duì)象、開放算子、有窮謂詞之間的包含、推導(dǎo)和函數(shù)應(yīng)用關(guān)系。

其次，本文使用該系統(tǒng)對(duì)有窮開放立場(chǎng)和潛無窮立場(chǎng)進(jìn)行了區(qū)分：有窮開放立場(chǎng)下的開放類型系統(tǒng)對(duì)于遞歸公理和遞歸生成自然數(shù)的過程采取較為謹(jǐn)慎的態(tài)度。本文通過有窮謂詞分層避免了可以無限制地通過迭代函數(shù)遞歸生成對(duì)象的情形。在有窮開放分層系統(tǒng)中，遞歸生成對(duì)象或自然數(shù)的過程并不能無限制地進(jìn)行下去。

最后，我們證明了文中的若干開放類型系統(tǒng)（如系統(tǒng)BaseO2、BaseO3、BaseO4與系統(tǒng)BaseO）之間的包含關(guān)系。并證明了文中構(gòu)建得到的系統(tǒng)的一致性。

在下一步的工作中，我們將對(duì)開放類型系統(tǒng)中部分公理進(jìn)行調(diào)整，以研究各種調(diào)整后生成的變形系統(tǒng)的不同性質(zhì)，以及它們與各種算數(shù)系統(tǒng)之間的聯(lián)系，進(jìn)而探討有窮開放主義哲學(xué)觀下的自然數(shù)理論與各種算數(shù)系統(tǒng)之間的異同。如調(diào)整系統(tǒng)中對(duì)于遞歸生成對(duì)象和自然數(shù)的過程的限制，可能會(huì)關(guān)聯(lián)到一些和計(jì)算復(fù)雜性領(lǐng)域或數(shù)論領(lǐng)域相關(guān)的結(jié)論。

如所周知，在形式系統(tǒng)中描述帶有不確定性的對(duì)象是一件非常困難的事情。本文的工作是對(duì)描述具有這種不確定性的有窮開放類的初步嘗試，定會(huì)有不完善之處。我們希望在未來的工作中，進(jìn)一步完善和發(fā)展現(xiàn)有結(jié)果。