On Apr 19, 5:35 pm, Zuhair <zaljo...@gmail.com> wrote: > Using theories that *interpret* Z; ZF can greatly shrink the > axiomatics needed for proving the consistency of those theories, an > old observation of course. The following couple of first order > theories is a nice demonstration of that: > > C shall be used to denote the known subset relation. > > Theory 1 is the closure of all sentences following from: > > 1. Separation If phi is a formula in which y is free but not x, > then all closures of: > > For all A Exist x For all y (y in x iff y C A & phi) > > are axioms. > > 2. Infinity. > > This interprets Z. > > Theory 2 is the closure of all sentences following from: > > (1) Replacement: If phi(x,y) is a formula in which x,y are free but > not B, > then all closures of: > > For all A ([For all x C A Exist z for all y (Phi(x,y) -> y C z)] > -> Exist B for all y (y in B iff Exist x C A (phi(x,y)))) >
Or we can use:
VA EB [(VyeB(ExeA.P)) & (VxeA (Ey.P -> EyeB.P))]
Where V signifies "for all"
> are axioms. > > (2) Infinity > > This interprets ZF. > > If one seeks to prove the consistency of Z or ZF, then proving the > above theories would be sufficient, there is no need to try prove ALL > the known axioms of those theories. > > Zuhair