Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Formalisation

16 views
Skip to first unread message

Aatu Koskensilta

unread,
Jun 5, 2007, 8:34:52 AM6/5/07
to
Once again, against my better knowledge, I find myself in a "debate" with
George Greene. Struggling with myself, I hope to withdraw, leaving George
basking in the glory of his victory by default. However, for benefit of
those wondering what I've been going on about -- a vast multitude, no doubt
-- I'll say a few words (ha-ha!) about formalisation. In the following I'll
concentrate on formalisation of arithmetical statements, properties,
relations and such like, for simplicity. I have also chosen not to be too
fussy about details; the reader is asked to mentally insert the standard
fluff about a variable being free for substitution in a formula,
simple-minded pedantry about the use-mention distinction, and so on.

An important note about terminology: in the following 'statement' will
always refer to a mathematical statement in ordinary mathematical English
while 'sentence' or 'formal sentence' will usually refer to a string of
symbols in the mathematically defined language.

Why should we want to formalise arithmetical statements and notions in the
first place? One possible reason is that we'd like to know, with
mathematical certainty, whether some statement can be proved using these or
those principles. Mathematical statements aren't mathematically defined
objects and thus there can be no question of mathematically proving stuff
about them; thus we need to provide some mathematical model of our
mathematical reasoning and mathematical language, a model that captures
faithfully those aspects of our mathematical reasoning and language we're
interested in, if we are to investigate these things mathematically. Hence:
formalisation.

To get started we define a language with mathematically defined syntax and
semantics, that, hopefully, is expressive enough to allow us to rephrase
arithmetical statements and notions in a form amenable to mathematical
analysis. First, we have symbols for addition, multiplication, equality, 0
and 1: "+", "*", "=", "0" and "1". In addition to these we have an infinite
supply of variables "x1","x2","x3", ... and so on. The syntax of our language
is defined inductively in two stages. First, there are /terms/ which are given
by

1) "0" and "1" are terms
2) a variable is a term
3) if t and r are terms, (r "+" t) and (r "*" t) are terms

Then there are formulas:

1) if t and r are terms, r "=" t is a formula
2) if P and Q are formulas, (P & Q), (P --> Q), (P <--> Q) and (P \/ Q) are
formulas
3) if P is a formula, ~P is a formula
4) if x is a variable and P a formula, (x)P and (Ex)P are formulas

The meaning of these expressions should be clear given that we are
attempting to model our arithmetical language (or, certain aspects of it),
but in order for us to reason about such things rigorously we need to
provide a mathematical definition, which we do by giving a truth definition
as follows.

A term is said to be /closed/ if it contains no variables. The value of a
closed term t, v(t), is given by recursion:

v("0") = 0, v("1") = 1
v((r "+" t)) = v(r) + v(t)
v((r "*" t)) = v(r) * v(t)

For every natural n, there is a term num(n), the /numeral/ for n, with the
property that v(num(n)) = n. Num(n) is again defined by recursion:

num(0) = "0"
num(n+1) = (num(n) "+" "1")

The result of /substituting/ a term t for a variable x in a term q, q[t/x],
is, surprisingly, defined by recursion:

"0"[t/x] = "1"[t/x]

y[t/x] = y if y is not x
y[t/x] = t if y is x
when y is a variable

(p "+" r)[t/x] = (p[t/x] "+" r[t/x])
(p "*" r)[t/x] = (p[t/x] "+" r[t/x])

There's one last definition left before we get to truth. The result of
substituting a term t for a variable x in a formula P, P[t/x], given by

(r "=" q)[t/x] = (r[t/x] "=" q[t/x])
(~P)[t/x] = ~(P[t/x])
(P @ Q)[t/x] = (P[t/x] @ Q[t/x]) where @ is &, \/, <-->, or -->

((y)P)[t/x] = (y)(P[t/x]) if y is not x
= (y)P otherwise

((Ey)P)[t/x] = (Ey)(P[t/x]) if y is not x
= (Ey)P otherwise

(For notational convenience we will write P[x1/t1, ..., xn/tn] for
((...(P[x1/t1])[x2/t2])...)[xn/tn], blithely ignoring any boring problems
with variable clashes).

At last, we get to truth. The notion of a sentence, that is, a formula with
no free variables, P being true is defined by recursion (on complexity of P):

(t "=" r) is true iff v(t) = v(r)
(P & Q) is true iff P is true and Q is true
(P \/ Q) is true iff P is true or Q is true
(P --> Q) is true iff P is not true or Q is true
(P <--> Q) is true iff either both P and Q are true, or both P and Q are
not true
~P is true iff P is not true
(x)P is true iff P[num(n)/x] is true for every n
(Ex)P is true iff there is an n, such that P[num(n)/x] is true

Inspecting this definition, it is not difficult to see that, in a very clear
sense, "+" expresses addition, "*" multiplication, & conjunction, and so
on, in their usual mathematical meaning. When we ask for a formalisation of
some arithmetical relation or statement, we are asking for a formula or
sentence in our language that /expresses/ that relation or statement. Before
explaining what this means -- and it will turn out it's not a mathematical
notion, which is not surprising; as said in the introductory paragraphs,
mathematical statements are not mathematical objects and thus their relation
to mathematical structures and objects is not a mathematical matter -- we
need to introduce a few extensional, mathematical notions.

If we consider a formula R with free variables x1, .., xn we can note that
it /defines/ a relation, namely the relation P(y1, ..., yn) of naturals
which holds exactly when R[num(y1)/x1, ..., num(yn)/xn] is true. In less
obfuscated language, the relation P defined by R holds for a1, ..., an
exactly when R is true /of/ a1, ..., an. For example, the formula

(Ex1)((~(x1 "=" "0")) & ((x2 "+" x) "=" x3))

which can be written in more readable form, if we adopt a few familiar
conventions -- which we now adopt without explicitly listing them -- as

(Ez)(z =/= 0 & x + z = y)

defines the familiar less-than relation <. As an another example, the formula

x =/= 0 & x =/= 1 & (z)(y)(y*z = x --> y = x \/ z = x)

defines the property (unary relation) of being a prime number.

At first it might seem that a sentence P expresses a mathematical statement A
if the truth of P -- which, it is important to recall, is a mathematical
property defined a few paragraphs ago -- is equivalent to A, and that a
formula R expresses a mathematical relation P of naturals if

R[num(a1)/x1, ..., num(an)/xn] is true iff P(a1, ..., an)

A moment's reflection shows that this is way too weak a requirement. For
example, the following sentence, FLT3, is true just in case Fermat's last
theorem holds for n = 3

~(Ex)(Ey)(Ez)(x =/= 0 & y =/= 0 & z =/= 0 & x*x*x + y*y*y = z*z*z)

The following sentence P, in turn, expresses the infinitude of primes:

(x)(Ey)(x < y & Prime(y))

where > and Prime are abbreviations for the formulas we gave earlier. If we
now consider the sentence P & FLT3 we can observe that, since FLT3 is true,
it is true just in case there are infinitely many primes. But it clearly
does not /express/ the infinitude of primes; rather, it seems obvious it
expresses that there infinitely many primes and Fermat's last theorem holds
for n = 3. If, as stipulated in the beginning, we're interested in finding
out whether e.g. the infinitude of primes follows from some bunch of
statements nothing can be concluded if we establish that the truth of P &
FLT3 does not follow; it might be that the infinitude of primes does follow
from that bunch of statements, but the fact that Fermat's last theorem holds
for n = 3 does not. Finer distinctions are called for.

Let's have a closer look at the sentence P from above. Using the definition
of truth, we can unravel the condition for P being true as follows:

1. (x)(Ey)(x < y & Prime(y)) is true iff (Ey)(num(n) < y & Prime(y))
is true for every n
2. (Ey)(num(n) < y & Prime(y)) is true iff there is a m, s.t.
(num(n) < num(m) & Prime(num(m)))

3. Combining 1. and 2. we get that P is true if for every n there is
an m, s.t. (num(m) < num(n) & Prime(num(m)). Recalling that < defines
the less than relation and Prime the property of being a prime, we get
that P is true iff for every n there is an m, such that n < m and m
is a prime; in other words, P is true iff for every n there is an m,
such that m > n and m is a prime, which is the ordinary statement of the
the infinitude of primes.

So we can say that P expresses, or formalises, the infinitude of primes in
the sense that if, using the definition of truth for sentences in our
language, we recursively figure out what it's being true amounts to, we get
that P's truth is equivalent to the usual statement of the infinitude of
primes. The important point is that in establishing this equivalence we
relied on nothing but the definition of truth and utterly trivial
mathematical reasoning (e.g. that x < y if y > x). To recapitulate: a
sentence P formalises, or expresses, a mathematical statement if it's truth
is equivalent to the statement using trivial mathematical reasoning, and a
formula R(x1, ..., xn) formalises, or expresses, a mathematical relation P
if it can be established, using trivial mathematical reasoning, that
for all a1, ..., an R[num(a1)/x1, ..., num(an)/xn] is true iff P(a1, ..., an).

In fact, we cheated in the above. We relied on the fact that < defines the
less-than relation and Prime primality. To be painstakingly thorough we
would need to carry out similar analysis to establish that, using the
definition of truth and trivial mathematical reasoning, for all n, the
truth of Prime(num(n)) is equivalent to n being prime, and that for all n,m
the truth of num(n) < num(m) is equivalent to n being less than m. The
interested reader -- optimism is not a sin -- might do that for himself if
he's into being bored to death.

Now that we know what it means for a formal sentence to express an
arithmetical statement, or for a formula to express an arithmetical
relation, we can move to the original question of determining whether some
statement follows from a bunch of statements. In order to study this
question mathematically we need a mathematical analysis of what it means for
a sentence in our language to follow from a bunch of sentences, an analysis
that can be seen to capture the notion of a statement following from a bunch
of statements, i.e. one for which we can see that a statement P follows from
a bunch of statements A iff the formalisation of P -- the (or a) sentences
expressing P -- follows, in the mathematically defined sense furnished by
the analysis, from the formalisations of the statements in A.

In fact, there are two distinct notions at issue here: a statement P being
provable from a bunch of statements A, and a statement P following from a
bunch of statements A. Informally, a statement P follows from a bunch of
statements A if it is impossible for all of A to be true without P being
true; and a statement P is provable from a bunch of statements A if there is
a proof of P on assumption that all of A holds. There's nothing, on the face
of it, to say that these two notions coincide. So when asking whether some
statement P follows from some bunch of statements A -- apologies for the
tautology -- we need to be clear about which of these two notions we are
interested in.

Mathematics is, at least for a large part, about proving stuff, so it is
perhaps natural to first consider the question of provability, e.g. the
question of whether some statement can be proved from some bunch of
statements. In order to study such questions mathematically we need to
define a relation |- of derivability, between sets of sentences and
sentences in our language. We must also verify that if a statement P is
provable from a bunch of statements A, A' |- P', where A' is the set of
formalisations of the sentences in A and P' the formalisation of P. (We're
being lax here; we should really speak of 'a formalisation'); for otherwise
establishing e.g. that it is not the case that A' |- P' will not necessarily
tell us anything about whether P is provable given A.

We define |- (or, actually, A |- * as a unary predicate for each A) inductively
as follows.

- A |- a for all a in A
- if A |- a and A |- b then A |- (a & b)
- if A |- (a & b) then A |- a and A |- b
- if A |- a then A |- (a \/ b) and A |- (b \/ a) for all b
- if A |- (a --> b) and A |- a then A |- b
- ... and so on; consult a logic book to fill in the details.

Having defined the relation |- of a sentence being derivable from a set of
sentences we now turn to the question of whether it adequately captures the
relevant aspects of mathematical provability, i.e. whether A |- P just in
case P expresses a mathematical statement that is provable from the bunch of
mathematical statements expressed by the elements of A.

Notational aside: From now on, whenever P is a sentence in our
mathematically defined language, P* is the mathematical statement it
expresses; this notational device extends to sets of sentences in the
obvious fashion. Similarly, whenever P is a mathematical statement that can
be expressed in our language, P^ is (one of) its formalisation(s).

To show that if A |- P then P is a formalisation of a mathematical statement
that is provable from the statements the formalisations of which the
elements of A are is not difficult. Notice that this is not a mathematical
result, since it concerns the notion of mathematical proof, which has no
mathematical definition; rather, it's an example of /informal rigour/ in
Kreisel's sense, non-mathematical, but perfectly rigorous and conclusive
reasoning. The argument is simple, and proceeds by induction. First we note
that if a in A then we can obviously conclude, on basis of A*, that a*. Such
a step in a proof would usually go something like "a*, by assumption". Next,
we go through all the inductive clauses in the definition of |-, noting for
example that if (a & b)* is provable on basis of A*, we can certainly
conclude that a*, and that b*; such a step would look something like "Since
(a & b)*, in particular a*" or "Since (a & b)*, in particular b*". So, if A
|- P, i.e. if P is derivable from A, there is a mathematical proof, which
might of course be utterly incomprehensible to actual human beings, of the
mathematical statement P expresses, from the mathematical statements the
elements of A express.

