ZFC

… The axiom system of set theory, first presented by Zermelo in 1908, was supplemented by AAFraenkel in 1922, then formalized and extended by J. von Neumann using symbolic logic, and then refined by P. Bernays and Gödel. There are two types of axiom system of set theory: Zermelo-Fraenkel set theory (ZFC) and Bernays-Gödel set theory (BG or NBG), but the latter is a formal extension of the former, and the two are considered to be the same in content, so we will discuss ZFC below. ZFC is a system formalized in first-order predicate logic, with only = and ∈ symbols other than predicate logic symbols. Its axioms are: (1) extensional axiom ∀ a ∀ b (∀ x ( x ∈ a ↔ x ∈ b )→ a ＝ b ) (2) existence axiom of the empty set ∃ a ∀ x ( x ∉ a ) (set a whose existence is guaranteed by this axiom is shown to be unique by axiom (1) (similar below), represented by φ) (3) pair axiom ∀ a ∀ b ∃ c ∀ x ( x ∈ c ↔( x ＝ a ∨ x ＝ b )) (set c defined by this axiom for sets a and b is represented by { a , b }, and when a ＝ b , it is simply written as { a }) (4) union axiom ∀ a ∃ b ∀ x ( x ∈ b ↔∃y ( x ∈ y ∧ y ∈ a ))(5)Power set axiom ∀ a ∃ b ∀ x ( x ∈ b ↔ x ⊆ a )(6)Infinity axiom ∃ a (φ∈ a ∧∀ x ( x ∈ a → x ∪{ x }∈a ) )(If the smallest set of such a set a is ω, and φ is 0, n ∪{ n } is n + 1, then ω＝{0,1,……, n ,……} and the piano axiom is true, as shown by the above axioms and the division axiom described below)(7)Substitution axiom ∀ x ∀ y ∀ z (φ( x , y )∧φ( x , z )→ y ＝ z ), for any logical formula φ( x , y ), ∀ a ∃ b ∀ y ( y ∈ b ↔∃ x ( x ∈ a ∧φ( x , y )))(8)It consists of the regularity axiom ∀a ( a ≠φ→∃ x ( x ∈ a ∧ x ∩ a ＝φ)) and the axiom of choice. …

*Some of the terminology explanations that mention "ZFC" are listed below.

Source | Heibonsha World Encyclopedia 2nd Edition | Information

…　1908年，ツェルメロによって初めて提示された集合論の公理系は，22年にフレンケルA.A.Fraenkelによって補強され，次いでJ.フォン･ノイマンによる記号論理を用いて形式化や形式上の拡張を経て，P.ベルナイス，ゲーデルによって整備された。集合論の公理系として，ツェルメロ=フレンケルの集合論(ZFC)と呼ばれるものと，ベルナイス=ゲーデルの集合論(BGあるいはNBG)と呼ばれるものとがあるが，後者は前者の形式上の拡張であって，両者は内容的には同じものと考えられるので，以下ZFCについて述べる。　ZFCは述語論理の記号以外には＝と∈だけの記号をもった第1階の述語論理で形式化された体系であって，その公理系は，(1)外延性の公理　∀a∀b(∀x(x∈a↔x∈b)→a＝b)(2)空集合の存在公理　∃a∀x(x∉a)(これによって存在を保障される集合aは公理(1)によりただ一つであることが示され(以下同様)，φで表す)(3)対の公理　∀a∀b∃c∀x(x∈c↔(x＝a∨x＝b))(集合a,bに対して，この公理によって規定される集合cを｛a,b｝で表し，a＝bのときは単に｛a｝とかく)(4)和集合の公理　∀a∃b∀x(x∈b↔∃y(x∈y∧y∈a))(5)べき集合の公理　∀a∃b∀x(x∈b↔x⊆a)(6)無限公理　∃a(φ∈a∧∀x(x∈a→x∪｛x｝∈a))(このような集合aの最小の集合がωであって，φを0,n∪｛n｝をn＋1とすれば，ω＝｛0,1，……，n，……｝でかつピアノの公理が成り立つことが以上の公理および後述の分出公理とから示される)(7)置換公理　∀x∀y∀z(φ(x,y)∧φ(x,z)→y＝z)を満たす論理式φ(x,y)に対して，∀a∃b∀y(y∈b↔∃x(x∈a∧φ(x,y)))(8)正則性公理　∀a(a≠φ→∃x(x∈a∧x∩a＝φ))および選択公理とからなっている。…

※「ZFC」について言及している用語解説の一部を掲載しています。

出典｜株式会社平凡社世界大百科事典 第２版について | 情報