Re: Multilayer Set Theory:

On May 27, 10:59 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2007-05-27, in sci.math, zuhair wrote:

I don't know, regarding this point.
But as I see neither Vi nor Vj are constants
they are variables that range over constants V1,V2,V3,...,Vn ( the
finite version) or
over V1,V2,V3,...... in the infinite version.

There is no apparatus in first order logic for quantifying over syntactic
elements of the first order language in question. AViAvj(...) is simply
not well-formed.


Accordingly axiom 3 should be schematized to:

3) Layers schema: For every i,j such that j>i the sentence
Ax(xeVi -> xeVj) & ~ Vi=Vj
is an axiom.

What about the other axioms should they be schams also
Like for example pairing

AaeViAbeViExeViAy(yex<->(y=a v y=b)).

Should that be changed to the following schema:

For every i the sentence

AaeViAbeViExeViAy(yex<->(y=a v y=b))

is an axiom.




I always like to speak in terms of MK rather than ZF.
so essentially what I did is Omega-order MK type theory.

What you're doing is omega-order MK, not MK in omega-order type theory. As
said, in type theory comprehension is restricted so that we can only
quantify over elements of Vi when defining sets in Vi. In your theory, and
in omega-order MK, there is no such restriction.

--
Aatu Koskensilta (aatu.koskensi...@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus


.

Relevant Pages

  • Re: Multilayer Set Theory:
    ... There is no apparatus in first order logic for quantifying over syntactic ... What you're doing is omega-order MK, not MK in omega-order type theory. ...
    (sci.math)
  • Re: Qi vs. SPAD/Aldor?
    ... implemented in Lisp, and I'm curious because some of the discussions ... advanced mathematical programming as Aldor (given some library ... I've not used Axiom or SPAD. ... Study 1 on the type theory of interval arithmetic ...
    (comp.lang.lisp)
  • Re: Induction in second order arithmetic
    ... post in which he indulged in his adorable habit of wanton shouting, ... simple, and non-simple type theory. ... Russell postulated the axiom of reducibility which effectively reduces ... What other logics ...
    (sci.logic)
  • Re: Induction in second order arithmetic
    ... post in which he indulged in his adorable habit of wanton shouting, ... simple, and non-simple type theory. ... Russell postulated the axiom of reducibility which effectively reduces ... What other logics ...
    (sci.logic)
  • Re: Skolems Paradox and why is math the way it is?
    ... >>interpretation why not have that axiom instead? ... > The first problem with your suggestion is that it uses the predicate ... Modern mathematics needs a two type theory anyway. ...
    (sci.math)