Notice that there is a property of |- that is purely mathematical, which is
that it is truth preserving: if every sentence in A is true and A |- P, then
P is also true. A much stronger property that we will soon meet also holds.

The other direction, showing that if there is a mathematical proof of P from
A then A^ |- P^, is more problematic. At first, it appears we would need a
detailed analysis of mathematical proofs, perhaps going through a vast bulk
of proofs in journals, textbooks, and so on. Happily, this is not necessary.
Here's where the notion of logical consequence, of a statement (logically)
following from some bunch of statements, comes into play. If we could show
that for every statement P and for every bunch of statements A, A^ |- P^ if
and only if P follows from A, we could conclude that P is mathematically
provable from A just in case A^ |- P^. This is because a mathematical proof
certainly cannot establish P if it does not follow from A -- though, as
said, it is not obvious that if P follows from A there should be a
mathematical proof of this -- and thus, if there is a mathematical proof of
P from A, P follows from A; but then, provided A^ |- P^ whenever P follows
from A, we must have A^ |- P^.

In fact, we *can* show that A^ |- P^ iff P follows from A, thanks to Kurt
Gödel, the old codger, his 1929 dissertation, and a few observations by
Kreisel. Following the now familiar pattern, we define a mathematical
relation A |= P, read "P is a logical consequence of A" -- we use "logical
consequence" for the mathematically defined relation between a set of
sentences and a sentence, and "follows" for the relation of a statement
following from a bunch of statements -- and then argue that A |= P just in
case P* follows from A*.

Our definition of |= is based on the idea that a statement P (expressible in
our language) follows from a bunch of statements A, if and only if it is
impossible for 0,1,+ and * to have the properties stipulated by A and P be
false. That is, we allow 0,1,+ and * behave as wildly as they want as long
as what A says is true, and ask whether P could be false. If it is
impossible for P to be false, it follows from A. Moving to sentences and
mathematical stuff, we introduce the notion of an /interpretation/. An
interpretation consists of a set of objects D, the domain of the
interpretation, together with two objects o and z (for "one" and "zero"),
and two functions f:D^2 --> D and g:D^2 --> D, i.e. an interpretation I
is a tuple <D,o,z,f,g>. The notion of a sentence P being true on
interpretation I, I |= P (we're overloading the |= symbol) is now defined
as follows.

First, we extend our language by introducing for every a in D a symbol ca
and extending the definition of term so that ca is a term for every a. The
definition of the value of a closed term t, v(t), is a simple generalisation
of the definition for the original language, with o, z, f and g playing the
roles of 1, 0, + and *:

v("0") = z
v("1") = o
v((t "+" q)) = f(v(t),v(q))
v((t "*" q)) = g(v(t),v(q))

The definition of P being true on I, I |= P, is similarly a simple
generalisation of P being true:

(t "=" r) is true on I iff v(t) = v(r)
(P & Q) is true on I iff P is true on I and Q is true on I
(P \/ Q) is true on I iff P is true on I or Q is true on I
(P --> Q) is true on I iff P is not true on I or Q is true on I
(P <--> Q) is true on I iff either both P and Q are true on I, or
both P and Q are not-true-on-I
~P is true on I iff P is not true on I
(x)P is true on I iff P[ca/x] is true on on I for every a
in D
(Ex)P is true on I iff there is an a in D, such that
P[ca/x] is true

The definition of P being a logical consequence of A, A |= P, is then given
by stipulating that A |= P iff for every interpretation I such that I |= A,
that is, I |= Q for every Q in A, we have I |= P.

The result alluded to some paragraphs ago is, of course, the completeness
theorem (or, a trivial corollary of the completeness theorem as we're only
considering the language of arithmetic):

A |= P if and only if A |- P

That is, P is a logical consequence of A if and only if P is derivable from
A.

How about the question of whether P follows from A just in case A^ |= P^? If
A^ |= P^ we have, by the completeness theorem, that A^ |- P^, and, by our
previous observation about mathematical provability and derivability, that P
is provable from A. Since only stuff that follows from A is provable from A,
we can conclude that if A^ |= P^, P follows from A. In the other direction,
assume that P^ is not a logical consequence of A^. Then there is an
interpretation of A^ on which P^ is false. Such an interpretation shows also
that all that A says of +,*,0 and 1 can be true without P being true, i.e. P
does not follow from A. This also provides answer to our question whether
the provability of P from A implies the derivability of P^ from A^: if P is
provable from A, P follows from A, and hence A^ |= P^, and, by the
completeness theorem, A^ |- P^.

There we have it finally. We have provided a mathematical analysis (of
certain aspects) of our mathematical reasoning and language and argued that it
is an adequate model of these aspects. Thus we can answer such questions as
"Does the statement P follow from statements A?" and "Is the statement P
provable from statements A?" by proving the corresponding mathematical
statements concerning the formalisations of A and P. Wonderful.

Before we're done there's but one last issue that needs to be addressed. We
have all this time been dealing with a language in which mathematical
statements and properties of naturals that only involve 0, 1, multiplication
and addition are expressible. This hardly covers much of number theory.
While we can express Goldbach's conjecture there is no apparent way to
express even such simple claims as Fermat's last theorem, involving as they
do exponentiation, or basic principles that involve finite sequences or sets
of naturals. In order to deal with this problem we need to introduce the
notion of /coding/. That will, however, have to wait to a later occasion;
this post is already ludicrously long.

Well, that took some doing. Ta-ta.

--
Aatu Koskensilta (aatu.kos...@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Peter_Smith

unread,
Jun 5, 2007, 4:42:01 PM6/5/07
to
Well, since no one else has bothered to respond, I'll just say: great
stuff Aatu.

What you say is a very nice counter to two confusions that people do
seem to be tempted by.

(1) Some think that formalization is of the essence of mathematics (so
no formalization, no genuine proofs). Not so. As you say, mathematical
proofs can and usually are conducted in "ordinary mathematical
English" (or Finnish, or whatever!): formalization comes in if and
when we want to mathematically model such proofs in certain ways for
certain purposes.

(2) Some think that going formal means turning our backs on semantic
notions like truth. Not so. The formalized languages we are usually
interested in are, on the contrary, interpreted languages (not just
empty syntax), and we can typically give neat definitions of the truth-
conditions of the sentences of the languages, as you do for a language
for elementary arithmetic.


Aatu Koskensilta

unread,
Jun 5, 2007, 5:13:25 PM6/5/07
to
On 2007-06-05, in sci.logic, Peter_Smith wrote:
> Well, since no one else has bothered to respond, I'll just say: great
> stuff Aatu.

Thank you, Peter.

Countering precisely these two misconceptions or confusions was the point of
my post, as you might have surmised. Sadly, I know of no logic book that
takes the sort of approach exemplified in my post to these issues, perhaps
with the exception of Torkel's _Inexhaustibility_.

My memory is not particularly reliable, and my introspective faculties liable
to lie unabashedly to me, but I seem to be pretty certain that it was the
writings of Kreisel, Torkel, Feferman and others of similar bent, that finally
led me to see the light. Before that I was one of the numerous victims of
the two confusions you mention; indeed, I would be bewildered with the
apparent circularity of studying logic by mathematical means, and so on -- a
bewilderment that many students of logic interested in foundations suffer
of, most of them without the benefit that befell me, of having the
opportunity to think about, read about, talk about, these issues for a
considerable span of time, until a simple realisation dawns: logic is
but a branch of mathematics, and as always, when applying mathematics to
something, be it physics, the practice of mathematics, linguistics, or what
have you, we need not have any pretence of *justifying* those things in terms
of mathematical analysis, and that there is a need, on the other hand, to
justify the *applicability* of the mathematical model in drawing any
concluding about the non-mathematical stuff.

PS. George Greene will be happy for your spelling. For some unfathomable
reason he finds it worth complaining about my spelling 'formalisation'
instead of 'formalization'. More ammo for him!

On second thought, that's pointless baiting of George. My most insincere
apologies.

abo

unread,
Jun 5, 2007, 5:53:26 PM6/5/07
to
On Jun 5, 2:34 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:

< a fine exposition>

In the spirit of offering *some* comment, I would consider this
paragraph:

> Having defined the relation |- of a sentence being derivable from a set of
> sentences we now turn to the question of whether it adequately captures the
> relevant aspects of mathematical provability, i.e. whether A |- P just in
> case P expresses a mathematical statement that is provable from the bunch of
> mathematical statements expressed by the elements of A.

May I suggest that instead of "mathematical provability" you should
put "informal provability"? Generally, I think one would say that
mathematical statements are provable mathematically if they follow
from generally accepted axioms. So e.g. we don't in general say,
"Euclid's Theorem is mathematically provable from the Peano Axioms;"
instead we say, "Euclid's Theorem is mathematically provable." So
"mathematically provable" often does away with the A by assuming it
implicitly.

And another quibble here:

> Before we're done there's but one last issue that needs to be addressed. We
> have all this time been dealing with a language in which mathematical
> statements and properties of naturals that only involve 0, 1, multiplication
> and addition are expressible. This hardly covers much of number theory.
> While we can express Goldbach's conjecture there is no apparent way to
> express even such simple claims as Fermat's last theorem, involving as they
> do exponentiation, or basic principles that involve finite sequences or sets
> of naturals. In order to deal with this problem we need to introduce the
> notion of /coding/. That will, however, have to wait to a later occasion;
> this post is already ludicrously long.

Surely one could introduce the concept of sequences directly; so while
we need something extra, we don't need coding; coding is just one way
of handling it.

Aatu Koskensilta

unread,
Jun 5, 2007, 6:04:03 PM6/5/07
to
On 2007-06-05, in sci.logic, abo wrote:
> May I suggest that instead of "mathematical provability" you should
> put "informal provability"?

That would be in line with standard terminology. My issue with "informal" is
that it carries certain connotations of non-rigour, causality, and so on. A
better term would, perhaps, be "non-formal". Alas, if I start going on about
"non-formal" stuff no one has the slightest clue as to what it is I'm
rambling about.


> Generally, I think one would say that mathematical statements are provable
> mathematically if they follow from generally accepted axioms.

Indeed. That is something I will, hopefully, address in the future. In my
post I have been concerned solely with some statement P being provable on
assumptions A, without any unmentioned mathematical axioms or principles.

> Surely one could introduce the concept of sequences directly; so while
> we need something extra, we don't need coding; coding is just one way
> of handling it.

Sure. That is something I intend to talk about when I get to talking about
coding.

Peter_Smith

unread,
Jun 5, 2007, 6:07:41 PM6/5/07
to
On 5 Jun, 22:13, Aatu Koskensilta <aatu.koskensi...@xortec.fi> wrote:

> Countering precisely these two misconceptions or confusions was the point of
> my post, as you might have surmised. Sadly, I know of no logic book that
> takes the sort of approach exemplified in my post to these issues, perhaps
> with the exception of Torkel's _Inexhaustibility_.

Well, [cue shameless self-advertising!!] I think you'll find

http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521674539

sympathetic to your approach too.

> My memory is not particularly reliable, and my introspective faculties liable
> to lie unabashedly to me, but I seem to be pretty certain that it was the
> writings of Kreisel, Torkel, Feferman and others of similar bent, that finally
> led me to see the light.

For me, that reluctant publisher Timothy Smiley (who set generations
of Cambridge students thinking on the right lines) is also a major
influence ...

=============================
logicmatters.blogspot.com

Aatu Koskensilta

unread,
Jun 5, 2007, 6:39:42 PM6/5/07
to
On 2007-06-05, in sci.logic, Peter_Smith wrote:
> Well, [cue shameless self-advertising!!] I think you'll find
>
> http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521674539
>
> sympathetic to your approach too.

Ah, Peter; I was -- of course -- thinking of books *in print*, or, rather,
books I have happened to encounter. As I have said, I think your Goedel book
is splendid. There are some parts I'd take objection to, but on the whole
-- ***advertising*** -- it is a splendid book.

> For me, that reluctant publisher Timothy Smiley (who set generations

> of Cambridge students thinking you the right lines) is also a major
> influence ...

What was it that he did?

Peter_Smith

unread,
Jun 6, 2007, 3:10:05 AM6/6/07
to
On 5 Jun, 23:39, Aatu Koskensilta <aatu.koskensi...@xortec.fi> wrote:

> > For me, that reluctant publisher Timothy Smiley (who set generations
> > of Cambridge students thinking you the right lines) is also a major
> > influence ...
>
> What was it that he did?

I'm not sure quite what you are asking, Aatu. In one sense, what Tim
Smiley did was teach logic in the Cambridge Philosophy Faculty for
about 40 years -- ending up Knightbridge Professor -- retiring about
1998(?).

For a remark of his that says something about how he viewed/views
logic (and which you should find sympathetic, given what we've been
saying here), well how about this from Mind 1995 on Carroll's Achilles
and the Tortoise, where Smiley has the Tortoise conclude "I suggest
you reclassify [logic] as a branch of theoretical applied mathematics.
Theoretical because no one in their senses would formalise arguments
except for some theoretical -- philosophical, metamathematical --
purpose."

If you want to know what he did in the sense of his major papers,
etc., well, there's just one book, Shoesmith & Smiley, Multiple
Conclusion Logic (CUP, 1978). But important papers include his "The
Theory of Descriptions." Proceedings of the British Academy 67 (1981),
331-337, which is a classic. And there is the current series of papers
he is writing with Alex Oliver on the logic of plurals.

=============
logicmatters.blogspot.com

Aatu Koskensilta

unread,
Jun 6, 2007, 3:18:55 AM6/6/07
to
On 2007-06-06, in sci.logic, Peter_Smith wrote:
> For a remark of his that says something about how he viewed/views
> logic (and which you should find sympathetic, given what we've been
> saying here), well how about this from Mind 1995 on Carroll's Achilles
> and the Tortoise, where Smiley has the Tortoise conclude "I suggest
> you reclassify [logic] as a branch of theoretical applied mathematics.
> Theoretical because no one in their senses would formalise arguments
> except for some theoretical -- philosophical, metamathematical --
> purpose."

I do indeed find that sympathetic! That would be an apt summary of how I
think we should think about logic.

> If you want to know what he did in the sense of his major papers,
> etc., well, there's just one book, Shoesmith & Smiley, Multiple
> Conclusion Logic (CUP, 1978). But important papers include his "The
> Theory of Descriptions." Proceedings of the British Academy 67 (1981),
> 331-337, which is a classic. And there is the current series of papers
> he is writing with Alex Oliver on the logic of plurals.

If it's a classic I must have a peek at it. Thanks.

Chris Menzel

unread,
Jun 5, 2007, 11:05:54 PM6/5/07
to
On Tue, 05 Jun 2007 15:07:41 -0700, Peter_Smith <ps...@cam.ac.uk> said:
> ...
> =============================
> logicmatters.blogspot.com

Peter only advertises his blog by providing its URL, but it is well
worth subscribing to via your favorite RSS aggregator. In the past few
weeks, in particular, along with random reflections on grading tripos
papers and good restaurants in Cambridge, he's provided fine, readable
commentary on a recent collection entitled _Church's Thesis After 70
Years_. Check it out.

Peter_Smith

unread,
Jun 6, 2007, 3:57:03 PM6/6/07
to
Cheers, Chris. :))


