```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=YBRgQgAACAAJThe 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|FyThe first step introduces a contingency strokebecause its assumption wff is to the left ofthe turnstile.The second step introduces a contingency strokebecause the subwff is removed from the scope ofthe quantifier.The first and second steps are ordered assumptionsteps.The last step is the quantifier elimination anddischarges the contingency of the second step.|- AxAy(x=y -> y=x)|x=y|x=x|y=xx=y -> y=xAy(x=y -> y=x)AxAy(x=y -> y=x)The first step is given a contingency stroke relative tothe 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 wffjustified by the assumption in the first step.The fourth step is the discharge with the contingencyaccounted for by the conditional.The rules for identity in his system of derivationare:=Intro'a=a' is an axiom=Elim From phi and 'a=b', infer psi, where phi is atomicand psi is obtained from phi by replacing one ormore occurrences of a in phi with b.These have no contingency strokes and are consideredderivations in the system,|- Ax(x=x)x=xAx(x=x)|- Ex(x=x)x=xEx(x=x)|- AxEy(x=y)x=xEy(x=y)AxEy(x=y)Quantifier rules:Direct:AElim From 'Ax(phi)', infer phi[x/y] if y is free for x in phiEIntro From phi[x/y], infer 'Ex(phi)', if y is free for x in phiStructural:AIntroIf the last step obtained so far has as its orderedassumption wffs phi_1,phi_2,...,phi_n (n may be 0)and if a step (preceding the last step or identicalwith it) has the same ordered assumption steps asdoes the last step and has as its wff phi and ifx is not free in phi_1,phi_2,...,phi_n: then, as anew step, you may extend all contingency strokes of thelast 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_nFor n=0.:phi.:psi'Ax(phi)'EElimIf the last step obtained so far contains at leastone contingency stroke, has as its ordered assumptionwffs phi_1,phi_2,...,phi_n, has as its wff psi andif a step (preceding the last step) has the sameordered assumption steps as the (n-1)-th orderedassumption-step of the last step and has as itswff 'Ex(phi_n)' and if x is not free inphi_1,phi_2,...,phi_(n-1) and if x is not freein psi: then as a new step, you may extendall contingency strokes of the last step exceptthe rightmost one and write psiScheme.:|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 useof informative identity without prior contingency in a formalderivation.http://plato.stanford.edu/entries/identity-relative/#1And, yes... I had to learn this the hard way.As mathematicians, what we want to work with is somethinglike 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 continueto refer to "the dog."  You will ask, "Which dog?"I say, "THE dog. Of course!"  Because you see many dogsin the room, it is clear that I am not describing thesituation sensibly.By the received paradigm on these matters, "objects" are"self-identical."  Constants and singular terms purportto 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 anothersystemically.When Dedekind devised his sequence of ordinal numbers,he did not "purport" invariance.  He formulated a theorybased on successive involutions.  That is, he *modeled*it:Definition:  A system |N is said to be simplyinfinite when there exists as similar transformationF of |N in itself such that |N appears as chain ofan element not contained in F(|N).  We call thiselement, which we shall denote in what follows bythe symbol '1', the base-element of |N and say thesimply infinite system is *set in order* by thistransformation F.Dedekind's finite initial segments are not "strokes"on a page.  They are fixed in relation to a systemdescribed by successive transformation.Now, for comparison, here is Lesniewski's partrelation: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, thenobject P is a part of object P_2.Although not at any forefront of research, therehave been people studying mereology for years.They all follow the practices of first-orderlogic 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 iswrong 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 twoinfinite schemasAxAy(xcy <-> (...))AxAy(xey <-> (...))whose predicates have invariant interpretationrelative to substitutions.I use these to form a proper notion of identitybased on topological separation (which is preciselyFrege's description of first-order identity) whichis concomitant with extensionality.No one seems to grasp this because they are allsatisfied with "purporting".In any case, my notion of constant is in relationto a sense of "constancy" rather than to definitionsin 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 hadoriginally been envisioned?
```