On 7/4/2013 11:42 PM, apoorv wrote: > > Second, unnameable reals as arbitrary infinite sequences are ' really unnameable' as no property > Could be used to name them.
In response to this, let my quote Hilbert and Brouwer.
Hilbert's remark is discussing the nature of identity with respect to "formal axiomatics". Brouwer's remark is discussing identity from an intuitionist perspective.
"While the constructive method introduces objects of a theory as a genus of things, an axiomatic theory refers to a fixed system of things which is delimited from the outset and constitutes a domain of subjects for all predicates and propositions of the theory.
"There is the assumption that the domain of individuals is given as a whole."
"A species is called discrete if any two of its elements can be proved to be equal or to be different."
What I hope to convey here is that your expectation concerning the role of a "property" as a defining characteristic is relevant to the differences between these notions.
In particular, it has no role in the formal axiomatics to which Hilbert refers. It is *assumed* that the domain is *given*. Moreover, it is *assumed* that the domain is *given* as *a whole*. And, finally, it is assumed to be *delimited* *from* *the* *outset*.
For the Brouwerian statement things are different. Yet, your ideas are meaningless to intuitionistic logic as it has been developed and to constructive mathematics as it has been developed in the small amount of literature of which I am aware (and not an expert upon by any means).
That is, intuitionistic logic introduced an "absurdity" symbol to accommodate aspects of Brouwer's philosophy as expressed by
"Two mathematical entities will be called different if their equality proves absurd."
In my source for this remark, Brouwer's statement is formalized as
AxAy( ~(x=y) -> _|_ )
where '_|_' is the absurdity symbol.
Your ideas (as well as my personal views) seem to be directed at what is called a definite description. The relevant parts of Hilbert's work is unavailable to me. It is mentioned, however, in Kleene's "Introduction to Metamathematics".
Kleene states that definite descriptions had been shown to be eliminable by Hilbert and Bernays in 1934 with the publication of "Foundations of Mathematics". In Kleene's presentation of the material, the relationship of constants, definite descriptions, and proofs related to the formulas involved are discussed. It is very technical.
Consider I have already described to you concerning how language extensions create new languages. In addition, consider that the examples by which I extended a language signature intoduced one symbol at a time. This is one of Kleene's remarks:
"It suffices to consider the introduction of one new function symbol at a time"
Now, the syntax of a definite description is usually associated with an operator,
This operator is asserting that the formula expresses a "distinctive property" (Aristotle) for the object described. Now, here are part of Kleene's conditions from the statement of the relevant theorem:
"Let x_1,...,x_n,w (n>=0) be distinct variables, and F(x_1,...,x_n,w) be a formula which contains free only x_1,...,x_n,w, and in which x_1,...,x_n are free for w. Suppose that
is provable [in language] S_1.
"Let [language] S_2 be obtained from [language] S_1 by adjoining a new n-place function symbol 'f' and the new axiom,
In order to relate this to a more familiar notation, note that the statement of a lemma used to prove eliminability of descriptions by the theorem from which the previous quote is excerpted is given by
"In the predicate calculus with equality axioms for the function and predicate symbols of [language] S_1 only but with 'f' admitted to the symbolism (a fortiori, in the predicate calculus with equality), the conjunction of (i) and (ii) is interdeducible with
(iii) f(x_1,...,x_n) <-> F(x_1,...,x_n,w)
Hence, (iii) is provable in [language] S_2"
Note that when n=0, these remarks of Kleene's discuss the definition of constants that are intended to denote individuals.
In other words, when mathematical entities are viewed as obtained through definability with respect to properties, the Brouwerian notion of proving identity or proving difference makes sense.
But, this is foreign both to Hilbert's formal axiomatics and to the intuitionistic logic that arose from formalizing Brouwer's protests.
What makes it even worse is that the modern paradigm has encapsulated the notion of definability to be "definability within a model". So, the constant intended to denote an individual may not be taken as instantiated by an individual.
This latter aspect is consistent with the Russellian interpretation of definite descriptions and his descriptivist theory of names.
If this seems a bit much, remember that I told you that mathematicians avoid the question of "What is an object?" and "How is an object named?"
All I can tell you is that you believe your ideas to be simple and straightforward. They are, in fact, neither. Mathematics has a long history with extensive commentary. That cannot be ignored when it comes to your assertions.