Nam D. Nguyen

unread,
Jun 8, 2007, 12:35:25 AM6/8/07
to
Aatu Koskensilta wrote:
> On 2007-06-05, in sci.logic, Peter_Smith wrote:
>> Well, since no one else has bothered to respond, I'll just say: great
>> stuff Aatu.
>
> Thank you, Peter.
>
>> What you say is a very nice counter to two confusions that people do
>> seem to be tempted by.
>>
>> (1) Some think that formalization is of the essence of mathematics (so
>> no formalization, no genuine proofs). Not so.

I wonder, if it's "Not so [that] formalization is of the essence of
mathematics", then why did Shoenfield waste his time to write an
entire book about FOL *formalism* and name it "*Mathematical* Logic".
Wait... he did say "...mathematical logic is the study of the type
of reasoning done by *mathematicians*". Given what Shoenfield said
and given title of the thread is "Formalisation", I find the "Not so",
which you agree with, is very queer!

>> proofs can and usually are conducted in "ordinary mathematical
>> English" (or Finnish, or whatever!): formalization comes in if and
>> when we want to mathematically model such proofs in certain ways for
>> certain purposes.

Right. People have conducted proofs in "ordinary mathematical English
[or any natural language]" all the time! That's why often we've had
paradoxes and crank-talk truths!

Good grief! How do we end up with 'proofs can and usually are conducted
in "ordinary mathematical English"', from "Formalisation" of the thread's
title?

>>
>> (2) Some think that going formal means turning our backs on semantic
>> notions like truth. Not so.

"Going formal" means precisely that. If you don't believe so, name something
about truth that can't be replaced with syntactical part of formalism!

>> The formalized languages we are usually
>> interested in are, on the contrary, interpreted languages (not just
>> empty syntax), and we can typically give neat definitions of the truth-
>> conditions of the sentences of the languages, as you do for a language
>> for elementary arithmetic.

What in the name of mathematical formalism does "The formalized languages
we are _usually interested_ in" mean? And what is the formal definition
for the difference between "interpreted" languages and "non-interpreted" ones?

>
> Countering precisely these two misconceptions or confusions was the point of
> my post, as you might have surmised.

> Sadly, I know of no logic book that
> takes the sort of approach exemplified in my post to these issues, perhaps
> with the exception of Torkel's _Inexhaustibility_.

"Sadly"? So you mean to say Shoenfield's "Mathematical Logic" is not a good
book, because only the Inexhaustibility would take "the sort of approach
exemplified in my post"? [You might have forgot, Torkel highly regarded
Shoenfield's book!]

>
> My memory is not particularly reliable, and my introspective faculties liable
> to lie unabashedly to me, but I seem to be pretty certain that it was the
> writings of Kreisel, Torkel, Feferman and others of similar bent, that finally
> led me to see the light. Before that I was one of the numerous victims of
> the two confusions you mention; indeed, I would be bewildered with the
> apparent circularity of studying logic by mathematical means, and so on -- a
> bewilderment that many students of logic interested in foundations suffer
> of, most of them without the benefit that befell me, of having the
> opportunity to think about, read about, talk about, these issues for a
> considerable span of time, until a simple realisation dawns:

> logic is but a branch of mathematics,

So "Mathematical Logic" is a recursive name?

MoeBlee

unread,
Jun 8, 2007, 1:03:44 AM6/8/07
to
On Jun 7, 9:35 pm, "Nam D. Nguyen" <namducngu...@shaw.ca> wrote:
> I wonder, if it's "Not so [that] formalization is of the essence of
> mathematics", then why did Shoenfield waste his time to write an
> entire book about FOL *formalism* and name it "*Mathematical* Logic".
> Wait... he did say "...mathematical logic is the study of the type
> of reasoning done by *mathematicians*". Given what Shoenfield said
> and given title of the thread is "Formalisation", I find the "Not so",
> which you agree with, is very queer!

Oh, not so fast, brave Shoenfield quoter...

"We may describe what a mathematician does as follows. He presents us
with certain basic CONCEPTS [emphasis added] and certain axioms ABOUT
[emphasis added] these concepts. He then explains these concepts to us
until we understand them sufficiently well to see that the axioms are
true. He then proceeds to define derived concepts and to prove
theorems about both basic and derived concepts. The entire edifice
which he constructs, consisting of basic concepts, axioms, and
theorems, is called an axiom system." - Shoenfied, 'Mathematical
Logic' pg 2..

MoeBlee

Nam D. Nguyen

unread,
Jun 8, 2007, 1:25:45 AM6/8/07
to

So where did Shoenfield indicate (allude to) that it's "Not so [that]
formalization is of the essence of mathematics"?

MoeBlee

unread,
Jun 8, 2007, 1:45:54 AM6/8/07
to
> formalization is of the essence of mathematics"?- Hide quoted text -

There are two separate questions:

(1) Did Koskensilta claim that Shoenfield says that formalization is
not the essence of mathematics? If Koskensilta chooses to make that
claim, then Koskensilta can choose whether he wants to support it. But
unless Koskensilta does choose to claim it, then there's no reason for
him, let alone for me, to support it.

(2) Are you claiming that Shoenfield says that formalization is the
essence of mathematics? If so, then it's up to you whether you choose
to support it.

In any case, what I quoted is pretty strong reason to regard
Shoenfield as not saying that formalization is the essence of
mathematics. And that is different from the question of whether
Shoenfield is saying that formalization is not the essence of
mathematics.

As best I can get an impression of your purpose for quoting
Shoenfield, it was to show that Shoenfield is saying that
formalization is the essence of mathematics (correct me if needed).
However, the quote I produced very strongly supports that Shoenfield
is not claiming that formalization is the essence of mathematics.

MoeBlee


Aatu Koskensilta

unread,
Jun 8, 2007, 1:53:51 AM6/8/07
to
On 2007-06-08, in sci.logic, Nam D. Nguyen wrote:
> "Sadly"? So you mean to say Shoenfield's "Mathematical Logic" is not a good
> book, because only the Inexhaustibility would take "the sort of approach
> exemplified in my post"? [You might have forgot, Torkel highly regarded
> Shoenfield's book!]

I am at loss as to why you think I mean to badmouth Shoenfield's
_Mathematical Logic_ in any way. As I've on many occasions said, it's an
excellent text, and one of my personal favourites. What I was lamenting is
that very few logic books bother to even acknowledge the need for the sort
of considerations put forth in my post, for example moving from results of
form "the formalisation of P is formally unprovable from the formalisations
of the sentences A" to "P can't be proved on basis of A" with no explicit
justification.

I suggest you reflect on the following words from Kreisel

- - having accepted the formalist scheme, one is not merely /unwilling/
to appreciate (or study!) further work in foundations, but simply
/unable/ to do so with reexamining his ideas.

and, instead of bizarre claims -- the idea that formalisation alone allows
us to avoid errors, confusion and paradoxes, is patently absurd -- and vague
generalities, provide specific criticism -- that is, reading my post, and
pointing out any unclarities, errors, unjustified claims, you find.

Aatu Koskensilta

unread,
Jun 8, 2007, 2:06:32 AM6/8/07
to
On 2007-06-08, in sci.logic, MoeBlee wrote:
> (1) Did Koskensilta claim that Shoenfield says that formalization is
> not the essence of mathematics?

Quite obviously not -- I didn't mention Shoenfield at all.

> If Koskensilta chooses to make that claim, then Koskensilta can choose
> whether he wants to support it. But unless Koskensilta does choose to
> claim it, then there's no reason for him, let alone for me, to support
> it.

I'm happy to emphatically and most forcefully assert that formalisation is
not the essence of mathematics! Formalisation is needed when we wish to
study mathematical reasoning by mathematical means, an undertaking that
necessitates the creation of a mathematical model of the relevant aspects of
our mathematical reasoning, but is by no stretch of imagination the
"essence of mathematics" anymore than, say, a mathematical model of social
networking is the essence of making friends. This does not mean that
mathematical logic, and formalisation, plays no role in our mathematical
reasoning and reasoning about mathematics, only that this role is not
constitutional.

MoeBlee

unread,
Jun 8, 2007, 2:28:01 AM6/8/07
to
On Jun 7, 11:06 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:

> On 2007-06-08, in sci.logic, MoeBlee wrote:
>
> > (1) Did Koskensilta claim that Shoenfield says that formalization is
> > not the essence of mathematics?
>
> Quite obviously not -- I didn't mention Shoenfield at all.
>
> > If Koskensilta chooses to make that claim, then Koskensilta can choose
> > whether he wants to support it. But unless Koskensilta does choose to
> > claim it, then there's no reason for him, let alone for me, to support
> > it.
>
> I'm happy to emphatically and most forcefully assert that formalisation is
> not the essence of mathematics! Formalisation is needed when we wish to
> study mathematical reasoning by mathematical means, an undertaking that
> necessitates the creation of a mathematical model of the relevant aspects of
> our mathematical reasoning, but is by no stretch of imagination the
> "essence of mathematics" anymore than, say, a mathematical model of social
> networking is the essence of making friends. This does not mean that
> mathematical logic, and formalisation, plays no role in our mathematical
> reasoning and reasoning about mathematics, only that this role is not
> constitutional.

That is (as usual for you) quite well said. And I basically agree with
it (though I also take my own branch from it). My point to Nguyen is
that neither you nor I are obligated to defend a claim that Shoenfield
says that formalization is not the essence of mathematics, since
whether Shoenfield says that or not, neither you nor I had claimed
that he did.

To me, it's fairly clear that, at the very least, one would have to
reject any sweeping generalization that the way mathematicians
themselves regard their work is as a study of formal systems. I mean,
such a sweeping claim just has no basis. Someone might wish to argue
for the notion that an ideal mathematician's study is that of formal
systems or that one's own studies are of mathematics in terms of
formalization. But that is a long way from taking the essence of
mathematics as it is actually practiced and conceived by
mathematicians to be that of formalization. Moreover, there is hardly
basis to claim (if it is what Nguyen is claiming) that Shoenfield says
that the essence of mathematics is formalization.

MoeBlee

Mitch

unread,
Jun 8, 2007, 10:43:46 AM6/8/07
to
On Jun 8, 2:06 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:

>
> I'm happy to emphatically and most forcefully assert that formalisation is
> not the essence of mathematics! Formalisation is needed when we wish to
> study mathematical reasoning by mathematical means, an undertaking that
> necessitates the creation of a mathematical model of the relevant aspects of
> our mathematical reasoning, but is by no stretch of imagination the
> "essence of mathematics" anymore than, say, a mathematical model of social
> networking is the essence of making friends. This does not mean that
> mathematical logic, and formalisation, plays no role in our mathematical
> reasoning and reasoning about mathematics, only that this role is not
> constitutional.

