FOM: Axioms of Substitution

Matt Insall montez at
Wed Sep 20 19:47:20 EDT 2000

Professor Shavrukov pointed out that my substitution axioms did not do what
I said they do.  I agreed, so here is a correction of the schema.  I hope
this takes care of the difficulties:

(forall x)(forall y)(forall z)[{[psi(x,y)&psi(x,z)] implies y=z} implies
(thereis w)(forall y){[y is in w] iff (thereis x)[(x is in w)&psi(x,y)}&{(w
is a set) iff (x is a set)}]

Dr. Matt Insall

More information about the FOM mailing list