FOM: mea culpa

[Jon.Barwise@tarski.phil.indiana.edu]

Vaughan writes, in response to my previous message:
>
>What is broken in my view is the basic premise that mathematics
>traffics in propositions, with constructions as a mere currency.  I
>claim that mathematics traffics equally in propositions and
>constructions.
>

I'll accept Vaughan's criticism and even support it with an example.  As
some of you know, I have been taken by Aczel's work on the anti-foundation
axiom and the universe of anti-founded sets.  One of the most important
parts of that theory is the CONSTRUCTION which shows how to take any
universe of wellfounded sets and extend it to form a larger universe of
antifounded sets.  Of course you can always describe this construction by
means of a proposition and construe the construction itself as a proof of
the proposition.  So in a way it all gets tidied up at the level of
propositions, but that does not really answer to Vaughan's point.  It is
the construction itself that is important.

To me, the history of the antifounded universe is an excellent example of
foundations of mathematics in action.  I, at least, simply did not take
non-wellfounded sets at all seriously prior to Aczel's book.  They seemed
to me ad hoc and without any foundation what-so-ever.  (This is not to say
that no one had written anything good about them, but that I was not aware
of it.) However, Aczel's book provided me with a way to think about
non-wellfounded sets, to work with them, to use them to model real world
circular phenomena that interested me.  In other words, it provided them
with a foundation.

There is a fairly easy to tell story that relates the antifounded universe
with real world phenomena.  In this regard, it is worth noting that the
impetus for Aczel's work was work in computer science, Robin Milner's
calculus CCS of communicating systems.  CCS itself is really a
construction, so there you are again, Vaughan.

Thanks for the reminder.
Jon