I don't see how mathematics/mathematical reasoning/etc. could be
themselves without some sense of formality/precision/removal of
vagueness/questioning of premises (and supplying resolution to them).
Other sciences may do this, too but it's all that mathematics has.
When Babylonians noticed/used the tool which later became known as the
Pythagorean theorem, they never really bothered to attempt to prove it/
formalise it like the Greeks did (well, at least that's all that the
historical record shows), but they were still figuring out and
following rules.

Mitch

(which is not to say that the explanations and distinctions that you
and Peter are discussing aren't totally on target. I'm just saying
that the particular range of the term 'formal' that you are using (one
that I also use often) may be too restrictive with respect to Nam.)

Peter_Smith

unread,
Jun 8, 2007, 12:06:47 PM6/8/07
to
On 8 Jun, 05:35, "Nam D. Nguyen" <namducngu...@shaw.ca> wrote:

> >> (1) Some think that formalization is of the essence of mathematics (so
> >> no formalization, no genuine proofs). Not so.
>
> I wonder, if it's "Not so [that] formalization is of the essence of
> mathematics", then why did Shoenfield waste his time to write an
> entire book about FOL *formalism* and name it "*Mathematical* Logic".
> Wait... he did say "...mathematical logic is the study of the type
> of reasoning done by *mathematicians*".

Shoenfield is right. Mathematical logic is that bit of maths whose aim
is to model the sort of reasoning done (inter alia) by mathematicians.
The theory proceeds by using e.g. formalized languages in the
modelling process. But of course, nearly all mathematicians rightly
proceed in cheerful disregard of the logicians looking over their
shoulders, commenting from the sidelines! The mathematicians normally
reason away using in mathematical English, or whatever, using whatever
symbolic augmentation is useful for the purposes at hand, but not
using -- of course -- fully formalized languages or specifying their
logical framework. Formalization, in that sense, isn't of the essence
of ordinary mathematics.

> Given what Shoenfield said
> and given title of the thread is "Formalisation", I find the "Not so" ... very queer!

Not queer at all. Just marking the plain distinction between (a)
ordinary mathical reasoning and (b) formalized arguments as studied in
mathematical logic, which appear in models of ordinary mathematical
reasoning.


J. Burse

unread,
Jun 8, 2007, 4:26:21 PM6/8/07
to Aatu Koskensilta
Aatu Koskensilta wrote:
> Once again, against my better knowledge, I find myself in a "debate" with
> George Greene. Struggling with myself, I hope to withdraw, leaving George
> basking in the glory of his victory by default. However, for benefit of
> those wondering what I've been going on about -- a vast multitude, no doubt
> -- I'll say a few words (ha-ha!) about formalisation. In the following I'll
> concentrate on formalisation of arithmetical statements, properties,
> relations and such like, for simplicity. I have also chosen not to be too
> fussy about details; the reader is asked to mentally insert the standard
> fluff about a variable being free for substitution in a formula,
> simple-minded pedantry about the use-mention distinction, and so on.

A pedantry that often occurs in this thread is
that there are two basic views on formalization
in mathematics:
- The algebraists view: Everything is equations and models.
- The logicists view: Everything is deductions and syntax.

And these two views often clash. For example if
you present to someone the notion of provability,
i.e. "T |- A", then if he comes from the algebraists
camp, he will not understand you, because he
will look for some "truth equations". A similar
clash might occur vice versa.

Interrestingly the two views can be combined, whereas
the algebraists has to give in for a few new inductive
concept, otherwise he will end up in some orthomodular
logic with strange non standard models.

In my opinion, good mathematics is formal to the
excess. I don't believe in some informal proofs,
etc.. Clearly there will be some math english in
a proof etc.. But without the tools of formalization
it would be impossible today to produce the amount
of results that is available now.

Best Regards

J. Burse

unread,
Jun 8, 2007, 4:28:35 PM6/8/07
to Aatu Koskensilta
J. Burse wrote:
> A pedantry that often occurs in this thread is
> that there are two basic views on formalization
> in mathematics:
Typo: in this thread --> in this newsgroup

Peter_Smith

unread,
Jun 8, 2007, 6:15:02 PM6/8/07
to
On 8 Jun, 21:26, "J. Burse" <janbu...@fastmail.fm> wrote:

> In my opinion, good mathematics is formal to the
> excess. I don't believe in some informal proofs,
> etc.. Clearly there will be some math english in
> a proof etc.. But without the tools of formalization
> it would be impossible today to produce the amount
> of results that is available now.

Careful. Of course it is true that mathematicians use special notation
all the time and couldn't sensibly do without it. But I think Aatu and
I are both counting that as part of the mathematician's everyday lingo
-- mathematician's English in the stretched sense. To take the
simplest sort of case, we write "the sum of blah, blah from 0 to n"
using a sigma notation.The sigma symbol is just a neat extension of
mathematician's English: we all learn how to use it (and without ever
being given explicit syntactic rules, or an explicit semantics -- or
indeed even being told its semantic category!) Using symbols like this
is to be distinguished from using a formalized language.

To put it briskly: mathematicians' symbolically augmented English is
no more a fully formalized language that street English is.

Nam D. Nguyen

unread,
Jun 9, 2007, 12:10:12 PM6/9/07
to
Aatu Koskensilta wrote:
> On 2007-06-08, in sci.logic, Nam D. Nguyen wrote:
>> "Sadly"? So you mean to say Shoenfield's "Mathematical Logic" is not a good
>> book, because only the Inexhaustibility would take "the sort of approach
>> exemplified in my post"? [You might have forgot, Torkel highly regarded
>> Shoenfield's book!]
>
> I am at loss as to why you think I mean to badmouth Shoenfield's
> _Mathematical Logic_ in any way. As I've on many occasions said, it's an
> excellent text, and one of my personal favourites.

In the thread "Shoenfield's Mathematical Logic", Mar 26th, you said:

"What he means is virtually always very clear, but often he has rather
complicated stuff in mind with an apparently off-hand remark.

One could also complain about the quality of the historical and philosophical
sections;"

Imho, "_complain_ about the quality" is synonymous with "poor quality".
The "historical and philosophical sections" are probably the first few
sections he used to lay out his view as to what the foundation of FOL
formalism is, which you simply (though politely) dismissed as "poor quality"!
Seriously. Your mis-characterization of those sections puts you at odd with
him at some important notions, e.g.: in March you said in the thread
"help with Godel's":

'"Arithmetic or the naturals" is not in any obvious sense a formal system.'

while to Shoenfield:

"We give two examples of [formal] theory. The first, which we designate by N,
formalizes a classical axiom system for the natural numbers. The nonlogical
symbols of N are the constant 0, the unary functional symbol S ...."

Against that background that you're in sharp contrast with Shoenfield on some
foundational notions, your op does nothing to explain the contrast and you seem
to be too quick to claim your side of the contrast is the correct side:

"Countering precisely these two misconceptions or confusions was the point of

my post, as you [Peter Smith] might have surmised."

And after all of that, you simply felt "Sadly" that Torkel's book is the only book
that is on your "correct" side: formalism is inferior to intuition reasoning!

Pitting intuitionism against formalism is not my aim, at all! They *both* serve
purposes in FOL. I'm just trying to point the limitation in both so we could
try to improve the overall FOL reasoning. To which you and others simply
(wrongly, imho) dismissed as "misconceptions or confusions".

So if I'm "furious" about yours and PS' comments, there are reasons imho.

Aatu Koskensilta

unread,
Jun 10, 2007, 6:55:37 AM6/10/07
to
On 2007-06-08, in sci.logic, Mitch wrote:
> (which is not to say that the explanations and distinctions that you
> and Peter are discussing aren't totally on target. I'm just saying
> that the particular range of the term 'formal' that you are using (one
> that I also use often) may be too restrictive with respect to Nam.)

It is true that in the ordinary sense mathematics is quite formal, and
precision, rigour, tedious attention to details, and all that, are hallmarks
of mathematics. My post concerned formalisation only in the technical sense.
About Nam's use of 'formal' and 'formalisation' I really have nothing much
to say; his going on about "the FOL framework" and similar things might
suggest he has the technical meaning in mind.

Aatu Koskensilta

unread,
Jun 10, 2007, 7:04:57 AM6/10/07
to
On 2007-06-08, in sci.logic, Peter_Smith wrote:
> To put it briskly: mathematicians' symbolically augmented English is
> no more a fully formalized language that street English is.

Briskly and correctly did you put it, Peter. As a side-note, there is a
supposedly profound cliché about mathematics, that it is a "language". I've
never been particularly impressed with this -- to me it seems as profound as
the insistence by an acquaintance of mine that mathematics is "three-valued
logic". Mathematicians do have their own jargon, special notation, idioms
that make grammarians grind their teeth, but so do art historians,
physicists, philosophers, accountants, car mechanics, Usenet kookologists,
generals, chimney sweeps. Of course, the cliché might be interpreted in all
sorts of ways that make sense, but usually these ideas can be better conveyed
with rather boring trivialities, such as "mathematics is useful in modelling
all sorts of things".

Aatu Koskensilta

unread,
Jun 10, 2007, 7:11:47 AM6/10/07
to
On 2007-06-09, in sci.logic, Nam D. Nguyen wrote:
> In the thread "Shoenfield's Mathematical Logic", Mar 26th, you said:
>
> "What he means is virtually always very clear, but often he has rather
> complicated stuff in mind with an apparently off-hand remark.
>
> One could also complain about the quality of the historical and philosophical
> sections;"
>
> Imho, "_complain_ about the quality" is synonymous with "poor quality".

That might be so in your humble opinion. That there is something to complain
about the historical and philosophical sections, and about the rather
byzantine notation, does not mean that they're of "proof quality". Indeed, a
few sentences later I describe the complaints as "trifling".

> Seriously. Your mis-characterization of those sections puts you at odd with
> him at some important notions, e.g.: in March you said in the thread
> "help with Godel's":
>
> '"Arithmetic or the naturals" is not in any obvious sense a formal system.'
>
> while to Shoenfield:
>
> "We give two examples of [formal] theory. The first, which we designate by N,
> formalizes a classical axiom system for the natural numbers. The nonlogical
> symbols of N are the constant 0, the unary functional symbol S ...."

I'm puzzled. Nowhere did I say that all sorts of classical axiom systems,
and other pieces of mathematics, can't be formalised. Also, what
mis-characterisation do you have in mind?

> Pitting intuitionism against formalism is not my aim, at all! They *both* serve
> purposes in FOL. I'm just trying to point the limitation in both so we could
> try to improve the overall FOL reasoning.

What are the "purposes in FOL"? What improvements have you mind to "the
overall FOL reasoning" whatever that is?

translogi

unread,
Jun 10, 2007, 10:21:18 AM6/10/07
to
On Jun 10, 12:11 pm, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)

>
> "Wovon man nicht sprechen kann, daruber muss man schweigen"
> - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Sorry i will have to go back in time a bit

>From an earlier post


suggest you reflect on the following words from Kreisel
- - having accepted the formalist scheme, one is not merely /
unwilling/
to appreciate (or study!) further work in foundations, but simply
/unable/ to do so with reexamining his ideas

can you give me the referece to this text (looks an interesting
article)
(Am studiing Kuhn)

Aatu Koskensilta

unread,
Jun 10, 2007, 10:37:38 AM6/10/07
to
On 2007-06-10, in sci.logic, translogi wrote:
> can you give me the referece to this text (looks an interesting
> article)
> (Am studiing Kuhn)

It's from _Observations of Popular Discussions on Foundations_, in Axiomatic
Set Theory, Symposia in Pure Mathematics XIII, part I, if memory serves.

--
Aatu Koskensilta (aatu.kos...@xortec.fi)

Frederick Williams

unread,
Jun 10, 2007, 11:01:03 AM6/10/07
to
Peter_Smith wrote:
>
> On 8 Jun, 21:26, "J. Burse" <janbu...@fastmail.fm> wrote:
>
> > In my opinion, good mathematics is formal to the
> > excess. I don't believe in some informal proofs,
> > etc.. Clearly there will be some math english in
> > a proof etc.. But without the tools of formalization
> > it would be impossible today to produce the amount
> > of results that is available now.
>
> Careful. Of course it is true that mathematicians use special notation
> all the time and couldn't sensibly do without it. But I think Aatu and
> I are both counting that as part of the mathematician's everyday lingo
> -- mathematician's English in the stretched sense. To take the
> simplest sort of case, we write "the sum of blah, blah from 0 to n"
> using a sigma notation.The sigma symbol is just a neat extension of
> mathematician's English: we all learn how to use it (and without ever
> being given explicit syntactic rules, or an explicit semantics -- or
> indeed even being told its semantic category!) Using symbols like this
> is to be distinguished from using a formalized language.

Is it the mathematicians' claim that the mathematical English could
always be translated into, say, ZFC, with the proofs going over into
valid ZFC proofs?

