On 2/15/2013 8:56 AM, Jesse F. Hughes wrote: > fom <fomJUNK@nyms.net> writes: > >> Here is where my complexity when interpreting >> Aristotle's remarks arise: >> >> Something like >> >> x=y >> >> is called informative identity. >> >> But, within a formal proof, one can never >> write that as an assumption. In a formal >> proof, one begins with true sentences and >> ends with true sentences. So all the >> metalogical analysis of meaning outside >> of a deduction is "armchair quarterbacking" >> whereas what happens in a proof is >> "regulation time". > > I'm afraid I have no idea what you mean here. Natural deduction > proofs involve assumptions all the darned time. For instance, one may > begin the proof that sqrt(2) is irrational by: > > Assume that a and b are natural numbers such that (a/b)^2 = 2. > > Now, given what you say below (snipped, since I don't really > understand what you're getting at and have no comment), it may be that > you think such a statement involves quantifiers and so is an exception > to the rule you state above. But, honestly, there is *NOTHING* in the > usual presentation of natural deduction that entails an equation > cannot be taken as an assumption. > > Do you think that these comments of yours are widely accepted or > original? > >
Not widely accepted, and, I would not say original since my eventual understanding of matters is close to Lesniewski's.
I never have any difficulty with a proof such as you are indicating here. That is how mathematics is, and should be, done.
What I refer to (and should have been more precise about) is the idea that "mathematical logic" is a logic that has a formal deductive calculus in which all proofs such as the one you initiated are claimed to occur (in principle).
In that context, what does it mean to "work in ZFC"?
Perhaps mistakenly, I take that to mean one is using the quantified statements of the theory inside of a formal deductive calculus.
Since modern set theory, influenced by logical atomism and minimalism, claims that there is no need for names such as "2" in your statement above -- its signature is either <e> or <e,=> depending on how one feels concerning "eliminability of identity" -- one must make the effort to understand its implementation.
In your statement above, you are designating variables to be parameters. What I mean by this is that you are assigning two arbitrary symbols that have no intrinsic semantic interpretation a "definite quality".
In a formal proof, this is an application of the axiom of reflexiveness
Now you have the epistemic problem. Of course, if you assert distinctness
a=a b=b |-(a=b)
that becomes an assumption that must be discharged. The dischargeable assumption of your statement is much more complex.
Your use of a "constant", or "name" is something that requires introduction through definite descriptions,
Definition of bottom: Ax(x=null() <-> Ay(-(xcy <-> x=y)))
Assumption of bottom: ExAy(-(xcy <-> x=y))
Definition of successor function: AxAy(x=S(y) <-> (Ez(ycz) /\ Az(zex <-> (zey \/ z=y))))
Assumption of successor set: Ax(Ey(xcy) -> Ey(Az(zey <-> (zex \/ z=x)) /\ Ez(ycz)))
Definition of 2 Ax(x=2() <-> x=S(S(null())))
So, the truth of your deduction is not only contingent on your dischargeable assumptions, but also on the relationship of definite descriptions to model theory.