本原命題函詞(primitive propositional func- tiom) GB系統中的一類合式公式。
本原命題函詞(primitive propositional func- tiom) GB系統中的一類合式公式，在GB系統中，本原命題函詞指僅含變元、特殊類符號A AZ, ... Ak，屬於符號任、命題連結詞並且其中的約束變元都是集合中變元的合式公式.例如，tlu(uEX->uE A)是本原命題函詞;而當」X或bY在合式公式中出現時，則就不是本原命題函詞.又如，tlx<xE A一二C y)也不是本原命題函詞，因為其中出現了定義符號里.
顯然，本原命題函詞範圍很窄，大量的謂詞涉及定義符號，因而要對本原命題函詞進行擴張. (axiom of choice) GB系統的集合論公理.指GB系統中的第5組(即E組)公理.指存在著單值的類A，對任何非空集合二，都有二的元y 存在，使有<y,x)EA.其符號表達式為 El衛{Un<A)八愉[-I Cm (x)一取<yEx八 }y,x)任A)]}. 因為單值關係就是函式，故上述E1中之A，實際上就是全選擇函式.因而E1就是指無條件承認存在著這樣的全選擇函式A，它能從任何一個非空集合中惟一地選出一個元素來.