--
Remove "antispam" and ".invalid" for e-mail address.
"He that giveth to the poor lendeth to the Lord, and shall be repaid,"
said Mrs Fairchild, hastily slipping a shilling into the poor woman's
hand.

Peter_Smith

unread,
Jun 11, 2007, 6:54:19 AM6/11/07
to
On Jun 10, 4:01 pm, Frederick Williams <"Frederick
Williams"@antispamhotmail.co.uk.invalid> wrote:

> Is it the mathematicians' claim that the mathematical English could
> always be translated into, say, ZFC, with the proofs going over into
> valid ZFC proofs?

Odd, a post didn't appear. I'll try again (more briefly)!

"Translate" isn't perhaps the right word. But sure, we find proxies
for other mathematical structures (most of them, anyway) inside ZFC --
as when we take a certain set of sets to stand proxy for the natural
numbers. And then claims about those structures get mapped, hopefully,
to ZFC theorems. But what does that show, exactly??

Say, if you like, that (most) mathematics is, in this sense,
formalizable into the framework of a certain theory that has a
canonical formal presentation. But formalizABLE doesn't mean
formalizED (any more than breakable means broken). The fact remains
that everyday mathematics does not proceed in a formalized framework
(most mathematicians would be completely stumped if you asked them to
give the axioms of ZFC!) -- and it is none the worse for that.

george

unread,
Jun 12, 2007, 2:19:55 PM6/12/07
to
On Jun 5, 8:34 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>

wrote:
> Once again, against my better knowledge, I find myself in a "debate" with
> George Greene. Struggling with myself, I hope to withdraw, leaving George
> basking in the glory of his victory by default. However, for benefit of
> those wondering what I've been going on about -- a vast multitude, no doubt
> --

Don't sweat it.
There is after all a real world.
Life is finite.
"I'm going to DIE, so who CARES what's provable?"
That was probably the single most irritating thing about
having to debate Phil.

Seriously, though, when I was posting during May 25-28, it was
from a hotel lobby in Time Square, between social obligations
associated with the wedding of my youngest sister, who met a
nice young man from Queens and decided to have a wedding
with him on the campus of Columbia University. I had to participate
in some small way, and I had to be there throughout the weekend.
Then I had to deal with attending a high school reunion this
past weekend in Massachusetts, followed by (FINALLY, after
almost 3 years) an interview for an actual computer job -- I
apparently
had to do a long penance for not actually FINISHING a dissertation
@cs.unc.edu.

So I am only just now getting back to this. And I may not be here
long; if the interview was successful then I will have to move from
North Carolina to Connecticut and that will also keep me too busy
with real-world issues for "recreational arguing".

> I'll say a few words (ha-ha!) about formalisation. In the following I'll
> concentrate on formalisation of arithmetical statements, properties,
> relations and such like, for simplicity. I have also chosen not to be too
> fussy about details; the reader is asked to mentally insert the standard
> fluff about a variable being free for substitution in a formula,
> simple-minded pedantry about the use-mention distinction, and so on.

This does somewhat raise questions of the target audience.
The use-mention distinction is NOT trivial (although only trivial
aspects of it may be necessary to make *these* points).
Evaluation UNDER quotation requires care, for example.

My main motive, as a student who sometimes got confused,
was to whine that entrenched aspects of terminology were themselves
more responsible than my personal ignorance for some of that
confusion.
The canonical presentation was not as conceptually well-patterned,
or regular, as it MIGHT have been. Now, obviously, scientific
revolutions
in general are already hard enough that trying to bring about a mere
terminological revolution when the actual CONTENT/meaning of what
is being said is NOT going to change, well, might seem to be the most
VAIN sort of tilting at windmills (in both senses of vain).

But I was very badly surprised by the kinds of reactions I got to
suggesting that maybe we ought to phrase some things a little
differently. Torkel in particular got not only ridiculously rude but
ridiculously prone to over-simplify, distort, and mis-analogize, IN
ORDER to be able to rebut strawmen. The last thing I did before
departing to deal with the real world was try to explain how AK had
recently repeated that mistake.

> An important note about terminology: in the following 'statement' will
> always refer to a mathematical statement in ordinary mathematical English
> while 'sentence' or 'formal sentence' will usually refer to a string of
> symbols in the mathematically defined language.

This message has mostly been about WHY I was absent from the
conversation, so I will save my substantive reactions for the next
one,
but the first point, here, again, is about target audience. The
pedagogical
community at large Really Does Already Have A Standard Natural Way of
talking about these things. WHY, therefore, DOES ANYone need to
restate
a personal conception of THAT way?? THE ONLY motivation for BOTHERING
to REpresent (present again, not explicate or translate) that
treatment would
HAVE to be to IMPROVE on it in some way, to publicly AGREE WITH
GEORGE GREENE that just MAYBE what is entrenched HAS NOT yet
been perfected and that we-here-in-this-newsgroup COULD strike a blow
for IMPROVING the presentation somehow!

My point is that AK in I were actually in a serious conflict (EVEN if
it
was a tempest in a teapot) and that if he is now going to present a
new treatment, HE IS CONCEDING the CORE issue that the conflict
was about (namely, whether the canonical presentation and terminology
did or did not need improving).

Of course, I suppose we could maintain the conflict by insisting that
the
improvements that HE might advocate were in the opposite direction
from,
or otherwise incompatible with, the improvements that I might
advocate,
but to me personally, that would almost be beside the point. The
HARDER
problem is figuring out how, given ANY sort of objection to the
entrenched
linguistic pedagogical practice, to make that objection EFFECTIVELY,
to
actually make the community at large BOTHER with anything we might
be saying!

I would consider anybody seriously trying to do that to be co-
operating
and not competing (with/vs. my agenda), up to a point. But conflict
even
over *this* question of *means* could RE-arise if AK is going to
insist
on trying to prove that "if you want to be effective, you need to
write
as coolly and carefully as possible", whereas I would insist the exact
opposite, namely, that the only errors that are SEVERE enough to be
worth BOTHERING to TRY to correct are the ones that are SO bad that
you are ENTITLED to be angry about them, that EVERYbody who is
complaining about them NEEDS to sound angry in the process.

george

unread,
Jun 12, 2007, 2:58:36 PM6/12/07
to
On Jun 5, 8:34 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:
> An important note about terminology: in the following 'statement' will
> always refer to a mathematical statement in ordinary mathematical English
> while 'sentence' or 'formal sentence' will usually refer to a string of
> symbols in the mathematically defined language.
>
> Why should we want to formalise arithmetical
> statements and notions in the first place?

You cannot put the genie back in the bottle.
If you stand on the shoulders of giants, you cannot
get back down, not easily enough to make bothering-with-it
worthwhile, anyway. Analogy:
http://www.amazon.com/Wild-Trees-Story-Passion-Daring/dp/product-description/0812975596
It turns out that the tallest trees in the world
(northern California coast redwoods)
are so tall that
>> The deep redwood canopy is a vertical Eden filled with mosses,
>> lichens, spotted salamanders, hanging gardens of ferns, and thickets
>> of huckleberry bushes, all growing out of massive trunk systems that
>> have fused and formed flying buttresses, sometimes carved into blackened
>> chambers, hollowed out by fire, called "fire caves."
>> Thick layers of soil sitting on limbs
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>> harbor animal and plant life that is unknown to science.
>> Humans move through the deep canopy suspended on ropes,
>> far out of sight of the ground, knowing that the price of a small
>> mistake can be a plunge to one's death.

My point is, if you want to view modern mathematical knowledge
as growing up from some soil and forming an ecosystem, I think
my opponents are mis-identifying the soil it is growing in. It is NOT
growing in the GROUND. It is NOT growing from basic simple things
that mathematically unlearned people think about. IT IS RATHER
growing
in the soil matted in the redwood canopy, the soil accumulating ON
THE BRANCHES that are ALREADY 300 FEET UP OFF the ground.
Everything WE think about math, we think in an intellectual context
brought to us AFTER Godel, AFTER Cantor, AFTER Russell, AFTER
Frege and Gauss. Piagetian innocence IS NOT re-capturable.
It WOULD NOT be reasonable to try to re-plant this ecosystem
300 feet down on the same ground that the redwood trunk is growing
out of! It is higher and better and JUST RIGHT JUST WHERE it IS!

> One possible reason is that we'd like to know, with
> mathematical certainty, whether some statement can be proved

No. Statements cannot be proved. END of story.
You yourself will say this later. But before we agree
with your point (modulo one single misused word "about"),
I want to make MY point.
My point here is that alleging that
> we want to formalise arithmetical
> statements and notions
is preposterous. Don't parse that adjective as "ridiculous" or some
other simplistic blanket condemnation. I chose it carefully; I meant
it literally: "preposterous" as in putting what ought to be
"posterior"
in the "pre" or "before" position, i.e., it is ASS-BACKWARDS.
Because:
NO notion *is* ARITHMETICAL to begin with
UNLESS it is FORMAL to BEGIN with!
You CAN'T be talking about FORMALIZING something that
NECESSARILY AND BY DEFINITION STARTED OUT formal!
This is NOT a question of the language you phrase it in!
Its MEANING/CONTENT IS INHERENTLY formal!
Numbers and all other mathematical entities are, precisely to the
extent
that they are mathematical, ABSTRACT AND THEREfore
formal TO BEGIN with! IT IS NOT as though we BEGAN
with some NATURAL language notion that was born correct and
meant exactly what we wanted it to mean, NOT if we are talking
about THIS stuff! IT IS RATHER that we began with some knowledge
about a realm that was INHERENTLY ABSTRACT AND FORMAL TO
BEGIN WITH and then ATTEMPTED TO APPROXIMATELY DESCRIBE
it using natural language! To the extent that that began to seem
inconvenient,
we then tried with various formal languages or linguistic paradigms,
but
because they were formal, we were able to PROVE that THEY were
not merely inconvenient to use, but actually inaccurate in certain
ways.
Of course, to say of anything that it is inaccurate is to claim
knowledge
on some level of ideal that it was supposed to match, but my point
is, natural language IS NOT so perfect that you can claim that our
natural-linguistic practice in trying to point at and describe that
ideal
is itself necessarily successful, because:
Fundamentally, natural languages are simply inconsistent.
You can ameliorate some of that by making them partial,
but that, too, takes A LOT of work.

In any case, natural languages do not even NEED to be RELEVANT
in the FIRST place, GIVEN that the WHOLE REALM here IS FORMAL
to begin with!


> using these or those principles.
> Mathematical statements aren't mathematically defined
> objects

OH, SHUT UP.
You can have a mathematical theory of natural language just as easily
as you can have a mathematical theory of anything else.
LETTERS, TOO, are abstractions. Sounds are not but they're close;
just because all the tokens have to be concrete doesn't mean the class
is.

