Math Forum Discussions

fom

Posts: 1,037
Registered: 12/4/12

Re: distinguishability - in context, according to definitions
Posted: Feb 19, 2013 5:24 PM

Plain Text

On 2/19/2013 6:50 AM, Shmuel (Seymour J.) Metz wrote:
> In <soOdnWuz7siUXbzMnZ2dnUVZ_rqdnZ2d@giganews.com>, on 02/17/2013
> at 11:45 PM, fom <fomJUNK@nyms.net> said:
>
>> In that book, the reflexive axiom is implemented by simply writing
>> down the identity. As an axiom of identity, it will not require
>> discharge. Thus, when one wants to say,
>
>> "Let a and b be such that not a=b."
>
>> One has in the derivation,
>
>> a=a
>> b=b
>> |-(a=b)
>
> That's not a derivation.

It may not be a great book, but it is what I have.

http://books.google.com/books/about/Symbolic_Logic.html?id=YBRgQgAACAAJ

The fragment was just for illustration.

Here are some samples to see his rules in practice:

Ex(Fx /\ x=y) |- Fy

|Ex(Fx /\ x=y)
||Fx /\ x=y
||Fx
||x=y
||Fy
|Fy

The first step introduces a contingency stroke
because its assumption wff is to the left of
the turnstile.
The second step introduces a contingency stroke
because the subwff is removed from the scope of
the quantifier.
The first and second steps are ordered assumption
steps.
The last step is the quantifier elimination and
discharges the contingency of the second step.

|- AxAy(x=y -> y=x)

|x=y
|x=x
|y=x
x=y -> y=x
Ay(x=y -> y=x)
AxAy(x=y -> y=x)

The first step is given a contingency stroke relative to
the presumed antecedent introduced to construct the wff.
The second step is the axiom of reflexiveness being applied.
The third step is the substitution into the second step wff
justified by the assumption in the first step.
The fourth step is the discharge with the contingency
accounted for by the conditional.

The rules for identity in his system of derivation
are:

=Intro
'a=a' is an axiom

=Elim
From phi and 'a=b', infer psi, where phi is atomic
and psi is obtained from phi by replacing one or
more occurrences of a in phi with b.

These have no contingency strokes and are considered
derivations in the system,

|- Ax(x=x)

x=x
Ax(x=x)

|- Ex(x=x)

x=x
Ex(x=x)

|- AxEy(x=y)

x=x
Ey(x=y)
AxEy(x=y)

Quantifier rules:

Direct:

AElim
From 'Ax(phi)', infer phi[x/y] if y is free for x in phi

EIntro
From phi[x/y], infer 'Ex(phi)', if y is free for x in phi

Structural:

AIntro
If the last step obtained so far has as its ordered
assumption wffs phi_1,phi_2,...,phi_n (n may be 0)
and if a step (preceding the last step or identical
with it) has the same ordered assumption steps as
does the last step and has as its wff phi and if
x is not free in phi_1,phi_2,...,phi_n: then, as a
new step, you may extend all contingency strokes of the
last step and write 'Ax(phi)'

Scheme

.
:
| phi_1
|.
|:
|...|phi_n
|...|.
|...|:
|...|phi (k-th step)
|...|.
|...|:
|...|psi ("last step")
|...|'Ax(phi)' ("new step")

where x is not free in phi_1,phi_2,...,phi_n

For n=0

.
:
phi
.
:
psi
'Ax(phi)'

EElim
If the last step obtained so far contains at least
one contingency stroke, has as its ordered assumption
wffs phi_1,phi_2,...,phi_n, has as its wff psi and
if a step (preceding the last step) has the same
ordered assumption steps as the (n-1)-th ordered
assumption-step of the last step and has as its
wff 'Ex(phi_n)' and if x is not free in
phi_1,phi_2,...,phi_(n-1) and if x is not free
in psi: then as a new step, you may extend
all contingency strokes of the last step except
the rightmost one and write psi

