FOM: Platonism and social constructivism

[Vaughan Pratt]

Machover:
>one of the most profound problems of the philosophy of maths only
>*begins*: how to account for the ineluctable, necessary, objective nature
>of mathematical propositions.

Sazonov:
>I am not sure that I properly understand the point of this question.  
>It is formulated in too general terms. 

A very good general problem, which hopefully is closely related to what
Machover has in mind, is that of the correlation between membership
in a theory and objective truth.  More specifically, is every theory
necessarily about something; to which theories can one naturally associate
a canonical model; and do mathematical objects necessarily exist outside
their referring theories?  In the area of programming languages, a
related question is, what constitutes a correct implementation of a
datatype specification?

Equational theories are a nice playground to start exploring such
questions.  One might think at first that the most natural model of an
equational theory would be the free algebra on some number of generators,
say zero, one, or countably many.  This works out nicely for the natural
numbers (respectively integers) as the free monoid (respectively group)
on one generator.  This was the point of view taken by the ADJ group
(Goguen, Thatcher, Wagner, Wright) in the mid 1970's, but then John Guttag
pointed out that most specification tend in practice to be incomplete
and that the incompletenesses can be corrected naturally by taking
observational equivalence or finality as the criterion.  Mitch Wand
proposed the notion of "almost final algebra" in a paper in JCSS 1979.
There was extensive discussion of these issues on Albert Meyer's types
mailing list in the late 1980's, see

	http://www.cs.indiana.edu/hyplan/pierce/types/archives/index.html

in particular

	http://www.cs.indiana.edu/hyplan/pierce/types/archives/1988/

towards the end of the year, as well as early in the 1989 postings.

The datatype business seems to have largely stabilized by now and most of
its participants have moved on to other areas such as the role of state
in functional programming, the semantics of Java, programming language
support for security, etc.  Philosophers inquiring into the nature of
truth should find a trove of useful ideas in the datatype literature
between 1975 and 1995.  (I have no axe of my own to grind here, I stayed
completely out of that area during that period.)

Vaughan Pratt