> and thus there can be no question of mathematically proving stuff
> about them;
Almost right. This is the agreement I was speaking of above.
This is you and me AGREEING that natural language statements
canNOT be PROVED. ALMOST: because you said
> proving stuff about them.
Bzzzzt. INcorrect use of ABOUT.
There can be no question of mathematically proving THEM, the
statements,
THEMSELVES, BECAUSE THEY are in natural language, while proof,
like numbers, is, again, INHERENTLY abstract and formal.
But proving things ABOUT natlang statements (mathematical or
otherwise;
THAT doesn't even MATTER) is entirely possible; again, you just
postulate
some axioms for a formal theory about the natural language.

> thus we need to provide some mathematical model of our
> mathematical reasoning and mathematical language, a model that captures
> faithfully those aspects of our mathematical reasoning and language we're
> interested in, if we are to investigate these things mathematically.

Completely false.
Again, this assumes that all the true mathematical statements and
therefore all the reasoning proving new ones from old ones WAS going
on in natural language, and that we are just trying to formalize it.
THAT IS NOT THE CASE. That cannot POSSIBLY be the case
EXCEPT to the extent that the natural language HAS INCORPORATED
DEFINED PARTS OF some formalism, IS APING a formalism (it is
plastic enough to do that).

> Hence: formalisation.

No. Hence, naturalization, for purposes of shared communication,
of a process that was formal but perhaps idiosyncratic (the way I
reason about addition may not be the way you do). People inherently
have a faculty for formal reasoning and dealing with abstractions.
It is not necessarily properly expressed or encumbered with the
separate
faculty for dealing with natural language (though of course there is
some
intersection; my point is simply that it IS intersection at the
SUPERstructural
level and NATURAL language IS NOT the FOUNDATION or substructure
for reasoning WITH or about ABSTRACTIONS).

> To get started we define

Oh, shut up.
Before you can issue/utter a definition, you have to have
already defined some criteria for how THAT'S permissible.
How are you supposed to define anything if you don't even
know what a definition is (unless you are Phil)? How are you
supposed to learn what a definition is before somebody TELLS
you the DEFINITION of "definition"? You can't be simplistic
and blase' about how we get started. You have to DEFEND
your choice of starting point.

Frederick Williams

unread,
Jun 14, 2007, 10:43:34 AM6/14/07
to
Peter_Smith wrote:
>
> On Jun 10, 4:01 pm, Frederick Williams <"Frederick
> Williams"@antispamhotmail.co.uk.invalid> wrote:
>
> > Is it the mathematicians' claim that the mathematical English could
> > always be translated into, say, ZFC, with the proofs going over into
> > valid ZFC proofs?
>
> Odd, a post didn't appear. I'll try again (more briefly)!
>
> "Translate" isn't perhaps the right word. But sure, we find proxies
> for other mathematical structures (most of them, anyway) inside ZFC --
> as when we take a certain set of sets to stand proxy for the natural
> numbers. And then claims about those structures get mapped, hopefully,
> to ZFC theorems. But what does that show, exactly??

What it might have meant once, is that theorems about natural numbers
(say) where about something that one might almost call "concrete" and
that the theorems' truth was thereby guaranteed.

I recall reading something by Russell in which he said that Peano's
axioms didn't tell one what 0 and ' _really_ are because 0 could mean
one and ' could mean half-of so long as one then took the natural
numbers to be 1, 1/2, 1/4, ... . All the consequences of Peano's axioms
would be true of those numbers but they would not be numbers in the
everyday sense. This presumably ties in with Russell's realism--numbers
are as real as animals in a zoo.

I think Z (if not ZF) dates from 1908 (a bit before PM). Was Zermelo
trying to say what numbers (etc) really _were_ and were his intentions,
like those of Russell and Frege, to give a solid foundation for
mathematics?

Now, when one studies ZFC as a mathematical entity itself, it seems no
more certain than let's say analysis.

> Say, if you like, that (most) mathematics is, in this sense,
> formalizable into the framework of a certain theory that has a
> canonical formal presentation. But formalizABLE doesn't mean
> formalizED (any more than breakable means broken). The fact remains
> that everyday mathematics does not proceed in a formalized framework
> (most mathematicians would be completely stumped if you asked them to
> give the axioms of ZFC!) -- and it is none the worse for that.

--

george

unread,
Jun 14, 2007, 1:21:16 PM6/14/07
to
On Jun 5, 8:34 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:
> To get started we define a language with mathematically defined syntax and
> semantics, that, hopefully, is expressive enough to allow us to rephrase
> arithmetical statements and notions in a form amenable to mathematical
> analysis.

This is just utterly silly. You are presupposing that we have
"arithmetical
statements" in natural language. Natural language already has rules
of
grammar and syntax. The PIECE of natural language IN which we were
going to make these "arithmetical statements" COULD ITSELF HAVE
BEEN *FORMAL* to start with! You can decree that some statements are
going to be in natural language, but you can then also decree that
rather
than availing yourself of every last construction that can be dreamt
up in
natural language, you are going to use natural language in a
restricted and
therefore formalized way, and that these statements, YOUR preferred
language
for discussing arithmetic, are going to conform to some extra
structural rules
on top of the ones for natural language.

> First, we have symbols for addition,
> multiplication, equality, 0 and 1:

And this is NOT merely silly: THIS is IDIOTIC.
YOU ARE GOING to wind up using a first-order language here.
YOU ARE GOING to wind up stating axioms in this language.
IT IS NOT going to MATTER *which* symbols you use for these
concepts! The concepts are going to be DEFINED BY THE AXIOMS
AND NOT by the natural language "statements" that you are trying to
"translate"!

> "+", "*", "=", "0" and "1".

No, no, no, no, no.
You are going to have two binary functions, one binary predicate,
and two 0-ary functions or constants.
And it is, I repeat, NOT going to MATTER how they are SPELLED!

For that matter, it is also not going to matter that you chose this
particular signature as opposed to another. Using s(.) instead of 1
has lots of advantages, the most important of which is that the
function
that adds 1 to something ALREADY LOOKS like a function, instead of
lemmatically needing to be proved to be a function.

george

unread,
Jun 14, 2007, 1:34:07 PM6/14/07
to
On Jun 5, 4:42 pm, Peter_Smith <p...@cam.ac.uk> wrote:
> Well, since no one else has bothered to respond,
> I'll just say: great stuff Aatu.

Yeah, these mutual masturbation societies can
be VERY gratifying.


> What you say is a very nice counter to two confusions that people do
> seem to be tempted by.

In your ignorant personal opinion.

> (1) Some think that formalization is of the essence of mathematics (so
> no formalization, no genuine proofs). Not so.

Oh, shut up.
We don't even have to THINK that. We can just DEFINE it.
It does MATTER what things MEAN.

> As you say, mathematical


> proofs can and usually are conducted in "ordinary mathematical
> English" (or Finnish, or whatever!):

That is laughable on its face.
Just because that is how people usually
talk does NOT mean that EVEN a majority OF THOSE
TALKERS would agree with this!

A proof is an inherently formal thing,
just as surely as a symbol or a number is.
All these things are abstractions. That people
choose to talk about them using natural language is
IRrelevant to the issue at hand; people can and do use natural
language to talk about EVERYthing -- that's what natural
language is FOR. The fact that such talk goes on DOES NOT
CHANGE the INHERENTLY abstract character of the things that
this natural language IS ABOUT.

> formalization comes in

NO, IT DOESN'T. Formality WAS ALWAYS present.
The things being talked about WERE INHERENTLY ALWAYS
formal. Two BY DEFINITION ALWAYS HAS a FORM that looks like
some replicated and concatenated version of WHATEVER form
ONE had.

> if and when we want to mathematically model such proofs

This is completely absurd. The natural language description of the
proof was just that, always: a description and an approximation.
The proof or proof-object itself WAS ALWAYS an inherently formal
thing, just as surely as three was always a number.

> in certain ways for certain purposes.

Well, it is true that various realms of discourse were inherently
amenable to axiomatization in more than one way, that formal
treatment will suffer from a "multiple reduction problem".
It is at least imaginable in principle that somebody could have a
natural-language proof of a truth-in-such-a-realm with the property
that it remained convincing WITHOUT being tied to any PARTICULAR
axiomatization. BUT WE ARE NOT HOLDING OUR BREATH.
What you will almost always find in all real-world cases is that
the natural-language proof DOES wind up eventually relying on
PARTICULAR axioms, or, at best, ON LEMMAS, which will then
stand themselves in need of some natural-language justification,
which, if it is forthcoming and correct, will, EVENTUALLY, rest
on axioms, and EVEN IN THE NATURAL LANGUAGE TREATMENT,
those axioms WILL BE apparent.

> (2) Some think that going formal means turning our backs on semantic

> notions like truth. Not so. The formalized languages we are usually


> interested in are, on the contrary, interpreted languages

Shut the FUCK up!
There is NEVER ANY NEED to interpret ANY first-order
language IF you are willing to claim THE FIRST-ORDER
CONSEQUENCES (of your axioms) and NOT go beyond that!
And IF you go beyond that you ARE CERTAINLY
going to need TO JUSTIFY going beyond that!

"We are usually interested in interpreted languages"
IS JUST A DAMN LIE. Unless "We are usually using 2nd-
order logic", BOTHERING to interpret your language ISN'T EVEN
GOING TO *gain* you anything!

> (not just empty syntax),

Syntax IS NOT *empty*,
YOU FUCKING MORON!

> and we can typically give neat definitions of the truth-
> conditions of the sentences of the languages,

Well, we usually call those axioms.

What you THINK you are doing is just begging
bunches of actually relevant questions.

Seriously, this is one of the most embarrassing things you have
ever posted. "Empty syntax"?!? IN a LOGIC group?????

Peter_Smith

unread,
Jun 14, 2007, 3:01:59 PM6/14/07
to
In the middle of exam marking, I find myself giving George a lower
second for content (and a fail for style!).


Peter_Smith

unread,
Jun 14, 2007, 3:19:55 PM6/14/07
to
>> Sure, we find proxies

> > for other mathematical structures (most of them, anyway) inside ZFC --
> > as when we take a certain set of sets to stand proxy for the natural
> > numbers. And then claims about those structures get mapped, hopefully,
> > to ZFC theorems. But what does that show, exactly??
>
> What it might have meant once, is that theorems about natural numbers
> (say) where about something that one might almost call "concrete" and
> that the theorems' truth was thereby guaranteed.

I wonder exactly what (almost) "concrete" means here? In what sense is
the hierarchy of pure sets almost concrete?

I wonder too in quite what sense e.g. reconstructing Peano Arithmetic
inside ZFC "guarantees" the truth of its theorems in a way they
weren't guaranteed before??


herbzet

unread,
Jun 14, 2007, 10:05:26 PM6/14/07
to

Peter_Smith wrote:
>
> In the middle of exam marking, I find myself giving George a lower
> second for content (and a fail for style!).

Oh, you just need to learn to appreciate the subtleties of
George's style, that's all.

--
hz

--
Posted via a free Usenet account from http://www.teranews.com

george

unread,
Jun 15, 2007, 11:44:28 AM6/15/07
to
On Jun 5, 4:42 pm, Peter_Smith <p...@cam.ac.uk> wrote:
> (2) Some think that going formal means
> turning our backs on semantic notions

Not really.
The completeness theorem means that (at least at 1st-
order and below) you can define logical consequence
EITHER in terms of syntax or semantics and that BOTH
definitions are EQUIVALENT. It is NOT like there can be
COMPETITION between these viewpoints, at 1st-order.
You have to go up to make the difference MATTER.

> like truth. Not so. The formalized languages we are usually
> interested in are, on the contrary, interpreted languages

At first-order, that is just bullshit.
There is simply never any NEED to interpret
a first-order language as long as you have term-constructors
(via skolemization or something) for the existential quantifiers.
If the signature is rich enough to generate infinitely many syntactic
terms then the theory is guaranteed to have a model where the
terms are interpreted as THEMSELVES, and it is NOT like anybody
NEEDS any other models. If they really want them then obviously
they are welcome to add axioms producing them (or at least getting
closer to them).

> (not just empty syntax),
previously dismissed

> and we can typically give neat definitions of the truth-conditions

If they really are CONDITIONS then that implies -- in the form of
a CONDITIONAL -- that IF these conditions are true,
THEN the sentence MUST be true! THIS IS MODAL!
This is PROVED! In a THEORY! SYNTACTICALLY!
FROM AXIOMS! So claiming that this is somehow a semantic
as OPPOSED to a syntactic take on it is ridiculous. It is just
syntactic all over again IN THE META-THEORY.

> of the sentences of the languages, as you do for a language
> for elementary arithmetic.

Again, those conditions wind up looking a lot like the first-
order axioms.

george

unread,
Jun 15, 2007, 12:01:34 PM6/15/07
to
On Jun 10, 6:55 am, Aatu Koskensilta <aatu.koskensi...@xortec.fi>
wrote:

> It is true that in the ordinary sense mathematics is quite formal, and
> precision, rigour, tedious attention to details,
> and all that, are hallmarks of mathematics.

Then YOU LOSE. JEEzus. Your whole founding post
of the thread is just bullshit, in that case.

> My post concerned formalisation only in the technical sense.

You have no clue whatsoever what that sense EVEN IS.
AS YOU are basically already conceding, THE WHOLE SUBJECT
MATTER *IS* formal -- BECAUSE it is ABSTRACT -- to BEGIN
with! It therefore CANNOT EVER GET formal*IZED*!

It does MATTER at this juncture that the name of THIS group
is sci.logic AS OPPOSED to sci.math! We are NOT HERE
so VERY much ABOUT what "mathematicians" in GENERAL
may or may not be doing! We are SPECIFICALLY concerned
with approaching this FROM A *LOGICAL* point of view!

Crispin Wright and the whole neo-Fregean programme very
much legitimize that effort. But a lot of what you have been
trying to say in allegedly debating me is just COMPLETELY
ineffective. You don't even have a thesis, let alone a case.
"I have an interpreted language", you say.
And that is just bullshit. The particular symbols you claim
constitute your language ARE PURELY CULTURALLY
CONVENTIONAL and are NOT necessary OR EVEN GERMANE
to the enterprise! It is a DEFINING feature of THIS enterprise, of
the
MATHematicality of this enterprise, that ANY old symbols would do!
It is BECAUSE THIS is MATH, that any old symbols would do!
If it WEREN'T math then they WOULDN'T! You are being LESS,
NOT MORE, mathematical, and LESS, not MORE, *arithmetical*,
IF you try to insist that "the" language of arithmetic involves
some specific names for the operators, or some specific numerals.
The fact that these symbols are the ones
that have been typically used is of pedagogical importance for
adolescents but completely IRrelevant to adults! So, first of all,
you DON'T have an "interpreted language" because you don't have
A language. It is NOT EVEN IMPORTANT which language is used.
The only reason why we APPEAR to have *A* language is simply
that if all of us want to talk about arithmetic, it is easier to
conventionally do it with 1 vocabulary than to force everybody to
re-explain their personal choice at the beginning of every article.
And even WITH the substantial agreements and conventions on
a language for arithmetic, YOU STILL can't agree with others
about whether successor(1) should be spelled s(s(0)) or 1 + 1.


You could then of course continue that regardless of what other
symbol anyone might use for 0, or 1, or +, or *, that those
alternate symbols could then be interpreted. Of course they
could. But they do NOT *need* to be! Anything that is going
to be true under ALL reasonable interpretations of those symbols
is going to be PROVABLE, SYNTACTICALLY, WITHOUT recourse
TO ANY interpretations! So, second of all, you DON'T have an
interpreted language because you can't JUSTIFY BOTHERING with
any interpretations, at least not until you discover "Con(PA)" or
some other sentence, that, because it is undecided, simply DOES
NOT MEAN what you "want" it to mean.


george

unread,
Jun 15, 2007, 12:03:36 PM6/15/07
to
On Jun 14, 3:01 pm, Peter_Smith <p...@cam.ac.uk> wrote:
> In the middle of exam marking, I find myself giving George a lower
> second for content (and a fail for style!).

You have greatly mis-identified who is in whose class, here.


george

unread,
Jun 15, 2007, 12:22:31 PM6/15/07
to
On Jun 14, 3:01 pm, Peter_Smith <p...@cam.ac.uk> wrote:
> In the middle of exam marking, I find myself giving George a lower
> second for content (and a fail for style!).

OK, I concede that calling you a *F*IN' MORON!"
was failing. But surely even you must concede that
to say, INside a logic group, that "syntax" is "empty"
is akin to farting in church. First-order theories founded
on recursive axiom-sets ARE PURELY syntactic; all
the theorems that are proved from the axioms are proved
by purely syntactic means. 1st-order PA may not be
able to prove Con(PA) or the Paris-Harrington-Ramsey
theorem, and you may know that these things must
be true in the intended model, but that STILL DOES NOT
obligate you to resort to "semantics instead of syntax"!
YOU HAVE a PREFERRED MEANS of constructing
"semanticses", and, precisely as this appendix (of
a text about Godel's theorem) argues, your preferred
tool for building models and investigating model theory
IS ITSELF A (syntactic!) FIRST-ORDER (recursively-
axiomatizable) theory, NAMELY, FIRST-order ZFC!
http://www.ltn.lv/~podnieks/gta.html

Peter_Smith

unread,
Jun 15, 2007, 8:15:33 PM6/15/07
to
> First-order theories founded
> on recursive axiom-sets ARE PURELY syntactic; all
> the theorems that are proved from the axioms are proved
> by purely syntactic means.

While the second is true (quite trivially, by the standard definition
of a theorem), the first is plain false. The sort of first-order
theories we are typically interested in are built in interpreted
languages, and have semantic as well as syntactic properties.

As for the rest of the remarks, they are based on an elementary
misunderstanding. We can, of course, model anything more or less
anything you like, with a bit of cunning, in ZFC. Which means that the
fact that you can formally model semantic theories inside ZFC doesn't
tell us any more about the nature of semantic properties than the fact
that you can formally model mechanics in ZFC tells you about the
nature of physical properties, or the fact that we can model the
trajectory of Paris Hilton in and out of jail in ZFC tells us about
the nature of modern celebrity. Don't confuse a mathematical model of
semantics with semantics. (And of course, first-order ZFC is itself an
interpreted theory with a well understood intended interpretation.)

Barb Knox

unread,
Jun 17, 2007, 7:25:02 PM6/17/07
to
In article <1181923294.9...@q66g2000hsg.googlegroups.com>,
george <gre...@cs.unc.edu> wrote:
[most snipped]

> THE WHOLE SUBJECTMATTER *IS* formal -- BECAUSE it is ABSTRACT --
> to BEGIN with!

In several posts you state that anything abstract must necessarily be
formal. That's an interesting claim, and I'd like to see some
justification for it.

Presumably anything formal is necessarily abstract, so you appear to be
implying that abstract <-> formal. Right? But at least in English, the
two notions seem rather different, although they do intersect. One can
have a formal procedure (a "formula" or recipe) for doing something
thoroughly concrete, like cooking dinner, or mixing concrete (pun not
originally intended).

Also, in ontological philosophy, there are various sorts of abstractions
that don't seem at first glance to be formal. For example, universals.
The class or concept "chair" is fully abstract, but do you really think
it's formal? If so, what's its formalisation?


--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------

Nam D. Nguyen

unread,
Jun 18, 2007, 2:17:00 AM6/18/07
to

It seems to me the rules of inference as part of (syntactical) formalism
do serve a purpose in FOL: correct reasoning; and so does intuition some
purposes: without it there can be no models or mathematical concepts.
But given our reasoning ability is finite, how far could either (syntactical)
formalism or intuition go, in term of helping us to reflect our "correct"
reasoning on abstract mathematical concepts? Imho, not very far!
If "limitation" connotes "problem" then let me take this opportunity
to outline families of major problems in current reasoning framework
(through FOL).

1) Problem type 1: Subjectivity (relativity) of abstract concepts, hence of
mathematical truths.

Imagine a spherical surface without the 2 "polar" points. Now, given
a particular "structural" relation R among the lines of the sphere
so that we could interpret R(L1, L2) as true. But suppose further
the underlying language L has a binary predicate Parallel(l1,l2)
where l1,l2 are L's symbols denoting some particular lines. But to me
for instance, I could interpret L1, L2 as parallel on the account
that they don't intersect! Or alternatively I could *see* them as *not*
parallel on the account that their distances seem to converge to 0 as they
approach either poles (for a suitable definition of "distance" e.g.)!
The point is even if R(L1, L2) is a true interpretation of in the language L,
the mental mapping between that truth and either Parallel(l1,l2),
or ~Parallel(l1,l2) of the formal language L is a subjective choice
(between the 2 abstract concepts of being parallel, or not).
Hence mathematical truths, which originate from an individual's abstraction
*will* always be subjective (i.e. relative). Look at it in another way,
if ~(1+1=0) were an absolute truth that saying otherwise would blatantly
violate logical reasoning framework, then we'd *never* be able to say 1+1=0
as an mathematical truth, which is not true: arithmetic modulo 2 would allow
us that!

2) Problem type 2: Finiteness-Limitation of FOL framework.

