[FOM] Generalization Axiom Scheme

[Zuhair Abdul Ghafoor Al-Johar]

To scrutinize this further, every subformula of phi(y) (when phi(y)
has parameters) must not hold for finites only.

To re-write the scheme:

for all n=0,1,2,3,...; if phi(y) is a formula
in which only z1...zn occur as parameters, in which
x is not free, and in which u doesn't occur, and
where Q1...Qm are all subformulas of it, then:

(n>0 ->(not[(u).Q1(u) -> finite(u)]&...& not[(u).Qm(u) -> finite(u)])) and
((z1)...(zn) are HF. (y). phi(y) -> y is HF)
->
(z1)...(zn) are sets. Exist x. set(x) & (y). y e x iff phi(y)

is an axiom.

Qi(u) refers to the formula Qi but with all occurrences of one of the free
variables in Qi replaced by u.
/

Zuhair Al-Johar