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.
>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...
>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.
>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.
Unsolicited bulk E-mail subject to legal action. I reserve the right to publicly post or ridicule any abusive E-mail. Reply to domain Patriot dot net user shmuel+news to contact me. Do not reply to firstname.lastname@example.org