Type 2a: Individual-Finiteness.

We could say a *finite* numbers of sentences such as 2 is a prime",
"3 is a prime", "4 is not a prime", ... But there are *infinite* of
such sentences, and if arithmetic is consistent and we accept our
reasoning ability is finite, then there *will* exist,
*for each individual*, a number in which the individual can't know
if it's a prime or not! Currently, FOL framework "condones" this
type of limitation, in the sense that an individual A might have
a number p as this type of limitation, while another individual B
might not have p as this kind of limit (e.g. B's limitation number
in this context might be p' which might be much ... much greater
than p!). Hence FOL framework would treat it as if this kind of
limitation were non-existent (since in principle, there might
exist individuals who would not see p as a limitation number!).

Imho, if this were the only type of limitation then that would be
OK. In reality, there is another type of limitation on the whole
FOL framework, then it's not OK to ignore this type of limitation.

Type 2b: FOL-Finiteness.

If arithmetic is not consistent, there will be an arithmetic theorem
of the form (F /\ ~F), whose proof in principle would be "visible"
to some reasoning individuals (human or not). If on the other hand
arithmetic is consistent, no finite-ability individual (human or not)
will ever be able to prove *that fact*, within FOL syntactical
formalism.


These 2 major families of limitations (problems) are among the reasons I've
proposed we modify FOL to improve it. If we don't improve FOL framework
to formally acknowledge these limitations, we'll pay a heavy price: there
will be arithmetic truths that we could express as a formula, and yet we
could *never* prove its truth!

Nam D. Nguyen

unread,
Jun 18, 2007, 2:23:45 AM6/18/07
to
Barb Knox wrote:
> In article <1181923294.9...@q66g2000hsg.googlegroups.com>,
> george <gre...@cs.unc.edu> wrote:
> [most snipped]
>
>> THE WHOLE SUBJECTMATTER *IS* formal -- BECAUSE it is ABSTRACT --
>> to BEGIN with!
>
> In several posts you state that anything abstract must necessarily be
> formal. That's an interesting claim, and I'd like to see some
> justification for it.
>
> Presumably anything formal is necessarily abstract, so you appear to be
> implying that abstract <-> formal. Right? But at least in English, the
> two notions seem rather different, although they do intersect. One can
> have a formal procedure (a "formula" or recipe) for doing something
> thoroughly concrete, like cooking dinner, or mixing concrete (pun not
> originally intended).
>
> Also, in ontological philosophy, there are various sorts of abstractions
> that don't seem at first glance to be formal. For example, universals.
> The class or concept "chair" is fully abstract, but do you really think
> it's formal? If so, what's its formalisation?

According to Shoenfield, "a formal system is the syntactical part of an axiom
system" and which would comprises of 3 main components:

- a language
- the axioms
- The rules of inferences (which are common to all formal systems).

Naturally.


>
>

george

unread,
Jun 18, 2007, 2:26:51 PM6/18/07
to
> > First-order theories founded
> > on recursive axiom-sets ARE PURELY syntactic; all
> > the theorems that are proved from the axioms are proved
> > by purely syntactic means.

Peter Smith replied,


> While the second is true (quite trivially, by the standard definition
> of a theorem),

Thank goodness. The battle is at least half over.

> the first is plain false.

NO, DUMBASS, the first is EQUIVALENT.

> The sort of first-order
> theories we are typically interested in

Oh, shut up. YOU ARE NOT TYPICAL,
ESPECIALLY not in the context of a group that is
NAMED sci.LOGIC! I repeat, this is NOT sci.MATH!

To refute your claim about "the first" part, *I* *SAID*,
first-order theories FOUNDED ON RECURSIVE AXIOM-SETS.
YOU, by contrast, continued

> are built in interpreted languages,

Obviously, as YOU already know too well, IT DOES
MAKE A *DIFFERENCE* whether you are taking, as the
prior founding precept, the axiom-set or the intended model!
It is the whole import of Godel's 1st incompleteness theorem
that if the first-order theory of the standard model is what
you are interested in, THEN NO theory founded on a
recursive first-order axiom-set will completely cover the truths
of your alleged interpretation!

You are welcome to allege that founding things on recursive
first-order axiom-sets is simply too limiting, too Procrustean,
to be of interest to mathematicians generally, but my short retort
to that is that that is why I decided to study computer science and
logic instead of true/standard number theory.

> and have semantic as well as syntactic properties.

BY DEFINITION, by the completeness theorem, IF you
are dealing with the theory defined as the closure (under
consequence) of the (recursive) first-order axiom-set, this
is a distinction WITHOUT a difference! The approaches are
COMPLETELY COEXTENSIVE AND EQUIVALENT! You DO
NOT get to argue that one has anything "as well as" or in
addition to the other!

If you want to claim that you have some alleged interpretation
of the language that transcends all known r.e. theories, then
you have a burden of specification that you fundamentally
simply cannot meet. You simply do NOT KNOW WHAT
your allegedly standard model SAYS about TOO many questions.
You cannot even IDENTIFY the standard model at first-order
without appealing to ZFC. But if you appeal to FIRST-order
ZFC then THAT, AGAIN, is a recursively axiomatizable theory
that DOES NOT NEED to be interpreted IN ANY way in order
to accomplish your goal (or a reasonable approximation thereof).

> As for the rest of the remarks, they are based on an elementary
> misunderstanding.

Oh, shut up.
You have to actually SHOW that somebody has misunderstood
something. You can't just disagree with it for spite.

> We can, of course, model anything more or less
> anything you like, with a bit of cunning, in ZFC.

Not the issue. What you need specifically is THE INNER
model of PA, the model that occurs as a submodel of all
the other models, the standard model.

> Which means that the fact that you can formally
> model semantic theories

Bzzzt. There is no such thing as a semantic
theory. Theories are sets of sentences that are
closed under logical consequence. At first-order,
logical consequence is definable as a PURELY syntactic
relation.

> inside ZFC doesn't tell us any more about the
>nature of semantic properties

