Eliminability of identity -- For George Greene
mitch
In the appendix of "General Topology" by Kelley, there is an interesting
footnote:
"One is tempted to make this the definition of equality,
thus dispensing with one axiom and with all logical
presuppositions about equality. This is perfectly
feasible. However, there would be no unlimited
substituition rule for equality and one would have to
assume as an axiom: If xez and y=x, then yez"
Hopefully, it is clear from this remark that Kelley is referring to the
axiom of extension. It is in the presentation of this axiom that he
directs the readers attention to this observation.
Now, formally the new axiom would be given by
AxAyAz((xez & Au(uey <-> uex)) -> yez)
So, Mr. Greene, given your continual criticisms of my ideas, I have a
number of questions.
How can eliminability of identity be accomplished in first-order logic
if the presuppositions of identity that define it are necessarily
abandoned?
I believe you have put yourself in a position to explain how things are
done around here... Need I quote you?
Given that eliminability of identity requires an axiom not normally
found in set theories, I would like to know how you justify the axiom
that you have never explicitly presented while making your many claims?
I believe you have put yourself in a position to explain how things are
done around here... Why would I bother to quote you?
And, yes. I really do understand first-order logic.
:-)
mitch
mitch
mitch wrote:
> And, yes. I really do understand first-order logic.
>
George, don't really bother replying to this thread. I am tired of your
glee over causing flame wars, and, I know that from a purely logical
position you need only retreat to first-order logic without identity. Of
course, when I first started posting, you refused to acknowledge
equality-free logics in any form.
The point of this thread is that there are issues associated with usage of
the identity predicate in set theory, and, they arise precisely because of
the question of eliminability of the identity predicate relative to the
assertion of the axiom of extension. From a mathematical perspective, this
is not a good thing.
If you look at Lawvere and Schanuel's discussion of toposes in "Conceptual
Mathematics" you will see that the justifications are given in terms of
parts as this concept provides for a notion of "one-to-one" for the
morphisms. It would seem from a comparison of toposes and absoluteness for
transitive models of set theory that this concept of "one-to-one" is
fundamental from a mathematical perspective. It is preserved when an
identity relation or a part relation is a fundamental relation of the
language being interpreted.
For what it is worth, I do respect the rigor with which you approach these
matters. You should get yourself a copy of Jech's "Set Theory" or some
other suitable text to help you where you do have a lack of knowledge. But,
it is important to get something comprehensive. Countable transitive models
depend on the reflection principle, and therefore, a pre-existing set.
Discussions like Kunen's "people in M" or your own "in the opinion of the
model" just do not make sense because the underlying lack of rigor transfers
the problem of infinite regress from the logic to the meta-logic as Aatu
tried to tell you.
As far as things are done from a purely logical perspective, John Correy's
approach to handling the issues presented by Kelley's footnote are far more
conventional than the one I took. I am uncertain about what exact
consequences his sentences may have, but they attempt to deal with the issue
using an infinitist schema rather than a coherentist circularity. And, of
course, from the purely formalist perspective of manipulating syntax, that
is also nothing more than added complexity.
:-)
mitch
George Greene
: In the appendix of "General Topology" by Kelley, there is an interesting
: footnote:
:
: "One is tempted to make this the definition of equality,
: thus dispensing with one axiom and with all logical
: presuppositions about equality. This is perfectly
: feasible. However, there would be no unlimited
: substituition rule for equality and one would have to
: assume as an axiom: If xez and y=x, then yez"
Kelley doesn't know where he is.
There are TWO flavors of first-order logic, as I KEEP
trying to tell you. ONE is first-order logic WITHOUT equality.
The other is first-order logic WITH equality.
First-order logic WITH equality has TWO MORE INFERENCE RULES
than first-order logic without equality. They are the ones
that make = a logical symbol AS OPPOSED to something definable.
They are |- Ax[x=x]
and x=y |- phi(x)->phi(y)
: Hopefully, it is clear from this remark that Kelley is referring to the
: axiom of extension.
That is stupid. It is NEVER clear because YOU are
not smart enough to be trustable. You just have to quote
more of him. The problem is that there are TWO DIFFERENT
axioms of extensionality, DEPENDING on whether you are doing
1st-order ZFC in FOL WITH equality or WITHOUT.
: It is in the presentation of this axiom that he
: directs the readers attention to this observation.
OK, I guess that counts.
: Now, formally the new axiom would be given by
:
: AxAyAz((xez & Au(uey <-> uex)) -> yez)
The fact that he feels the need to do this seems to imply
that he is working in FOL withOUT equality. Fine.
That is the case for which eliminability is relevant.
Obviously you can't eliminate = from theories where the
underlying logic is keeping it around. But the need for
this extra axiom sort of needs to be explored. There
need to be exhibited some countermodels where substitutivity
fails. All the other axioms together are going to constrain
a lot of things.
: So, Mr. Greene, given your continual criticisms of my ideas, I have a
: number of questions.
:
: How can eliminability of identity be accomplished in first-order logic
: if the presuppositions of identity that define it are necessarily
: abandoned?
I repeat, there are two flavors. You had never before engaged the
discussion enough to clarify that substitutivity might fail in
one flavor.
: I believe you have put yourself in a position to explain how things are
: done around here... Need I quote you?
I think you need to come up with a counter-
model. I imagine the way things are normally done entails
being in FOL WITH equality.
: Given that eliminability of identity requires an axiom not normally
: found in set theories, I would like to know how you justify the axiom
: that you have never explicitly presented while making your many claims?
I have not been making "many" claims. I have just been harping
on this one issue, mostly; any of my other "many" claims have NOT
been made WHILE stressing this point.
: I believe you have put yourself in a position to explain how things are
: done around here... Why would I bother to quote you?
Because coherent discussion is impossible without it,
and because refusal to do so proves intellectual dishonesty,
THAT's why.
: And, yes. I really do understand first-order logic.
If you don't understand the difference between FOL without
equality vs. with, then NO, you DON'T really understand
first-order logic.
--
---
"It's difficult ... you need to be united to have any
strength, but internal issues have to be addressed."
--- E. Ray Lewis, on liberalism in America
George Greene
: mitch wrote:
:
: > And, yes. I really do understand first-order logic.
: >
:
: George, don't really bother replying to this thread. I am tired of your
: glee over causing flame wars,
Fuck you, bitch.
I don't have any glee over causing flame wars.
That is not a reasonable inference from anything *I* have
ever posted. YOU are the one who came into a logic forum
talking about how deficient the usual logic was and how
you understood it so much better, and then refused to engage
any points, instead just calling people flamers.
: and, I know that from a purely logical
: position you need only retreat to first-order logic without identity.
That is basically wrong; FOL without identity is where the problem
you cited in the previous message arises. In FOL with identity,
there is basically nothing to discuss; obviously identity is not
going to be eliminable from THAT.
: Of course, when I first started posting, you refused to acknowledge
: equality-free logics in any form.
QUOTE ME OR SHUT THE FUCK UP, BITCH.
I was OBVIOUSLY acknowledging FOL in general, and
UNLIKE YOU, I DID know that it came in TWO flavors.
You can't quote me claiming or presuming or "acknowledging"
otherwise. All you can do is insult people by LYING about their
positions, WITHOUT quoting them. And *I'm* the one who takes
glee in causing flame wars?
You just need to go to hell and stay there, asshole.
G. Frege
"I. Axiom of Extent.
For each x and each y it is true that x = y if and only if
for each z, z e x when and only when z e y."
(John L. Kelley, General Topology)
AxAy(x = y <-> Az(z e x <-> z e y))
"One is tempted to make this the definition of equality,
thus dispensing with one axiom and with all logical
presuppositions about equality. This is perfectly
feasible. However, there would be no unlimited
substitution rule for equality and one would have to
assume as an axiom: If x e z and y = x, then y e z"
AxAyAz(x e z & y = x -> y e z).
>
> ...an axiom not normally found in set theories.
>
Actually, you may find an account in A. A. Fraenkels "Historical
Introduction" to P. Bernays' "Axiomatic Set Theory" (1958).
There he starts with the
"Definition I. If s and t are sets such that, for all x, x e s
implies x e t, s is called a subset of t, in symbols s c t."
In modern notation:
x c y :<-> Az(z e x -> z e y)
And states:
"...equality is defined in ... the following way ...:
Definition II. If s c t and t c s, then s = t; otherwise
s =/= t. That is to say, sets containing the same objects
are equal."
Comment. In modern notation the definition would read:
x = y :<-> x c y & y c x
Or, if we plug in the definition of "c":
x = y :<-> Az(z e x -> z e y) & Az(z e y -> z e x)
Which actually would be equivalent with:
x = y :<-> Az(z e x <-> z e y).
Finally Fraenkel states his
"Axiom I. x e s and x = y imply y e s."
In modern notation:
AxAyAz(x e z & x = y -> y e z).
There you have it.
-----------------------------------------------------
Once more. Fraenkel introduces "identity" (into his system of set
theory) the following way:
Def.: x = y :<-> Az(z e x <-> z e y)
Ax.1: AxAyAz(x e z & x = y -> y e z)
But "=" is not part of his underlying logical framework.
F.
P.S. Indeed, P. Bernays writes (in the main part of the mentioned book):
"2.9 a = b <-> (x)(x e a <-> x e b).
[...] We could have taken, as A. Fraenkel did [1926], the
formula 2.9 as defining equality."
G. Frege
***George Greene*** wrote:
(referring to the text where Kelley introduced
***Morse-Kelley Set Theory***)
>
> K e l l e y doesn't know where he is.
>
George Greene
: The point of this thread is that there are issues associated with usage of
: the identity predicate in set theory,
Not if it is eliminable.
: and, they arise precisely because of the question of
: eliminability of the identity predicate relative to the
: assertion of the axiom of extension.
If it is eliminated then there can't be any questions arising about
it; it is just gone. The questions, if they are going to persist,
are going to have to be questions about the inconveniently necessary
connection between co-extensionality and substitutivity.
: If you look at Lawvere and Schanuel's discussion of toposes in "Conceptual
: Mathematics" you will see that the justifications are given in terms of
: parts as this concept provides for a notion of "one-to-one" for the
: morphisms.
You're being STUPID again.
CATEGORY THEORY IS AN ALTERNATIVE FOUNDATION.
That just has nothing to do with set theory at all.
: It would seem from a comparison of toposes and absoluteness for
: transitive models of set theory that this concept of "one-to-one" is
: fundamental from a mathematical perspective.
"One-to-one mappings" are indeed fundamental. You can't
have an interpretation (of a theory, under the canonical
paradigm) without them.
: It is preserved when an
: identity relation or a part relation is a fundamental relation of the
: language being interpreted.
So what? What does THAT have to do with identity in set theory?
: Countable transitive models depend on the reflection principle,
I don't personally care a whole lot about transitive models,
and as for countable ones, the downward LST does NOT depend
on the reflection principle.
: and therefore, a pre-existing set.
EVERYthing depends on a pre-existing set,
EVEN if it is just a pre-existing set of letters
in an alphabet. That is just NOT important.
What IS important is not presuming any MORE set
theory than you NEED to found FOL. In particular,
you do not need to presume all of ZFC in order to
prove that every consistent theory has a model, nor
do you need to presume that it is reasonable to limit
your candidate models to sets.
: Discussions like Kunen's "people in M" or your own "in the opinion of the
: model" just do not make sense
If they do not make sense to you, then that is purely
because of your personal lack of sense.
: because the underlying lack of rigor transfers
: the problem of infinite regress from the logic to the meta-logic as Aatu
: tried to tell you.
Except that there IS NO underlying lack of
rigor, so both of you are just full of shit.
What's going on in the meta-logic is irrelevant.
EVERYbody has to deal with regress. You do, too.
You just go circular IMMEDIATELY and then
try to ACT like that's not an inadmissibly infinite regress. Jeezus.
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>
> There are TWO flavors of first-order logic, as I KEEP trying to tell you.
> ONE is first-order logic WITHOUT equality. The other is first-order logic
> WITH equality.
>
Right. FOPL with or without identity. :-)
>
> First-order logic WITH equality has TWO MORE INFERENCE RULES
> than first-order logic without equality. They are the ones
> that make '=' a logical symbol AS OPPOSED to something definable.
>
> They are
>
> |- Ax[x=x] (*)
> and x=y |- phi(x)->phi(y) (**)
>
Or so. Right.
This is exactly what Kelley had in mind when he claimed:
"One is tempted to [define] equality [in set theory],
thus dispensing [...] with all logical presuppositions
about equality [i.e. (*) and (**)]. This is perfectly
feasible. However, [then] there would be no unlimited
substitution rule for equality and one would have to
assume as an axiom: If x e z and y = x, then y e z."
>
> The fact that he feels the need to do this seems to imply
> that he is working in FOL withOUT equality.
>
Right, this is just what he said:
"One is tempted to [define] equality [in set theory],
thus dispensing [...] with all logical presuppositions
about equality."
(But actually h e didn't do that.)
>
> Fine.
>
>
> I repeat, there are two flavors. You had never before engaged the
> discussion enough to clarify that substitutivity might fail in
> one flavor. [...]
>
> If you don't understand the difference between FOL without
> equality vs. with, then NO, you DON'T really understand
> first-order logic.
>
Right.
F.
George Greene
: On Fri, 03 Oct 2003 18:50:59 -0500, mitch <mit...@rcnNOSPAM.com> wrote:
:
:
: "I. Axiom of Extent.
:
: For each x and each y it is true that x = y if and only if
: for each z, z e x when and only when z e y."
:
: (John L. Kelley, General Topology)
:
:
: AxAy(x = y <-> Az(z e x <-> z e y))
:
:
: "One is tempted to make this the definition of equality,
: thus dispensing with one axiom and with all logical
: presuppositions about equality. This is perfectly
: feasible. However, there would be no unlimited
: substitution rule for equality and one would have to
: assume as an axiom: If x e z and y = x, then y e z"
:
:
: AxAyAz(x e z & y = x -> y e z).
No, Franz, I'm sorry, you're just wrong.
Mitch did NOT write that.
On Fri, 03 Oct 2003 18:50:59 -0500, mitch <mit...@rcnNOSPAM.com>
ACTUALLY wrote:
: In the appendix of "General Topology" by Kelley, there is an interesting
: footnote:
:
: "One is tempted to make this the definition of equality,
: thus dispensing with one axiom and with all logical
: presuppositions about equality. This is perfectly
: feasible. However, there would be no unlimited
: substituition rule for equality and one would have to
: assume as an axiom: If xez and y=x, then yez"
:
:
: Hopefully, it is clear from this remark that Kelley is referring to the
: axiom of extension. It is in the presentation of this axiom that he
: directs the readers attention to this observation.
:
: Now, formally the new axiom would be given by
:
: AxAyAz((xez & Au(uey <-> uex)) -> yez)
WITHOUT the prior introduction that would've made
it clearer what Kelley was doing. And withOUT the
further note that this is
:
: >
: > ...an axiom not normally found in set theories.
: >
So I don't know what to say.
I will have to guess.
Did he send you a different version from the
one he sent me? Are we reading this in two different
newsgroups? Is there an improved later draft somewhere?
George Greene
: >
I stand by that.
Your presentation is much more helpful than
mitch's but it still clarifies that he was
actually considering "dispensing with" logical
rules about equality, i.e., that he wasn't locked down
to either of FOL with= or FOL without=. Given that he ultimately
didn't dispense with the logical rules, it is clear that
he finally chose to remain in FOL with=,
but given that he actually talked about defining = eliminably,
he was at least allowing for the possibility of going without=.
He gave a good reason, fundamentally the same one as mitch,
for sticking with & not going without. But mitch did NOT quote Kelley's
immediately prior statement of the axiom of extent, and even
though he stole Kelley's other-axiom-for-recovering-substitutivity,
he didn't credit that AS a quote, either.
Why are you chewing mitch's food for him?
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>>
>> ...an axiom not normally found in set theories.
>>
>
> So I don't know what to say.
> I will have to guess.
>
No need to guess. Mitch just screwed it up. Again. As usually.
F.
P.S.
I mean if SOMEONE writes
"we would have to assume as an axiom:
If x e z and y = x, then y e z"
then *I* would translate this with:
AxAyAz(x e z & y = x -> y e z).
(Especially, when the same guy also stated:
"We shall frequently omit "for each x" or "for each y"
in the statement of a theorem or definition. If a variable,
for example "x", occurs and is not preceded by "for each x"
or "for some x" it is understood that "for each x" is to be
prefixed to the theorem or definition in question.")
Im mean, that's just what HE -Kelley- SAID! No? :-o
Hence it's beyond my comprehension how SOMEONE could come up with the
following claim:
"Now, formally the new axiom would be given by
AxAyAz((xez & Au(uey <-> uex)) -> yez)"
Well, OF COURSE we might replace the definiendum in
AxAyAz(x e z & y = x -> y e z).
with its definiens. But WHY the hell would anyone DO THIS when stating
_the axiom related to the *defined* notion_? (Strange!)
Indeed, Fraenkels axiom reads [quote]:
"Axiom I. x e s and x = y imply y e s."
(Where '=' is a defined relation.)
mitch
George Greene wrote:
> mitch <mit...@rcnNOSPAM.com> writes:
>
> : mitch wrote:
> :
> : > And, yes. I really do understand first-order logic.
> : >
> :
> : George, don't really bother replying to this thread. I am tired of your
> : glee over causing flame wars,
>
> YOU are the one who came into a logic forum
> talking about how deficient the usual logic was and how
> you understood it so much better
In "Speech Acts" John Searle writes:
"Sometimes in order to explain adequately a
piece of human behavior we have to suppose
that it was done in accordance with a rule,
even though the agent himself may not be
able to state the rule and may not even be
conscious of the fact that he is acting in accordance
with a rule. The agent's knowing how to do
something may only be adequately explicable
on the hypothesis the he knows (has acquired,
internalized, learned) a rule to the effect that
such and such, even though in an important
sense he may not know that he knows the
rule or that he does what he does in part because
of the rule. Two of the marks of rule-governed
as opposed to merely regular behavior are
that we generally recognize deviations from the
pattern as somehow wrong or defective and
that the rule unlike the past regularity automatically
covers new cases. Confronted with a case he
has never seen before, the agent knows what to
do."
Mathematicians establish the invariance of the structures they study through
the act of definition. Period.
Any nonsense introduced by the beliefs of philosophers that alters that fact is
irrelevant to the foundations of mathematics.
Axioms are not definitions. They do not define predicates.
Language invariance is characterized topologically.
For the record, I am not the one who failed to make a use-case analysis of
mathematical practice before accepting the beliefs propounded by my logic
instructors.
:-)
mitch
>>Marshall H Stone, "The Theory of Representation for Boolean Algebras",
>>TAMS, v40, (1936), pp 37-111 and "Applications of the Theory of Boolean
>>Rings to General Topology" TAMS v41, (1937) pp 385-471.
According to Johnstone, these two papers are a major (as in really really
big) landmark in 20th century mathematics. In addition to the carefully
worked out implicitly categorical concepts of universal solution and
adjoint pair, the very idea of constructing a topological representation
for anything algebraic first appears here. The Zariski topology, in fact,
is Stone's construction on not-necessarily-Boolean rings.
You really are an ass (along with F. for that matter). I have generally made
appropriate restrictions in all of my remarks concerning these matters.
mitch
"G. Frege" wrote:
> On Fri, 03 Oct 2003 18:50:59 -0500, mitch <mit...@rcnNOSPAM.com> wrote:
>
> "I. Axiom of Extent.
>
> For each x and each y it is true that x = y if and only if
> for each z, z e x when and only when z e y."
>
> (John L. Kelley, General Topology)
>
> AxAy(x = y <-> Az(z e x <-> z e y))
>
>
> "One is tempted to make this the definition of equality,
> thus dispensing with one axiom and with all logical
> presuppositions about equality. This is perfectly
> feasible. However, there would be no unlimited
> substitution rule for equality and one would have to
> assume as an axiom: If x e z and y = x, then y e z"
>
>
> AxAyAz(x e z & y = x -> y e z).
>
> >
> > ...an axiom not normally found in set theories.
> >
>
> Actually, you may find an account in A. A. Fraenkels "Historical
> Introduction" to P. Bernays' "Axiomatic Set Theory" (1958).
>
> There he starts with the
>
> "Definition I. If s and t are sets such that, for all x, x e s
> implies x e t, s is called a subset of t, in symbols s c t."
>
> In modern notation:
>
> x c y :<-> Az(z e x -> z e y)
>
Right. Use a trivial syntactic construction to transform a reflexive
logical operation into a reflexive predicate thus obtaining...
>
> And states:
>
> "...equality is defined in ... the following way ...:
>
> Definition II. If s c t and t c s, then s = t; otherwise
> s =/= t. That is to say, sets containing the same objects
> are equal."
>
...a reflexive predicate that is symmetric.
Wow!!! What insight!
>
> Comment. In modern notation the definition would read:
>
> x = y :<-> x c y & y c x
>
> Or, if we plug in the definition of "c":
>
> x = y :<-> Az(z e x -> z e y) & Az(z e y -> z e x)
>
> Which actually would be equivalent with:
>
> x = y :<-> Az(z e x <-> z e y).
>
> Finally Fraenkel states his
>
> "Axiom I. x e s and x = y imply y e s."
>
> In modern notation:
>
> AxAyAz(x e z & x = y -> y e z).
>
> There you have it.
>
> -----------------------------------------------------
>
> Once more. Fraenkel introduces "identity" (into his system of set
> theory) the following way:
>
> Def.: x = y :<-> Az(z e x <-> z e y)
> Ax.1: AxAyAz(x e z & x = y -> y e z)
>
> But "=" is not part of his underlying logical framework.
>
> F.
>
> P.S. Indeed, P. Bernays writes (in the main part of the mentioned book):
>
> "2.9 a = b <-> (x)(x e a <-> x e b).
>
> [...] We could have taken, as A. Fraenkel did [1926], the
> formula 2.9 as defining equality."
But, for all of this... you know that the issue is that of individuation vs.
identity. I have no problem with the logical framework. We have been
through this.
Giving me a lecture on syntactic forms is senseless. Long ago in posts you
did not read, I posted the same relationships dealing with the
Boolean-valued interpretation of these predicates. Do you think I do not
understand the syntactic manipulations?
You just had to get on my case because you could. Well, if it gives you
your jollies...
:-)
mitch
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
"K e l l e y doesn't know where he is."
>
> I stand by that.
>
That's just fine. But imho
a) this is a rather bold claim
b) you are wrong.
>
> Your presentation is much more helpful than
> mitch's but it still clarifies that he was
> actually considering "dispensing with" logical
> rules about equality, i.e., that he wasn't locked down
> to either of FOL with= or FOL without=.
>
I see... Actually, Kelley made that clear at an earlier state of his
presentation.
"Equality is always used in the sense of logical identity; "1 + 1 = 2"
is to mean that "1 + 1" and "2" are names of the same object. Besides
the usual axioms for equality an unrestricted substitution rule is
assumed: in particular the result of changing a theorem by replacing an
object by its equal is again a theorem.
There are two primitive (undefined) constants besides "=" and the other
logical constants. The first of these is "e", which is read "is a member
of" or "belongs to". The second constant is denoted, rather strangely,
"{ · : ···}" and is read "the class of all · such that ···". It is the
classifier."
Note that he made clear several things here, he mentioned
"the usual axioms for equality"
as well as an
"unrestricted substitution rule"
With other words, your rules:
"|- Ax[x=x]
and x=y |- phi(x)->phi(y)"
And he acknowledges that "=" is a
"primitive (undefined) [logical] constant" (!)
i.e. part of our underlying logical framework.
>
> Given that he ultimately didn't dispense with the logical rules,
> it is clear that he finally chose to remain in FOL with=.
>
Right. Remember, it really was just a FOOTNOTE (pointing out a mere
alternative POSSIBILITY to treat the matter).
>
> ... given that he actually talked about defining = eliminably,
> he was at least allowing for the possibility of going without=.
>
Right. (See Fraenkel's approach I mentioned/quoted.)
>
> He gave a good reason, fundamentally [...] for sticking with & not
> going without.
>
Right.
"[It] is perfectly feasible [technically]. However,
there would be no unlimited substitution rule for
equality and one would have to assume as an axiom:
If x e z and y = x, then y e z."
>
> But mitch did NOT quote Kelley's immediately prior statement
> of the axiom of extent [...]
>
Right. [...]
>
> Why are you chewing mitch's food for him?
>
Well, actually I'm interested myself in some of these things. To some
extend.
F.
G. Frege
>
> you know that the issue is that of individuation vs. identity.
>
No I didn't know that. Actually, I tried to correct ONE of your
nonsensical (read: wrong) claims.
Kelley writes (1955):
"[...] one would have to assume as an axiom:
If x e z and y = x, then y e z"
Mitch:
"...an axiom not normally found in set theories."
Actually, we may find in Bernays' "Axiomatic Set Theory" (1958), the
following statement by Fraenkel:
"Axiom I. x e s and x = y imply y e s."
I mean..., at least *I* could find it... :-)
Moreover
> >
> > P. Bernays writes (in the main part of the mentioned book):
> >
> > "2.9 a = b <-> (x)(x e a <-> x e b).
> >
> > [...] We could have taken, as A. Fraenkel did [1926], the
> > formula 2.9 as defining equality."
> >
Hence I GUESS the mentioned axiom could already be found in Fraenkel's
paper [1926].
(Given the fact that Fraenkel is one of the main figures
in ZFC Set Theory, the claim that this might be an "axiom
not normally found in set theories" sounds rather strange.)
>
> Do you think I do not understand the syntactic manipulations?
>
Well, I don't know. And I'm not interested in discussing THIS (OT)
question.
F.
mitch
George Greene wrote:
> You just go circular IMMEDIATELY and then
> try to ACT like that's not an inadmissibly infinite regress. Jeezus.
>
First of all, the circularity in my system is merely apparent. If you had
followed my instructions for interpreting the predicates with diagramatic
representations you would have realized that the parallelism of the syntax is
crucial as a starting point.
Second, even if the two definitions are interpreted separately, it is not a
problematic infinite regress. Infinite regress is problematic when there is an
additional requirement that the definiens may not contain occurrences of the
definiendum. In contrast circular syntax expresses the constancy of
interpretation that would be necessary to any possible notion of
self-consistency.
There are two major objections to the use of circular reference. The first is
irrelevant for predication because circular definition is not the same as
circular reasoning (but, the criterion of well definition for functions and
constant bindings does mean it should be applicable in these cases). The second
has to do with information content. But, a specification of internal
organization that admits intepretation of the predicate as information has
nothing to do with the existential import of instantiating a relation anyhow.
It is true that I choose to go circular immediately. But, at least, I then
encapsulate that circularity That is an honest approach.
In contrast, consider the fact that Hilbert's definition of a line segment is
essentially the axiom of pairing. Using that analogy, the formation of true
pairs (cardinality = 2) corresponds with a line segment. On the other hand, the
use of the axiom of pairing to form singletons essentially describes a
self-referencing loop. How curious it is that when Hodges is discussing the use
of constants in language signatures and homomorphisms between structures he
writes:
"The following compromise works well in
practice. We use the elements a_i as
constants naming themselves."
Please do not lecture me about circularity when it is implicit to the use of
reflexive predicates as foundational predicates. At least, the circularity I
invoke expresses the reflexive nature of identity as a matter of construction
based both on internal constituency and external isolability.
:-)
mitch
George Greene
: On 05 Oct 2003 10:05:12 -0400, George Greene
: <gre...@greeneg-cs.cs.unc.edu> wrote:
:
:
: "K e l l e y doesn't know where he is."
:
: >
: > I stand by that.
: >
: That's just fine. But imho
:
: a) this is a rather bold claim
: b) you are wrong.
You are not far enough inside Kelley's mind to
know that. YOURS is the overly bold claim.
: > Your presentation is much more helpful than
: > mitch's but it still clarifies that he was
: > actually considering "dispensing with" logical
: > rules about equality, i.e., that he wasn't locked down
: > to either of FOL with= or FOL without=.
: >
: I see... Actually, Kelley made that clear at an earlier state of his
: presentation.
:
: "Equality is always used in the sense of logical identity; "1 + 1 = 2"
: is to mean that "1 + 1" and "2" are names of the same object. Besides
: the usual axioms for equality an unrestricted substitution rule is
: assumed: in particular the result of changing a theorem by replacing an
: object by its equal is again a theorem.
My point here is that THIS IS OLD. SO old that by modern
standards he is STILL a little unclear where he is.
"The usual axioms for equality"?? WTF does he MEAN??
Reflexivity, Symmetry, and transitivity?
Those ARE NOT, in modern usage, usual axioms for equality!
What is NOWadays USUAL is what he is calling an UNusual "unrestricted
substitution rule"! Nowadays the LOGIC (if it is FOL=) comes with
2 more INFERENCE RULES defining = and there are NO "axioms" for = !
And what he was calling the usual axioms are THEOREMS, and what
he was alleging to be "in addition to the usual axioms" is ITSELF
one of the two MOST USUAL DEFINING axioms (or rules of inference;
it arguably doesn't matter which; we just prefer to call it a rule
in order to wed it to the logic, to make it less likely that people
will think they might get along without it or use = in a non-
standard way).
: There are two primitive (undefined) constants besides "=" and the other
: logical constants. The first of these is "e", which is read "is a member
: of" or "belongs to". The second constant is denoted, rather strangely,
: "{ · : ···}" and is read "the class of all · such that ···". It is the
: classifier."
:
: Note that he made clear several things here, he mentioned
:
: "the usual axioms for equality"
:
: as well as an
:
: "unrestricted substitution rule"
:
: With other words, your rules:
:
: "|- Ax[x=x]
: and x=y |- phi(x)->phi(y)"
:
: And he acknowledges that "=" is a
:
: "primitive (undefined) [logical] constant" (!)
:
: i.e. part of our underlying logical framework.
:
: >
: > Given that he ultimately didn't dispense with the logical rules,
: > it is clear that he finally chose to remain in FOL with=.
: >
: Right. Remember, it really was just a FOOTNOTE (pointing out a mere
: alternative POSSIBILITY to treat the matter).
Right.
Everything in your presentation is helpful.
But that is because you quoted a whole lot of Kelley.
Mitch just quoted the footnote, so I reacted to what
was presented.
If he wants somebody to react to
the presentation (Kelley's) on its own merits then
he needs to present it carefully and faithfully AS YOU DID.
It would be easy for him to watch & learn & emulate,
IF he felt like it.
George Greene
: But, for all of this... you know that the issue is that of
: individuation vs. identity.
No, you lying asshole, THE issue IS NOT individuation vs.
identity. THE ISSUE is the way you keep attacking my character
and accusing me of saying things I didn't say INSTEAD OF
responding to technical points
:. I have no problem with the logical framework.
Of course not: first you would have to have an understanding of it.
: We have been through this.
No, we HAVE NOT. We have NEVER BEEN ANYwhere where you should
an awareness of the difference between FOL with equality and
without, until today.
: Giving me a lecture on syntactic forms is senseless.
It was MK. You yourself were quoting it, so how
can that be senseless?
: Long ago in posts you did not read, I posted the
: same relationships dealing with the Boolean-valued
: interpretation of these predicates.
Same relationships AS WHAT? These predicates?? WHICH predicates?
Equality is only ONE predicate!
: Do you think I do not understand the syntactic manipulations?
Yes, mitch, we all think that.
And the issue IS NOT individuation vs. identity.
FOL= has an identity paradigm.
ZFC has an axiom of extent.
Neither of these poses ANY problems for "individuation",
whatever the heck you may think that is.
The burden of proof has ALWAYS been on you to EXPLAIN
WHAT IS WRONG with the CANONICAL paradigm.
You have NEVER done this coherently.
All you have done is propose alternatives with NO motivation,
alternatives whose flaws were EASY for us to state for you.
But you still have no statement of the flaws of the canonical
paradigm.
George Greene
: Mathematicians establish the invariance of the structures they study through
: the act of definition. Period.
"Period" my ass. You personally cannot even offer a
coherent definition OF "the act of definition". And
for you to presume to so pontificate in A ROOM FULL OF
MATHEMATICIANS, WHEN YOU ARE NOT ONE, ought to lay to rest
once and for all any debate about just who it is that
takes glee in starting flamewars.
: Any nonsense introduced by the beliefs of philosophers that
: alters that fact is irrelevant to the foundations of
: mathematics.
And that statement is irrelevant to this discussion,
until and unless you can quote some poster in this
newsgroup DOING that.
: Axioms are not definitions. They do not define predicates.
What UTTER bullshit.
Any statement of the form
P(x)<->some wff involving x
is BY DEFINITION a definition of the predicate P.
If it is asserted as an axiom then it IS BOTH an
axiom and a definition.
Even conjunctions of things involving P can also
be viewed as definitions. The whole of ZFC is just
one long definition of epsilon, arguably. If you
choose to argue otherwise then 1) you will not be
able to cite any authorities or any practice
in support of that view, and 2) you will just flaunt
your stupidity.
: Language invariance is characterized topologically.
And all mimsy are the borogoves, you frumious bandersnatch.
mitch
George Greene wrote:
>
> Mitch just quoted the footnote, so I reacted to what
> was presented.
>
> If he wants somebody to react to
> the presentation (Kelley's) on its own merits then
> he needs to present it carefully and faithfully AS YOU DID.
> It would be easy for him to watch & learn & emulate,
> IF he felt like it.
More precisely, you simply reacted to mitch.
The fact of the matter is that I have a history of taking the time to reproduce long
faithful quotes. You do not.
What Kelley has stated is sound and well-thought. I was not arguing with that and
there was no reason to present it. What I would like to see is any evidence that you
understand how you fluctuate between paradigms that include equality and that do not
include equality when you are attacking people in this newsgroup--not me,
personally. Our disputes are of a different character because of your fundamental
personality flaws.
All I asked in making this post originally is that you explain *your* basis in terms
of a reasonable statement about how presuppositions differ when one eliminates
identity. Unfortunately, I have come to expect little--to-nothing of substance from
you and--in keeping with my own fundamental personality flaws--couched that request
sarcastically.
Oh well.
:-)
mitch
George Greene
to restore context.
G. Frege <no_...@aol.com> writes:
: Actually, I tried to correct ONE of your
: nonsensical (read: wrong) claims.
:
: Kelley writes (1955):
:
: "[...] one would have to assume as an axiom:
:
: If x e z and y = x, then y e z"
:
: Mitch:
:
: "...an axiom not normally found in set theories."
:
: Actually, we may find in Bernays' "Axiomatic Set Theory" (1958), the
: following statement by Fraenkel:
:
: "Axiom I. x e s and x = y imply y e s."
:
: I mean..., at least *I* could find it... :-)
That is not the point. Mitch was arguing with ME, not
Bernays or Frankel. I was talking about usual modern
set theories like ZFC and the canonical usual modern
NBG. Both of those have extensionality, and in the context
of FOL *with* equality, extensionality is
Aab[ Ax[xea<->xeb] -> x=y ].
IF you have THAT, then indeed, you will NOT have this
half-backward substitution axiom that mitch was CORRECTLY
calling unusual. Of course, the main reason you will
not have it is that you will have a FULL forward substitution
rule as part of the definition of = in the underlying logic:
since you already have x=y |- phi(x) -> phi(y)
(single-arrow suffices because reflexivity allows you
to derive symmetry of equality which then allows
you to prove the back-arrow), you will AGAIN NOT need
something specific to xes & x=y.
Mitch had basically scored a valid point.
I had insisted that = was eliminable from
first-order ZFC when you were doing it without
equality because the axiom of extent was a valid
definition of =. He was able to support a rebuttal
of that via Kelley (and now FF does likewise via Fraenkel)
by pointing out that if you do that, you risk losing half
of substitutivity and you have to put it back in as an
additional separate axiom.
But I'm still not conceding. I want to see a counter-
model. I am personally bummed by the non-provability of
Ax[xea<->xeb] -> Ax[aex<->bex].
That very problem arguably DOES highlight identity
vs. individuation. If two sets look "downward"-
indiscernible, how are they managing to get "upward"-individuated?
In real/true/correct acutal ZF, the answer of course is
THEY DON'T, but the fact that all the rest of the ammo
of ZFC still doesn't force it is a big disappointment.
George Greene
: George Greene wrote:
:
: > You just go circular IMMEDIATELY and then
: > try to ACT like that's not an inadmissibly infinite regress. Jeezus.
mitch <mit...@rcnNOSPAM.com> writes:
: First of all, the circularity in my system is merely apparent.
Again, basic, 1st-grade stuff.
Circularity is syntactic. If it APPEARS to be circular it is BECAUSE IT IS.
JEEzus.
: If you had followed my instructions for interpreting the
: predicates with diagramatic representations
If what you are saying just can't be said at all syntactically then
one wonders WHY YOU BOTHER. Over here, in sci.LOGIC, when we
state axioms, we DON'T CARE how you interpret them because ANY
old interpretation that makes all of them TRUE is PRECISELY the
class of interpreatations we are trying to talk about.
: you would have realized that the parallelism of the syntax is
: crucial as a starting point.
I.e., that the circularity is absolutely necessary. Well,
that's not surprising.
: Second, even if the two definitions are interpreted separately, it is not a
: problematic infinite regress. Infinite regress is problematic when there is an
: additional requirement that the definiens may not contain occurrences of the
: definiendum.
That is incoherent, mitch. You are flaunting unfamiliarity with the dictionary.
"When there is an additional requirement that"? That "when" would be NEVER.
There is NEVER such a requirement. But circularity is only even MENTIONED
as POSSIBLE when the definiendum recurs on the right. Regress is avoidable
when you can prove that this is some sort of well-founded recursion, but that's
the only USUAL way.
: In contrast circular syntax expresses the constancy of
: interpretation that would be necessary to any possible notion of
: self-consistency.
Any possile notion. Wow. Mitch knows any possible, even among greater
minds yet to be born. How very impressive. And "Self-consistency".
Now there's a redundant redundancy.
: There are two major objections to the use of circular reference.
But you are not competent to articulate either of them so we'll
just cut to the chase.
: It is true that I choose to go circular immediately. But, at least, I then
: encapsulate that circularity
That's commendable.
: That is an honest approach.
Not really, not if what you are going to chide everybody else for
is infinite regress. You still haven't explained how you're
avoiding it. Encapsulating it is nice but it's not sufficient.
:
: In contrast, consider the fact that Hilbert's definition of a line segment is
: essentially the axiom of pairing. Using that analogy, the formation of true
: pairs (cardinality = 2) corresponds with a line segment. On the other hand, the
: use of the axiom of pairing to form singletons essentially describes a
: self-referencing loop.
That's just your personal astrology.
: How curious it is that when Hodges is discussing the use
: of constants in language signatures and homomorphisms between structures he
: writes:
That is not curious, it is just irrelevant. Nobody
here gives a shit about Hodges and you cannot justify
anything by saying that he did it first.
: "The following compromise works well in
: practice. We use the elements a_i as
: constants naming themselves."
That's what WE do. It is every bit as admissible has having
an identity function and it IS NOT REGRESS of ANY kind. You just
go ONE time around that circle AND STOP.
The Herbrand model of any consistent first-order theory does the same
thing (the interpretation interprets every term of the theory as itself).
: Please do not lecture me about circularity when it is implicit to the use of
: reflexive predicates as foundational predicates.
There is nothing circular about a reflexive predicate, DUMBASS.
: At least, the circularity I invoke expresses the reflexive
: nature of identity as a matter of construction
: based both on internal constituency and external isolability.
That's equally true of the Herbrand interpretaion, if it's true
of anything. You are NOT innovating here.
George Greene
: > the presentation (Kelley's) on its own merits then
: > he needs to present it carefully and faithfully AS YOU DID.
: > It would be easy for him to watch & learn & emulate,
: > IF he felt like it.
mitch <mit...@rcnNOSPAM.com> writes:
: More precisely, you simply reacted to mitch.
Fuck you, bitch. You are the biggest liar and asshole in this forum
: The fact of the matter is that I have a history of taking the time to reproduce long
: faithful quotes. You do not.
The fact of the matter is that YOU ARE A DAMN LIAR.
The fact of the matter is that YOU DID NOT reproduce a long faithful
quote of Kelley in this instance, and the far more important point is
that you have A LONG HISTORY OF *NEVER* *QUOTING* *ME* when you attack me!
*I* by contrast AM the one with the long history of quoting people
scrupulously when I disagree with them.
Just keep on circularly EATING SHIT, ASSHOLE.
George Greene
: What Kelley has stated is sound and well-thought.
Of course, but you did not post it.
The situation was greatly confused when Franz DID post
the relevant helpful context with a mis-attribution falsely
claiming that YOU HAD posted it.
: I was not arguing with that and there was no reason to present it.
Dipshit, you WERE ARGUING it EVEN if you were not arguing WITH it
and if you expect ANYBODY TO UNDERSTAND what you are presenting,
THEN YOU DAMN WELL BETTER present it.
: What I would like to see is any evidence that you understand
: how you fluctuate between paradigms that include equality and that do not
: include equality
FUCK you, bitch -- I DO NOT so fluctuate.
: when you are attacking people in this newsgroup--not me, personally.
You cannot name EVEN ONE OTHER PERSON whom I have EVER attacked while
so fluctuating.
: Our disputes are of a different character because of your fundamental
: personality flaws.
That much is true, but nothing has 1 cause, and the proximate
cause HERE is YOUR personality flaws, which are greatly amplified
because you TURN THEM INTO TECHNICAL INTELLECTUAL FLAWS by committing
so many intellectual sins in their name.
: All I asked in making this post originally is that you explain *your* basis in terms
: of a reasonable statement about how presuppositions differ when one eliminates
: identity.
And THAT is A DAMN LIE. Quote YOURSELF or shut the fuck up.
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
> >
> > Actually, Kelley made that clear at an earlier state of his
> > presentation.
> >
> > "Equality is always used in the sense of logical identity; "1 + 1 = 2"
> > is to mean that "1 + 1" and "2" are names of the same object. Besides
> > the usual axioms for equality an unrestricted substitution rule is
> > assumed: in particular the result of changing a theorem by replacing an
> > object by its equal is again a theorem.
> >
> My point here is that THIS IS OLD.
>
Agree.
>
> SO old that by modern standards he is STILL a little unclear where he is.
>
Actually, he is using a rather sloppy language. Agree with you. :-)
>
> "The usual axioms for equality"?? WTF does he MEAN?
>
Probably one would have to begin at the beginning, when talking about
Kelley's Appendix in "General Topology".
----------------------------------------------------------------------
Appendix
Elementary Set Theory
This appendix is devoted to elementary set theory. The ordinal and
cardinal numbers are constructed and the most commonly used theorems are
proved. The non-negative integers are defined and Peano's postulates are
proved as theorems.
A working knowledge of elementary logic is assumed, but acquaintance
with formal logic is not essential. However, an understanding of the
nature of a mathematical system (in the technical sense) helps to
clarify and motivate some of the discussion. Tarski's excellent
exposition [2] describes such systems very lucidly and is particularly
recommended for general background.
This presentation of set theory is arranged so that it may be translated
without difficulty into a completely formal language*). In order to
facilitate either formal or informal treatment the introductory material
is split into two sections, the second of which is essentially a precise
restatement of part of the first. It may be omitted without loss of
continuity.
The system of axioms adopted is a variant of systems of Skolem and of
A. P. Morse and owes much to the Hilbert-Bernays-von Neumann system as
formulated by Gödel. The formulation used here is designed to give
quickly and naturally a foundation for mathematics which is free from
the more obvious paradoxes.
For this reason a finite axiom system is abandoned and the development
is based on eight axioms and one axiom scheme (that is, all statements
of a certain prescribed form are accepted as axioms). [...]
-----
*) That is, it is possible to write the theorems in terms of logical
constants, logical variables, and the constants of the system, and the
proofs may be derived from the axioms by means of rules of inference. Of
course, a foundation in formal logic is necessary for this sort of
development. I have used (essentially) Quine's meta-axioms for logic [1]
in making this kind of presentation for a course.
----------------------------------------------------------------------
References:
[1] W.V.O. Quine, Mathematical Logic, 2nd Ed., Cambridge (USA), 1951.
[2] A. Tarski, Introduction to Logic, 2nd Ed., New York, 1946.
>
> Reflexivity, Symmetry, and transitivity? Those ARE NOT, in modern usage,
> usual axioms for equality!
>
Right. Actually, IMHO he is referring to the two axioms/rules you
mentioned. (I _guess_, he had Quine's "Mathematical Logic" in mind,
when talking about "the usual axioms for equality".)
>
> [...] Nowadays the LOGIC (if it is FOL=) comes with 2 more INFERENCE RULES
> defining '=' and there are NO "axioms" for '='!
>
No, _not in general_. Actually, this just depends on the very "form" of
the formal system you adopt: axiomatic form, or ND style. (Though even
if ND style is rather popular these days there are (still) many _modern_
presentations still adopting an axiomatic approach.)
*For example* in "A Problem Course in Mathematical Logic" by Stefan
Bilaniuk (Version 1.6, 2003) you will find the two AXIOM SCHEMAS:
A7: x = x
A8: (x = y -> (A -> B)), if A is atomic and B is obtained from
A by replacing some occurrences (possibly
all or none) of x in A by y.
Source:
http://euclid.trentu.ca/math/sb/pcml/welcome.html
(Of course, it may very well be the case that your favorite standard
textbooks ALL adopt an ND approach. I don't know.)
Hence, probably we BOTH (?) might agree in claiming:
Nowadays FOPL with identity usually comes
with 2 more INFERENCE RULES concerning '=',
and [then] there are NO "axioms" for '='.
F.
George Greene
: > usual axioms for equality!
G. Frege <no_...@aol.com> writes:
: Right. Actually, IMHO he is referring to the two axioms/rules you
: mentioned. (I _guess_, he had Quine's "Mathematical Logic" in mind,
: when talking about "the usual axioms for equality".)
Well, no I don't think he could've meant those; the whole point
was he was doing this AS AN ALTERNATIVE to those; he wouldn't've
NEEDED *these* if he had *those*.
: > [...] Nowadays the LOGIC (if it is FOL=) comes with 2 more INFERENCE RULES
: > defining '=' and there are NO "axioms" for '='!
: >
: No, _not in general_. Actually, this just depends on the very "form" of
: the formal system you adopt: axiomatic form, or ND style. (Though even
: if ND style is rather popular these days there are (still) many _modern_
: presentations still adopting an axiomatic approach.)
:
: *For example* in "A Problem Course in Mathematical Logic" by Stefan
: Bilaniuk (Version 1.6, 2003) you will find the two AXIOM SCHEMAS:
:
: A7: x = x
: A8: (x = y -> (A -> B)), if A is atomic and B is obtained from
: A by replacing some occurrences (possibly
: all or none) of x in A by y.
:
: Source:
: http://euclid.trentu.ca/math/sb/pcml/welcome.html
Sure, but phrasing these as axiom schemata implies
that they are specific to that axiom set. In fact,
if you are using FOL with equality, these "axioms"
are NECESSARY components of EVERY axiom-set involving
=; they are axioms A-1 and A0 for EVERY axiom-set.
That is why it makes more sense to call them rules of
inference. You have not clarified in this treatment
what A1-A6 are ABOUT (what is this axiom-set FOR)?
My point is that anything that is general about the logic,
applying to ALL axiomatic reasoning in the logic, under/from
ALL axiom sets, is NOT properly called an axiom.
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>
> I don't want Franz to get mad at me but it is important
> to restore context.
>
I always appreciate your OT statements! (If only... YAH KNOW! :-)
And, BTW, anyone (except mitch, of course) knows that you have a rather
profound understanding of t h i s very topic (the role of "identity" in
FOPL and/or some set theory, etc.).
>>
>> Actually, I tried to correct ONE of your
>> nonsensical (read: wrong) claims.
>>
>> Kelley writes (1955):
>>
>> "[...] one would have to assume as an axiom:
>>
>> If x e z and y = x, then y e z"
>>
>> Mitch:
>>
>> "...an axiom not normally found in set theories."
>>
>> Actually, we may find in Bernays' "Axiomatic Set Theory" (1958), the
>> following statement by Fraenkel:
>>
>> "Axiom I. x e s and x = y imply y e s."
>>
>> I mean..., at least *I* could find it... :-)
>>
>
> That is not the point. Mitch was arguing with ME, not
> Bernays or Fraenkel. I was talking about usual modern
> set theories like ZFC and the canonical usual modern
> NBG. Both of those have extensionality, and in the context
> of FOL *with* equality, extensionality is
> Aab[ Ax[xea<->xeb] -> x=y ].
>
Right.
>
> IF you have THAT, then indeed, you will NOT have this
> half-backward substitution axiom that mitch was CORRECTLY
> calling unusual.
>
Right.
>
> Of course, the main reason you will
> not have it is that you will have a FULL forward substitution
> rule as part of the definition of = in the underlying logic:
> since you already have x=y |- phi(x) -> phi(y)
>
Right. Right. Right. (I really hope MITCH is reading this :-)
>
> (single-arrow suffices because reflexivity allows you
> to derive symmetry of equality which then allows
> you to prove the back-arrow), you will AGAIN NOT need
> something specific to x e s & x = y.
>
Right.
>
> Mitch had basically scored a valid point.
>
Well... If YOU say so... (I guess I have to accept it.)
>
> I had insisted that = was eliminable from
> first-order ZFC when you were doing it without
> equality because the axiom of extent was a valid
> definition of =.
>
Right. We all KNOW that. (I mean we just have to add an additional
axiom, but that is well known. And *I* am sure YOU knew that too. Or
would have remembered when considering this approach in more detail.)
>
> He was able to support a rebuttal
> of that via Kelley (and now FF does likewise via Fraenkel)
> by pointing out that if you do that, you risk losing half
> of substitutivity and you have to put it back in as an
> additional separate axiom.
>
Right. This is the usual way to deal with it (in this case).
>
> But I'm still not conceding.
>
Ah?
>
> I want to see a countermodel.
>
I see. (On the other hand, a _proof theoretic_ argument would do too, I
guess - if applicable. Right?)
>
> I am personally bummed by the non-provability of
> Ax[xea<->xeb] -> Ax[aex<->bex].
>
Well, all I could do FOR THE MOMENT would be quoting more *relevant*
material..., but I guess that ultimately could be considered as a mere
appeal to authority. :-(
F.
mitch
George Greene wrote:
> I don't want Franz to get mad at me but it is important
> to restore context.
>
I think he said he had a slight interest in the issue as well.
>
> But I'm still not conceding.
Nor would I expect that.
The issue exists. And, I have been asking for help in understanding it for
more years than I care to think.
For my part, I wrote my own formalization so that I had some representation
of the question. I knew it was not a usual formulation of first-order
logic, and, with what limited means available to me, I formulated a
rationale and found a philosophical grounding in the Kantian distinction
between synthetic and analytic.
For whatever that is or is not worth, that is what a competent
mathematician/logician is supposed to do. I truly am sorry for the enmity
that has arisen between us.
> I want to see a counter-
> model. I am personally bummed by the non-provability of
> Ax[xea<->xeb] -> Ax[aex<->bex].
> That very problem arguably DOES highlight identity
> vs. individuation. If two sets look "downward"-
> indiscernible, how are they managing to get "upward"-individuated?
> In real/true/correct acutal ZF, the answer of course is
> THEY DON'T, but the fact that all the rest of the ammo
> of ZFC still doesn't force it is a big disappointment.
I have tried to avoid saying that the received paradigm is fundamentally
wrong. I am certain it has been implicit. I am certain that I said it
when angry as in this very thread. But, that has more to do with temper
than temperament and the fact that it was necessary to argue from within
the box that I was trying to distance myself from. I noted before that
when I formulated my sentences, I tried to be as careful as possible about
introducing conflicts with mathematics.
And, in fact, when faced with choosing a notion of identity within my
system, I actually had a choice between
Ax[xea<->xeb]
and
Ax[aex<->bex]
My mathematical instincts made me choose what I refer to as "topological
separation of points."
In any case, as has been made quite clear, my intuitions are worthless
without some way to direct them to a relevant conclusion. I have ideas
along these lines, but now that my question is at least acknowledged,
perhaps it is better to listen and offer feedback when asked.
:-)
mitch
G. Frege
>
> I always appreciate your OT statements! (If only... YAH KNOW! :-)
>
Ohhh...
Of course 'OT' meant "ON TOPIC"
in this context. (Sorry.)
F.
George Greene
: : If you look at Lawvere and Schanuel's discussion of toposes in "Conceptual
: : Mathematics" you will see that the justifications are given in terms of
: : parts as this concept provides for a notion of "one-to-one" for the
: : morphisms.
: : transitive models of set theory that this concept of "one-to-one" is
: : fundamental from a mathematical perspective.
I haven't noticed any whole books about topoi on your reading list.
But if you want to read something on dueling foundational perspectives
by people who actually know what they're talking about (including
one message from Lawvere himself on Mar.17 1996) then read this:
http://www.mta.ca/~cat-dist/catlist/1999/set-memb-func-comp
A lot shorter and far more helpful than "Conceptual Mathematics",
for which you probably don't have the background anyway.
mitch
"G. Frege" wrote:
> Right. Right. Right. (I really hope MITCH is reading this :-)
>
I did read the whole post, although I snipped much of it in my response.
Thanks for the encouragement.
:-)
mitch
mitch
George Greene wrote:
>
> http://www.mta.ca/~cat-dist/catlist/1999/set-memb-func-comp
>
> A lot shorter and far more helpful than "Conceptual Mathematics",
> for which you probably don't have the background anyway.
Thanks for the link.
I have an undergraduate degree in Pure Mathematics from the University of Chicago.
Unfortunately, I became ill just when I applied to graduate programs. I had been
accepted to a number of top schools (Princeton, Berkeley, Harvard, Yale, MIT) but
chose to attend the University of Illinois because my health was in doubt.
Champaign was close to my family in case something happened.
I was unable to complete a graduate program. I have less than a year of graduate
school.
I scored 790 on the math SAT when entering college. I sort of forgot how to do
calculus by the time I applied for graduate school (I could not afford the
University of Chicago and went part-time for a number of years). So, I chose not to
answer 50% of the math GRE. I still placed in a percentile above 85.
I actually can and do work with conventional approaches quite adeptly. However,
these foundational issues do create difficulties for me with which other students of
mathematics do not have to worry about.
You are correct, however, in the sense that I do not have the mathematical,
philosophical, and logical background necessary to ask the questions that I have.
And, the questions that I have mangle contexts so completely for me that I present
as being incoherent.
:-)
mitch
George Greene
: And, in fact, when faced with choosing a notion of identity within my
: system, I actually had a choice between
:
:
: and
:
: Ax[aex<->bex] (looking up&out)
But I don't understand why you were faced with this choice.
The received paradigm never had to make this choice: it just
affirms BOTH.
Because I was trained in the received paradigm,
I personally was surprised that the outer version was
not a consequence of the inner one (if two things have
the same parts arranged in the same structure then they
look identical). What the outer constraint does is outlaw
clones/twins, basically; it reaffirms the identity of indiscernibles.
: My mathematical instincts made me choose what I refer to as "topological
: separation of points."
That is a peg in search of a hole, unless you are clarifying that
you are in FOL with equality as opposed to without. The elimination
of identity dodge arguably only arises in the case without. In that
case, the elimination takes 1 more axiom than I thought but I still
insist it is eliminable; you still have an axiom of extent, it just
looks like Ax[xea<->xeb] -> Ax[aex<->bex]
i.e., since = has been eliminated, co-extensionality now implies,
INSTEAD of =, the one thing you most needed = FOR, namely,
substitutivity.
But if you are in FOL with equality, then = is already real
and what you have to decide is what sort of part-relationships
or topological relationships will force/imply equality.
In FOL *with* equality, we have Ax[xea<->xeb] -> a=b.
What you need is [ something topological ] -> a=b,
possibly coupled with something implying ~a=b in other
circumstances.
George Greene
mitch <mit...@rcnNOSPAM.com> writes:
: George Greene wrote:
:
: >
: > http://www.mta.ca/~cat-dist/catlist/1999/set-memb-func-comp
: >
: > A lot shorter and far more helpful than "Conceptual Mathematics",
: > for which you probably don't have the background anyway.
:
: Thanks for the link.
:
: I have an undergraduate degree in Pure Mathematics from the University of Chicago.
Did it involve a lot of category theory?
: Unfortunately, I became ill just when I applied to graduate programs. I had been
: accepted to a number of top schools (Princeton, Berkeley, Harvard, Yale, MIT) but
: chose to attend the University of Illinois because my health was in doubt.
: Champaign was close to my family in case something happened.
Well, that is a damn shame. I feel at this point I should just
make a humanitarian exception. I was admitted to Stanford and MIT
as an undergrad but did badly at Stanford and did not get into their
Ph.D. program. I did get into their M.S. program but I decided to
do my Ph.D. at my home-state university.
: I was unable to complete a graduate program. I have less than a year of graduate
: school.
I am now in my 8th year of graduate school (I couldn't get them to un-count
the 3 years I was working full-time for Lucent during the internet boom) but
I may also yet prove unable to complete, so be grateful that you will have
the 1 thing that I will not: an excuse!
: I scored 790 on the math SAT when entering college.
Me too.
: I sort of forgot how to do
: calculus by the time I applied for graduate school (I could not afford the
: University of Chicago and went part-time for a number of years).
Whether my family could or couldn't afford Stanford was hotly debated.
The Stanford financial aid office gave them just enough aid to make the
question complicated. I also worked a lot while I was in school but
it was nothing compared to the tuition; it was just pocket money.
: So, I chose not to
: answer 50% of the math GRE. I still placed in a percentile above 85.
I had been out of school for TEN years when I took the Comp.Sci. GRE.
I scored 95%ile but that was not high enough to overcome my GPA.
I was bitter because I took the position that Stanford's non-
having of a B.S. in Comp.Sci (I had to get a B.A. in Philosophy, in
a special program that subsequently BECAME the B.S. in symbolic systems)
and the way they separated student computer staff from the academic
department had a lot to do with my underachievement.
: You are correct, however, in the sense that I do not have the mathematical,
: philosophical, and logical background necessary to ask the questions that I have.
: And, the questions that I have mangle contexts so completely for me that I present
: as being incoherent.
Honestly, mitch, that is NOT the problem.
The problem IS that you paraphrase too much and quote too little.
We could stop fighting tomorrow if you would just make it your
law to quote something accurately (instead of paraphrasing it and
distorting it) before you disagree with it (if it's someone else
in the group), and to do likewise when you agree with it (and are
presenting it as authoritative). It might also help if you didn't let
on in advance how much you agree with the authority. If the authority
has done something outmoded or unclear then there is certainly
no reason why YOU should suffer for it.
mitch
George Greene wrote:
> mitch <mit...@rcnNOSPAM.com> writes:
> : And, in fact, when faced with choosing a notion of identity within my
> : system, I actually had a choice between
> :
> : Ax[xea<->xeb] (looking down&in)
> :
> : and
> :
> : Ax[aex<->bex] (looking up&out)
>
> But I don't understand why you were faced with this choice.
> The received paradigm never had to make this choice: it just
> affirms BOTH.
>
Irrelevant Background:
I told you once before that my first logic class was in a philosophy
department. I accepted extensional models but reserved my opinion about the
membership predicate because of its metalinguistic (?) role in specifying the
interpretations. I truly expected something completely rigorous when I started
studying mathematics. I did not get what I expected.
Somewhat More Relevant Background:
When I was left to my own devices (after I could no longer attend school), I
began searching for a sentence that could qualify syntactically as a definition
for membership in terms of itself since I could think of no other way to
satisfy *my* sense (wrong or right, I was unaware of the admonitions against at
the time) of what was meant by a foundation (for *model* theory). I used Venn
diagrams and obtained a sentence almost as unconvincing as the one I posted to
interpret Kelley's remark.
It was not that it wasn't a good formulation (as is Kelley's... or whomever did
it first). It was that there was nothing I could grasp intrinsically about
membership to "justify" the sentence as an axiom.
On the other hand, the *process* of formulating it involved the "dot"/"circle"
distinction in the Venn diagrams. Slowly, I came to accept the need for both
predicates; I found a circular syntax (self-defining) for the proper subset
relation; and, then, I rewrote the circular syntax for the membership
"definition" with its semantic dependency (hence, morphemic rather than
self-defining) on the proper subset relation.
Suddenly, I was faced with a language having two predicates different from
equality.
Now I applied a variation of the received paradigm to two fundamental
predicates to obtain
(sorry about the longhand version-it was the fastest cut & paste)
for all a for all b( a equiv b iff (
for all c ( a proper_part c iff b proper_part c )
and
for all c ( c proper_part a iff c proper_part b )
and
for all c ( a in c iff b in c )
and
for all c ( c in a iff c in b ) )
The obvious strategy is to make all of the relevant subformulas logically
equivalent to one another. That is where the choice arises.
>
> Because I was trained in the received paradigm,
> I personally was surprised that the outer version was
> not a consequence of the inner one (if two things have
> the same parts arranged in the same structure then they
> look identical). What the outer constraint does is outlaw
> clones/twins, basically; it reaffirms the identity of indiscernibles.
Right. This is normally handled by the use of inclusive disjunction in the
axiom of pairing.
But, my approach deals with the question of indiscernibility prior to the
question of existence of pairs.
It should be noted that pairing is a fundamental concept in all of this. As
soon as Andreas Blass noticed that my axioms restricted to exactly one
singleton, I immediately began investigating interval logic for the ordinals
since this is related to equivalence classes for models of set theory.
>
>
> : My mathematical instincts made me choose what I refer to as "topological
> : separation of points."
>
> That is a peg in search of a hole,
Right.
I needed to rationalize an entirely different approach just to ask questions
without being dismissed.
> unless you are clarifying that
> you are in FOL with equality as opposed to without. The elimination
> of identity dodge arguably only arises in the case without.
Right.
> In that
> case, the elimination takes 1 more axiom than I thought but I still
> insist it is eliminable; you still have an axiom of extent, it just
> looks like Ax[xea<->xeb] -> Ax[aex<->bex]
> i.e., since = has been eliminated, co-extensionality now implies,
> INSTEAD of =, the one thing you most needed = FOR, namely,
> substitutivity.
>
Right.
What aspect in the development of set theory justifies our understanding of
substitutivity in terms of coextensionality?
I mean, right now you are manipulating syntactic forms into the correct
positions to have the same theory. And, in terms of symbol manipluation and
formalism, I have no problem with the logic.
But, what does this say about the usage of identity in mathematics? I mean,
that is supposed to be a fundamental application of set theory. This is why I
knew I had to isolate what I was doing from standard paradigms.
The introduction of axiom systems is supposed to coincide with justifications
for those axioms. Is it not? Why should anyone accept them otherwise?
>
> But if you are in FOL with equality, then = is already real
> and what you have to decide is what sort of part-relationships
> or topological relationships will force/imply equality.
> In FOL *with* equality, we have Ax[xea<->xeb] -> a=b.
> What you need is [ something topological ] -> a=b,
> possibly coupled with something implying ~a=b in other
> circumstances.
Right.
I did/am doing that. But, of course, in trying to figure it out, I have broken
all of the rules and alienated myself from everyone else.
"Humpty dumpty sat on a wall..."
What can I say? I did not mean to.
:-)
mitch
G. Frege
>
> And, in fact, when faced with choosing a notion of identity within my
> system, I actually had a choice between
>
> Ax[x e a <-> x e b]
>
> and
>
> Ax[a e x <-> b e x]
>
P. Bernays:
" a = b <-> (x)(x e a <-> x e b).
[...] We could have taken, as A. Fraenkel did [1926], [this]
formula as defining equality. [...] There would also be the
possibility of defining equality by the equivalence
a = b <-> (x)(a e x <-> b e x)
what would be in the line of the definition given in Principia
Mathematica."
(P. Bernays, Axiomatic set Theory, p. 53)
F.
"There's nothing new under the sun."
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>>
>> And, in fact, when faced with choosing a notion of identity within my
>> system, I actually had a choice between
>>
>> Ax[x e a <-> x e b]
>>
>> and
>>
>> Ax[a e x <-> b e x]
>>
George, the following might be of interest for you?
Actually, I have abbreviated Fraenkel's exposition slightly. In the
following you will find a full[er] quote:
"Definition I. If s and t are sets such that, for all x, x e s
implies x e t, s is called a subset of t, in symbols s c t.
[...] In accordance with earlier remarks, equality is defined
in either of the following ways.
Definition IIa. If, for all x, s e x implies t e x and
conversely, s equals t (s = t); the negation is s =/= t
(s differs from t). That is to say, sets are equal if
contained in the same objects (sets).
Definition IIb. If s c t and t c s, then s = t; otherwise
s =/= t. That is to say, sets containing the same objects
are equal."
Equality is a reflexive, symmetrical and transitive relation.
[...] Equality is substitutive with regard to the second
argument of e, i.e. from x e s and s = t it follows that x e t.
[ Footnote: This is evident in view of IIb; for the proof in
view of IIa, cf. A. Robinso(h)n [1939], footnote 4. ] But IIa
does not yield extensionality nor does IIb yield substitutivity
regarding the first argument; hence we supplement IIa and IIb
respectively with the axioms
Axiom Ia. s c t and t c s imply s = t.
Axiom Ib. x e s and x = y imply y e s.
It makes no difference whether we adopt Definition IIa and
Axiom Ia, or IIb and Ib. Hence we shall simply speak of
_the Definition (II) of Equality_ and the _Axiom (I) of
Extensionality_.
(A. A. Fraenkel in P. Bernays, "Axiomatix Set Theory", p. 8)
F.
John
A different candidate for such a definition would be:
"a = b" means "(x)[(x e a <-> x e b) & (set a & set b)]"
Of course, if they did not ignore this unsanctified intruder, the
Boyz would trot out their usual *ad verecundiam* arguments favouring
the definition under whose auspices they transact their piffling
academic business.
--John
G. Frege
Dear mitch,
probably the following remarks by A. A. Fraenkel might be of some help
concerning the topic in quest.
" Prior to a systematic exposition, we start with some informal
remarks to motivate the method adopted afterwards.
Within a certain non-empty domain of objects we take, as the
only primitive relation of our axiomatic system Z, the membership
relation e [...]. If x and y denote any objects of the domain,
the statement x e y shall either hold true or not. While those
parts of logic that are necessary for Z, in particular the rules of
inference and quantification with respect to thing-variables, are
assumed to be pre-established, the relation of _equality_ should be
treated explicitly. Here the following attitudes are possible.
1) Equality in its _logical meaning as identity_ Zermelo adopts
this attitude by calling x and y equal "if they denote the same
thing (object)". When the objects are sets he in addition rests on
an axiom of extensionality [...] which states that a set is
determined by its elements.
Thus Zermelo's axiom differs intrinsically from the Axiom of
Extensionality as expressed below (p. 8), which refers to _all_ objects
of the domain.
2) Equality as a (second) _primitive relation_ within Z. Then
the usual properties of an equivalence (equality) relation must
be guaranteed axiomatically, in particular substitutivity with
regard to e in the two-fold sense: of extensionality as above, and
of equal objects being elements of the same sets.
3) Equality as a _mathematically defined relation_. We may define
x = y either by "if every set that contains x contains also y and
vice versa", or by "if x and y contain the same elements". The
second way is possible only if, as assumed in the following, every
object is a set (including the null-set). In the former case, exten-
sionality must be postulated axiomatically; in the latter an axiom
has to guarantee the former property.
In this part we adopt method 3), which seems superior to 2)
insofar as a single primitive relation only occurs in the system,
and to 1) since the system is constructed upon a weaker basic
discipline. It makes no essential difference which of the two
definitions of equality is chosen, provided we take a suitable
decision about the existence of _individuals_ (called _Urelemente_ in
Zermelo [1930]), i.e. of objects which contains no element. [...]"
(A. A. Fraenkel in P. Bernays, "Axiomatic Set Theory", pp. 6-7)
"We know outline the system Z, which is not empty and whose only
primitive relation is the dyadic relation e of membership whose
arguments are sets.
Definition I. If s and t are sets such that, for all x, x e s
implies x e t, s is called a subset of t, in symbols s c t.
[...] In accordance with earlier remarks, _equality_ is defined
in either of the following ways.
Definition IIa. If, for all x, s e x implies t e x and
conversely, s equals t (s = t); the negation is s =/= t
(s differs from t). That is to say, sets are equal if
contained in the same objects (sets).
Definition IIb. If s c t and t c s, then s = t; otherwise
s =/= t. That is to say, sets containing the same objects
are equal."
Equality is a reflexive, symmetrical and transitive relation.
The definitions are somehow peculiar to Z; in fact, in the system
[mentioned below, NBG] not every object can become an element of
another object, as against IIa, while in Zermelo's own system
there may exist different objects without elements, as against IIb.
Equality is substitutive with regard to the second
argument of e, i.e. from x e s and s = t it follows that x e t.
[ Footnote: This is evident in view of IIb; for the proof in
view of IIa, cf. A. Robinso(h)n [1939], footnote 4. ] But IIa
does not yield extensionality nor does IIb yield substitutivity
regarding the first argument; hence we supplement IIa and IIb
respectively with the axioms
Axiom Ia. s c t and t c s imply s = t.
Axiom Ib. x e s and x = y imply y e s.
It makes no difference whether we adopt Definition IIa and
Axiom Ia, or IIb and Ib. Hence we shall simply speak of
_the Definition (II) of Equality_ and the _Axiom (I) of
Extensionality_.
(A. A. Fraenkel in P. Bernays, "Axiomatic Set Theory", pp. 7-8)
---------------------------------------------------------------
A short comment: Of course approach 1) mentioned above ("Equality in its
_logical meaning as identity_") is the standard approach these days.
Here '=' is just part of the underlying logical system.
George Greene:
"First-order logic WITH equality has two more inference rules
than first-order logic without equality. They are the ones
that make '=' a logical symbol AS OPPOSED to something
definable. They are
|- Ax[x=x]
and
x=y |- phi(x)->phi(y)."
And of course this is the approach followed by Kelley:
"Equality is always used in the sense of logical identity;
"1 + 1 = 2" is to mean that "1 + 1" and "2" are names of the
same object. Besides the usual axioms for equality an
unrestricted substitution rule is assumed: in particular the
result of changing a theorem by replacing an object by its
equal is again a theorem.
There are two primitive (undefined) constants besides "=" and
the other logical constants. The first of these is "e", which
is read "is a member of" or "belongs to". The second constant
is denoted, rather strangely, "{ · : ···}" and is read "the
class of all · such that ···". It is the _classifier_."
Though Kelley also _mentions_ the third approach [in a footnote]:
"One is tempted to make (*) the definition of equality, thus
dispensing with one axiom and with all logical presuppositions
about equality. This is perfectly feasible. However, there
would be no unlimited substitution rule for equality and one
would have to assume as an axiom: If x e z and y = x, then
y e z."
Where (*) is Kelley's _Axiom of Extent_:
AxAy(x = y <-> Ay(z e x <-> z e y).
This possibility is also mentioned by Bernays:
"2.9 a = b <-> (x)(x e a <-> x e b).
[...] We could have taken, as A. Fraenkel did [1926], the
formula 2.9 as defining equality."
But he adds:
"We do not introduce here equality by an explicit definition,
because we want to suggest the interpretation of equality as
individual identity, whereas by 2.9 (...) taken as definition,
equality is introduced only as an equivalence relation. Besides
by employing an explicit definition of equality the axioms
which include equality become more complicate, if expressed
with the primitive symbols."
(P. Bernays, Axiomatic set Theory, p. 53)
Actually, Bernays adopted approach 2) mentioned above in Fraenkel's
quote. (!)
------------------------------------
F.
Mattias Wikstr?m
> In the appendix of "General Topology" by Kelley, there is an interesting
> footnote:
>
> "One is tempted to make this the definition of equality,
> thus dispensing with one axiom and with all logical
> presuppositions about equality. This is perfectly
> feasible. However, there would be no unlimited
> assume as an axiom: If xez and y=x, then yez"
There certainly is a substitution rule for equality. Formulating
correct substitution rules is tricky, so I will not attempt it, but it
seems to me that a substitution rule will be like an ordinary
substitution rule except that the formula in which one substitutes and
the term one substitutes for terms in the formula have to be
set-theoretic, where by set-theoretic I mean that predicates,
functions, and constants appearing in them should be definable in
terms of the membership predicate.
Moreover, the extra axiom is something that can be proved in standard
ZF, so in that sence it is no new assumption.
In summary, it is possible to give an axiom system equivalent to
standard ZF in which equality is never mentioned -- there is no catch.
If someone asks "What do people mean by equality between sets?," we
say that the following things are equivalent:
1. x=y
2. The members of x are the same as the members of y.
3. x and y are members of the same things.
>
>
> Hopefully, it is clear from this remark that Kelley is referring to the
> axiom of extension.
Well, from the quote above it seems Kelley is referring to the
following property:
x=y <-> Az(zex <-> zey)
I think Az(zex <-> zey) -> x=y is what is normally understood by the
axiom of extension.
> It is in the presentation of this axiom that he
> directs the readers attention to this observation.
OK.
>
> Now, formally the new axiom would be given by
>
> AxAyAz((xez & Au(uey <-> uex)) -> yez)
Yes.
>
> So, Mr. Greene, given your continual criticisms of my ideas, I have a
> number of questions.
I will try to give my own answers to the questions intended for George
Greene.
>
> How can eliminability of identity be accomplished in first-order logic
> if the presuppositions of identity that define it are necessarily
> abandoned?
[snip]
I find this question strange; I will do my best to answer it.
First I will try to make it clear from what thing it is that equality
(I assume you mean the same thing by identity and equality) can be
eliminated and in what sence it can be eliminated. When one deals with
equality in first-order logic there are two approaches one may take:
i. Let equality be part of the logic. In this case our logic is
first-order logic with equality.
ii. Let equality be a predicate among the others and add appropriate
axioms (reflexivity, symmetry, transitivity, and congruence). In this
case our logic is first-order logic without equality.
The equality appearing in standard ZF may be interpreted either way.
Now, whichever approach one takes, there is a sence in which equality
can be eliminated from any formula:
For any formula there is an equivalent formula that does not contain
equality and in which the only predicate, function, or constant is the
membership predicate.
Here "any formula" refers to formulas that may contain the membership
predicate, equality, and things definable in terms of theese (if you
add altogether new predicates, the principle no longer holds).
This principle has the consequence that we can "throw away" equality
(in case i. this means that we move from first-order logic with
equality to first-order logic without equality; in case ii. it means
that we throw away a predicate from our collection of predicates,
functions, and constants) without throwing away any truths (because
any truth can be expressed without equality). Thus we can eliminate
equality not just from any formula, but also from our logic/our
collection of predicates, functions, and constants.
Now, let me try to answer your question: "How can eliminability of
identity be accomplished in first-order logic if the presuppositions
of identity that define it are necessarily abandoned?" I would say
that as we throw away equality, we also forget about any properties
equality had. We throw away equality along with its properties. If we
reintroduce equality, it gets exactly the same properties as the old
equality had. I see no problem here.
Maybe you want to change some of the rules of equality, but in that
case what you mean by equality is not what people ordinarily mean by
equality. We may or may not want to explicitly refer to equality when
describing what a set-theoretic universe is -- that is just a matter
of taste. Given a set-theoretic universe we can define what we mean by
two sets (or classes, for that matter) being equal. Indeed there is a
perfectly standard meaning for equality of sets.
Someone with a love for paradoxes could say that equality can be
thrown away if and only if it cannot be thrown away. Equality can be
thrown away if and only if it can be reintroduced. Equality can be
reintroduced if and only if it cannot be thrown away. I hope that
makes sence. ;-)
>
> Given that eliminability of identity requires an axiom not normally
> found in set theories, I would like to know how you justify the axiom
> that you have never explicitly presented while making your many claims?
[snip]
It is to be expected, that as we change our collection of primitive
symbols, we also have to change our axioms. In general it is not
meaningful to compare the axioms of two axiom systems one by one.
Instead, one compares the systems in their entirety. For two axiom
systems S1 and S2, one shows how the primitive symbols of S1 can be
defined in S2 and how the primitive symbols of S2 can be defined in
S1, and with theese definitions one shows that S1 and S2 are
equivalent (or that one is stronger than the other, or that they are
independent).
Mattias
mitch
"G. Frege" wrote:
>
> "There's nothing new under the sun."
I know. Except that I inadvertently stumbled on mereology. The transitive
closure operation satisfies the Kuratowski axioms and those axioms make no
direct reference to a universe as would the definition of a topology. But,
I had no way to motivate a topology given that everyone seemed to be
assuming that one needed sets to define a topology. Mereology changes
that.
And, in contrast to the advocates of mereology, my understanding of the
situation does not deny set theory or classical logic its due. The
question for me at this point is not one of replacing any particular
system, but of understanding how they reconcile with one another. I have
also tried to make analogies with situation theory and possible world
theory because of roles played by a primitive order relation.
Still, I can't get much further without learning "the old" or obtaining the
assistance of those who have more familiarity.
:-)
mitch
mitch
George Greene wrote:
>
> Did it involve a lot of category theory?
>
None. I was made aware of categories by the sections in Hungerford's "Algebra." I read
large portions of Lawvere's "Conceptual Mathematics" late last year. I realize that that
is nowhere near what I need to know.
>
> : Unfortunately, I became ill just when I applied to graduate programs. I had been
> : accepted to a number of top schools (Princeton, Berkeley, Harvard, Yale, MIT) but
> : chose to attend the University of Illinois because my health was in doubt.
> : Champaign was close to my family in case something happened.
>
> Well, that is a damn shame. I feel at this point I should just
> make a humanitarian exception. I was admitted to Stanford and MIT
> as an undergrad but did badly at Stanford and did not get into their
> Ph.D. program. I did get into their M.S. program but I decided to
> do my Ph.D. at my home-state university.
>
Good luck with it.
<snip>
>
> : You are correct, however, in the sense that I do not have the mathematical,
> : philosophical, and logical background necessary to ask the questions that I have.
> : And, the questions that I have mangle contexts so completely for me that I present
> : as being incoherent.
>
> Honestly, mitch, that is NOT the problem.
Actually, it is. My illness makes it that way.
I will, however, attempt to do better when referring to your statements in the future.
How do you run searches to find comments or specific posts? I realize that that is
specific to a newsgroup reader. I am running Netscape 4.77. I don't really expect an
answer on that basis. But, I once asked about something else and was able to figure out
what I needed to do just because they used the feature name.
:-)
mitch
mitch
"G. Frege" wrote:
> Dear mitch,
>
> probably the following remarks by A. A. Fraenkel might be of some help
> concerning the topic in quest.
>
Thanks F. They were great.
One thing to keep in mind is that I made choices that were different from
classical ones for whatever reasons. Now that I have a modern text on
philosophical logic, I have a better idea about why I might have made the
choices I did. For example, epistemic logic is strongly modal (Let's not
forget my Kantian influences now). Thus, it makes sense that my
understanding of completeness is bound with labeling concepts since this can
be used for characterizing completeness in modal logic.
So, my "confusion" leaves me so that I cannot restrict to the classical
paradigm no matter how well I may or may not understand it. On the other
hand, I really see no reason not to investigate possibilities. That is what
I had been doing with the interval logic, for example. Perhaps I am wrong
in thinking this way, though.
Consider this. Suppose you recognize my result as combining mereo-theoretic
principles with set-theoretic principles in a rational way (this is
hypothetical :-). The fact that it results in a system that can only be
extended to an ordinal sequence rather than a full-fledged set theory might
be interpreted as a constraint on models of set-theory that disallow those
that cannot be put in a correspondence with the ordinal sequence. The
rationale here is that it would violate a notion of modal completeness that
depends on an algebra of labels described by an irreflexive transitive
order.
Who knows? Even you recognize the importance of natural language
explications toward establishing relevance. :-) I have had to concentrate
so much effort just to establish the possibility of an issue between
identity and individuation that other avenues of investigation remain
unexplored.
:-)
mitch
Witt
Hi John,
I am not so sure that either your definition "a = b" means "(x)[(x e a
<-> x e b) & (set a & set b)]" or "a = b <-> (x)(a e x <-> b e x)"
will do.
Take an instance of Leibnitz's Law: x=y -> (Fx <-> Fy), as:
x=y -> ~(x e x) <-> ~(y e y).
Since the Russell Class does not exist, x e (x:~(x e x)) <-> y e
{x:~(x e x),
is not equivalent to ~(x e x) <-> ~(y e y).
Given that,(x:~(x e x)) is not a set,
How then do we derive, x=y ->. ~(x e x) <-> ~(y e y)?
I wrote to Quine about this point in Feb 1997, and he agreed that
there is a problem.
"You are right about the gap in "New Foundatiions." Moreover we miss
out not just on identity but on unstratified formulas more widely. I
discovered this in 1938 or 9 cand closed the gap by adding a domain of
ultimate classes, that is, classes not eligible for membership in
classes ... W.V.Quine"
I find that the admission of ultimate classes or of proper classes
does not solve the difficulty. Note: y e {x:~(x e x)} is
contradictory.
Witt
G. Frege
> >
> > " a = b <-> (x)(x e a <-> x e b).
> >
> > [...] We could have taken, as A. Fraenkel did [1926], [this]
> > formula as defining equality. [...] There would also be the
> > possibility of defining equality by the equivalence
> >
> > a = b <-> (x)(a e x <-> b e x)
> >
> > what would be in the line of the definition given in Principia
> > Mathematica."
> >
> > (P. Bernays, Axiomatic set Theory, p. 53)
> >
>
> A different candidate for such a definition would be:
>
> "a = b" means "(x)[(x e a <-> x e b) & (set a & set b)]"
>
Indeed. This way we would define set-equality. Of course set-equality
wouldn't hold if one (or both classes in quest) were proper classes.
Now the funny thing is, in Bernays' version of NBG y o u r definition
and
a = b :<-> (x)(x e a <-> x e b)
would actually be "equivalent" - there wouldn't be _any_ benefit from
introducing the extra clause "& (set a & set b)". :-)
Why? 'cause 'a' and 'b' are _set variables_ in Bernays' system. Moreover
the domain of his system consists of _sets_ only! :-)
Right. That's the reason w h y imho YOU should better consider MK (not
NBG) to be the basis of your system. :-)
F.
George Greene
: Irrelevant Background:
:
: I told you once before that my first logic class was in a philosophy
: department. I accepted extensional models but reserved my opinion about the
: membership predicate because of its metalinguistic (?) role in specifying the
: interpretations.
This is NOT irrelevant!
This issue is DIRECTLY relevant to another argument I am
having with Chris Menzel and Aatu Koskensilta on the subject
of whether models do or don't absolutely HAVE to be sets, by
definition.
In any case, you have made a category/level object/meta
ERROR by doing that. There is NO SUCH THING as "the"
membership predicate. The membership predicate IN THE
OBJECT langauge is ONE predicate. The kind of membership
that you might need in talking about defining and assinging
interpretations is IN THE META-language and no matter HOW
isomorphic or intensionally similar it may be to the membership
predicate being defined in the first-order object--language
of ZFC, IT IS STILL *JUST* A *DIFFERENT* thing. EVEN if
it is an identical copy exactly 1.0 semantic levels up,
it is STILL a DIFFERENT clone from the same template.
George Greene
I just had to re-quote all of this to emphasize sheer gratitude.
G. Frege <no_...@aol.com> writes:
: Dear mitch,
THIS is the kind of background which would've made the whole misunderstanding
between me and mitch impossible. It is EXACTLY what was needed by way
of clarification. I sincerely need to repent of my prior attitude that
you were too much into things old and historical. I was afraid they
would do more harm than good pedagogically, because their misleading
aspects had been corrected/subsumed/superseded by more modern approaches.
But this proves that sometimes, the evolution of the understanding of an
individual questor (mitch in this case) can parallel the historical
evolution of the field, which means that somewhere back there, some
giant was dealing with PRECISELY the issues that are confusing the
newbie. And the beauty of it is that you probably actually ENJOYED
researching and presenting that. The forum is certainly blessed to
have someone around to play that role. Please pardon my naivete in
having originally presumed otherwise.
Just by way of excusing my prior misgivings, though, I would point
out that a modern approach would have a different take on prong 2)
above. In that approach, the equivalence-relation and substitutivity
properties, guaranteed "axiomatically", actually have to be (in modern
parlance) guaranteed even more deeply than that, as part of the
underlying logic. The axioms are by definition defining the particular
theory (in this case set theory). The rules about equality NEED, by
CONTRAST, in modern parlance, to be inference rules INSTEAD OF axioms; the
modern perspective knows it is IMPORTANT to know what pertains to the logic
as OPPOSED to what pertains to particular axiom-sets and the theories that
are their closures under consequence. I know you cited a source from
2003 that wasn't that cut and dried about it, but we are addressing
that in another message.
George Greene
: I will, however, attempt to do better when referring to your statements in the future.
: How do you run searches to find comments or specific posts? I realize that that is
: specific to a newsgroup reader. I am running Netscape 4.77.
If you really feel a need to search back then I would recommend
Google groups but that is not really the issue. If you would just
get in the habit of quoting what you are replying to then everything
else would take care of itself.
Alan Smaill
> I just had to re-quote all of this to emphasize sheer gratitude.
....
> THIS is the kind of background which would've made the whole misunderstanding
> between me and mitch impossible. It is EXACTLY what was needed by way
> of clarification. I sincerely need to repent of my prior attitude that
> you were too much into things old and historical. I was afraid they
> would do more harm than good pedagogically, because their misleading
> aspects had been corrected/subsumed/superseded by more modern approaches.
> But this proves that sometimes, the evolution of the understanding of an
> individual questor (mitch in this case) can parallel the historical
> evolution of the field, which means that somewhere back there, some
> giant was dealing with PRECISELY the issues that are confusing the
> newbie. And the beauty of it is that you probably actually ENJOYED
> researching and presenting that. The forum is certainly blessed to
> have someone around to play that role. Please pardon my naivete in
> having originally presumed otherwise.
Glory halleluia!
there was good faith on both sides all along ....
(occasionally well hidden)
--
Alan Smaill
School of Informatics tel: 44-131-650-2710
University of Edinburgh
John
As I'm unfamiliar with Quine's "New Foundations", and don't
know how set abstracts are introduced and eliminated in
your system--forgive me if you've made this clear and I've
missed it--I'll approach your problem from the standpoint
of my own (perhaps faulty) understanding of how set abstracts
work in C.
In view of the things I mentioned to G. Frege some time back,
I understand {x:Fx} as a set abstract--and "x e {x:Fx}" as
meaning (i):
(i) Ey(y=y & x e y & Az(z e y <-> (z=z & Fz)))
Based on the foregoing, "x e {x: ~(x e x)}" cashes out as (ii):
ii) Ey(y=y & x e y & Az(z e y <-> (z=z & ~(z e z))))
However, granted that every class of non-self-membered sets
is a *proper* class, and that proper classes are not self-
identical, from (ii) there follows (iii).
iii) ~Ey(y=y & x e y & Az(z e y <-> (z=z & ~(z e z))))
But (iii) cashes out as (iv):
iv) ~(x e {x: ~(x e x)})
But x is arbitrary. Hence {x: ~(x e x)} has no members:
v) Ax~(x e {x: ~(x e x)})
Therefore, {x: ~(x e x)} is the empty set (the existence of which in C
is established in news:<70f94e16.02090...@posting.google.com>).
Hmm. In news:<s%G_7.200471$KT.48...@news4.rdc1.on.home.com>,
didn't some guy by the name of Holden say, "The Russell set is
the null set"?
To change the subject, here's the abstract to a paper by
David Hyder, entitled "Foucault, Cavaillès and Husserl
on the Historical Epistemology of the Sciences".
"This paper discusses the origins of two key notions in
Foucault's work up to and including The Archaeology of
Knowledge. The first of these notions is the notion of
"archaeology" itself, a form of historical investigation
of knowledge that is distinguished from the mere history
of ideas in part by its unearthing what Foucault calls
"historical a prioris". Both notions, I argue, are derived
from Husserlian phenomenology. But both are modified by
Foucault in the light of Jean Cavaillès's critique of
Husserl's theory of science. On Husserl's view, we
demand that propositions holding of scientific objects
be intersubjective and invariant, but this demand conflicts
with our immediate experience, which is essentially bound
to a subject's perspective. Thus the mathematical and
physical sciences must utilise formal languages to fix
these truths independently of the thoughts of a particular
subject. This necessary procedure leads to the sedimentation
of these formal systems: we forget their source in the concrete
experiences of individuals, and use them as purely technical
means. The technique of reactivating the intentional acts
in which sedimented formal systems originated is thus, in
Fink's terminology, an archaeological method. Foucault and
Cavaillès retain the general outlines of this archaeology
of the sciences, but they reject its appeal to conscious
acts of meaning, to what Cavaillès calls "the philosophy of
consciousness". I conclude by discussing the implicit
difficulties in the "linguistic transcendentalism" proposed
as an alternative by these French critics of Husserl."
Of particular relevance to the foregoing is how
the Boyz react to those of us who dare contemplate
alternatives to the sedimented formal systems which
constitute the stock-in-trade of the professoriate.
--John
G. Frege
A short comment concerning Kelley's Axiom of Extend
---------------------------------------------------
"Axiom of Extent.
For each x and each y it is true that x = y if and only if
for each z, z e x when and only when z e y."
(John L. Kelley, General Topology, 1955)
Using logical symbols his axiom would read:
AxAy(x = y <-> Az(z e x <-> z e y))
Now G. Greene made a most valuable comment (in a message he sent me):
The usual axiom of extensionality (which needs a -> arrow,
NOT a biconditional) should be STRESSED as meaningful only
in FOPL *with* equality. And the most familiar version,
WITH the biconditional arrow [i.e.]
AxAy(x = y <-> Az(z e x <-> z e y))
should be outlawed from axiom-sets altogether and consigned
to the realm of what it is, namely a DEFINITION that just
introduces an abbreviatory symbol, that does NOT affect
the content of the theory in ANY way (sort of like the
definition of the subset symbol).
I guess, G. Greene has a point here. (Please bear with me...)
In the (rather informal) Introduction of his "Introduction to Axiomatic
Set Theory" (1968) E. J. Lemmon writes:
"But what does = mean between classes? The usual view, which
we shall follow, is that classes v and w are considered
identical if and only if they have exactly the same members.
For example, the classes
{Julius Caesar, 3}
and
{The man killed by Brutus, 4-1}
are identical, since they have exactly the same two
members. They are also identical with the class
{Julius Caesar, 5-2, 6-3, 7-4, 8-5}.
This view of identity means, in effect, that we are
accepting the principle
(8) x = y <-> Az(z e x <-> z e y),
that x is identical with y if and only if anything is a
member of x if and only if it is a member of y. (8)
suggest the possibility of _defining_ identity in terms of
class membership (together with propositional calcu-
lus connectives and the universal quantifier), and this
course is followed in several brands of set theory.
There are both gains and disadvantages in such a course.
Here, again, we make a choice: to take identity as a
primitive notion for what follows, and regard it as part
of our underlying logical framework."
(E. J. Lemmon, Introduction to Axiomatic Set Theory, pp. 10-11)
It's indeed funny to compare this explanation with Kelley's footnote
(referring to his "Axiom of Extend"):
"One is tempted to make this the definition of equality,
thus dispensing with one axiom and with all logical
presuppositions about equality. This is perfectly
feasible. However, there would be no unlimited
substitution rule for equality and one would have to
assume as an axiom: If x e z and y = x, then y e z."
Finally, Lemmon starts with "Chapter I - The General Theory of Classes":
"We are now in a position to introduce the basic
axioms of our formal set theory, and to prove some
elementary theorems. We saw in the Introduction
that we are viewing classes x and y as identical just in
case they have exactly the same members:
(1) x = y <-> Az(z e x <-> z e y)
Now of the two halves of (1), the conditional from left
to right, namely
(2) x = y -> Az(z e x <-> z e y)
is simply a theorem of predicate calculus with identity.
(Assuming that x = y and z e x, z e y follows; assuming
x = y and z e y, z e x follows - in each case by identity
theory.) It is the other half of (1) that is specifically
set-theoretic. Accordingly, our first axiom is the uni-
versal quantification of this half:
A1: AxAy(Az(z e x <-> z e y) -> x = y).
This axiom is called _the axiom of extensionality_ It
states that, for any x and y, if the membership of x and
y are the same, then x any y are the same. (If identity
were not part of our underlying logic, then we should
need to take (1) itself as a definition of identity.)"
(E. J. Lemmon, Introduction to Axiomatic Set Theory, pp. 14-15)
:-)
Probably its worth to note that Lemmon's intention is/was to present
a version of Morse-Kelley Set Theory in his booklet! Hence, obviously
George's criticism would have been shared by Lemmon - or better, was
already anticipated by him! :-)
F.
P.S.
Strange thing. Sometimes "short comments" grow rather long. :-)
G. Frege
-------------------------------------------------------------------------
>
> I am not so sure that [the] definition "a = b <-> (x)(a e x <-> b e x)"
> will do.
>
Why?!
(Actually, I know why - see the follow up to this post, if
you are interested in this topic.)
Anyway:
Of course, an additional _axiom_ is needed in this case - at least in
the set theories _we_ are talking about. This is well known.
We might take:
(Ext) AxAy(Az(z e x <-> z e y) -> x = y) // Extensionality
-------------------------------------------------------------------------
>
> Take an instance of Leibnitz's Law: x = y -> (Fx <-> Fy), as:
> x = y ->. ~(x e x) <-> ~(y e y).
>
So what?
>
> Since the Russell Class does not exist, x e {x:~(x e x)} <->
> y e {x:~(x e x)}, is not equivalent to ~(x e x) <-> ~(y e y).
>
Errr...? Actually, in BOTH approaches NBG/Bernays as well as MK the
_Russell Class_ DOES exist! (It's a so called proper class in MK.)
Moreover the following holds in Bernays' version of NBG (von
Neumann-Bernays-Gödel set theory):
From
a e {x:~(x e x)} <-> b e {x:~(x e x)}
by the Church schema we get *immediately*:
~(a e a) <-> ~(b e b)
and vice versa. Simple as that!
-------------------------------------------------------------------------
But the following question is _meaningful_, and may be asked in set
theories like MK (which deals with both sets and non-sets):
>
> Given that {x:~(x e x)} is not a set, how then do we derive
>
> x = y ->. ~(x e x) <-> ~(y e y) ?
>
I will try to address this question in a separate (follow up) post.
(Already mentioned above.)
-------------------------------------------------------------------------
Quine, referring to his "New foundations":
>
> "[...] we miss out not just on identity but on unstratified formulas
> more widely. I discovered this in 1938 or 9 and closed the gap by
> adding a domain of ultimate classes, that is, classes not eligible
> for membership in classes. The idea goes back to von Neumann. [...]"
>
> (W.V. Quine)
>
Indeed, the "problem" you mentioned _isn't_ a problem in von Neumann-
Bernays-Gödel (NBG) Set Theory and/or Morse-Kelley (MK) Set Theory.
-------------------------------------------------------------------------
>
> I find that the admission of ultimate classes or of proper classes
> does not solve the difficulty.
>
Actually, the "difficulty" ISN'T THERE, not even in "New foundations"!
Quine:
"[...] your formula
x = y .->: ~(x e x) .<->. ~(y e y)
is indeed demonstrable within "New Foundations"
despite failure of stratification."
(Of course, you might call Quine a liar; though I would think in this
case YOU would be the liar, actually.)
-------------------------------------------------------------------------
>
> Note: y e {x:~(x e x)} is contradictory.
>
??? In NBG/Bernays this formula is equivalent with
~(y e y).
Now from foundation we would have that the latter is true for any set y.
Where's the contradiction? :-o
-------------------------------------------------------------------------
F.
Witt
Your set abstract is what I am calling a class of sets determined by
some predicate F.
If we start (classical) set theory by assuming that the individual
variable refers to: sets, sets of sets, etc. then we need to define
classes of sets, some of which will exist and some will not exist.
AxFx -> Fy, Fy -> ExFx, Ax(Fx -> Gx) -> (AxFx -> AxGx), Ax(x=x), x=y
-> (Fx <-> Fy).
E!x defined x=x.
FOL=, works here.
The class of sets determined by the predicate F is described:
{x:Fx} defined (iy:Ax(x e y <-> Fx)).
G{x:Fx} <-> Ey(Ax(x e y <-> Fx) & Gy).
{x:Fx}={x:Fx} <-> Ey(Ax(x e y <-> Fx) & y=y)
{x:Fx}={x:Fx} <-> Ey(Ax(x e y <-> Fx)).
That is to say, when Ax(x e y <-> Fx) is false so is
{x:Fx}={x:Fx}, unlike sets.
Not all classes of sets are sets.
The classes of sets which do exist are values of the individual
variable ..i.e. they are sets.
But, the classes of sets which are not self identical do not exist,
they are not proper classes at all, nor are they anything else.
They do NOT exist.
They do not have any primary predications at all.
They are not members of any (existent class) set,
and there is no set that is a member of them.
~EyAx(x e y <-> Fx) <-> ~E!{x:Fx}.
>
> Based on the foregoing, "x e {x: ~(x e x)}" cashes out as (ii):
>
> ii) Ey(y=y & x e y & Az(z e y <-> (z=z & ~(z e z))))
>
> However, granted that every class of non-self-membered sets
> is a *proper* class, and that proper classes are not self-
> identical, from (ii) there follows (iii).
>
> iii) ~Ey(y=y & x e y & Az(z e y <-> (z=z & ~(z e z))))
>
> But (iii) cashes out as (iv):
>
> iv) ~(x e {x: ~(x e x)})
>
> But x is arbitrary. Hence {x: ~(x e x)} has no members:
>
> v) Ax~(x e {x: ~(x e x)})
Yes, I agree.
>
> Therefore, {x: ~(x e x)} is the empty set (the existence of which in C
> is established in news:<70f94e16.02090...@posting.google.com>).
But, {x:~(x e x)} not only has no members it is also not a member of
any set, unlike the null set. {} e 0, but, {x:~(x e x)} e 0, is
contradictory.
The class of sets {x:~(x e x)} does not exist, but, the set of sets
{x|~(x e x)} does exist and is equal to the null set.
Classes of sets are sets (of sets) iff they do exist.
> Hmm. In news:<s%G_7.200471$KT.48...@news4.rdc1.on.home.com>,
> didn't some guy by the name of Holden say, "The Russell set is
> the null set"?
I agree with Owen more than I do with anyone. (hahaha).
Agreed, to give the Russell class a special category of existence,
other than self identity, is inconsistent.
First order logic cannot (imho) define identity, it must be taken
primitive along with membership, which is all the better for your own
theory.
Witt
>
> --John
F. Fritsche
>
> Hence {x: ~(x e x)} has no members:
>
What a nonsensical approach!
John
In Lemmon's system--I still don't have the book--aren't all sets classes?
If so, I'd gladly use his axiom of classification--the only reason I
stopped using it was a quibble from one of the Boyz.
--John
John
I still have a problem with this terminology. It's unclear to me why
the existence of classes that are not elements (e.g. proper classes)
is any less certain than the existence of classes that are elements
(e.g. sets). After all, classes were around for a long, long time
before it occurred to anyone to distinguish classes that are elements
from classes that are not.
At any rate, although classes that are not sets are not well-liked
by sci.logickoi, these have been much more extensively dealt with by
set-theorists than their kissing cousins in logic, to which it is still
*de rigueur* in polite society to deny any status at all. Perhaps
this is why I am inclined to refer to such identical-with-nothings
as the present King of France as "non-existents"--the present King of
France having been much more stigmatized by logicians than the class
of non-self-membered sets by set theorists--but inclined to
refer to proper classes as "existents".
At any rate, at this stage what's important is to give a proper
account of the role that such things play in logic
and set theory.
>
> AxFx -> Fy, Fy -> ExFx, Ax(Fx -> Gx) -> (AxFx -> AxGx), Ax(x=x), x=y
> -> (Fx <-> Fy).
>
> E!x defined x=x.
>
> FOL=, works here.
>
> The class of sets determined by the predicate F is described:
>
> {x:Fx} defined (iy:Ax(x e y <-> Fx)).
>
> G{x:Fx} <-> Ey(Ax(x e y <-> Fx) & Gy).
>
> {x:Fx}={x:Fx} <-> Ey(Ax(x e y <-> Fx) & y=y)
> {x:Fx}={x:Fx} <-> Ey(Ax(x e y <-> Fx)).
>
> That is to say, when Ax(x e y <-> Fx) is false so is
> {x:Fx}={x:Fx}, unlike sets.
Decide whether {x:Fx} is a set abstract or
a class abstract. If {x:Fx} is a set abstract, then
{x:Fx} = {x:Fx} is ALWAYS true, and you can't say,
"{x:Fx}={x:Fx} is false, unlike sets."
G. Frege
>
> In Lemmon's system ... aren't all sets classes?
>
There is no such thing as "Lemmon's system". Lemmon presents a variant
(his version) of Morse-Kelley Set Theory (MK).
And yes. Of course all sets are classes in MK (but not all classes are
sets).
F.
G. Frege
Witt wrote:
"I am not so sure that [the] definition
a = b :<-> (x)(a e x <-> b e x)
will do."
Indeed, this definition wouldn't be appropriate for MK Set Theory,
but we COULD use it in NBG/Bernays or in a Zermelian approach (i.e.
a variant of ZFC).
In MK we would have the rather undesirable result that any proper
classes a,b would be equal. Hence in MK we might adopt the definition
a = b :<-> (x)(x e a <-> x e b)
instead.
Still we would have to add an additional axiom in this case, namely:
AxAyAz(x e z & x = y -> y e z).
All this is well known.
----------------------------------------------------------------------
Now let's stay in NBG/Bernays, with equality defined with:
a = b :<-> (x)(a e x <-> b e x)
(Hence equality is reflexive, symmetrical and transitive.)
Then your question was:
>
> Given that {x:~(x e x)} is not a set, how then do we derive
>
> x = y ->. ~(x e x) <-> ~(y e y) ?
>
Well, actually from foundation we would have that ~(x e x) and ~(y e y)
hold for any sets x,y. Hence ~(x e x) <-> ~(y e y) holds (is true). And
hence the implication holds for any sets x,y. (Note that in NBG/Bernays
x,y are set variables!)
Ok..., probably that was a little bit "unfair". So let's try to derive
it _without_ using foundation! (This is slightly more tricky.)
Actually we will make use of the following lemma:
a = b -> (x)(x e a <-> x e b).
(Proof omitted.)
Now with this lemma at hands the proof for
a = b -> ~(a e a) <-> ~(b e b)
is rather simple.
Proof:
Assume a = b. Then from our definition of = we have (x)(a e x <-> b e x)
and hence (with instantiation of x to a) we have a e a <-> b e a. (*)
Now from our lemma we have (x)(x e a <-> x e b), and (with an instant-
iation of x to b) we have b e a <-> b e b. (**). Hence from (*) and (**)
we have a e a <-> b e b. Which is equivalent with ~(a e a) <-> ~(b e b).
This means that a = b implies ~(a e a) <-> ~(b e b). qed.
F.
Witt
Franz, I do appreciate your logical rigor, but, I want to show that:
y e {x:Fx} <-> Fy, is invalid. In particular, y e {x:~(x e x)} <-> ~(y
e y), is false. Try to be patient and I will explain my point of view.
Do you agree with:
1.Gz <-> Ey(y=z & Gy)
2.G{x:Fx} <-> Ey(y={x:Fx} & Gy), when z has the value {x:Fx}.
3.G{x:Fx} <-> Ey(Ax(x e y <-> Fx) & Gy), in virtue of the axiom of
extensionality.
Therefore by 3,
3a. z e {x:Fx} <-> Ey(Ax(x e y <-> Fx) & z e y)
3b. z e {x:Fx} <-> Ey(Ax(x e y <-> Fx) & Fz)
3c. z e {x:Fx} <-> (EyAx(x e y <-> Fx) & Fz).
But, when Fx means ~(x e x), EyAx(x e y <-> ~(x e x)) is false.
Ax(x e y <-> ~(x e x)) -> (y e y <-> ~(y e y))
Therefore, ~Ey(Ax(x e y <-> ~(x e x)).
That is to say, EyAx(x e y <-> Fx) is not a theorem.
The assumption that it is a theorem leads to Russell's antinomy.
3c then becomes,
3d. z e {x:~(x e x)} <-> contradiction.
3e. Az~(z e {x:~(x e x)}).
Note: John Corry proved this same point in a different way.
E!{x:Fx} -> (z e {x:Fx} <-> Fz), is valid, but,
z e {x:Fx} <-> Fz, is not valid!
~E!{x:~(x e x)} is a theorem.
Witt
G. Frege
I'm happy that you actually answered to one of my posts. I mean... after
all we are interested in these (logical) questions/problems. Aren't we?
>
> [...] I want to show that:
>
> y e {x:Fx} <-> Fy, is invalid.
>
> [And] in particular [that]
>
> y e {x:~(x e x)} <-> ~(y e y), is false.
>
Right. But -I hope we agree- this questions depend on the very system of
set theory we are working with.
For example in Bernays' version of NBG
y e {x:Fx} <-> Fy
is JUST the "Church schema". Hence
y e {x:~(x e x)} <-> ~(y e y)
is a Theorem t h e r e!
"...we have the advantage that the operation of forming
a class {x | A(x)} from a predicate A(c) can be taken
as an unrestricted logical operation, not depending on
any comprehension axiom."
(P. Bernays, Axiomatic Set Theory, p. 42)
"The rules concerning the class term are: the formula schema
("Church schema")
c e {r | A(r)} <-> A(c),
expressing a conversion law, in the sense of A. Church [1932],
and ..."
(P. Bernays, Axiomatic Set Theory, p. 48)
Hence TO BE right, you would have to talk about some other system (of
set theory) - but I do not really know which. (See below.)
BTW: From foundation we would have that for any set y we have ~(y e y)
this would mean that for any set y y e {x:~(x e x)}, i.e. {x:~(x e x)}
is the universal class V.
>
> Do you agree with:
>
> 1. Gz <-> Ey(y = z & Gy)
>
Sure. This is a theorem of FOPL with identity.
But the following could NOT be formulated in Bernays' version of NBG.
Hence I have to stop here [for a moment] for some elaboration.
Now certainly we might try to consider some other theory, in which your
formulas could be expressed... Hmmm... Well, let me think about it. It
couldn't be ZFC, since THERE we wouldn't have "unrestricted
comprehension":
y e {x:Fx} <-> Fy (*)
Same with MK. How about NF? Isn't (*) a valid statement in NF - IF Fx is
stratified? I guess it is. (Note that ~(x e x) isn't stratified; hence
we couldn't substitute it for Fx in the set term in (*))
Actually, YOU are the expert for NF, so please
tell me; I really d o n't k n o w.
Well... seems that there is still some decent standard system of NBG
which might be considered. There we might have the following
comprehension axiom schema
EXAy(y e X <-> Fy) // if F is a /predicative/ formula and
X does not occur free in F.
Hence (I guess) we also would have
y e {x:Fx} <-> Fy // if F is a /predicative/ formula
here.
But note that we have to differentiate quantification over sets (denoted
with set variables x,y,z...) and quantification over classes (denoted
with class variables X,Y,Z...) here!
This means, that we can conclude
EX(a e X <-> Fa)
but NOT (directly)
Ex(a e x <-> Fa)
- since we don't know if the class {x:Fx} is a set or not!
Actually we have the axiom
AXAY(X e Y -> Ez(z = X))
"Every class which is a member of some other class,
is a set."
as well as the axiom
AxEY(x = Y).
"Every set is a class."
Ok... with this behind us we might look at your formulas...
>
> 2. G{x:Fx} <-> Ey(y={x:Fx} & Gy)
>
Since we don't have for all classes {x:Fx} that they are sets; i.e.
Ey(y = {x:Fx}),
we will have to use the formulation:
2' G{x:Fx} <-> EY(Y = {x:Fx} & GY)
That's certainly a theorem in our system.
>
> 3. G{x:Fx} <-> Ey(Ax(x e y <-> Fx) & Gy)
>
3' G{x:Fx} <-> EY(Ax(x e Y <-> Fx) & GY)
// if F is a /predicative/ formula
>
> Therefore by 3,
>
> 3a. z e {x:Fx} <-> Ey(Ax(x e y <-> Fx) & z e y)
>
3a' z e {x:Fx} <-> EY(Ax(x e Y <-> Fx) & z e Y)
> 3b. z e {x:Fx} <-> Ey(Ax(x e y <-> Fx) & Fz)
3b' z e {x:Fx} <-> EY(Ax(x e Y <-> Fx) & Fz)
> 3c. z e {x:Fx} <-> (EyAx(x e y <-> Fx) & Fz).
3c' z e {x:Fx} <-> EYAx(x e Y <-> Fx) & Fz
Indeed. From the comprehension axiom schema we have:
EYAx(x e Y <-> Fx).
Hence (finally)
3d' z e {x:Fx} <-> Fz.
(Note that z is a set variable!)
>
> But, when Fx means ~(x e x), EyAx(x e y <-> ~(x e x)) is false.
>
No. In NBG (as described above) we have (from the comprehension axiom):
EYAx(x e Y <-> ~(x e x)).
And also (from 3'd):
z e {x:~(x e x)} <-> ~(z e z).
Again, from foundation we would have
Az(~z e z)
and hence
Az(z e {x:~(x e x)})
Now with the definition of the universal class
V =df {x : x = x}
this means (from extensionality)
{x:~(x e x)} = V
Right. If we call {x:~(x e x)} the Russell class R, this means:
R = V.
A well knows fact.
>
> That is to say, EyAx(x e y <-> Fx) is not a theorem.
>
Right. But
EYAx(x e Y <-> Fx) [ if F is a /predicative/ formula ]
is a axiom (schema) in some systems of NBG (i.e. the one mentioned
above).
>
> The assumption that it is a theorem leads to Russell's antinomy.
>
It WOULD if we would not make a difference between (proper) classes and
sets!
The axiom just mentions ensures the existence of a CLASS Y such that any
set x is element of that class iff it's an F.
>
> z e {x:~(x e x)}
>
Right.
>
> 3e. Az(z e {x:~(x e x)}).
>
Right. (See result above.)
>
> Note: John Correy proved...
>
Actually, it does not interest me the LEAST what John Correy "proved" or
not. (Sorry.)
>
> E!{x:Fx} -> (z e {x:Fx} <-> Fz), is valid
>
Right. If we define (in some FL framework - instead of FOPL)
E!x =df EY(Y = {x:Fx}).
This way we might differentiate between class abstracts that don't
really denote a class (i.e. where F is n o t a /predicative/ formula)
and class abstracts which do. I like that idea!!! :-)
>
> but,
>
> z e {x:Fx} <-> Fz, is not valid!
>
Sure it is [if F is a /predicative/ formula]. (See comments above.)
>
> ~E!{x:~(x e x)} is a theorem.
>
No. I'm sorry. Neither in NBG/Bernays nor in the system of NBG described
above (due to Gödel) nor in MK Set Theory.
But it might be true in NF, I guess.
F.
P.S. The reason for this is -of course- that the Russell class can't be
a set [if we we don't accept contradictions]. And since there ARE ONLY
sets in NF, the Russell class doesn't exist _in the domain of NF_.
This is exactly what W.V. Quine meant when he wrote
"...we miss out not just on identity [in New Foundations]
but on unstratified formulas more widely. I discovered
this in 1983 or 9 and closed the gap by adding a domain
of ultimate classes, that is, classes not eligible for
membership in classes. The idea goes back to von Neumann."
You see... ALL the systems I talked above are variants of von
Neumann-Bernays-Gödel Set Theory.
(And all YOU said may be true in NF - I don't know, really.)
-----------------
Still NF has its merits:
See:
New Foundations home page
http://math.boisestate.edu/~holmes/holmes/nf.html
It seems that NFU (NF with urelements) is a very interesting and
powerful set theory:
"NFU: New Foundations with urelements. This system is consistent,
consistent with Choice, and does not prove Infinity but is consistent
with it ( Jensen, 1969). NFU + Infinity + Choice has the same
consistency strength as the theory of types with the Axiom of Infinity.
Its model theory is fairly simple and NFU can safely be extended as far
as you think ZFC can be extended. The consistency of NFU, which has the
full scheme of stratified comprehension, shows that the comprehension
scheme and resulting presence of "big" sets is not the problem with NF.
For an extended study of set theory in NFU, click here
http://www.lofs.ucl.ac.be/cnrl/Cahiers/Cahier10.html
Extensions of NFU are adequate vehicles for mathematics in a basically
familiar style."
John
You have nowhere *defined* {x: Fx}. So, how is any one supposed to
know what follows, or what does not follow, from "a e {x: Fx}"?
>
--John
G. Frege
>
> You have nowhere *defined* {x: Fx}. So, how is one supposed to
> know what follows, or what does not follow, from "a e {x: Fx}"?
>
In Bernays' system of NGB the class operator {r | A(r)} is part of his
logical frame. This means that...
"...we have the advantage that the operation of forming
a class {x | A(x)} from a predicate A(c) can be taken
as an unrestricted logical operation, not depending on
any comprehension axiom."
(P. Bernays, Axiomatic Set Theory, p. 42)
In addition he states a certain _logical_ rule, the formula schema
("Church schema"):
c e {r | A(r)} <-> A(c)
where c is a set variable.
"The rules concerning the class terms are: the formula schema
("Church schema")
c e {r | A(r)} <-> A(c),
expressing a conversion law, in the sense of A. Church [1932],
and ... "
(P. Bernays, Axiomatic Set Theory, p. 48)
> >
> > Then from
> >
> > a e {x:~(x e x)} <-> b e {x:~(x e x)}
> >
> > by the Church schema we get *immediately*:
> >
> > ~(a e a) <-> ~(b e b)
> >
> > and vice versa. Simple as that!
> >
F.
John
> On 10 Oct 2003 17:18:50 -0700, john_...@yahoo.com (John) wrote:
>
> >
> > You have nowhere *defined* {x: Fx}. So, how is one supposed to
> > know what follows, or what does not follow, from "a e {x: Fx}"?
> >
>
> In Bernays' system of NGB the class operator {r | A(r)} is part of his
> logical frame. This means that...
>
>
> "...we have the advantage that the operation of forming
> a class {x | A(x)} from a predicate A(c) can be taken
> as an unrestricted logical operation, not depending on
> any comprehension axiom."
>
> (P. Bernays, Axiomatic Set Theory, p. 42)
>
>
> In addition he states a certain _logical_ rule, the formula schema
> ("Church schema"):
>
> c e {r | A(r)} <-> A(c)
>
> where c is a set variable.
>
>
> "The rules concerning the class terms are: the formula schema
> ("Church schema")
>
> c e {r | A(r)} <-> A(c),
>
> expressing a conversion law, in the sense of A. Church [1932],
> and ... "
>
> (P. Bernays, Axiomatic Set Theory, p. 48)
Yes, but we're not talking about Bernays's or Church's systems, in which
'x=x' holds for classes that are members and classes that are not.
If you and I are talking about the *same* theory, in which 'x=x'
holds for sets but '~(x=x)' holds for proper clsses, I'd like to know
what you take 'x e {x: Fx}' to mean.
Otherwise, please continue to construe 'x e {x: Fx}' in whatever way
you wish.
--John
G. Frege
>
>
> I am not so sure that [...] "a = b :<-> (x)(a e x <-> b e x)"
> will do.
>
At least it will do in Quine's "New Foundations" (NF).
>
> How ... do we derive, x = y ->. ~(x e x) <-> ~(y e y)?
>
> I wrote to Quine about this point in Feb 1997, and he
>
wrote back:
"[...] in particular your formula
x = y .->: x !e x .=. y !e y
is indeed demonstrable within "New Foundations"
despite failure of stratification.
... W.V.Quine"
F.
P.S.
You might be interested in the paper "Identity of indiscernibles in
Quine's "New Foundations" and related theories" by M. Randall Holmes.
There he proves the theorem:
For any formula Phi, x = y -> Phi[x/a] <-> Phi[y/a].
Source:
http://math.boisestate.edu/~holmes/holmes/define_equality.ps.
George Greene
is the only person I know of here who was also on the FOM list back
when McLarty published his 3 axioms) to compare some basic
first-order axiomatizations of category theory. RBJ's web-site
hosts the definitive one (which he got from William Hatcher and
which need fully 6 axioms). Colin McLarty did a different
treatment with only 3 but he did not include any axioms defining
"defined" (as in, "what does it mean for the composition of two
arrows to be defined, as opposed to undefined?"). I found
McLarty's treatment to be less intuitive but I still think 6 axioms
is too many.
Actually, though, I am more interested in the philosophical
question of what the existence of this small foundational axiom-set
says about the validity of category theory as a foundation,
compared to alternative foundations. In the original FOM
discussion, Vaughn Pratt asked a rather naive question about
whether axioms such as these "define morphisms" (i.e., define
arrows) as opposed to defining categories, and TF actually claimed
that McLarty's first axioms was tautologous (or had a typo), but
the discussion seemed to die down after that, despite the opinion
of such giants as Solomon Feferman that these would not cut it as
foundations.
McLarty's treatment was:
> I will give the assumptions explicitly. Since composition is not
> defined for all pairs of arrows you might like to use a relation symbol
> Cfgh to say "h is the composite of f and g", but I will use operator
> notation gf=h for visual clarity.
>
> DEFINITION: An arrow u is an "identity" iff, for every arrow f with
> the composite fu defined, fu=f.
>
> AXIOM C1: If u is an identity, then for any arrow g with the composite
> gu defined, gu=g.
>
> AXIOM C2: For every arrow f there is a unique identity u with the
> composite fu defined, and a unique identity v with vf defined. We
> write f:u-->v to say u and v are identities and the composites are
> defined.
>
> AXIOM C3: For any arrows f, g, h, if gf and hg are defined then the
> associativity equation holds and both sides are defined:
>
> h(gf) = (hg)f
>
> These are first order axioms for a theory of arrows (i.e. for
> a category).
I think the correction to C1 might be "ug" as opposed to "gu"
("gu" is, as TF stated, just a re-statement of the definition
of "identity").
This other set of axioms from Hatcher via RBJ says:
> C.1. Ax1[ d(c(x1)) = c(x1) & c(d(x1)) = d(x1) ]
> The domain of the codomain of x1 is the codomain of x1,
> and the codomain of the domain of x1 is the domain of x1.
> C.2. Ax1x2x3x4 [ K(x1,x2,x3) & K(x1,x2,x4) --> x3=x4
> The composition of x1 with x2 is unique when it is defined.
> C.3. Ax1x2[ Ex3[ K(x1,x2,x3) <-> c(x1)=d(x2) ] ]
> The composition of x1 with x2 is defined if and only
> if the codomain of x1 is the domain of x2.
> C.4. Ax1x2x3[ K(x1,x2,x3) --> d(x3)=d(x1) & c(x3)=c(x2) ]
> If x3 is the composition of x1 with x2 then the
> domain of x3 is the domain of x1 and the codomain of x3 is the codomain of x2.
> C.5. Ax1[ K(d(x1),x1,x1) & K(x1,c(x1),x1)
> For any x1, the domain of x1 is a left identity
> for x1 under composition and the codomain is a right identity.
> C.6. Ax1x2x3x4x5x6x7 [ ( K(x1,x2,x4) & K(x2,x3,x5)
> & K(x1,x5,x6) & K(x4,x3,x7) ) --> x6=x7 ]
> Composition is associative when it is defined.
I am looking for a correct "compression" of the Hatcher
and a correct correction of the McLarty.
Roger Bishop Jones
> I would like to invite Roger Bishop Jones and Torkel Franzen (who
> is the only person I know of here who was also on the FOM list back
> when McLarty published his 3 axioms) to compare some basic
> first-order axiomatizations of category theory.
<snip>
> Actually, though, I am more interested in the philosophical
> question of what the existence of this small foundational axiom-set
> says about the validity of category theory as a foundation,
> compared to alternative foundations.
Very little at all.
Your use of the term "foundational" to describe these axiomatic
presentations of category theory is pretty inappropriate.
These axiom systems are a long way short of being foundation
systems.
For the record a "foundation for mathematics" in the relevant
sense for this discussion is a formal theory in which most
of mathematics can be developed **using only conservative
extensions** (i.e. definitions).
If you don't have this constraint then first order logic
without any "non-logical" axioms would qualify as a
foundation for mathematics (which it isn't normally
considered).
The axiomatisations of bare category theory
are not foundation systems in teh above sense.
This is best seen to be the case by noting that the
axioms are satisfied by a category containing just
one object.
Consequently there are not known to be enough objects
around even to do arithmetic.
Those who have advocated category theoretic rather than
purely set theoretic foundations ahve I think
usually advocated something along the lines of topos
theory.
If you are going this way then you need in addition
to the basic axioms for category theory, the additional
axioms for topos theory and then some more.
I think topos theory gets you as far as a weak
arithmetic, so you need more if you are to provide
a foundation for as much mathematics as can be done
in (say) ZFC. I'm not familiar with the details,
and I'm not at all sure than anyone has taken this
as far as a theory which matches the strength of ZFC.
[There is another way of providing a "category
theoretic" foundation system which I have some
material about on my web site, but since no-one
else but me has even considered this method I
shalln't go into it here]
On the specifics of the axiom systems,
the two are couched in different first order
languages and this accounts for some of the
differences in the axioms.
THe correction you mentioned to McLarty's is
needed.
Also, I think it is necessary to state the
conditions under which the composition of
two functions is defined.
There is some awkwardness here arising from
the fact that McClarty is using functional
notation rather than relational notation.
This helps to reduce the number of axioms
(and the fact that he has no domain and codomain
functions) but it leaves him with a difficulty
in talking about when composition is defined.
By time you have finished sorting out McClarty's
axioms you won't have any significant simplification
over Hatcher.
Roger Jones
Mattias Wikstr?m
> is the only person I know of here who was also on the FOM list back
> when McLarty published his 3 axioms) to compare some basic
> first-order axiomatizations of category theory. RBJ's web-site
> hosts the definitive one (which he got from William Hatcher and
> which need fully 6 axioms). Colin McLarty did a different
> treatment with only 3 but he did not include any axioms defining
> "defined" (as in, "what does it mean for the composition of two
> arrows to be defined, as opposed to undefined?").
Doing category theory in a single-sorted logic is just silly. With a
many-sorted logic, the logic itself takes care of "undefined"
(ill-typed) expressions, just as it takes care of ill-formed
expressions and incorrect proofs.
Some consider it inelegant to mention objects when defining a
category, prefering to talk solely about morphisms. With a many-sorted
logic this means not writing out sorts in the expressions (it should
then be possible to infer the sorts from the expressions).
Mattias
G. Frege
Concerning the definability of identity in set theory Witt wrote:
"I am not so sure that
a = b :<-> (x)(a e x <-> b e x)
will do. How do we derive
x = y ->. ~(x e x) <-> ~(y e y)?
then?"
----------------------------------
Well. Let's consider Quine's set theory "New Foundations" (NF) for
example.
There equality is defined with
Def. x = y :<-> Az(x e z -> y e z)
The only axioms are the following:
Ax. 1 EyAx(x e y <-> Phi(x))* // Comprehension
Ax. 2 AxAy(Az(z e x <-> z e y) -> x = y) // Extensionality
* If Phi(x) is "stratified", and y does not occur free in Phi(x).
----------------------------------
First of all, we might notice the slightly uncommon definition of the
identity relation. (Simple implication instead of a biconditional in the
definiens.)
So let's in a first step show that we can derive the
Theorem 1: AxAy(x = y -> Az(x e z <-> y e z))
in NF.
Proof: Let's assume that the theorem were false.
Hence there should be some sets a,b such that
a = b but ~Az(a e z <-> b e z). With other words,
Ez~(a e z <-> b e z). And hence there's some c
such that (a e c & b !e c) v (a !e c & b e c).
Without loss of generality we assume that a !e c
& b e c. Now from Ax. 1 we get that there is a
set c' such that Ax(x e c' <-> x !e c). And hence
we have that a e c' (since a !e c). Now from a = b
and the definition of equality, we get that
Az(a e z -> b e z). And with instantiation of z
with c', we get a e c' -> b e c'. And hence we have
that b e c' with (modus ponens). But b e c' means
that b !e c. Contradiction! []
From this we get immediately the quite natural
Corollary 1: AxAy(x = y <-> Az(x e z <-> y e z))
Proof: Directly from Theorem 1 and the definition of
equality.
Next we will derive the
Theorem 2: AxAy(x = y -> Az(z e x <-> z e y))
Proof: Let's assume that the theorem were false.
Hence there should be some sets a,b such that
a = b but ~Az(z e a <-> z e b). With other words,
Ez~(z e a <-> z e b). And hence there's some c
such that (c e a & c !e b) v (c !e a & c e b).
Without loss of generality we assume that c e a
& c !e b. Now from Ax. 1 we get that there is a
set d such that Ax(x e d <-> c e x). And hence
we have that a e d (since c e a). Now from a = b
and the definition of equality, we get that
Az(a e z -> b e z). And with instantiation of z
with d, we get a e d -> b e d. And hence we have
that b e d with (modus ponens). But b e d means
that c e b. Contradiction! []
From this we get immediately the
Corollary 2: AxAy(x = y <-> Az(z e x <-> z e y))
Proof: Directly from Theorem 2 and the extensionality axiom.
----------------------------------
Now with this theorems at hands the proof of
Theorem: AxAy(x = y -> ~(x e x) <-> ~(y e y))
is rather simple.
Proof: Assume a = b. Then from theorem 1 we have
Az(a e z <-> b e z) and hence (with instantiation
of z with b) we have a e b <-> b e b.(*) Now from
theorem 2 we have Az(z e a <-> z e b), and (with
an instantiation of z with a) we have a e a <->
a e b.(**) Hence from (*) and (**) we have a e a
<-> b e b. Which is equivalent with ~(a e a) <->
~(b e b). This means that a = b implies ~(a e a)
<-> ~(b e b). Or with other words we have a = b ->
~(a e a) <-> ~(b e b). Since a and b were arbitrary
we finally get AxAy(x = y -> ~(x e x) <-> ~(y e y)).
qed.
I guess this should answer your initial question - at least in NF.
Actually, in his paper "Identity of indiscernibles in Quine's 'New
Foundations' and related theories" M. Randall Holmes shows that the
following general theorem holds in NF (even without Extensionality!):
For any formula Phi, x = y -> Phi[x/a] <-> Phi[y/a].
This actually should make clear that a = b :<-> Ax(a e x <-> b e x)
certainly "would do" - at least in NF.
See:
http://math.boisestate.edu/~holmes/holmes/define_equality.ps.
F.
P.S.
Holems' result means that it is not necessary to "add an additional
axiom of identity ... e.g. x = y -> (Fx <-> Fy)" (Owen Holden) since we
can actually p r o v e this statement to hold in NF (!).
Of course this result allows for a much simpler proof (of the statement
in quest) than the proof presented above.
G. Frege
> "I am not so sure that
>
>
> will do. How do we derive
>
>
> then?" (Witt)
>
>
Well. First, let's consider just the core axiom of Quine's set theory
"New Foundations" (NF):
Axiom (schema): EyAx(x e y <-> Phi)* // Comprehension
If Phi is a /stratified/ formula in which the variable y is not free.
Please note:
"Informally, {x | Phi} exists when Phi is stratified (in the
absence of extensionality assumptions, there may be more than
one such "set"; [hence] any use of the notation {x | Phi}
[here] refers to some witness to the appropriate instance of
the comprehension axiom, and does not implicitly assume the
existence of a unique or even canonical witness."
(M. Randall Holmes, Identity of indiscernibles in Quine's
"New Foundations" and related theories)
And, second, let's define equality with
Def. x = y :<-> Az(x e z <-> y e z),
as proposed.
Then we can prove the formula
x = y -> ~(x e x) <-> ~(y e y)
quite easily.
Proof:
Ax. Def=
Let x = y. x e x <-> x e {z | x e z} <-> y e {z | x e z} <->
Ax. Ax. Def= Ax.
<-> x e y <-> x e {z | z e y} <-> y e {z | z e y} <-> y e y.
Hence we have shown x e x <-> y e y. But that's logically
equivalent with ~(x e x) <-> ~(y e y). Hence we have shown
that x = y implies ~(x e x) <-> ~(y e y). With other words,
x = y -> ~(x e x) <-> ~(y e y). qed.
F.
G. Frege
>
> ...we can prove the formula
>
> x = y -> ~(x e x) <-> ~(y e y)
>
> quite easily [in NF].
>
Actually, we can prove the theorem straightforward:
Proof:
Ax. Def=
Let x = y. Then ~(x e x) <-> x e {z | ~(x e z)} <-> y e {z | ~(x e z)}
Ax. Ax. Def= Ax.
<-> ~(x e y) <-> x e {z | ~(z e y)} <-> y e {z | ~(z e y)} <-> ~(y e y).
Thus we have shown that x = y implies ~(x e x) <-> ~(y e y). With other
George Greene
: I know. Except that I inadvertently stumbled on mereology. The transitive
: closure operation satisfies the Kuratowski axioms and those axioms make no
: direct reference to a universe as would the definition of a topology. But,
: I had no way to motivate a topology given that everyone seemed to be
: assuming that one needed sets to define a topology.
We don't ASSUME that. THE AXIOMS DEFINING a topology PRESUME
sets. THEY TALK ABOUT OPEN *SETS*. These open sets don't have to be
ZFC sets; they don't even have to be sets at all; you could just
call them "opens" and get awat with it. But the other axioms then
WOULD talk about certain other things being "in" them, so again,
they would still look set-like. EVEN if you don't need ZFC, you STILL
need sets.
: Mereology changes that.
NO, IT *DOESN'T* !! JEEzus! WHERE DO YOU *GET* THIS SHIT?!?!?
The axioms defining a topology ARE THE SAME, COMPLETELY
irrespective of whether anyone ever has or hasn't heard of
mereology, OR of any axioms defining IT!
The world would be a better place if you would just
post the first-order axioms defining a topology, just to prove that
you know them. That is very much in doubt given that you
can make statements like the above.
George Greene
How many sorts are needed?
The only usual/typical requirement is 2 (objects vs. arrows)
which is ITSELF silly. I presume you have more sorts, and less
silliness, in mind? Please present!
> Some consider it inelegant to mention objects when defining a
> category, prefering to talk solely about morphisms.
Actually, we prefer to call them arrows.
I suppose some people might want to call them triples
(source, target, label?), although "triple" has a more
robust definition as a sort of reserved word in the larger theory.
> With a many-sorted
> logic this means not writing out sorts in the expressions (it should
> then be possible to infer the sorts from the expressions).
Well, any foundational treatment should clarify what the
indispensably necessary sorts are and why they are indispensable.
Mattias Wikstr?m
> mattias...@hotmail.com (Mattias Wikstrom) wrote
> > Doing category theory in a single-sorted logic is just silly.
>
> How many sorts are needed?
> The only usual/typical requirement is 2 (objects vs. arrows)
> which is ITSELF silly. I presume you have more sorts, and less
> silliness, in mind? Please present!
Two arrows are of the same sort iff they have the same source and the
same target. Typically there are therefore infinitely many arrow
sorts. Arrow sorts are also known as sequents, and the sequent with
source A and target B is written A->B. To say that an arrow f belongs
to the sequent A->B one writes f:A->B.
The advantage with using a many-sorted theory is that one does not
have to deal with "nonsence" expressions like ff, where f:A->B and A
and B are different objects. This makes the axioms simpler. In fact,
all the axioms needed are the following:
(fg)h=f(gh)
f id=f
id f=f
The primitives here are composition and identity:
_ _ : (A->B), (B->C) |- (A->C)
id : (A->A)
Mattias
Bill Taylor
> > How many sorts are needed?
> > The only usual/typical requirement is 2 (objects vs. arrows)
> The advantage with using a many-sorted theory is that one does not
> have to deal with "nonsence" expressions like ff, where f:A->B and A=/=B
I always thought an elegant, barely artificial way of dealing with things
was to adopt (1) the semistandard identification of objects with identity
morphisms, to relieve the need to speak of objects at all; and
(2) remove the need to talk about composition "being defined" or not,
merely by introducing a special object (i.e. morphism) "0", say,
adjoined to any category not previously closed under composition,
and meaning "undefined", acting as a sort of trash bin.
I have never seen it done in books or papers, but it seems simple enough:
Ax 1: f(gh) = (fg)h
Ax 2: f0 = 0f = 0
Ax 3: (Ax)(Ei,j) [ (ix = x = xj) ^ (iu = u or 0) ^ (vi = v or 0)]
Ax 4: u.v ^ u.w ^ t.v ==> t.w { where a.b is an abbreviation for ab =/= 0 }
[As often, an axiom is considered to be the universal closure of that given.]
2&4 are just bookkeeping axioms telling us about compositions being defined,
1 is associativity and 3 is identities.
Would that do?
......
And I take this opportunity once again to note that "bookkeeping" and its
variants are the only words in English to have three consecutive double
letters! Or so says my subbookkeeper.
------------------------------------------------------------------------------
Bill Taylor W.Ta...@math.canterbury.ac.nz
------------------------------------------------------------------------------
Category mistake:- something that is not only not right, but not even wrong.
------------------------------------------------------------------------------
Roger Bishop Jones
> The advantage with using a many-sorted theory is that one does not
> have to deal with "nonsence" expressions like ff, where f:A->B and A
> and B are different objects. This makes the axioms simpler. In fact,
> all the axioms needed are the following:
> (fg)h=f(gh)
> f id=f
> id f=f
> The primitives here are composition and identity:
> _ _ : (A->B), (B->C) |- (A->C)
> id : (A->A)
You have moved some of the "complexity" in a theory of
categories from the non-logical axioms into the logic.
Since you have not presented the logic, it is unclear
whether on balance there is any gain.
More importantly, this falls a long way short of
providing any kind of "foundation" system,
and does not appear to address any of the
questions which arise in founding mathematics
in category theory (except the elementary question
of "what is a category").
Roger Jones
Mattias Wikstr?m
> mattias...@hotmail.com (Mattias Wikstr?m) wrote
>
> > > How many sorts are needed?
> > > The only usual/typical requirement is 2 (objects vs. arrows)
>
> > The advantage with using a many-sorted theory is that one does not
> > have to deal with "nonsence" expressions like ff, where f:A->B and A=/=B
>
> I always thought an elegant, barely artificial way of dealing with things
> was to adopt (1) the semistandard identification of objects with identity
> morphisms, to relieve the need to speak of objects at all; and
> (2) remove the need to talk about composition "being defined" or not,
> merely by introducing a special object (i.e. morphism) "0", say,
> adjoined to any category not previously closed under composition,
> and meaning "undefined", acting as a sort of trash bin.
>
> I have never seen it done in books or papers, but it seems simple enough:
>
> Ax 1: f(gh) = (fg)h
>
> Ax 2: f0 = 0f = 0
>
> Ax 3: (Ax)(Ei,j) [ (ix = x = xj) ^ (iu = u or 0) ^ (vi = v or 0)]
>
> Ax 4: u.v ^ u.w ^ t.v ==> t.w { where a.b is an abbreviation for ab =/= 0 }
I think it was Frege who first got the idea that when the result of
applying a function to a specific object would normally be said to be
undefined, one can choose an arbitrary object as the value. The use of
a special object, "Undefined," which when it appears as part of an
(ordinary) expression causes the value of the expression to be
"Undefined," is also well-known (I am not sure, but perhaps it should
be attributed to Kleene).
Using a special object for undefined expressions is perhaps as elegant
as we can get without using a many-sorted theory.
Mattias
Roger Bishop Jones
> I always thought an elegant, barely artificial way of dealing with things
> was to adopt (1) the semistandard identification of objects with identity
> morphisms, to relieve the need to speak of objects at all; and
> (2) remove the need to talk about composition "being defined" or not,
> merely by introducing a special object (i.e. morphism) "0", say,
> adjoined to any category not previously closed under composition,
> and meaning "undefined", acting as a sort of trash bin.
>
> I have never seen it done in books or papers, but it seems simple enough:
>
> Ax 1: f(gh) = (fg)h
>
> Ax 2: f0 = 0f = 0
>
> Ax 3: (Ax)(Ei,j) [ (ix = x = xj) ^ (iu = u or 0) ^ (vi = v or 0)]
>
> Ax 4: u.v ^ u.w ^ t.v ==> t.w { where a.b is an abbreviation for ab =/= 0 }
>
> [As often, an axiom is considered to be the universal closure of that given.]
It looks to me like Ax. 3 needs universal quantifiers for u and v
inside the square brackets (and by your convention doesn't need
the quantifier for x).
I also can't see how you get away without saying for "j" what you
said for "i" in that axiom.
Ax 4. gives sufficient conditions for composition to be
defined, but does not give necessary conditions.
How would you prove that the composition is always
undefined when the right identity of the left operand
isn't the same as the left identity of the right operand?
I can't say I am certain that your axioms are not
sufficient, but it is harder to satisfy
myself on that point than I would expect.
The use of your abbreviation for the statement
that composition is defined confused a proper
evaluation of the complexity of this axiomatisation.
Other axiom systems can probably be made to appear
simpler by the use of such simplifications.
Ultimately, however, which axiom system is "best"
will likely depend on what you want to do with it.
Roger Jones
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>
> I was talking about usual modern set theories like ZFC
> [which] have extensionality. And in the context of FOL
> with [identity], extensionality is
A1 AxAy(Az(z e x <-> z e y) -> x = y).
Right.
>
> IF you have THAT, then indeed, you will NOT have this
> half-backward substitution axiom [mentioned by] mitch.
>
> Of course, the main reason you will not have it is that
> you will have a FULL forward substitution rule as part
> [of] the underlying logic.
>
"First-order logic WITH [identity] has TWO MORE
INFERENCE RULES than first-order logic without
[identity]. They are the ones that make '=' a
logical symbol AS OPPOSED to something definable.
They are
|- Ax(x = x) (*)
and
x = y |- phi(x) -> phi(y) (**)"
(George Greene)
>
> [Now] since you already have x = y |- phi(x) -> phi(y)
> you will NOT need something specific to x e s & x = y.
>
> Mitch had basically scored a valid point.
>
Well, not really..., see below.
>
> I had insisted that = was eliminable from first-order
> [based] ZFC when you were doing it without equality,
> because the axiom of extent was a valid definition of =.
>
Actually, you were /almost/ right. You just mixed up the notion of
"explicit definition" with that of "axiom". (No, they are n o t
"one and the same".)
Now the funny thing is... we can use /FOPL without identity/ as our
framework and DEFINE equality (in our version of ZF(C)) with
a = b :<-> Ax(a e x <-> b e x)
instead, and NOTHING would change! (We would just KEEP our /axiom of
extensionality/ mentioned above.) No n e w axiom would have to be added!
And the "substitution rule for equality" could be proved!
Indeed, in a first step we can prove
a = b -> Ax(x e a <-> x e b).
from our definition of "=" above and the axioms of (our version of) ZFC.
(Proof omitted.)
Hence we actually would have now in our system the two theorems:
a = b -> Ax(a e x <-> b e x)
and
a = b -> Ax(x e a <-> x e b).
It's rather obvious that these are a sufficient basis for a general
substitution (meta-)theorem.
Now, concerning an alternative definition of identity (proposed by
mitch), you wrote:
>
> I am personally bummed by the non-provability of Ax[x e a<->x e b] ->
> Ax[a e x<->b e x]. [...] If two sets look "downward"-indiscernible, how
> are they managing to get "upward"-individuated? In real/true/correct
> actual ZF, the answer of course is THEY DON'T, but the fact that all
> the rest of the ammo of ZFC still doesn't force it is a big disappoint-
> ment.
>
No need to be disappointed. When we define "=" with Ax(a e x <-> b e x),
the "rest of the ammo of ZFC" DOES force a = b -> Ax(x e a <-> x e b).
F.
P.S.
In the light of was just said, the following claim by mitch is proved to
be *completely* baseless:
"Given that eliminability of identity requires an axiom not
normally found in set theories, I would like to know how you
justify the axiom that you have never explicitly presented
while making your many claims?"
There just IS NO "axiom not normally found in set theories" (when
adopting the definition of "=" proposed above). :-)
George Greene
was WAY too many. Don't they usually call those "hom-sets"
(short for homomorphism-sets) instead of sorts? If there
were going to be another sort then I would expect hom-set ITSELF
to be a sort.
> mattias...@hotmail.com (Mattias Wikstr?m) wrote in message news:<e47110b3.03101...@posting.google.com>...
>
> > The advantage with using a many-sorted theory is that one does not
> > have to deal with "nonsence" expressions like ff, where f:A->B and A
> > and B are different objects. This makes the axioms simpler. In fact,
> > all the axioms needed are the following:
> > (fg)h=f(gh)
> > f id=f
> > id f=f
You are about to disprove that by requiring more below:
> > The primitives here are composition and identity:
> > _ _ : (A->B), (B->C) |- (A->C)
> > id : (A->A)
But ":" and "->" are not primitives of FOL.
Does every multi-sorted 1st-order logic need these symbols
in order to express sortal constraints?
r...@rbjones.com (Roger Bishop Jones) wrote in message news:<d7e5c214.0310...@posting.google.com>...
>
> You have moved some of the "complexity" in a theory of
> categories from the non-logical axioms into the logic.
> Since you have not presented the logic, it is unclear
> whether on balance there is any gain.
I fully agree with RBJ, for this round.
Roger Bishop Jones
> I really thought a whole separate sort for every pair of objects
> was WAY too many. Don't they usually call those "hom-sets"
> (short for homomorphism-sets) instead of sorts? If there
> were going to be another sort then I would expect hom-set ITSELF
> to be a sort.
I think that's what I would expect from a treatment
of category theory in many sorted first order logic.
One sort for objects and one for morphisms.
I have recently been working on the axioms for a
categorial foundation system in HOL which uses these
two sorts.
A treatment in which there is a "sort" for every
pair of objects would normally be termed a type-theory
since you then need expressions to denote types
rather than simply a number of sort names.
> > mattias...@hotmail.com (Mattias Wikstr?m) wrote in message news:<e47110b3.03101...@posting.google.com>...
> >
> > > The advantage with using a many-sorted theory is that one does not
> > > have to deal with "nonsence" expressions like ff, where f:A->B and A
> > > and B are different objects. This makes the axioms simpler. In fact,
> > > all the axioms needed are the following:
> > > (fg)h=f(gh)
> > > f id=f
> > > id f=f
>
> You are about to disprove that by requiring more below:
> > > The primitives here are composition and identity:
> > > _ _ : (A->B), (B->C) |- (A->C)
> > > id : (A->A)
>
> But ":" and "->" are not primitives of FOL.
> Does every multi-sorted 1st-order logic need these symbols
> in order to express sortal constraints?
I don't myself recall seeing many sorted first order
languages with these features, though they are usual
in type theories.
Another question to ask is whether there are any
foundation systems which are based in a category
theory formulated in this way.
Roger Jones
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
Kelley wrote:
"Equality is always used in the sense of logical identity;
'1 + 1 = 2' is to mean that '1 + 1' and '2' are names of the
same object. Besides the usual axioms for equality an
unrestricted substitution rule is assumed: in particular
the result of changing a theorem by replacing an
object by its equal is again a theorem.
>
> "The usual axioms for equality"?? WTF does he MEAN??
>
Well, he referred to Quine's "Mathematical Logic" in this context. Now I
recently stumbled over the following quote by Quine (in his "Set Theory
and its Logic"), which almost sounds like an answer to your question :-)
"Adequate axoms of identity are 'x = x' and all instances
of the schema "x = y . Fx .-> Fy' of /substitutivity of
identity/."
Indeed these are just the usual axioms (if any). Actually, this backs up
my opinion concerning this question (already expressed):
"IMHO he is referring to the two axioms/rules you mentioned.
(I *guess*, he had Quine's 'Mathematical Logic' in mind, when
talking about 'the usual axioms for equality'.)"
F.
Funny thing, Fraenkel wrote in the Historical Introduction of Bernays'
Axiomatic Set Theory (1958):
"...the following attitudes are possible.
1) Equality in its _logical meaning as identity_ Zermelo adopts
this attitude by calling x and y equal 'if they denote the same
thing (object)'."
Kelley (1955):
"Equality is always used in the sense of logical identity;
'1 + 1 = 2' is to mean that '1 + 1' and '2' are names of the
same object."
It's OBVIOUS that they both have the same approach in mind.
G. Frege
George:
First-order logic WITH equality has TWO MORE INFERENCE RULES
than first-order logic without equality. They are the ones
that make '=' a logical symbol AS OPPOSED to something
definable.
They {usually] are
|- Ax[x=x] (*)
and x=y |- phi(x)->phi(y) (**)
Frege:
This is exactly what Kelley had in mind when he claimed:
"One is tempted to [define] equality [in set theory],
thus dispensing [...] with all logical presuppositions
about equality [i.e. (*) and (**)]. This is perfectly
feasible. However, [then] there would be no unlimited
substitution rule for equality and one would have to
assume as an axiom: If x e z and y = x, then y e z."
George:
You are not far enough inside Kelley's mind to
know that.
Frege:
I guess, my interpretation is backed up by the following
quote of Quine's "Set Theory and its Logic"
"Adequate axoms of identity are 'x = x' and all instances
of the schema "x = y . Fx .-> Fy' of /substitutivity of
identity/."
since Kelley (a) also talked about "the usual axioms for
equality" and (b) mentioned that
"...it is possible to write the theorems in terms of logical
constants, logical variables, and the constants of the system,
and the proofs may be derived from the axioms by means of rules
of inference."
F.
George Greene
:
: "Equality is always used in the sense of logical identity;
: '1 + 1 = 2' is to mean that '1 + 1' and '2' are names of the
: same object. Besides the usual axioms for equality an
: unrestricted substitution rule is assumed: in particular
: the result of changing a theorem by replacing an
: object by its equal is again a theorem.
I replied,
: >
: > "The usual axioms for equality"?? WTF does he MEAN??
: >
G. Frege <no_...@aol.com> writes:
: Well, he referred to Quine's "Mathematical Logic" in this context. Now I
: recently stumbled over the following quote by Quine (in his "Set Theory
: and its Logic"), which almost sounds like an answer to your question :-)
:
: "Adequate axoms of identity are 'x = x' and all instances
: of the schema "x = y . Fx .-> Fy' of /substitutivity of
: identity/."
:
: Indeed these are just the usual axioms (if any). Actually, this backs up
: my opinion concerning this question (already expressed):
:
: "IMHO he is referring to the two axioms/rules you mentioned.
: (I *guess*, he had Quine's 'Mathematical Logic' in mind, when
: talking about 'the usual axioms for equality'.)"
:
:
: F.
One reason I didn't get this automatically is that "axiom" is just
the wrong word, here. These are indeed adequate as "axioms"
OF IDENTITY, but we are talking about a context in which what we
are CONCERNED about are the axioms OF SET THEORY and where equality
is in fact governed NOT so much by axioms AS by *RULES OF INFERENCE*,
i.e., the underlying LOGIC is being taken as classical FOPL *with*
EQUALITY, with equality PREdefined INTO THE LOGIC, as OPPOSED to
being defined by axioms. There are still books in 2003 that don't
split this hair (or pick this nit), but that doesn't mean that the
world wouldn't be a better place (or at least one more easily
understood by new questors) if they did.
George Greene
: On Sun, 05 Oct 2003 15:43:58 +0200, G. Frege <no_...@aol.com> wrote:
:
: George:
: First-order logic WITH equality has TWO MORE INFERENCE RULES
: than first-order logic without equality. They are the ones
: that make '=' a logical symbol AS OPPOSED to something
: definable.
:
: They {usually] are
:
: |- Ax[x=x] (*)
: and x=y |- phi(x)->phi(y) (**)
:
: Frege:
: This is exactly what Kelley had in mind when he claimed:
:
: "One is tempted to [define] equality [in set theory],
: thus dispensing [...] with all logical presuppositions
: about equality [i.e. (*) and (**)]. This is perfectly
: feasible. However, [then] there would be no unlimited
: substitution rule for equality and one would have to
: assume as an axiom: If x e z and y = x, then y e z."
:
: George:
: You are not far enough inside Kelley's mind to
: know that.
Oh, come on. That is not the way it ultimately went down.
I thanked you for pointing this out by way of educating mitch.
: Frege:
: I guess, my interpretation is backed up by the following
: quote of Quine's "Set Theory and its Logic"
:
: "Adequate axoms of identity are 'x = x' and all instances
: of the schema "x = y . Fx .-> Fy' of /substitutivity of
: identity/."
:
: since Kelley (a) also talked about "the usual axioms for
: equality" and (b) mentioned that
:
: "...it is possible to write the theorems in terms of logical
: constants, logical variables, and the constants of the system,
: and the proofs may be derived from the axioms by means of rules
: of inference."
:
:
: F.
Kelley analyzed the situation correctly. If I didn't see
it first then I did see it later and I did thank you for
clarifying it. This is old! Why is back?
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>
> One reason I didn't get this automatically is that "axiom" is just
> the wrong word, here. These are indeed adequate as "axioms"
> OF IDENTITY, but we are talking about a context in which what we
> are CONCERNED about are the axioms OF SET THEORY and where equality
> is in fact governed NOT so much by axioms AS by *RULES OF INFERENCE*,
> i.e., the underlying LOGIC is being taken as classical FOPL *with*
> EQUALITY, with equality PREdefined INTO THE LOGIC, as OPPOSED to
> being defined by axioms. There are still books in 2003 that don't
> split this hair (or pick this nit), but that doesn't mean that the
> world wouldn't be a better place (or at least one more easily
> understood by new questors) if they did.
>
I see.
Actually, Lemmon writes (in the Introduction of his "Introduction to
Axiomatic Set Theory", 1968):
"[...] So much for the language L (though of course there
are many more definitions to come). What of the /logic/
of it? Here we shall be rather casual, in view of our
assumption that the reader is already familiar with
predicate calculus including identity. /Either/ you are
to assume that we grant ourselves some set of natural
deduction rules for predicate calculus with identity /or/
you are to assume that the formal theory takes as
axioms some set of wffs sufficient to provide the
standard theorems of that theory. In any case, our
proofs of set-theoretic theorems in the sequel remain
relatively informal. But the reader should satisfy him-
self, at least in the initial stages, that these proofs
provide the skeleton for a strictly formal proof in
conformity with whatever formulation of the under-
lying logic he knows. It would be intolerable to present
all our proofs formally - as well as undesirable. So we
shall content ourselves with justifications, in proofs,
of the form 'by propositional logic', 'by predicate
logic', 'by identity theory'. But the theoretical fact
should not be forgotten, that /all our theorems are
consequences of our axioms [of set theory] by elementary
reasoning/, i.e. by techniques of proof belonging to
predicate calculus with identity."
Lemmon again:
"But what does = mean between classes? The usual view, which
we shall follow, is that classes v and w are considered
identical if and only if they have exactly the same members.
For example, the classes
{Julius Caesar, 3}
and
{The man killed by Brutus, 4-1}
are identical, since they have exactly the same two
members. They are also identical with the class
{Julius Caesar, 5-2, 6-3, 7-4, 8-5}.
This view of identity means, in effect, that we are
accepting the principle
(8) x = y <-> Az(z e x <-> z e y),
that x is identical with y if and only if anything is a
member of x if and only if it is a member of y. (8)
suggest the possibility of /defining/ identity in terms of
class membership (together with propositional calcu-
lus connectives and the universal quantifier), and this
course is followed in several brands of set theory.
There are both gains and disadvantages in such a course.
Here, again, we make a choice: to take identity as a
primitive notion for what follows, and regard it as part
of our underlying logical framework."
(E. J. Lemmon, Introduction to Axiomatic Set Theory)
F.
G. Frege
<gre...@greeneg-cs.cs.unc.edu> wrote:
>
> Kelley analyzed the situation correctly.
>
So I actually /have to/ admit that his language is rather sloppy
(partly); and you /are/ right (imho) to criticize that. (Even in 1955
he could have done better. On the other hand... you know, he was a
full-blooded mathematician, and not a logician.)
>
> This is old! Why is back?
>
Sorry, for that. Just wanted to post some sort of summary. (Actually, it
/really/ was triggered by Quine's quote I came across /recently/.)
F.
George Greene
(Quoting Lemmon)
: This view of identity means, in effect, that we are
: accepting the principle
:
: (8) x = y <-> Az(z e x <-> z e y),
:
: that x is identical with y if and only if anything is a
: member of x if and only if it is a member of y. (8)
: suggests the possibility of *defining* identity in terms of
: class membership (together with propositional calcu-
: lus connectives and the universal quantifier), and this
: course is followed in several brands of set theory.
: There are both gains and disadvantages in such a course.
: Here, again, we make a choice: to take identity as a
: primitive notion for what follows, and regard it as part
: of our underlying logical framework."
:
: (E. J. Lemmon, Introduction to Axiomatic Set Theory)
Well, I mean, obviously, I am glad that my perspective matched
that of SOME old master, somewhere. I mean, some is better than none.
What I was really concerned about in the thread, though, was mitch's
perspective. Lemmon's discussion here very much highlights the fact
that this choice (of whether the underlying FOL shall be With equality
or withOut) MUST be MADE!
Mitch spent a large part of the discussion neither knowing nor caring
about the choice. When it was finally rammed through his thick skull,
he whined, "you can just retreat to FOL without equality", but that is
actually non-trivial because the = symbol OCCURS AGAIN IN THE PAIRING
AXIOM! That occurrence is in fact why one NEEDS a definition of equality
(*either* via the axiom of extensionality or in the underlying logic).
I tried to point out to mitch way back at the beginning of the thread
that there are actually 3 semantically different KINDS of equality.
But he is the one who accuses ME of lacking the vocabulary to discuss
structural properties of set theory. Well, at least I know the
difference between FOL with equality and without. And at least
I understand why equality is different as bridge-predicate vs.
as instantiation of a bound variable.
Mattias Wikstr?m
> gre...@cs.unc.edu (George Greene) wrote in message news:<992b156f.03101...@posting.google.com>...
> > I really thought a whole separate sort for every pair of objects
> > was WAY too many. Don't they usually call those "hom-sets"
> > (short for homomorphism-sets) instead of sorts?
In a locally small category C, the set of arrows with source S and
target T is denoted Hom_C(S, T) and is called a hom-set. If C' is a
subcategory of C, Hom_C'(S, T) need not be the same as Hom_C(S, T).
> If there
> > were going to be another sort then I would expect hom-set ITSELF
> > to be a sort.
>
> I think that's what I would expect from a treatment
> of category theory in many sorted first order logic.
> One sort for objects and one for morphisms.
> I have recently been working on the axioms for a
> categorial foundation system in HOL which uses these
> two sorts.
>
> A treatment in which there is a "sort" for every
> pair of objects would normally be termed a type-theory
> since you then need expressions to denote types
> rather than simply a number of sort names.
I did not know the difference between "sort" and "type" when I wrote
my post. Thanks for the explanation.
>
> > > mattias...@hotmail.com (Mattias Wikstr?m) wrote in message news:<e47110b3.03101...@posting.google.com>...
> > >
> > > > The advantage with using a many-sorted theory is that one does not
> > > > have to deal with "nonsence" expressions like ff, where f:A->B and A
> > > > and B are different objects. This makes the axioms simpler. In fact,
> > > > all the axioms needed are the following:
> > > > (fg)h=f(gh)
> > > > f id=f
> > > > id f=f
> >
> > You are about to disprove that by requiring more below:
Theese are not axioms, but merely sortings. The counterpart for a
single-sorted theory is information on how many arguments each
predicate takes.
> > > > The primitives here are composition and identity:
> > > > _ _ : (A->B), (B->C) |- (A->C)
> > > > id : (A->A)
> >
> > But ":" and "->" are not primitives of FOL.
> > Does every multi-sorted 1st-order logic need these symbols
> > in order to express sortal constraints?
The ":" symbol is basic whenever one has more than one sort. The "->"
symbol is not.
>
> I don't myself recall seeing many sorted first order
> languages with these features, though they are usual
> in type theories.
I wonder what one really needs. Also, I wonder what one needs when
extending the theory to include, for example, the notation AxB for a
product of objects A and B.
>
> Another question to ask is whether there are any
> foundation systems which are based in a category
> theory formulated in this way.
I find this the most elegant and natural way of formulating category
theory. As far as foundations are conserned, I do not see how the way
we formulate category theory could be of any importance.
Mattias
Alfred Einstead
> The advantage with using a many-sorted theory is that one does not
> have to deal with "nonsence" expressions like ff, where f:A->B and A
> and B are different objects.
It can be dealt with internally within the single-sorted regime.
AB = 0 = BA, if A, B are different
AA = A
A0 = 0 = 0A, for all A
f = fA = Bf, precisely when f: A -> B.
Thus
ff = fABf = f0f = 0.
> This makes the axioms simpler. In fact,
> all the axioms needed are the following:
> (fg)h=f(gh)
which is essentially all that's required, in addition, here.
You can go the route of MacLane, using 0 to take care of
"undefined".
Roger Bishop Jones
> > [RBJ]
> > I don't myself recall seeing many sorted first order
> > languages with these features, though they are usual
> > in type theories.
>
> I wonder what one really needs. Also, I wonder what one needs when
> extending the theory to include, for example, the notation AxB for a
> product of objects A and B.
An advantage of a first order axiomatisation is that
once you have stated the non-logical axioms the complete
formal system is fully defined and people will know
what they are dealing with.
This advantage extends to a many-sorted first order
theory with a finite set of sort names and no sort
constructors.
However, as soon as you enter the realm of type
theories this advantage is lost.
If you specify the non-logical axioms for a formalisation
in a type theory, and don't specify the type theory
then no-one can have much clue what the formal
system is or make a judgement about whether it does
formalise the intended subject matter or about its
complexity.
This is because there are lots of different typematti...@hotmail.com (Mattias Wikstr?m) wrote in message news:<e47110b3.03102...@posting.google.com>...
> > [RBJ]
> > I don't myself recall seeing many sorted first order
> > languages with these features, though they are usual
> > in type theories.
>
> I wonder what one really needs. Also, I wonder what one needs when
> extending the theory to include, for example, the notation AxB for a
> product of objects A and B.
An advantage of a first order axiomatisation is that
once you have stated the non-logical axioms the complete
formal system is fully defined and people will know
what they are dealing with.
This advantage extends to a many-sorted first order
theory with a finite set of sort names and no sort
constructors.
However, as soon as you enter the realm of type
theories this advantage is lost.
If you specify the non-logical axioms for a formalisation
in a type theory, and don't specify the type theory
then no-one can have much clue what the formal
system is or make a judgement about whether it does
formalise the intended subject matter or about its
complexity.
This is because there are lots of different type
theories and the devil is in the detail.
Presumably you are suggesting a type theoretic
treatment of category theory because you have
seen this done somewhere, and if so you could
either refer us to the original or else summarise
for us the salient details of the logical system.
> > [RBJ]
theories and the devil is in the detail.
Presumably you are suggesting a type theoretic
treatment of category theory because you have
seen this done somewhere, and if so you could
either refer us to the original or else summarise
for us the salient details of the logical system.
> > [RBJ]
> > Another question to ask is whether there are any
> > foundation systems which are based in a category
> > theory formulated in this way.
>
> I find this the most elegant and natural way of formulating category
> theory. As far as foundations are conserned, I do not see how the way
> we formulate category theory could be of any importance.
It is of importance in this particular context
because the original question was asking about
the use of category theory as a foundation for
mathematics, which is a much more complicated
business than providind an axiomatisation
of category theory (though whether George Green
appreciated this when he posted the question is
not clear).
There is also the distinction between a category
theoretic foundation for mathematics and a foundation
for category theory, which may or may not be the
same thing.
Neither is as simple a matter as a first order
axiomatisation of category theory, which would
not be a suitable context in which to do any
serious category theory.
(and nor would be a many-sorted or type-theoretic
presentation which improved only the elegance
of presentation)
Roger Jones
Mattias Wikstr?m
> Presumably you are suggesting a type theoretic
> treatment of category theory because you have
> seen this done somewhere, and if so you could
> either refer us to the original or else summarise
> for us the salient details of the logical system.
See Huet, G. "Cartesian Closed Categories and Lambda Calculus".
/Logical Foundations of Functional Programming/, Huet, G., ed., pp.
7-23. The UT Year of Programming Series, Hamilton Richards Jr., ed.
Addison-Wesley, 1990.
Mattias
Roger Bishop Jones
I havn't seen that one, but I do have a copy of Huet's
lecture notes dated 1986 which has a chapter on category
theory along the lines you have described.
As far as the connection with the foundations of maths
is concerned, this line of development usually takes
you into constructive rather than classical mathematics.
(in the notes I have you end up in the Calculus
of Constructions).
However, in the calculus of constructions there is
no sense that you are "doing category theory"
(even though the semantics may be given in terms
of category theory).
I'm pretty unclear what people expect from
a categorical foundation for mathematics,
and I expect it varies a great deal from
person to person.
Roger Jones
Daryl McCullough
>As far as the connection with the foundations of maths
>is concerned, this line of development usually takes
>you into constructive rather than classical mathematics.
>(in the notes I have you end up in the Calculus
>of Constructions).
>However, in the calculus of constructions there is
>no sense that you are "doing category theory"
>(even though the semantics may be given in terms
>of category theory).
Hey! Somebody else who has heard of the calculus of constructions!
My favorite semantics for the calculus of constructions is Scedrov's
Partial Equivalence Relation semantics, which doesn't have anything
to do with category theory.
Basically, you have a set U of objects (they may be naturals, or they
could be Curry's combinators, or just about anything). You have a partial
binary operation "apply" on U (if U is the naturals, then apply(x,y) is
the output of running Turing machine program with index x on input y). A
"sort" is then a partial-equivalence relation on U (that is, it is
an equivalence relation on some subset of U, the "domain" of the
equivalence relation).
If A and B are sorts, then you define the sort A -> B as follows:
the domain of A->B is the set of all f in U such that
forall x,y in domain(A), if x ~~ y (according to equivalence
relation A) then apply(f,x) ~~ apply(f,y) (according to
equivalence relation B).
f1 and f2 are equivalent according to equivalence relation A->B
if for all x,y in domain(A), If x ~~ y (according to A) then
apply(f1,x) ~~ apply(f2,y) (according to B).
Polymorphic types are defined as follows: If F(A) is a function
from sorts to sorts, then
Pi A:sort . F(A)
is the partial equivalence relation defined by:
domain (Pi A:sort . F(A)) = intersection over all sorts A of domain(F(A)).
x ~~ y if they are equivalent according to each sort F(A).
Using this interpretation, you can prove that the only elements of
the "natural number" sort are the Church numerals, the only elements
of the "boolean" are the two truth values, the only elements of the
"ordered pair" type are indeed ordered pairs, etc.
--
Daryl McCullough
Ithaca, NY
Roger Bishop Jones
> My favorite semantics for the calculus of constructions is Scedrov's
> Partial Equivalence Relation semantics, which doesn't have anything
> to do with category theory.
<nice description omitted>
There must be a general result (though I
have never seen it) which says that any
consistent formal system has a term model.
(and a semantics in terms of it)
This may be a mess for some formal systems,
but for things based on the lambda calculus
term models are aguably the simplest and
most natural, and I have never understood
what Dana Scott had against them.
What you describe sounds to me like a pretty
natural "term model" so I would expect it
to be the easiest semantics for the Calculus
of Constructions.
I've never actually looked closely at any
of the accounts of its semantics which have
come my way, they have all looked way too
hard for me, but I'm pleased to hear that
someone has cut the crap and given it straiqht.
Roger Jones
George Greene
> da...@atc-nycorp.com (Daryl McCullough) wrote in message news:<bnrjh...@drn.newsguy.com>...
>
> > My favorite semantics for the calculus of constructions is Scedrov's
> > Partial Equivalence Relation semantics, which doesn't have anything
> > to do with category theory.
>
> <nice description omitted>
>
> There must be a general result (though I
> have never seen it) which says that any
> consistent formal system has a term model.
Well, I don't know about "any formal system"
("formal system" does not have a precise
specific definition; it is a very general term),
but there is a result saying that every consistent
first-order theory has a model, and there is probably
an algorithm for generating a "term model" from that.
But what exactly do you MEAN by "a term model"?
In my subfield, when we say "term", we mean a term
of a first-order language, just something like p(x,y)
where p is a function (as opposed to P(x,y), where P is
a predicate, and P(x,y) is a literal or an atom and NOT a term).
The easiest way to get a "term model" in that context is to
just pick a domain of interpretation in which everything is
one of the terms of the language, i.e., in which every term is
interpreted as itself.
But it is clear here that you guys are talking about
a DIFFERENT meaning of "term".
> (and a semantics in terms of it)
> This may be a mess for some formal systems,
> but for things based on the lambda calculus
> term models are aguably the simplest and
> most natural, and I have never understood
> what Dana Scott had against them.
>
> What you describe sounds to me like a pretty
> natural "term model" so I would expect it
> to be the easiest semantics for the Calculus
> of Constructions.
This has got to be the right time to ask people to Google the
Curry-Howard isomorphism.
Roger Bishop Jones
> r...@rbjones.com (Roger Bishop Jones) wrote in message news:<d7e5c214.03103...@posting.google.com>...
> > da...@atc-nycorp.com (Daryl McCullough) wrote in message news:<bnrjh...@drn.newsguy.com>...
> >
> > > My favorite semantics for the calculus of constructions is Scedrov's
> > > Partial Equivalence Relation semantics, which doesn't have anything
> > > to do with category theory.
> >
> > <nice description omitted>
> >
> > There must be a general result (though I
> > have never seen it) which says that any
> > consistent formal system has a term model.
>
> Well, I don't know about "any formal system"
> ("formal system" does not have a precise
> specific definition; it is a very general term),
> but there is a result saying that every consistent
> first-order theory has a model, and there is probably
> an algorithm for generating a "term model" from that.
It is certainly well established that every
consistent first order theory has a term model.
Term models are often used in the completeness
proof. I was musing about formal systems in general.
Formal systems have been given suitably general
definitions. Emile Post provided one using his
"post production systems", and this has given rise
to a generalisation of the concept of consistency
which is applicable to formal systems in which
negation does not occur (a formal system is consistent
in the sense of Post if there is any sentence of
the language which is not derivable using the
inference rules).
> But what exactly do you MEAN by "a term model"?
> In my subfield, when we say "term", we mean a term
> of a first-order language, just something like p(x,y)
> where p is a function (as opposed to P(x,y), where P is
> a predicate, and P(x,y) is a literal or an atom and NOT a term).
> The easiest way to get a "term model" in that context is to
> just pick a domain of interpretation in which everything is
> one of the terms of the language, i.e., in which every term is
> interpreted as itself.
That's the kind of I have in mind.
You just have to liberalise the idea enough for it to
be more widely applicable.
So instead of insisting on first order terms, you
allow terms of the language in question, and to allow
for the language to have its syntax defined using some
other concept than term you allow whatever syntactic
entities are available.
In the particular case of the semantics for CCC which
I was talking about I think the semantic domain was
the natural numbers. But I still think of it as a term
model, because the natural numbers are one-one with terms,
and it looked to me like they were surrogates for terms.
> But it is clear here that you guys are talking about
> a DIFFERENT meaning of "term".
>
> > (and a semantics in terms of it)
> > This may be a mess for some formal systems,
> > but for things based on the lambda calculus
> > term models are aguably the simplest and
> > most natural, and I have never understood
> > what Dana Scott had against them.
Here the term models are made using lambda terms.
> > What you describe sounds to me like a pretty
> > natural "term model" so I would expect it
> > to be the easiest semantics for the Calculus
> > of Constructions.
Here you could to it with the bits of syntax
used in CCC (can't remember the details).
However, without checking it as closely as I
should, I jumped to the conclusion that the semantics
given over the natural numebers was essentially
a term model in disguise.
> This has got to be the right time to ask people to Google the
> Curry-Howard isomorphism.
Well you certainly need that to understand the
Calculus of Constructions, but I'm don't think
it says anything about models.
Roger Jones
Roger Bishop Jones
> Hey! Somebody else who has heard of the calculus of constructions!
I might have mentioned at this point that I have
a web page on Barendregt's lambda cube:
http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm
and also one on his pure (aka generalised) type systems:
http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
(and now have)
Roger Jones