Date: Feb 19, 2013 5:24 PM Author: fom Subject: Re: distinguishability - in context, according to definitions 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?