Scheme

.
:
|phi_1
|.
|:
|...|phi_(n-1) ((n-1)-th assumption step)
|...|.
|...|:
|...|'Ex(phi_n)'
|...|.
|...|:
|...||phi_n (n-th assumption step)
|...||.
|...||:
|...||psi ("last step")
|...|psi ("new step")

where x is not free in phi_1,phi_2,...,phi_(n-1),psi

>
>> 0.999...=0.999...
>> 1.000...=1.000...
>> |1.000...=0.999...
>> since the assertion is that the two
>> symbols are equal.
>
> Then that assertion has to be the first step in the derivation and you
> get the trivial
>
> 1.000...=0.999...
> |- 1.000...=0.999...
>

Granted, my illustration was without any rules, but, there is no use
of informative identity without prior contingency in a formal
derivation.

http://plato.stanford.edu/entries/identity-relative/#1

And, yes... I had to learn this the hard way.

As mathematicians, what we want to work with is something
like what Tarski introduced in 1971,

AxAy(x=y <-> Ez(x=z /\ z=y))

>> If one is interested in proofs that begin with quantified
>> statements and that end with quantified statements, then the
>> presumption is that every constant used in the proof
>> is definable relative to a description.
>
> It is quite common for a theory to include constants. They are
> different from notational conventions that one defines in terms of
> other symbols; their nature is constrained only by the axioms.

Yes. But, in what way?

If we sit in a roomful of dogs. And, if I continue
to refer to "the dog." You will ask, "Which dog?"

I say, "THE dog. Of course!" Because you see many dogs
in the room, it is clear that I am not describing the
situation sensibly.

By the received paradigm on these matters, "objects" are
"self-identical." Constants and singular terms purport
to refer to individuals.

Just because I "purported" to be speaking about "the dog"
did not make it so.

Mathematics deals with abstract objects. More importantly,
mathematics deals with systems of abstract objects, and,
it would seem with objects as they relate to one another
systemically.

When Dedekind devised his sequence of ordinal numbers,
he did not "purport" invariance. He formulated a theory
based on successive involutions. That is, he *modeled*
it:

Definition: A system |N is said to be simply
infinite when there exists as similar transformation
F of |N in itself such that |N appears as chain of
an element not contained in F(|N). We call this
element, which we shall denote in what follows by
the symbol '1', the base-element of |N and say the
simply infinite system is *set in order* by this
transformation F.

Dedekind's finite initial segments are not "strokes"
on a page. They are fixed in relation to a system
described by successive transformation.

Now, for comparison, here is Lesniewski's part
relation:

Axiom 1: If object P is a part of object P_1,
then object P_1 is not a part of object P.

Axiom 2: If object P is a part of object P_1,
and object P_1 is a part of object P_2, then
object P is a part of object P_2.

Although not at any forefront of research, there
have been people studying mereology for years.
They all follow the practices of first-order
logic and purport reference to singular objects.

But, when I write:

AxAy(xcy <-> (Az(ycz -> xcz) /\ Ez(xcz /\ -ycz)))

and it says the same thing, what I have done is
wrong because it is "circular" or "impredicative".
That sentence has a companion,

AxAy(xey <-> (Az(ycz -> xez) /\ Ez(xez /\ -ycz)))

Where others see improper mathematics, I see two
infinite schemas

AxAy(xcy <-> (...))

AxAy(xey <-> (...))

whose predicates have invariant interpretation
relative to substitutions.

I use these to form a proper notion of identity
based on topological separation (which is precisely
Frege's description of first-order identity) which
is concomitant with extensionality.

No one seems to grasp this because they are all
satisfied with "purporting".

In any case, my notion of constant is in relation
to a sense of "constancy" rather than to definitions
in use.

>
>> It is just that the other axioms for a set theory need
>> to take the universal class into account.
>
> There are set theories in which there is no such class.
>

Correct. But is that the kind of set theory which had
originally been envisioned?