Bzzzt.
You are skipping a step here. The completeness theorem
invites SEMANTICS IN TOTO to be COMPLETELY EXILED
FROM THIS DISCUSSION. Your first burden of proof is
to JUSTIFY RE-introducing it AT ALL. NOBODY GIVES A
FLYING FUCK about the nature OF ANY alleged "semantic
properties"! Your mission should you choose to accept it
is to begin by giving a 1st example of why semantics might
be important (PA's standard model) and THEN a 1st example
OF a "semantic property" that this model MAKES relevant.
We are NOT holding our breath. Your assumption that you
are EVER entitled to do ANY semantics at all, that you
can JUSTIFY ever BOTHERING to interpret a language,
IS WHAT IS AT ISSUE here.

> than the fact that you can formally model
> mechanics in ZFC tells you about the
> nature of physical properties,
>or the fact that we can model the
> trajectory of Paris Hilton in and out of jail in ZFC tells us about
> the nature of modern celebrity.

I retract my retraction.
You REALLY ARE a complete fucking moron (if you
have children). WE ARE TALKING ABOUT ABSTRACTIONS
here. Semantics IS NOT a concrete thing in the way that
billiard balls or people are. Formality IS the essence OF ALL
these things. ESPECIALLY natural numbers.
The fact that a first-order formalism can't capture finitude
does NOT mean that finitude is not a FORMAL property!
Finitude absolutely IS an aspect of FORM!

> Don't confuse a mathematical model of
> semantics with semantics.

I repeat, go fuck yourself.

> (And of course, first-order ZFC is itself an
> interpreted theory with a well understood
> intended interpretation.)

Even if that were true, it would be irrelevant.
You do not NEED to interpret ZFC in order to
use it to identify the inner/standard model for PA.
And there is a very striking dichotomy between ZFC
and PA in that in PA, the standard model is inner,
whereas in ZFC, it is basically "outer"; the alleged intended
model is the one with the "biggest" powersets.
In any case, claims that people know what they
intend as the relevant standard full model of ZFC
(as if such a thing can even exist; you can no more
have a biggest model of ZFC than you can have a biggest
natural number) are hubristic beyond endurance.
Given that you never need all that suff anyway, your
insistence that it must be out there is puerile.

george

unread,
Jun 18, 2007, 2:34:23 PM6/18/07
to
On Jun 17, 7:25 pm, Barb Knox <s...@sig.below> wrote:
> One can have a formal procedure
> (a "formula" or recipe) for doing something
> thoroughly concrete, like cooking dinner,
> or mixing concrete (pun not
> originally intended).

My Philosophy degree is a Bachelor's.
I am just winging it here. I have not taken a relevant
course. I would begin by saying that the only difference
occurs at the 0th or foundational level. You can think
or talk about anything. Once you start having sentences
ABOUT things, yes, you have automatically introduced one
level or layer of abstraction or formality. Levels 1 and higher
are ALWAYS going to be abstract. So the only RELEVANT
question becomes about LEVEL 0. What about the ORIGINAL
FOUNDATIONAL things you were talking about? Were THEY
abstract or concrete? THAT is the question.

> The class or concept "chair" is fully abstract,
> but do you really think it's formal?

I think that abstractions are formal by definition.

> If so, what's its formalisation?

THAT is NOT the point.
The point is that CHAIRS are concrete AND NOT
abstract, BY DEFINITION.
Any theories that people may want to define ABOUT
chairs will be at least nominally/superficially formal
simply BECAUSE they are theories and not chairs,
but that is not the point. The point IS that theories
about concrete things are different from theories about
abstract things. If I am going to allege that something is
formal, your appropriate challenge-question IS NOT "what
is its formalization", BUT RATHER, "what is its" FORM.

george

unread,
Jun 18, 2007, 8:08:40 PM6/18/07
to
On Jun 17, 7:25 pm, Barb Knox <s...@sig.below> wrote:
> Presumably anything formal is necessarily abstract,

No, truly, that is NOT presumable.
Concrete things exhibit form.
The adjective "dihedral" is not "inherently abstract".
Dihedral is a form. Concrete things can be dihedral.
One could further insist that any abstract thing that
has been characterized as dihedral has been so classed
ONLY by metaphor and analogy FROM the UNDERlying
CONCRETE form.

> so you appear to be implying that abstract <-> formal.
> Right?

I don't even know.
I don't normally have cause to do anything
in natural language. We escaped FOR A REASON,
you know.

> But at least in English, the two notions seem rather different,

One of My General Missions In Life is to DEBUG OTHER
people's usage of English. I am not so much interested in what
generally happens as in what (obviously, in my personal opinion) NEEDS
to be happening.
[The prescriptive semanticist strikes again.]


> The class or concept "chair" is fully abstract,

Not really. It is a necessary property of chairs
that they are concrete as opposed to abstract.
Given ANY thing x, you can usually talk about the
class of or the concept of x, which seems to need to
be purely abstract. But even if you concede that, you get
two different kinds of abstractions: those for which x was
abstract and those for which x was concrete.
My point in the debate I was actually having is that you
can debate whether your formalization or formation-of-the-
concept of x is accurate or adequate when x is concrete:
you can allege that MERELY going from concrete to abstract
COSTS you something ESSENTIAL and that the concept of
x is different from x in some deep and important way, is just
fundamentally inadequate to the role it is trying to play.
But MY POINT has been that MY OPPONENTS are alleging
that kind of disconnect between (e.g.) formal theories of (e.g.)
the natural numbers (or other objects about which they have
waxed mathematically platonistic in a BAD way) and natural
numbers, and that whining about the disconnect between x
and your concept of x is NOT appropriate, at least not on
grounds of formality and abstraction, WHEN x WAS ITSELF
INHERENTLY BOTH formal and abstract TO BEGIN with.

> but do you really think it's formal? If so, what's its formalisation?

I think that the context in which that question is APPROPRIATE
is necessarily the context of
The First-Order Theory Of Furniture.

If one is outside THAT context then I think it is appropriate
to simply dismiss the question.

george

unread,
Jun 18, 2007, 8:22:29 PM6/18/07
to
On Jun 11, 6:54 am, Peter_Smith <p...@cam.ac.uk> wrote:
>The fact remains that everyday mathematics
> does not proceed in a formalized framework

Your decision to trumpet this fact is stupid.
This fact is utterly deplorable.

> (most mathematicians would be completely
> stumped if you asked them to
> give the axioms of ZFC!) -- and it is none the worse for that.

We politely beg to differ.
We happen to be in a situation where we don't
actually NEED any breakthroughs in math.
Math is so far ahead of Physics that is so far
ahead of Engineering that none of this stuff will
have applications for a long time. In practical terms,
good math is in GREAT OVERsupply right now.
IF we were running SHORT and actually needed
to RECRUIT MORE good minds to produce it quickly
and properly, THEN IT WOULD BE IMPORTANT
to DO IT RIGHT.

Rupert should consider himself re-invoked here because
he had a professor (NW) who was at pains to BEMOAN
the fact that sheer graduate PEDAGOGY in math is NOT
well-founded axiomatically. His point was that IT WOULD
*HELP* if it were! You seem to be taking the tired line
that the formalism just gets in the way, that there are lots
of different adequate formalisms and that therefore there is
no point in getting insistent on the details of any particular one.

Maybe I will just hunt the quote down and re-invoke, myself.

OK, I did. NW is Norm Wildberger.
The following is excerpted from his
http://web.maths.unsw.edu.au/~norman/views2.htm
under the heading, "The Problem With Foundations".


In the first year of university the student encounters calculus more
seriously and some linear algebra, perhaps with some discrete
mathematics thrown in. Sometime in their second or third year, a
dramatic change happens in the training of aspiring pure
mathematicians. They start being introduced to the idea of rigorous
thinking and proofs, and gradually become aware that they are not at
the peak of intellectual achievement, but just at the foothills of a
very onerous climb. Group theory, differential equations, fields,
rings, topological spaces, measure theory, operators, complex
analysis, special functions, manifolds, Hilbert spaces, posets and
lattices---it all piles up quickly. They learn to think about
mathematics less as a jumble of facts to be memorized and algorithms
to be mastered, but as a coherent logical structure. Assignment
problems increasingly require serious thinking, and soon all but the
very best are brain-tired and confused.

Do you suppose the curriculum at this point has time or inclination to
return to the material they learnt in public school and high school,
and finally organize it properly? When we start to get really picky
about logical correctness, doesn't it make sense to go back and ensure
that all those subjects that up to now have only been taught in a
loose and cavalier fashion get a proper rigorous treatment? Isn't this
the appropriate time to finally learn what a number in fact is, why
exactly the laws of arithmetic hold, what the correct definitions of a
line and a circle are, what we mean by a vector, a function, an area
and all the rest? You might think so, but there are two very good
reasons why this is nowhere done.

The first reason is that even the professors mostly don't know! They
too have gone through a similar indoctrination, and never had to prove
that multiplication is associative, for example, or learnt what is the
right order of topics in trigonometry. Of course they know how to
solve all the problems in elementary school texts, but this is quite
different from being able to correct all the logical defects contained
there, and give a complete and proper exposition of the material.

The modern mathematician walks around with her head full of the tight
logical relationships of the specialized theories she researches, with
only a rudimentary understanding of the logical foundations
underpinning the entire subject. But the worst part is, she is largely
unaware of this inadequacy in her training. She and her colleagues
really do believe they profoundly understand elementary mathematics.
But a few well-chosen questions reveal that this is not so. Ask them
just what a fraction is, or how to properly define an angle, or
whether a polynomial is really a function or not, and see what kind of
non-uniform rambling emerges! The more elementary the question, the
more likely the answer involves a lot of philosophizing and bluster.
The issue of the correct approach to the definition of a fraction is a
particularly crucial one to public school education.

Mathematicians like to reassure themselves that foundational questions
are resolved by some mumbo-jumbo about `Axioms' (more on that later)
but in reality successful mathematics requires familiarity with a
large collection of `elementary' concepts and underlying linguistic
and notational conventions. These are often unwritten, but are part of
the training of young people in the subject. For example, an entire
essay could be written on the use, implicit and explicit, of ordering
and brackets in mathematical statements and equations. Codifying this
kind of implicit syntax is a job professional mathematicians are not
particularly interested in.

The second reason is that any attempt to lay out elementary
mathematics properly would be resisted by both students and educators
as not going forward, but backwards. Who wants to spend time worrying
about the correct approach to polynomials when Measure theory and the
Residue calculus beckon instead? The consequence is that a large
amount of elementary mathematics is never properly taught anywhere.

But there are two foundational topics that are introduced in the early
undergraduate years: infinite set theory and real numbers.
Historically these are very controversial topics, fraught with logical
difficulties which embroiled mathematicians for decades. The
presentation these days is matter of fact---`an infinite set is a
collection of mathematical objects which isn't finite' and `a real
number is an equivalence class of Cauchy sequences of rational
numbers'.

Or some such nonsense. Set theory as presented to young people simply
doesn't make sense, and the resultant approach to real numbers is in
fact a joke! You heard it correctly---and I will try to explain
shortly. The point here is that these logically dubious topics are
slipped into the curriculum in an off-hand way when students are
already overworked and awed by all the other material before them.
There is not the time to ruminate and discuss the uncertainties of
generations gone by. With a slick enough presentation, the whole thing
goes down just like any other of the subjects they are struggling to
learn. From then on till their retirement years, mathematicians have a
busy schedule ahead of them, ensuring that few get around to
critically examining the subject matter of their student days.


george

unread,
Jun 18, 2007, 8:25:11 PM6/18/07
to
On Jun 11, 6:54 am, Peter_Smith <p...@cam.ac.uk> wrote:
> Say, if you like, that (most) mathematics is, in this sense,
> formalizable into the framework of a certain theory that has a
> canonical formal presentation. But formalizABLE doesn't mean
> formalizED (any more than breakable means broken).

Oh, shut up.
The fact that this stuff is formalizable IS THE IMPORTANT
part! The fact that we don't actually generally bother with
it is NOT the important part! You do NOT get to claim that
the fact that basically EVERYbody is going around not-
bothering MAKES not-bothering OK! Most people think
bothering would be boring and think on some level that they
have a PROOF that it would be boring! BUT THEY DON'T!

> The fact remains that everyday mathematics
> does not proceed in a formalized framework

And the fact also remains that you personally are
at a complete and utter loss to JUSTIFY this as a
REASONABLE state of affairs, DESPITE its factuality.


Peter_Smith

unread,
Jun 19, 2007, 2:34:50 AM6/19/07
to
On 18 Jun, 19:26, george <gree...@cs.unc.edu> wrote:

>>and have semantic as well as syntactic properties.
>
> BY DEFINITION, by the completeness theorem, IF you
> are dealing with the theory defined as the closure (under
> consequence) of the (recursive) first-order axiom-set, this
> is a distinction WITHOUT a difference!

Nonsense. Of course by completeness, in a first-order context, some
semantic properties are co-extensive with syntactic ones (e.g. the
property of being a logically valid sentence is co-extensive with the
property of being a logical theorem), other semantic properties aren't
(as you yourself mentioned, the property of being a truth of first-
order PA is not coextensive with some nice syntactic defined
property).

>You cannot even IDENTIFY the standard model at first-order
> without appealing to ZFC

Nonsense. You just start, "0" denotes zero, "+" denotes the addition
function, etc.

> Semantics IS NOT a concrete thing in the way that billiard balls or people are.

But it can involve relations between expressions and concrete things
(as when we give a semantics for a formal language for regimenting
some physical theory).

>You do not NEED to interpret ZFC in order to use it to identify the inner/standard model for PA.

Nonsense. Uninterpreted squiggles can't be used to identify anything.

Peter_Smith

unread,
Jun 19, 2007, 12:39:02 PM6/19/07
to
> > The fact remains that everyday mathematics
> > does not proceed in a formalized framework
>
> And the fact also remains that you personally are
> at a complete and utter loss to JUSTIFY this as a
> REASONABLE state of affairs, DESPITE its factuality.

I'm a bit stumped to know why anyone should think that the normal
practices of mathematicians generally stand in need of justification.

0 new messages