一個關于有窮開放過程的類型論系統

梁曉龍 鞠實兒

1 引論

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

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

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

進一步，根據開放過程生成對象的方式和時間節點的不同，開放過程可以被區分成不同的階段，而生成的對象也被相應地劃歸為各個不同階段。如數域擴張過程中，從自然數類到整數類、從整數類到有理數類、從有理數類到實數類等過程，均可看作數域擴張過程的不同階段；又如自然數生成過程中，生成104以內數、生成108以內數、生成1012以內數等過程，均可看作自然數生成過程的不同階段。各個階段可以按順序分別稱為第一階段、第二階段、等等。第一階段也稱初始階段。

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

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

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

根據以上所述，本文將在第2 節介紹類型論語言。在第3 節中，本文將以自然數類為典型案例，分析有窮和開放的分層和分階段屬性，并使用類型論語言進行形式化。第4 節中，本文將對第3 節的形式化系統進行一般化推廣，使用類型論語言構建關于有窮開放類的分層和分階段系統，給出有窮開放類型系統的形式化定義。

2 類型論語言的基本概念

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

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

其中x,x′,...為變元符，c,c′,...為項原始常元符，f,f′,...為定義常元符。

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

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

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

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

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

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

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

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

當上下文Γ 為空時，Γ?a:A和Γ?a ≡b:A可分別記為· ?a:A和·?a ≡b:A，或?a:A和?a ≡b:A。

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

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

推理規則中，橫線上方稱為推理規則的假設，橫線下方稱為推理規則的結論。

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

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

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

接下來本節將列出本文進行形式化時所需要涉及到的部分馬丁洛夫類型論中的推理規則。

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

定義8.類型宇宙的推理規則為：

類型宇宙推理規則給出了類型論語言中各個類型所在的宇宙之間的關系。

定義9.良形式推理規則為：

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

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

單元類型的引入規則和消去規則如下：

單元類型的形成規則和計算規則如下：

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

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

依賴乘積類型消去規則和計算規則為：

依賴乘積類型的唯一性規則為：

類型(Πx:A)B稱為依賴于類型A的到類型B的函數類型，也可記為Π(x:A)B、?x:A,B或(?x:A),B。若需要強調類型B根據變元x的取值變化，也可記為(Πx:A)B(x)、Π(x:A)B(x)、?x:A,B(x)以及(?x:A),B(x)。8多層的依賴乘積類型的符號可以進行簡寫，只保留最開始的Π 或?符號，如(Πx y: A)B、Π(x:A)(y:C)B、?(x: A)(y: C),B、(?x y: A),B 等等。在涉及類型宇宙的情況下(?A: Ui),B 可簡寫為(?A),B，若根據表達式能得出(?x: A),B 形式的式子中的A 的表達式時，也可簡寫為(?x),B。

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

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

函數類型在柯里-霍華德對應理論中對應蘊含命題，其引入規則對應蘊含引入規則；其消去規則對應MP 規則。

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

定義14.一個形如a:A的基本斷定可被稱為一個公理，其中a,A為項。

一組公理以及馬丁洛夫類型論的所有推理規則組成的整體，稱為一個基于馬丁洛夫類型論的公理系統，簡稱一個公理系統。

不失一般性，由于任意項的所在類型是唯一的，故可用項a來表示公理a:A；由于不同公理系統的推理規則均為馬丁洛夫類型論的推理規則，故可用公理系統的公理集表示公理系統本身。進一步，由于一組數量有窮的公理可以看作一個上下文，故也可用一個上下文表示一個公理系統。

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

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

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

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

本節將給出有窮開放分層和分階段的直觀圖景，以及一個自然數開放類的具體的構造過程；進而分析自然數開放類的各層次各階段對象，以及各層次各階段的有窮謂詞之間的關系；并使用類型論語言對此進行形式化，構建一個關于自然數開放類的類型論系統。

