FOM: Re: Definition of mathematics (continued)
jmyciel at euclid.Colorado.EDU
Tue Feb 15 15:04:30 EST 2000
MATHEMATICAL LOGIC AND PRIVATE LANGUAGES OF THOUGHTS
The following idea is important for a full understanding of the
philosophy of mathematics expressed in my letter on f.o.m. Jan 7, 2000.
When we have a complete informal mathematical proof which is
convincing to us, then in fact we have a formal proof in an certain
personal language PL in our mind. This language PL is somewhat different
from the language L of formal logic or from any common language. (In fact
the same informal proof can be explained in many ways in the same common
The existence of PL is established by introspection (for example
we think before we talk or write).
PL explains the psychological fact that if we understand fully a
complete informal proof then we are fully convinced that the axioms used
in that proof imply its conclusion.
By L we understand here (as in my earlier letter) Hilbert's
epsilon extension of multi-sorted first-order logic with quantifiers
viewed as abbreviations of certain formulas involving the epsilon
operator. Let us assume also that L is definitionally closed, that is,
there are short relation symbols abbreviating longer formulas and short
constant andfunction symbols abbreviating longer terms. L is our
mathematical model of PL.
We do not know fully our PL nor the PL's of other people. Our best
description of PL is: PL is a finite fragment of L (different systems of
relation and function symbols in the PL's of different individuals, whence
I called it private.) I may add that various images in our imaginations
may play the role of various terms. Perhaps also some well tested ability
for transforming some imagined objects play the role of function symbols,
as if a finite table of a finite function f was replacing (sometimes) the
function symbol for f.
Likewise, we do not know fully any common language. Again
everybody has a private version of his common languages. E.g. I have my
private versions od English, French, Polish and Russian, but I do not know
any synthetic definition of any of them. However, linguists have worked
out the theories (grammars) of many common languages, or even tried to
find general laws pertaining to all of them. Thus they try to find X such
(X / (Private Common Language)) = (L / PL).
QUESTION: Are there any important properties or tools of PL which
are not represented in the model L?
More information about the FOM