Re: What is a proof, exactly?

From: J.E. (troubled6man_at_yahoo.com)
Date: 12/16/04 

Date: 16 Dec 2004 09:33:33 -0800

KRamsay wrote:
> In article <1102954242.069991.172750@z14g2000cwz.googlegroups.com>,
"J.E."
> <troubled6man@yahoo.com> writes:
> |I've heard that before, but is it really required.
>
> You've heard *what* before? You didn't quote anything.

That you need eqality/extension at all. But I never understoof the
rationale. We have an iff, so the first thing one can with the axiom
of equality/extension is replace all FOL sentences and formulas with
equality with equivalent (given axiom of equality/extension) sentences
and formulas without equality. And once you've done that you could
take that axiom and throw it in the garbage, never needing it again.
For instance the "definition" of S being a bijection becomes (As (seS
=> Ea Eb (a,b)eS))&AaAbAcAd( ((a,b)eS & (c,d)eS) => ( (Af (fea <=>
fec)) <=> (Af (feb <=> fed)) ) ) instead of the original (As (seS => Ea
Eb (a,b)eS))&AaAbAcAd( ((a,b)eS & (c,d)eS) => (a=c <=> b=d) )

> I'm guessing from the context that you are referring to the version
> of the axiom of extensionality that one uses when equality is treated
> as a defined term. Certainly this version of the axiom is a
consequence
> of the other one, and there's no way of proving it from just axioms
of
> ZF besides extensionality.

I'm asking "why do we have to prove it at all", if you had a FOL
without equality, how can the question even "be asked" within the
language, maybe
"Ey (yez Ax ~xey) & Ay (yez => Ax ~xey)" could be true of some z but
the formula "Ay (yez <=> Ax ~xey)" could be false? Which leads to my
bootstraping example where I consider ONLY the sentences of the form
"Ez Ay yez <=> S(y,z)" to be candidates for sethood. If I bootstrap
like that, can the axiom of equality be redundant based on the
syntactical form of the candidate sets? Which leads to the question of
whether there is a syntactical form for the candidate sets which then
requires no axioms, and just the rules of logic.

Without considering the models without the axiom of equality, it would
be rather difficult for me to find a way to make it superfluous.

> You seem to be trying to show here that it's irrelevant somehow,
> but your reasoning is very handwavy. Perhaps the crux of it is
> this:
>
> [...]
> |I think the idea of whether there is one empty set or many is silly
and
> |unecissary, since a FO language with no logical equality and just a
> |binary relation can't distinguish between any sets x that make the
> |sentance "Az (z in x <=> S[z])" true,
>
> Incorrect. There's no guarantee that such sets are indistinguishable
> by first-order sentences. They may have the same members, but they
> may still be distinguishable by not being members of the same other
> sets themselves.
>
> If the form of the axiom of extensionality that I gave holds true,
> then while in principle it's still possible for there to be nonequal
> sets having the same members, it's not very relevant, since one can
> simply identify them. By identify them, I mean consider instead
> equivalence classes under the relationship of extensional equality
> (having the same members). These equivalence classes would then
> satisfy the usual axiom of extensionality.
>
> That construction relies upon the axiom holding, though. If the
> equivalence relation is ~, and a~b, c~d, then we know by the
> definition of ~ that a is a member of c iff a is a member of d,
> and b is a member of c iff b is a member of d. But we also need
> to know that a is a member of c iff b is a member of c, which
> doesn't automatically follow unless the axiom holds. With the
> axiom, a is a member of c iff b is a member of d and the simple
> equivalence-class construction goes through.
>
> If one leaves this axiom out, however, things become more
> complicated. There is a way of converting a set theory which
> doesn't satisfy extensionality into one that does, but it involves
> more than simply identifying sets having the same members. Not only
> do you identify sets having the same members, but also sets which
> originally had different members, but were caused to have the same
> members once their members whose members were the same were
identified
> with each other. And so on-- it can be thought of as a transfinite
> induction.
>
> Please try a little harder to think this kind of thing through
> before concluding that what most people say about it is "silly".