為了實現目標，本節先用類型論語言描述一個自然數的系統，它可以作為有窮開放過程以及由此生成的有窮開放類的典型案例。通過分析這一案例，可以展示有窮開放類構建過程及其分層和分階段的一般結構。

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

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

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

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

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

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

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

對于每一個被認為是第0 層第一階段有窮的對象，需要有一個關于“第0 層第一階段有窮”的謂詞，以及相應的公理宣稱其有窮。

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

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

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

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

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

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

根據前文所述，給定的三個第1 層第一階段的算子為：

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

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

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

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

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

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

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

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

當需要開放過程是擴充過程的情形時，可得F1與F2之間的關系公理：

該關系公理也稱為擴充公理。

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

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

可以注意到，若不對有窮謂詞作區分，認為F1與F2相同，則上述公理可變形為：

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

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

繼續上述構建系統過程，當已獲得若干第0 層第一、二階段有窮對象以及若干第1 層第一階段有窮的開放算子之后，會有下一層的開放算子。通過第0 層對象和第1 層開放中的對象，生成更多的對象，即為第2 層開放算子所產生的效果。

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

f+為自然數的二元加法函數；f(-)2為二次的迭代函數；f0和分別為定義域為自然數和定義域為自然數上一元函數的兩個常函數，其函數值均為自然數0。

故在給定關于第2 層開放算子的有窮謂詞時，需要根據對象的類型規定不同的有窮謂詞，故第2 層開放算子的有窮謂詞需要帶有類型參數。

不失一般性，當類型A和B可以通過上下文確定的時候，可簡寫為

對于上述四個不同類型的函數，分別用相應公理宣稱其在第2 層中是第一階段有窮的。

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

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

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

