ST類型論
下面的系統是Mendelson的（1997: 289-93）ST。量化的域被劃分成上升的類型層次，帶有所有的個體都被指派了一個類型。量化的變量確立範圍只在一個類型上；所以底層邏輯是一階邏輯。ST是"簡單的"（相對於《數學原理》中的類型論）主要是因為任何關係的域和陪域的所有成員都必須是同一個類型的。
有一個最低的類型，它的個體沒有成員並且是次最低類型的成員。最低類型的個體對應於特定集合論中的基本元素（urelement）。每個類型都有一個更高的類型，類似於在皮亞諾算術中後繼者。ST對是否有極大類型保持沉默，形成超限數個類型沒有困難。這些因素，和回應於皮亞諾公理，使它方便和習慣於指派自然數到每個類型，開始於0給最低類型。這個類型論不要求自然數的先決定義。
ST的特有符號是加右上角標的變量和中綴。在任何給定的公式中，無角標的變量都有相同的類型，而有角標的變量（）取值於更高的類型上。ST的原子公式與兩種形式，（同一性）和。中綴符號暗示了預想的釋義，集合成員關係。
出現在同一性定義和外延和概括公理中所有變量都取值於連貫的兩個類型之上。一個"低層"類型和另一個"高層"類型。取值於高層類型上的變量加角標；而取值於低層類型的變量不加。ST的一階公式化排除在類型上的量化。所以每對連續的類型都要求它自己的外延和概括公理，如果「外延」和「概括」公理採用公理模式的方式取值於類型上就是可能的。
同一性定義：。
![{\displaystyle x=y\Leftrightarrow \forall z'[x\in z'\leftrightarrow y\in z']}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f538805b00ad49b5797aa9eac9a5a14c747065a5)
![{\displaystyle \forall x[x\in y'\leftrightarrow x\in z']\Rightarrow y'=z'}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2ff5d9fb42ed7ed0e147a4ca2eaaad58632c3b16)
概括公理模式：。
![{\displaystyle \exists z'\forall x[x\in z'\leftrightarrow \Phi (x)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eb4a658d2361622ebd2a3a36796fcd632e6094da)
備註:相同類型的元素的任何搜集都可以形成更高類型的一個對象。概括公理有關於也有關於類型。
無窮公理。存在著在最低層類型的個體之上的非空二元關係R，它是反自反的、傳遞的和強連接的（）。
![{\displaystyle \forall x,y[xRy\lor yRx]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cfb6c11a0acd492a9a947672b8014daf418592bb)
備註:無窮公理是ST的唯一真正的，並且本質上完全是數學的公理。R也是一個嚴格全序，帶有同一的域和陪域。如果0被指派給最低層類型（依次1是對（雙元素集合，單元素集合），2是有序對），R的類型是3。這個公理強迫一個無窮集合的存在，因為只有R的（陪）域是無窮的時候它才可以被滿足。如果關係以有序對的方式定義，這個公理要求有序對的先決定義；ST接受Kuratowski的定義。文獻沒有給出ZFC和其他集合論的無窮公理（存在歸納集合）不能結合於ST的理由。
ST披露了類型論可以制定得何其類似於公理化集合論。而ST更加精緻的本體論，根源於現在所謂的「集合的迭代構想」，導致了遠比有著更簡單的本體論的常規集合論如ZFC簡單得多的公理（模式）。公理化集合論起步於類型論，但是它的公理、本體論和術語不同於上面所述ST系統，還包括新基礎和Scott-Potter集合論。
參見
[編輯]參考文獻
[編輯]- Mendelson, Elliot, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
- W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.