I think you've missed the point entirely. I know that it's not "as
easy" as making equivalence classes of sets, because I consider that
very idea a week ago long before posting the idea to usenet. I didn't
say that I wanted an equivalent theory. Consider the qeustion to be
about intended models if that's easier. You can say that your intended
model was such that a nonlogical = relation can be defined such that
AxAy (x=y <=> (Az (xez <=> yez))&(Az (zex <=> zey)) ) is true a true
statement of your model (and then you might as well have had an axiom
to make that be true). But I can just ask "why that model", or "why
that axiom", which is what I was trying to do. What I meant about
silly was "an unrelective assertion", a "non-sequitor", or a "'cause it
does" level of response. Being silly by being cavalier, not by being
stupid. If someone is clear about only wanting models where that
statement is true as intended models, then that's not silly at all, but
it will lead to me asking about these intended models, what they are
like, why they like them, and what do they not like about other models,
etc. So for instance: if one had a model where "there was no such
relation = that could make AxAy (x=y <=> (Az (xez <=> yez))&(Az (zex
<=> zey)) ) true", then why is that not a good model? That would be a
question for someone that wasn't merely being silly about "wanting the
axiom". So with the usual axiom or the equivalent new one that asserts
the consistency of asserting the existence of a relation like =, any
set such that all of it's memebrs are empty is equal to the others, but
a priori I don't see why we should choose to either disallow or fail to
distinguish a set that contains AN empty set from a set that contains
ALL the empty sets, from one that contains "some but not all" empty
sets, and I don't see any reason to care which one we have for
classical math, since classical math assume that all those sets
described where the same anyway, so having more in a consistent manner
just gives a more plentiful universe without breaking anything. One of
the those set satisifies Az (zey <=> Ax ~xez), but there is no reason
to expect that only that set was useful, but assering your non-logical
axiom would restrict us to models where the other two sets don't exist.
They all are naive correspondances from the syntactic form {{}}, and I
can reason about all three sets with a FO language with a binary
relation and no equality to ask questions like Ax Ey S[x,y].
Uniqueness, e.g. S[x,y]=>(x=y) can be rephrased from the logical level
to the phrase S[x,y]=>(Az (zex <=> zey)), at the level of the binary
relation and classical mathematics works just as well, it won't have
the same intended meaning, but the theorems of mathematics hold over
just fine for the intended sets. The point is that there is a level at
which people can distinguish sets (contains all empty sets) versus
(contains some empty sets but not all) that can be different than the
level at which the FO sentences dinstinguish between them. People can
reflect on many levels. Consider the following case that may or may
turn out to be useful: if one considered the class of all sets k such
that ~kex, then you could have a subuniverse that treats x like the
empty set, and if the subclass of that subuniverse is appropriately
grounded like the whole universe is sometimes considered to be grounded
to the empty set, then maybe applying a theorem about the whole set
universe to that isomorphic class would produce an interesting result.
How am I supposed to know a priori that that is never useful? I am I
just dumb and it's obvious to everyone else?

I'm worried that we are unecissarily cutting off validity preserving
proof techniques like that isomorphism of classes. In that particular
case, I expect that a standard proof would exist, but that leads to the
whole idea of nonstandard proofs. In nonstandard analysis, any
statement without the term "standard" that has a nonstandard proof,
also has a standard proof. But what if someone made a technique such
that instead of saying "existence of weird proof implies existence of
normal proof" but instead said "existence of weird proof implies truth
of statement even if statement has no normal proof", then this would be
a bona fide useful new thing. I don't know if new axioms, less axioms,
or a stronger logic (like IF logic) could do these things. But I also
don't know that they can't, and I'd like to either know that they can't
or have the supposition that they might be taken seriously. That's all.

Relevant Pages

  • Re: Largest Set in ZFC?
    ... declare that there exists a set that has no members. ... But if we wish the '0' in the infinity axiom to denote the empty set, ...
    (sci.logic)
  • Re: ZFC? countable?uncountable?
    ... I said that the power set axiom only proves that there exists the ... us is what properties the members of the power set of x have other ... stating the uncountability of the power set of N does not ...
    (sci.math)
  • Re: ZF subtheory of T
    ... Of course a union b is the class of exactly all members of a and b. ... Actually a fifth axiom can be added which is the axiom schema of Large ...
    (sci.logic)
  • Re: ZF subtheory of T
    ... Of course a union b is the class of exactly all members of a and b. ... minus regularity pluse the axiom for all x: ...
    (sci.logic)
  • Re: The MetaMathematical Theorem that Almost Was
    ... >> Prove that you can't prove that the empty set exists. ... in what contest? ... By the axiom of extensionality, ... there is exactly one set with no members. ...
    (sci.logic)