ZF subtheory of T
zuhair
Theory T.
Language: FOL with identity,epsilon membership and the primitive one
place predicate V.
Define: y is transitive <-> for all mn ((n in m & m in y) -> n in y).
Define: y subset z <-> for all x (x in y -> x in z).
Define: y proper subset z <-> (y subset z & ~y=z).
Define: y superset z <-> z subset y.
Axioms:
1)Extensionaltiy: for all z ((z in x <-> z in y) -> x=y).
2)Transitive closure:
for all x exist y ((y superset x & y is transitive) &
forall z ((z superset x and z is transitive)
-> y subset z)).
Now y would be unqiue!
Define: y=Tc(x) <-> ((y superset x & y is transitive) &
forall z ((z superset x and z is transitive)
-> y subset z)).
were Tc(x) stands for "the transitive closure of x".
3) Class comprehension schema: If Q(y,x1,....,xn) is a formula in
which V do not occure, and x1 in V,....,xn in V, and in which c is not
free, then all closures of
exist c for all y (y in c <-> (y in V & Q(y,x1,....,xn)))
are axioms.
Define:
c={y|Q} <-> for all y (y in c <-> (y in V & Q(y,x1,....,xn))).
were Q have the same restrictions in class comprehension.
4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
V do not occure, and x1 in V,....,xn in V, and in which c is not free,
and c={y|Q}, then all closures of
[~Q(c) &
for all z ((c in Tc(z) or c proper subset z) -> ~Q(z))]
->
c in V
are axioms.
Theory definition finished/
Now it appears to me that for all well founded sets in V, we can have
ZF as a subtheory of this theory.
Define: x is well founded <-> ~ x in Tc(x).
Zuhair
zuhair
Lets take the class of all well founded elements of V.
In this theory we define set in the following manner
for all x (x is a set <-> x in V).
so V is the class of all sets.
Now from class comprehension we can have the class of all well
founded
sets which is unique and lets denote it as W.
Now one can easily prove all the following theorems.
For all a in W,b in W (a union b in W).
For all x in W ( Union x in W)
For all x in (Power (x) in W)
exist N in W (0 in N & Ay (y in N -> y union {y} in N))
also separation on well founded sets and replacement restricted
within
W can be proved here easily.
Of course a union b is the class of exactly all members of a and b.
Union x is the class of exactly all members of members of x.
Power (x) is the class of exactly all subsets of x.
I don't know how to prove regularity, but I do not think it can be
proved, and same to be said of choice.
It appears as if W is comparable to the universe of discourse of ZF
minus regularity pluse the axiom for all x : ~ x in Tc(x).
I would appreciate if any body point to an inconsistency with this
theory.
Actually a fifth axiom can be added which is the axiom schema of
Large
sets
5) Large Sets comprehension schema: If Q(y,x1,....,xn) is a formula
in
which V do not occure, and x1 in V,....,xn in V, and in which c is
not
free, and c' is not free, and c={y|Q}, and c'={y|~Q}then all closures
of
[Q(c) & Q(c')] -> c in V.
are axioms
if we add this axiom, then a lot of Large sets that are not proved to
exist by ZF would be proved to exist. like the set of all sets, the
set of all sets supernumerous to a set, absolute complementary set
for
each set?, also this theory can prove that the set of all sets that
are in themselfs is in itself.
I do greatly doubt that axiom schema 5, might lead to inconsistencies,
and
even if not I doubt its usefullness. One can easily see that the set
of all sets equi-numerouse to a set is not a set, it is a proper
class.
This theory share's Ackermann's class theory in that there must be
proper classes (subsets of V that are not in V) that are members of
other classes, otherwise it would be inconsistent.
This theory might be equivalent to Ackermann's class theory minus
Regularity for sets plus the axiom : for all x ( ~ x in Tc(x) ).
Regards
Zuhair
zuhair
This can be reduced to the following:
4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
V do not occur, and x1 in V,....,xn in V, and in which {y|Q} is not
free,then all closures of
for all z ({y|Q} subset Tc(z) -> ~Q(z))
->
{y|Q} in V
MoeBlee
> 4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
> V do not occur, and x1 in V,....,xn in V, and in which {y|Q} is not
> free,then all closures of
>
> for all z ({y|Q} subset Tc(z) -> ~Q(z))
I would move the part about "x1,..., xn in V" down to be the
antecedent of the formula itself rather than as a clause in the
English part of the meta-statement. Similarly, for you other schemata
that have that kind of relativization to V.
But what does "{y |Q}" is not free" mean? You mean there are no free
variables in Q other than possbily 'y', I guess. (In that case we say
'{y | Q}' is a closed term, as opposed to an open term.)
But {y | Q} can't even occur in Q, lest you have infinite formula
within formula....
By the way, you might get by with your definition of '{y | Q}' but I
don't like the way you do it. Your formulation doesn't specify how to
understand '{y | Q}' in contexts other than as a term in an equation.
MoeBlee
zuhair
It seems that I have made a mistake then.
lets go about it again.
what I wanted to say is something like that:
4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
V do not occur, and x1 in V,....,xn in V, and in which c is not free,
and c={y|Q}, then all closures of
for all z (c subsetTc(z) -> ~Q(z))
->
c in V
are axioms
I already defined what c={y|Q}
c={y|Q} <-> for all y ( y in c <-> ( y in V and Q(y) ).
In the set comprehension schema what I really mean by c is the
following:
c={y|Q} <-> for all y ( y in c <-> ( y in V and Q(y,x1,...,xn) ).
were y,x1,...,xn are all free variables in Q and x1,...,xn are in V,
and of course c itself is not to occur free in Q. but instead of
saying c not occur free in Q, I just said
{y|Q} is not free in Q, which is apparantly what was my mistake.
So actually the axiom schema is:
4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
V do not occur, and x1 in V,....,xn in V, and in which c is not free,
then all closures of
for all c ( (c= {y|Q} & for all z (c subsetTc(z) -> ~Q(z)))
->
c in V )
are axioms
Or more extensively:
4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
V do not occur, and x1 in V,....,xn in V, and in which c is not free,
then all closures of
for all c ( (for all y ( y in c <-> ( y in V and Q(y,x1,...,xn) ).
& for all z (c subsetTc(z) -> ~Q(z)))
->
c in V )
are axioms.
I hope this clarify the matter.
Zuhair
zuhair
Sorry that is not the definition of W.
Define: x is linear <-> ~ x in Tc(x)
Define: x is optimally founded <-> for all y (y in Tc(x) -> y is
linear)
Now of course any set that is optimally founded is also linear.
Now W={x| x in V and x is optimally founded}
Now working in W we can prove all the following theorem:
For all a in W,b in W (a union b in W).
For all x in W ( Union x in W)
For all x in (Power (x) in W)
exist N in W (0 in N & Ay (y in N -> y union {y} in N))
also separation on optimally founded sets and replacement restricted
within W can be proved here easily.
so ZF is interpretable in this theory.
After many discussions with Mr. Randall Holmes who intially thought
the theory is inconsistent turned to believe that it *does* work, and
he see it is interesting.
He thinks that a prove similar to the prove of ZF being interpretable
in Ackermann's class theory, might work to prove that ZF is
interpretable in this theory.
Scheme 4 has the "reflextion principel* within it,so it does prove
separation for the same reason's Ackermann's does.
By the way do anybody know the exact proof of William
Reinhardt in which Zf was found to be interpretable in Ackermann's.
Zuhair
> Zuhair- Hide quoted text -
>
> - Show quoted text -
MoeBlee
> 4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
> V do not occur, and x1 in V,....,xn in V, and in which c is not free,
> and c={y|Q}, then all closures of
>
> for all z (c subsetTc(z) -> ~Q(z))
> ->
> c in V
>
> are axioms
You don't understand the advice I gave about x1 ... xn in V?
Try this:
If Q is a formula in which there is at least one free occurence of z,
and V does not occur, and c is not free, then all closures of
c={y | Q} &
x1 in V,....,xn in V &
Az(c subset of Tc(z) -> ~Q)
->
c in V
The stuff about "c={y | Q}" and "x1 in V,....,xn in V" is better in
the formula itself than in the meta-language header that concerns
stipulations about formulas and variables.
> I already defined what c={y|Q}
You haven't defined:
{x | Q} in z
{x | Q} in {x | P}
{x | Q} in {x | P}
z in {x | Q}
V{x | Q}
And what happens when the restrictions on Q you mention fail?
Moreover, your restriction about xn's in V is not DECIDABLE, so it is
not even decidable what is well formed in your syntax.
MoeBlee
See the first volume of Takeuti and Zaring for one of the better
treatments of this appraoch to class abstraction notation.
zuhair
> On Jul 7, 4:57 pm, zuhair <zaljo...@gmail.com> wrote:
>
> > 4) Set comprehension schema: If Q(y,x1,....,xn) is a formula in which
> > V do not occur, and x1 in V,....,xn in V, and in which c is not free,
> > and c={y|Q}, then all closures of
>
> > for all z (c subsetTc(z) -> ~Q(z))
> > ->
> > c in V
>
> > are axioms
>
> You don't understand the advice I gave about x1 ... xn in V?
>
> Try this:
>
> If Q is a formula in which there is at least one free occurence of z,
> and V does not occur, and c is not free, then all closures of
>
> c={y | Q} &
> x1 in V,....,xn in V &
> Az(c subset of Tc(z) -> ~Q)
> ->
> c in V
are axioms.
Any how, that is not that important. my intention was clear, and what
you say here is not that different, it is basically the same.
>
> The stuff about "c={y | Q}" and "x1 in V,....,xn in V" is better in
> the formula itself than in the meta-language header that concerns
> stipulations about formulas and variables.
>
> > I already defined what c={y|Q}
>
> You haven't defined:
>
> {x | Q} in z
> {x | Q} in {x | P}
> {x | Q} in {x | P}
> z in {x | Q}
> V{x | Q}
>
> And what happens when the restrictions on Q you mention fail?
> Moreover, your restriction about xn's in V is not DECIDABLE, so it is
> not even decidable what is well formed in your syntax.
Yea, you should tell that to Ackermann.
zuhair
>
> Theory T.
>
> Language: FOL with identity,epsilon membership and the primitive one
> place predicate V.
What is this. Sorry V is a primitive constant.
zuhair
Now I think I know the source of the confusion here. V is a primitive
constant, it is not a one place predicate symbole. I made a typo.
zuhair
what happens? you think I put restrictions that are not important?
what happens is that theory becomes inconsistent without these
restrictions, that is very clear, reveiw ackermann's class theory.
> Moreover, your restriction about xn's in V is not DECIDABLE, so it is
> not even decidable what is well formed in your syntax.
I should admit here that I don't know what you mean here, but V is a
primitive constant of the language so how come x in V is not well
formed?
MoeBlee
> Any how, that is not that important. my intention was clear, and what
> you say here is not that different, it is basically the same.
Sorry, I thought you might be interested in how to put your
formulations in a sharper way and also in a general notion that it is
more clear to put the parts of the formula in the formula and not
detached and within the header of the schema statement.
> > The stuff about "c={y | Q}" and "x1 in V,....,xn in V" is better in
> > the formula itself than in the meta-language header that concerns
> > stipulations about formulas and variables.
>
> > > I already defined what c={y|Q}
>
> > You haven't defined:
>
> > {x | Q} in z
> > {x | Q} in {x | P}
> > {x | Q} in {x | P}
> > z in {x | Q}
> > V{x | Q}
>
> > And what happens when the restrictions on Q you mention fail?
> > Moreover, your restriction about xn's in V is not DECIDABLE, so it is
> > not even decidable what is well formed in your syntax.
>
> Yea, you should tell that to Ackermann.
What specifically do you refer to?
MoeBlee
MoeBlee
> > > I already defined what c={y|Q}
>
> > You haven't defined:
>
> > {x | Q} in z
> > {x | Q} in {x | P}
> > {x | Q} in {x | P}
> > z in {x | Q}
> > V{x | Q}
>
> > And what happens when the restrictions on Q you mention fail?
> > Moreover, your restriction about xn's in V is not DECIDABLE, so it is
> > not even decidable what is well formed in your syntax.
>
> Now I think I know the source of the confusion here. V is a primitive
> constant, it is not a one place predicate symbole. I made a typo.
Then eliminate my mention of V{x | Q}. The rest of my remarks stand.
You have not given a definition of your class abstraction notation
that even provides for decidability of well-formedness in your syntax.
MoeBlee
zuhair
>
> - Show quoted text -
If Q is a formula in which there is at least one free occurence of z,
and V does not occur, and c is not free, then all closures of
[c={y | y in V and Q(y,x1,...,xn)} &
x1 in V,....,xn in V &
Az(c subset of Tc(z) -> ~Q(z,x1,...,xn))]
->
c in V
are axioms.
MoeBlee
> I should admit here that I don't know what you mean here, but V is a
> primitive constant of the language so how come x in V is not well
> formed?
I didn't say 'V' is not well formed. What I said is it is not
decidable whether a given string that employs your class abstraction
notation is well formed, since you've put the "xn's in V" restriction
on the notation. It is not decidable (or at least it is not
immediately clear that it is decidable) whether, for a given
instantiation of the xn's, we have those objects in V.
Moreover your "definition" of your class abstraction notation only
addresses the context of an equation and does not say what to do with
it in the other formula contexts I mentioned.
You can't just assume that the definitional forms for ordinary
predicate and function symbols are just like the forms or explanation
needed for variable binding notation such as your class abstraction
notation.
MoeBlee
zuhair
I don't know what you are talking about, you remarks are not clear to
me, what is exactly the problem?? you say x1 in V,...,xn in V is not
decidable, what do that means, I don't get it? anyhow you can tell
Ackermann's the same thing, because this is the formulation in his
theory.
Class here are pritty clear x={y|Q} is taken to mean x is the class of
exactly members of V that satisfy the property Q. what is the problem
with that
you can write it as x={y in V| Q} or you can write it as
x= {y| y in V and Q(y)}
for short I write it as x= {y|Q} to mean that x is the class of all
members of V that satisfy the property Q.
What is the problem with that?
MoeBlee
> I don't know what you are talking about, you remarks are not clear to
> me,
I bet, since you've never read a book on first order logic, its
syntax, definitions, and variable binding abstraction.
> what is exactly the problem?? you say x1 in V,...,xn in V is not
> decidable, what do that means,
It means there is no (or at least you haven't shown) that there is a
decision procedure to determine, for an arbitary term T, whether "T in
V" is or is not a theorem of your system.
This is only a problem in your context since your "definition" for the
variable binding {x | Q} depends on your condition regarding xn's in
V.
It is not the axiom schema I am referring to, but rather the even MORE
BASIC matter of your particular treatment for the {x | Q} notation.
Moreover, regarding that notation, you've only provided for it in
context of equations. If you wish for it to be used in other kinds of
formulas, then you need to show how to do that.
Again, I recommend Takeuti and Zaring for a quite good discussion of
this matter, which, in their system is somewhat differerent from your
system, but still the general ideas are useful.
> Ackermann's the same thing, because this is the formulation in his
> theory.
I've already asked you, please refer me to the specific paper or book
you are referring to.
> Class here are pritty clear x={y|Q} is taken to mean x is the class of
> exactly members of V that satisfy the property Q. what is the problem
> with that
> you can write it as x={y in V| Q} or you can write it as
> x= {y| y in V and Q(y)}
>
> for short I write it as x= {y|Q} to mean that x is the class of all
> members of V that satisfy the property Q.
>
> What is the problem with that?
I told you the problem. It does not provide for explication of the
notation other than in equations.
For example, please tell me the AUTOMATIC translation of
{y | Q} in {x | P}
back to your primitive language.
If you can tell me that AUTOMATIC translation, then you will have
supplied one of the needed clauses I mentioned earlier.
Moreover, this time you ommitted your restriction regarding the xn's
and V.
MoeBlee
MoeBlee
"c={y|Q} <-> for all y (y in c <-> (y in V & Q(y,x1,....,xn))).
where Q(y,x1,....,xn) is a formula in
which V do not occure, and x1 in V,....,xn in V, and in which c is not
free,"
But there is no algrorithm we know of to determine, for arbitrary term
T (such that your x's might be instantiated to), whether "T in V" is a
theorem thus whether for a given Q, your {y |Q} with the x's in Q
instantiated to terms T would be syntactical in your system.
Moreover, please show how to take the formulas
c={y | Q} <-> Ay(y in c <-> (y in V & Q(y,x1,....,xn)))
c={y | P} <-> Ay(y in c <-> (y in V & Q(y,x1,....,xn)))
and AUTOMATICALLY (i.e., without use of other previously UNstated
assumptions in your presentation) apply them to eliminate {y | Q} and
{x | P} from the formula
{y | Q} in {x | P}
so that we are back to a formula in the primitive language.
MoeBlee
zuhair
The way how I look at is is the following.
{y|Q} means the class of all members of V that satisfy the property Q.
{x|P} means the class of all members of V that satisfy the property P.
Now if you say {y|Q} in {x|P} then {y|Q} must be in V and must satisfy
the property P, otherwise {y|Q} is not in {x|P}.
Symbolically:
{y | Q} in {x | P} <-> {y|Q} in V and P{y|Q}
Is there a problem with that?
MoeBlee
> {y | Q} in {x | P} <-> {y|Q} in V and P{y|Q}
>
> Is there a problem with that?
Yeah there're a problem with it! It doesn't even address the question!
It doesn't eliminate the notation!
Moreover, STILL you've not settled the problem of your stipulation
about xn's in V.
Please listen carefully: The point is to show how to reduce back to a
formula in the PRIMITIVE language (i.e. NOT using the "{ | }"
notation.
What is the point in purporting to answer that question by just giving
another formula that uses the "{ | }" notation?!
But I want to reiterate something I said earlier. I said earlier that
I think you can skate by with your formulation (if you fix the part
about xn's in V). That is, for most working purposes, perhaps you can
express yourself with the notation in a way that will be well enough
understood. My point though is that your purported DEFINITION of the
notation is not a proper definition as it stands. I could suggest
either Takeuti or Zaring, as I have, or I could propose an informal
compromise that I actually use for plain Z set theory. Otherwise, one
may end up with the headache of taking abstraction notation as
primitive which involves the complication of simultaneous induction
and simultaneious recursio or such complicated vindications as in
Levy's 'Basic Set Theory'. In any case, it would be better just to
take the notation in an informal manner (as it is given, for example,
in the Stanford Philosophy online article that mentions Ackermann's
system) than to purport to give a definition, which actually is not
correctly formed.
MoeBlee
zuhair
> Putting your clauses together you wrote:
>
> "c={y|Q} <-> for all y (y in c <-> (y in V & Q(y,x1,....,xn))).
>
> where Q(y,x1,....,xn) is a formula in
> which V do not occure, and x1 in V,....,xn in V, and in which c is not
> free,"
>
> But there is no algrorithm we know of to determine, for arbitrary term
> T (such that your x's might be instantiated to), whether "T in V" is a
> theorem thus whether for a given Q, your {y |Q} with the x's in Q
> instantiated to terms T would be syntactical in your system.
what algorithm you are talking about, I am talking about things that
are stipulated or rather forced to be, no things are to be determined
or decided.
Q(y,x1,...,xn) and the conditions of x1 in V,..., xn in V is well
known Ackermann's thoery, that's not my notation as you think, why you
don't review any subject on Ackermann's theory to understand it.
You are exactly objecting to a well known theory.
take the formula " y=x1 or y=x2" were x1 and x2 are "stipulated" to
be in V. what is the problem with that, what undecidability you are
talking about, we don't need a way to determine that x1 or x2 are in
V, WE STIPULATE them to be in V beforehand.
Let me take an example:
Let Q(y,x1,x2) <-> ( y=x1 or y=x2 )
Now axiom scheme 4 is stating the following
Acx1x2 ([x1 in V and x2 in V and c={y|y=x1 or y=x2} and
Az ( c subset Tc(z) -> (~z=x1 and ~z=x2) )]
-> c in V.
you want to tell me that this is not decidable,
How can that be.
For example if using this theory we proved that 0 in V and we proved
that {0} in V
then we used these instantations of x1 and x2, Now this theoy decided
before hands that 0 and {0} are in V, then we apply these
instantations in this schema
to reach at the conclusion that {0,{0}} in V, because it can be proved
in this theory that for every z such that {0,{0}} subset Tc(z) then z
is neither 0 nor {0}.
What is vague about that????
Zuhair
zuhair
> On Jul 8, 6:05 pm, zuhair <zaljo...@gmail.com> wrote:
>
> > {y | Q} in {x | P} <-> {y|Q} in V and P{y|Q}
>
> > Is there a problem with that?
>
> Yeah there're a problem with it! It doesn't even address the question!
>
> It doesn't eliminate the notation!
ah, Now I see what you mean. but we don't need to go their, it is only
a big headacke.
But I can go around it
for all c ( c= {y|Q} ->
({y|Q} in {x|P}) <-> (for all y (y in c <-> (y in V and Q(y))) and c
in V and Pc) ).
perhaps that is not satisfactory though.
MoeBlee
> On Jul 8, 5:44 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > Putting your clauses together you wrote:
>
> > "c={y|Q} <-> for all y (y in c <-> (y in V & Q(y,x1,....,xn))).
>
> > where Q(y,x1,....,xn) is a formula in
> > which V do not occure, and x1 in V,....,xn in V, and in which c is not
> > free,"
>
> > But there is no algrorithm we know of to determine, for arbitrary term
> > T (such that your x's might be instantiated to), whether "T in V" is a
> > theorem thus whether for a given Q, your {y |Q} with the x's in Q
> > instantiated to terms T would be syntactical in your system.
>
> what algorithm you are talking about, I am talking about things that
> are stipulated or rather forced to be, no things are to be determined
> or decided.
Do you understand the principle that for a formal language there must
an algorithm to test for certain syntactical matters?
> Q(y,x1,...,xn) and the conditions of x1 in V,..., xn in V is well
> known Ackermann's thoery, that's not my notation as you think, why you
> don't review any subject on Ackermann's theory to understand it.
> You are exactly objecting to a well known theory.
I asked you THREE times to refer me to your specific source. Why are
you rudely ignoring that I've been making this simple reasonable
request?
And I'm not objecting to a well known theory. I'm pointing out that
YOUR particular formulation that purports to be a DEFINITION of
abstraction notation in a certain context is not properly formed.
Rather than learn about such things by reading a book on the subject,
you prefer to bicker about it.
> take the formula " y=x1 or y=x2" were x1 and x2 are "stipulated" to
> be in V. what is the problem with that, what undecidability you are
> talking about, we don't need a way to determine that x1 or x2 are in
> V, WE STIPULATE them to be in V beforehand.
That's fine as an antecedent in an AXIOM, but it doesn't work in a
DEFINITION since given EXPRESSIONS themselves don't come with
stipulations as to whether such and such is in V or not.
Please, I can't explain the subject of definitions better than you
will find in a good book on mathematical logic, and especially as to
class abstraction notation better than is explained in Takeuti and
Zaring, for instance.
> Let me take an example:
>
> Let Q(y,x1,x2) <-> ( y=x1 or y=x2 )
>
> Now axiom scheme 4 is stating the following
>
> Acx1x2 ([x1 in V and x2 in V and c={y|y=x1 or y=x2} and
> Az ( c subset Tc(z) -> (~z=x1 and ~z=x2) )]
> -> c in V.
>
> you want to tell me that this is not decidable,
>
> How can that be.
YOU'RE NOT EVEN LISTENING TO WHAT I SAID!
I said SPECIFICALLY that the problem is not in the axiom schema but in
the more basic matter of your purported DEFINITION of the abstraction
notation.
> For example if using this theory we proved that 0 in V and we proved
> that {0} in V
> then we used these instantations of x1 and x2, Now this theoy decided
> before hands that 0 and {0} are in V, then we apply these
> instantations in this schema
YOU DIDN'T EVEN READ WHAT I WROTE. What is the purpose of my trying to
communicate with you if you're not going to read what I wrote?
I SPECIFICALLY said the problem is NOT In the schema itself but in the
prior, more basic matter of a purported DEFINITION of abstraction
notation.
Sheesh!
MoeBlee
zuhair
Another try.
{y|Q} in {x|P}
<->
for all c ( for all y ( y in c <-> ( y in V and Q(y))) -> ( c in V and
Pc)).
I think that is the translation that you need.
Zuhair
MoeBlee
> {y|Q} in {x|P}
> <->
> for all c ( for all y ( y in c <-> ( y in V and Q(y))) -> ( c in V and
> Pc)).
That's getting somewhat better.
But your stubborness, rudeness (why you won't even MENTION your
Ackermann source so I can read for myself), and evident lack of
reading my posts has worn me out for today.
MoeBlee
zuhair
You are speaking gibberish. what definition you are talking about and
what abstraction you are babbling about.
The notation are clear, and there is no difficulty in understanding
them, you have a difficulty that is fine, you go and read about it,
and don't blame others for not understanding it. surf the wikipedia,
standford encyclopedia about ackermann, read every source about
ackermann and you'll see what I mean.
You are only making simple understandable things a difficult jumbled
matter, algorthim you say and other shitty non understandable stuff.
Why the hell a man like Randall Holmes didn't make your clever notes,
ha, can you tell me, he never objected to any of these aspects of this
theory. You care a lot about the form, missing what is even more
important, and that is what that theory is saying. Why you don't just
state the best way to write the theory since it appears that you are
understanding it informally as you say, so that I compare and
understand what you are saying. I don't like terminology and refering
me to books and that stuff, just say what you propose to be right, so
that I can see for myself what you mean instead of philosophating
things.
Don't say algorthim , don't say any of that stuff, just show me in
simple terms what you mean. "in simple terms".
Why Ackermann didn't show the algorithm you wanted, can you tell me.
YOU ARE OBJECTING TO ACKERMANN'S class theory, that's what you are not
grasping till now, so and solve this question their?
Zuhair
>
> MoeBlee
zuhair
See it in "Wikipedia, Standford Encyclopedia, also I had a previous
source, which was given to me be one of the participants here, but I
lost it, it contain the details of Ackermann's formulae.
anyhow
zuhair
I remembered his name was G.Frege. he game me an article about
Ackermann's and explained some of it, I don't remember the original
language of it though.
Zuhair
zuhair
But you know very well that I meant this, so why you ask about
something that you know very well, that's why I don't like.'
Zuhair
MoeBlee
> You are speaking gibberish. what definition you are talking about and
> what abstraction you are babbling about.
You can be a real first class jerk sometimes. I love it when you say
*I* am speaking 'gibberish' and 'babbling'.
I'm talking about the definition of {y | Q} you gave! Just as I SAID I
was.
And the abstraction notation IS the "{ | }" notation.
> The notation are clear, and there is no difficulty in understanding
> them, you have a difficulty that is fine, you go and read about it,
> and don't blame others for not understanding it. surf the wikipedia,
> standford encyclopedia about ackermann, read every source about
> ackermann and you'll see what I mean.
I read it long ago and I just re-read it.
You DON'T find a DEFINITION of the notation there. But JUST AS I
ALREADY SAID, we see informal passing use that is, JUST AS I ALREADY
SAID, adequate for working purposes.
> You are only making simple understandable things a difficult jumbled
> matter, algorthim you say and other shitty non understandable stuff.
It's not understandable to YOU because you never read a damn book on
the subject, not even a damn article, not even a damn INTERNET article
on the subject.
> Why the hell a man like Randall Holmes didn't make your clever notes,
> ha, can you tell me, he never objected to any of these aspects of this
> theory.
So what? He may not be interested in giving notes about every single
detail in what you wrote. He may have whatever reasons for commenting
on what he comments on. You're posting to the Internet and not to
Randall Holmes personally. If you want only the kind of comments that
you get from Randall Holmes personally, then you'd be wiser to
correspond only with him.
> You care a lot about the form, missing what is even more
> important, and that is what that theory is saying.
I happen to be interested in certain technical details. That doesn't
mean I miss other things. Moreover, you present theories and then
ABANDON posting anything further about them the way I go through
orange cream sodas out my refrigerator over a hot weekend. I don't
have to address the full philosophical splendor of your latest theory
of the week just to make certain technical comments about it.
> Why you don't just
> state the best way to write the theory since it appears that you are
> understanding it informally as you say, so that I compare and
> understand what you are saying.
I was TRYING to let you onto some suggestions that would let you touch
up such details YOURSELF. I don't have to re-write each of your
theories. I've ALREADY done that kind of thing for you. I've ALREADY
done things like spend an entire weekend of my life writing up one of
your theories and various of its theorems. I don't have to do that
each time just to justify making certain technical comments when I
chose to do so.
> I don't like terminology and refering
> me to books and that stuff, just say what you propose to be right, so
> that I can see for myself what you mean instead of philosophating
> things.
It's not a matter of "just saying what is right". Moreover you
(effectively if not overtly) ASKED me to explain my comments. Damn,
what an ass you are to effectively ASK me to explain myself and then
to turn around and tell me that it's a bunch of 'gibberish',
'blabbering', and 'philosophizing' and that you don't want to hear it
after all.
> Don't say algorthim , don't say any of that stuff, just show me in
> simple terms what you mean. "in simple terms".
No, I'll say 'algorithm' all I want to say it. It's not even a formal
term. It's a simple concept. And I can't always simplify to the extent
you wish it to be simple. Sometimes things do get complicated and
careful attention to detail and to explanation, especially regarding
certain fine details about syntax and definition, etc.
And what I said WAS simple. I'll say it again: For a formal theory
there must be algorithms to determine answer syntactical questions
about the syntax.
For example, there must be an algorithm to determine whether any
arbitrary string of symbol is or is not a well formed formula. And
since 'well formed formula' usually depends on whether certain
substrings are TERMS, there must be an algorithm to determine whether
any arbitrary string of symbols is a term.
This is really basic stuff. If you're not interested, then suit
yourself. But then you're silly to say I haven't already given you
relatively simple explanation. Moreover, it's not my JOB to explain
stuff to you. And iff I post explanations you can take them or leave
them, whatever suits you, and you can find out about the subject on
your own or not, whatever suits you, but you're being a first class
jerk when you call my comments 'gibberish' and 'babbling'.
> Why Ackermann didn't show the algorithm you wanted, can you tell me.
> YOU ARE OBJECTING TO ACKERMANN'S class theory, that's what you are not
> grasping till now, so and solve this question their?
No, I am NOT objecting to Ackermann's theory. READ what I wrote about
that.
MoeBlee
zuhair
You haven't defined:
{x | Q} in z
{x | Q} in {x | P}
{x | Q} in {x | P}
z in {x | Q}
V{x | Q}
The answer is:
Definitions:
{x|Q} in z
<->
for all c for all z ( for all x ( x in c <-> ( x in V and Q(x) )) and
c in z )
{x|Q} in {x|P}
<->
for all c for all z ( for all x ( x in c <-> ( x in V and Q(x) )) and
for all x ( x in z <-> ( x in V and P(x) ))
and
c in z).
z in {x | Q}
<->
for all z for all c ( for all x ( x in c <-> ( x in V and Q(x) )) and
z in c ).
V is a primitive constant so V{x|Q} has no meaning.
Zuhair
MoeBlee
One more thing:
zuhair wrote:
> what that theory is saying.
Have you noticed that there aren't a whole hell of a lot of people
talking here about what your various theories are "saying"? Why is
that, zuhair? Maybe once in a while a poster or two, maybe even three
at most, will drop by to comment. Then you flit away onto yet some
other theory that you don't even bother to mention its reason for
invention or interest. On the other hand, I gave you some suggestions
as to how you might present your theories so that your presentations
are more INVITING for people to investigate and discuss your theories.
I notice you didn't even take those suggestions. And then when out of
a total of ZERO people who are commenting on your theory, I make a few
technical suggestions, the price for me is to read you saying to me
that my comments are "gibberish" and "babbling" and to deal with your
stubborness post after post. Damn, and let's not even count the
TEDIOUS hours of posting to you over the YEARS to even help you learn
how to write formulas so that you could express yourself with them.
You acted the same THEN as you do NOW: Insulting the very people
(there were a few more people back then who helped you) who were the
ones whose time and over-extended patience spent on you PROVIDED your
(still fragile) ability to express yourself in formulas. You were
DRAGGED, by your collar as you kicked and screamed, into the semi-
literacy with set theoretical notation that you have now. And so it
continues...
And as to your claim that I don't understand the overall meanings of
your weekly theories, hmm, I guess I didn't do such a bad job of it
when I wrote up an actual itemized description of the ontology of one
of your theores that even YOU incorporated into your presentation!
Oh, I'm sorry, I must have gotten off-topic. Of course the topic is
for people to gather around your posts, as if at the base of a
monolith, and give appreciation for all the wonderful things they are
"saying", along with a few other people who are to scurry like clerks
checking for YOU such things as equi-consistency. Sorry, I didn't mean
to spread downer vibes on this party of ZERO other people marveling at
what your theory is "saying". Please do continue your discussion with
all zero of these people...
MoeBlee
MoeBlee
Too late for me to give a damn now. You wasted my interest, spent
instead on tiresome squabbling just trying to deal with your
stubbornnes. Maybe later....
MoeBlee
zuhair
>
> - Show quoted text -
Ok then, later.
good night!
zuhair
> On Jul 8, 4:43 pm, zuhair <zaljo...@gmail.com> wrote:
>
> > I should admit here that I don't know what you mean here, but V is a
> > primitive constant of the language so how come x in V is not well
> > formed?
>
> I didn't say 'V' is not well formed. What I said is it is not
> decidable whether a given string that employs your class abstraction
> notation is well formed, since you've put the "xn's in V" restriction
> on the notation. It is not decidable (or at least it is not
> immediately clear that it is decidable) whether, for a given
> instantiation of the xn's, we have those objects in V.
This is a little bit vague to me (because of my ignorance of course),
but why do we need this decidability?
To me schem 4 is very simple, and we need not to be involved with
these decidability matters. of course for a given term x1 which is a
symbole one cannot decide wether it is in V or not, since V is a
symbole and x1 are symboles of the language, and there is no way to
decide that PRIOR to the theory (at the meta theoratic level) this
decision is left to the theory itself.
Let me clarify things, in scheme 4 what I am saying is that we have a
formula
Q(y,x1,...,xn) in which y,x1,...,xn are *all* its free variables, no
problem here, also we add the restiction of V not occuring in this
formula, no problem till here, we can know weather y or x1 or any xn
is occuring free in Q(y,x1,...,xn) or not, from the fact of it being
quantified in Q(y,x1,...,xn) or not, also V is a primitive constant
so we can know if it occur in the formula or not, also we add the
restriction of c not occuring free in Q(y,x1,...,xn) , up till now I
see no problem, here all the meta theoratic language specifying Q
(y,x1,...,xn) ends! (therer is no restriction on this notation at
metatheoratic level that x1,...,xn in V, this is not a part of the
metatheoratic restriction on notation), now we say that all closures
of
[c={y | Q} &
x1 in V,....,xn in V &
Az(c subset of Tc(z) -> ~Q(z))]
->
c in V
are axioms.
Now the question is what make us decide weather an instantation of x1
for example is in V, my simple answer is *theorems or axioms* in this
theory should lead you to that result, there is no way to decide that
PRIOR to them.
In this theory we have the theorem : 0 in V and {0} in V
Now take the formula y=0 or y={0}
what made us decide that 0 in V and {0} in V was the axiom above.
I always thought that the decidsion weather an instantion of xn is in
V, is something that the theory decides and not to be decided at
metatheoratic level.
Anyhow I don't know weather I have addressed this difficult techniqal
question.
If I didn't then I admit that I don't understand the whole grounds
for
that question.
Perhaps if Moe Blee show me an example of how this decidability is
done in other theories for similar formulaes perhaps I can undersand
the question, and perhaps I might answer it. Especially in
Ackermann's
since it uses exactly the same formulation used here with the same
restrictions, so how can Moe Blee question address the question of
decidability in Ackermann's would be relavent to this theory as well.
Regards
Zuhair
MoeBlee
> To me schem 4 is very simple, and we need not to be involved with
> these decidability matters.
For the FIFTH time (now even after I've SHOUTED it), I was not talking
about the axiom schema. I was talking about the clause about the xn's
in your definition of {y | Q} (i.e., the same clause as in your schema
but regarding not your schema but rather your defininition of {y | Q},
just as you mentioned it).
But now I'm sorry I even mentioned it. It hardly matters in the great
scheme of life. Please disregard the entire matter.
MoeBlee
zuhair
> On Jul 9, 5:10 am, zuhair <zaljo...@gmail.com> wrote:
>
> > To me schem 4 is very simple, and we need not to be involved with
> > these decidability matters.
>
> For the FIFTH time (now even after I've SHOUTED it), I was not talking
> about the axiom schema. I was talking about the clause about the xn's
> in your definition of {y | Q} (i.e., the same clause as in your schema
> but regarding not your schema but rather your defininition of {y | Q},
> just as you mentioned it).
What is wrong in my definition of {y|Q}?
actually the complete way to write it is {y|Q(y,x1,...,xn)}
Q(y,x1,...,xn) is a formula which has y,x1,...,xn as its sole free
variables, and in which c is not free, and in which V do not occur. is
there any problem with that notation?
Now define:
c={y|Q(y,x1,...,xn)} <-> for all y ( y in c<-> ( y in V and Q
(y,x1,...,xn) ) )
I really don't know what is wrong with that?
Perhaps you thought that the clasue "x1 in V,...,xn in V" is a part of
the definition of {y|Q(y,x1,...,xn)} which is NOT.
The clause "x1 in V,...,xn in V" is present in the schema 4 *ONLY*,
but not in the definition of {y|Q(y,x1,...,xn)}.
hope that helps.
Zuhair
MoeBlee
> What is wrong in my definition of {y|Q}?
> actually the complete way to write it is {y|Q(y,x1,...,xn)}
>
> Q(y,x1,...,xn) is a formula which has y,x1,...,xn as its sole free
> variables, and in which c is not free, and in which V do not occur. is
> there any problem with that notation?
***Please read the last paragraph of this post first so that you
don'lt bother typing line by line replys to the below.***
Looking quickly at your formulation above, it seems okay.
But I took your original formulation to include xn's in V, as you
mentioned "were Q have the same restrictions in class comprehension".
Ah, now I see that it was even MORE important that I suggest that in
the schema you separate the formula from the header material. You
squeezed the condition about xn's in V BETWEEN conditions for Q, and
in the header of the schema not in the following formula where should
be. Then when I read your stipulation about {y | Q} I took that
stipulation about the xn's in V along with it.
Moreover, not only should the part about xn's in V be in the formula
and not in the header, but it MUST be, since the CLOSURE is over the
xn's also, but the clause about the xn's in V stuck was stuck in the
header instead of the formlua, leaving the xn's dangling PRIOR to the
closure clause and thus not covered by the closure clause.
But, please, I'm DONE with this now. Please don't ask me more about
this if you don't understand what I just wrote. This is tiring and
boring, especially to communicate by posts, especially about details
that you really would rather not care about, especially about some
formulas of yours that will be forgotten by tomorrow as you move on to
some other theory by then.
So, okay? If you don't understand my notes above, then fine, please
let it go. Abstraction notation, and getting its detail just right (a
concern you don't seem to have nor perhaps should you even have) can
be a rather tricky, complicated business that can be tiring to try to
talk about in posts, and I'm not an expert anyway. So no more
questions about this one, please.
MoeBlee
zuhair
I understand now *all* of what is in this reply. I just thought you
were talking about something else, anyhow, you were right actually, In
this thread I wrote the theory in hast, I admit that, I didn't ment to
wright it in EXACT formal way as it might appear, However I re wrote
this theory in another topic.
Thanks
Regards
MoeBlee
> I understand now *all* of what is in this reply.
In a sense, part of the misreading was mine also. If I had caught that
earlier, it would have been better. Anyway, the reason I'm dropping
out of discussion about the rest of the details is (1) as I mentioned,
for working purposes you can avoid such details anyway, especially
since they are laborious, and a truly rigorous treatment of variable
binding operators is not easy, as even most established authors rest
on a relaxed approach, and (2) I got displeased with even my own part
in a thread of personal argument, since I've been in personal
arguments in other threads all week long.
MoeBlee
zuhair
Forget about the personal arguments, you did a good job!
what is important is that you mentioned a good point, and to say the
truth I became more appreciative of the delicate matters that you used
to say ( though I admit that before that I used to see it and
extravagant formalisim) for example I new long before you wrote here
that x1 in V,..., xn in V should be in the formula and not in the
header, but I was considering that matter trivial and not important,
however in this thread I came to realize that I am wrong, since it
causes a lot of confusion otherwise.
Thanks, your remarks has been really useful to me.
And sorry for the bad words.
Zuhair
MoeBlee
> sorry for the bad words.
Okay, me too then.
By the way, in your new thread, you don't need
"for all x1 in V,...,xn in V for all c" in the set comphrehension
schema.
The quanfiter "for all" is already taken care of when you say "all
closures of".
So, after the header, all you need is
x1...xn each in V &
c = {y | Q(y,x1,...,xn)} &
Az(c subset of Tc(z) -> ~Q(z,x1,...,xn))
->
c in V
Also, I don't know why you say 'superset' when you could just reverse
the variables and say 'subset', which is faster to absorb by dint of
familiarity
MoeBlee
zuhair
> On Jul 10, 2:20 pm, zuhair <zaljo...@gmail.com> wrote:
>
> > sorry for the bad words.
>
> Okay, me too then.
>
> By the way, in your new thread, you don't need
>
> "for all x1 in V,...,xn in V for all c" in the set comphrehension
> schema.
>
> The quanfiter "for all" is already taken care of when you say "all
> closures of".
>
> So, after the header, all you need is
>
> x1...xn each in V &
> c = {y | Q(y,x1,...,xn)} &
> Az(c subset of Tc(z) -> ~Q(z,x1,...,xn))
> ->
> c in V
But you forgot the paranthesis though,
it should be:
(x1...xn each in V &
c = {y | Q(y,x1,...,xn)} &
Az(c subset of Tc(z) -> ~Q(z,x1,...,xn)))
->
c in V
>
> Also, I don't know why you say 'superset' when you could just reverse
> the variables and say 'subset', which is faster to absorb by dint of
> familiarity
ah, Ok then.
>
> MoeBlee
MoeBlee
> On Jul 10, 4:36 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> > So, after the header, all you need is
>
> > x1...xn each in V &
> > c = {y | Q(y,x1,...,xn)} &
> > Az(c subset of Tc(z) -> ~Q(z,x1,...,xn))
> > ->
> > c in V
>
> But you forgot the paranthesis though,
> it should be:
>
> (x1...xn each in V &
> c = {y | Q(y,x1,...,xn)} &
> Az(c subset of Tc(z) -> ~Q(z,x1,...,xn)))
> ->
> c in V
You can just make it a notational convention that the conjucts are
understood to be grouped as indicated by putting the '->' sign on a
separate line. That makes for a nice uncluttered presentation:
hypothesis_1 &
hypothesis_2 &
hypothesis_3 &
...
hypothesis_n
->
conclusion
MoeBlee