ご苦労さまです それ解説ついているでしょ？（下記） >>612より en.wikipedia.org/wiki/Epsilon-induction Epsilon-induction Statement The schema is for any given property ψ of sets and states that, if for every set x, the truth of ψ(x) follows from the truth of ψ for all elements of x, then this property ψ holds for all sets. In symbols: ∀x.((∀(y∈x).ψ(y))→ψ(x))→∀z.ψ(z) Note that for the "bottom case" where x denotes the empty set {}, the subexpression ∀(y∈x).ψ(y) is vacuously true for all propositions and so that implication is proven by just proving ψ({})}. In words, if a property is persistent when collecting any sets with that property into a new set and is true for the empty set, then the property is simply true for all sets. Said differently, persistence of a property with respect to set formation suffices to reach each set in the domain of discourse. (引用終り)
なお、追加で下記など ご参考まで
www.researchgate.net/publication/2480936_Set_Theory_for_Verification_II_Induction_and_Recursion Set Theory for Verification: II Induction and Recursion Lawrence C. Paulson Computer Laboratory, University of Cambridge April 1995 Minor revisions, September 2000
