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.
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.
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,
x=x Ey(x=y) AxEy(x=y)
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
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)'
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
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.
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?