基本介紹
- 中文名：ST類型論
- 領域：計算機，數學
介紹,公式,參見,
介紹
有一個最低的類型，它的個體沒有成員並且是次最低類型的成員。最低類型的個體對應於特定集合論中的基本元素（urelement）。每個類型都有一個更高的類型，類似於在皮亞諾算術中後繼者。ST對是否有極大類型保持沉默，形成超限數個類型沒有困難。這些因素，和回應於皮亞諾公理，使它方便和習慣於指派自然數到每個類型，開始於0給最低類型。這個類型論不要求自然數的先決定義。
ST的特有符號是加右上角標的變數和中綴
。在任何給定的公式中，無角標的變數都有相同的類型，而有角標的變數（
）取值於更高的類型上。ST的原子公式與兩種形式，
（同一性）和{。中綴符號暗示了預想的釋義，集合成員關係。
出現在同一性定義和外延和概括公理中所有變數都取值於連貫的兩個類型之上。一個"低層"類型和另一個"高層"類型。取值於高層類型上的變數加角標；而取值於低層類型的變數不加。ST的一階公式化排除在類型上的量化。所以每對連續的類型都要求它自己的外延和概括公理，如果“外延”和“概括”公理採用公理模式的方式取值於類型上就是可能的。
公式
同一性定義：
。
外延公理模式：
。
概括公理模式：
。
備註:相同類型的元素的任何蒐集都可以形成更高類型的一個對象。概括公理有關於{\displaystyle \Phi (x)}也有關於類型。
備註:無窮公理是ST的唯一真正的，並且本質上完全是數學的公理。R也是一個嚴格全序，帶有同一的域和陪域。如果0被指派給最低層類型（依次1是對（雙元素集合，單元素集合），2是有序對），R的類型是3。這個公理強迫一個無窮集合的存在，因為只有R的（陪）域是無窮的時候它才可以被滿足。如果關係以有序對的方式定義，這個公理要求有序對的先決定義；ST接受Kuratowski的定義。文獻沒有給出ZFC和其他集合論的無窮公理（存在歸納集合）不能結合於ST的理由。
ST披露了類型論可以制定得何其類似於公理化集合論。而ST更加精緻的本體論，根源於現在所謂的“集合的疊代構想”，導致了遠比有著更簡單的本體論的常規集合論如ZFC簡單得多的公理（模式）。公理化集合論起步於類型論，但是它的公理、本體論和術語不同於上面所述ST系統，還包括新基礎和Scott-Potter集合論。