使用公理系統Open3N3，對證明結構進行歸納，可得出以下若干結果：(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 層開放等階段和層次。

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

當開放過程是擴充過程時，第三層開放的定義引入的謂詞，與之前已有謂詞之間的關系的公理如下：

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

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

可以注意到，每一個新的層次中，增加的有窮謂詞和開放算子的形式都與已有的層次是相似的；同時，每個新的層次中的公理也與已有的公理具有相同的形式。故后續階段以及更高層的算子、謂詞、公理等，均可以通過繼續此步驟各開出。進一步，可以從已有的示例中的層次出發，推理得出更高層次中對象、謂詞、公理的通項形式。本文將在下一節中給出這些形式的統一描述。

4 有窮開放類型系統

本節將對第三節中關于自然數開放類的類型論系統進行一般化推廣；構建描述有窮開放類的分層和分階段屬性的系統：開放類型系統；并構建用于描述只涉及若干層開放算子的有窮開放類的系統：有窮開放分層系統。此外，本節將證明第三節中構建的關于自然數開放類的系統是本節中的系統的子系統13系統A 是系統B 的子系統是指：系統A 中所有可證的斷定均是系統B 中可證的。；并證明第三節和本節中的各個關于開放類的系統的一致性。

第3 節中，關于自然數開放類的案例僅涉及了第0 層對象、第1、2、3 層開放算子。其中給出的關于不同階段不同層次的有窮謂詞、以及有窮謂詞之間關系的公理的角標均只涉及0,1,2,3,4。對于更高層次和更后續的階段，有窮謂詞和有窮謂詞之間關系的公理可以通過前幾階段和前幾層次的公理推廣得到。本節將根據上文中的典型案例，整理構建出關于有窮對象和開放算子的分階段和分層系統的一般結構。14本節中的類型定義使用了自然數作為角標，但使用自然數角標不是“必須”的。在實際構造過程中，可以用其他類型代替自然數作為角標給出上述的各種定義。此處選用自然數的定義僅僅是因為其記號較為方便，并且相關定義使用自然數作為參數更容易理解。

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

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

關于謂詞Di:Type→Prop 給出一組公理：

這些公理稱為層次函數公理，規定了開放層次謂詞與函數類型和類型Uopt之間的聯系。

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

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

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

該組公理表示：滿足某個階段有窮謂詞的項也會滿足更后續階段的有窮謂詞。

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

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

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

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

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

證明.對照可知，公理系統BaseO2、BaseO3、BaseO4中的各階段和各層次的有窮謂詞、及謂詞之間關系公理的角標情形均為公理系統BaseO 中公理的特例。故定理得證。

定理2.公理系統BaseO 是一致的。

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

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

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

推論1.公理系統nexBaseO 是一致的。

推論2.公理系統BaseO2、BaseO3、BaseO4是一致的。

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

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

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

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

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

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

證明.對類型A、B滿足FType的證明結構進行歸納即可證明prod A B滿足FType。

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

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

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

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

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

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

當一個類型滿足謂詞Inf時，也稱該類型為一個潛無窮類型；外延無窮的謂詞，也稱為外延潛無窮的謂詞。

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

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

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

如果一個基礎開放類型系統是一致的，則稱為開放類型系統。

定義27.一個公理系統稱為非擴張的基礎開放類型系統，若其包含：公理系統nexBaseO 中所有公理；用于給定每一層的初始階段中對象的公理，以及相應的宣稱給定的對象滿足該層次初始階段有窮謂詞的公理。

如果一個非擴張的基礎開放類型系統是一致的，則稱為非擴張的開放類型系統。

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

進一步，可以有如下定義：

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

定義29.對任意自然數n，若（非擴張的）開放類型系統S的一個子系統S′滿足：S′包含且僅包含S的所有前n層（非擴張的）開放類型公理，則稱S′為S的前n層（非擴張的）開放類型系統。

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

推論4.有窮開放類型系統是一致的。

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

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

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

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

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

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

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

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

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

定理3.一個（非擴張的）有窮開放類型系統歸納地描述了一個有窮開放類。

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

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

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

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

本節最后將給出兩個例子，說明開放類型系統的一些特點。

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

給定初始階段對象和算子及其相關公理如下：

對上述公理組成的公理系統中證明的證明結構使用歸納法可知，可證的關于有窮對象和開放算子的相關命題有且僅有：

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

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

從上述例子可以看出，對有窮和開放的分階段和分層的分析有助于澄清潛無窮觀點和有窮開放主義觀點之間的區別。該例子中系統作為有窮開放類型系統，根據定理3 可知其描述了一個關于自然數的有窮開放類。但若引入潛無窮觀點并對公理進行改動，則會導致不再能保證其描述了有窮開放類（這是因為第0 層的各階段有窮謂詞不再能保證是外延有窮的）。

例2.考慮公理系統Fb，令公理系統Fb包含BaseO 中所有公理，以及如下關于初始階段對象和算子的公理：

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

可知，函數h作用在數n上會得到值為n的常函數；函數g作用在值為n的常函數上，會得到+n函數；函數g作用在+n函數上，也會得到+n函數。

逐層分析可得到如下結論：

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

(7)依次類推……

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

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

5 結語

我們在有窮開放過程及其產物有窮開放類的直觀圖景的基礎上，采用類型論方法構建了描述有窮開放類的分階段和分層的系統。

首先，本文給出了該形式系統描述自然數開放類時的示例。在該系統中，描述了有窮對象和開放算子的分階段屬性和分層屬性，亦描述了開放類的各階段和各層次的對象、開放算子、有窮謂詞之間的包含、推導和函數應用關系。

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

最后，我們證明了文中的若干開放類型系統（如系統BaseO2、BaseO3、BaseO4與系統BaseO）之間的包含關系。并證明了文中構建得到的系統的一致性。

在下一步的工作中，我們將對開放類型系統中部分公理進行調整，以研究各種調整后生成的變形系統的不同性質，以及它們與各種算數系統之間的聯系，進而探討有窮開放主義哲學觀下的自然數理論與各種算數系統之間的異同。如調整系統中對于遞歸生成對象和自然數的過程的限制，可能會關聯到一些和計算復雜性領域或數論領域相關的結論。

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