Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Ordinals describable by a finite string of symbols
Replies: 27   Last Post: Jul 8, 2013 9:56 PM

 Messages: [ Previous | Next ]
 fom Posts: 1,968 Registered: 12/4/12
Re: Ordinals describable by a finite string of symbols
Posted: Jul 5, 2013 9:07 PM

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.

Hilbert:

"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."

Brouwer:

"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,

E!x

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

(i) E!w(F(x_1,...,x_n,w))

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,

(ii) F(x_1,...,x_n,f(x_1,...,x_n))"

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.

Description theory:

http://plato.stanford.edu/entries/descriptions/

Names:

http://plato.stanford.edu/entries/names/

And here is another you should probably consider:

http://plato.stanford.edu/entries/reference/

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.

Date Subject Author
7/5/13 fom
7/5/13 fom
7/6/13 Shmuel (Seymour J.) Metz
7/7/13 Peter Percival
7/7/13 fom
7/8/13 Shmuel (Seymour J.) Metz
7/8/13 fom
7/5/13 fom
7/5/13 fom
7/6/13 LudovicoVan
7/6/13 fom
7/6/13 LudovicoVan
7/6/13 fom
7/6/13 LudovicoVan
7/7/13 LudovicoVan
7/7/13 LudovicoVan
7/7/13 fom
7/7/13 LudovicoVan
7/7/13 fom
7/7/13 LudovicoVan
7/7/13 fom
7/7/13 LudovicoVan
7/7/13 fom
7/8/13 apoorv
7/7/13 fom
7/7/13 LudovicoVan
7/7/13 fom