FOM: Barendregt's f.o.m. and c.f.o.m.

[Vaughan Pratt]

From: Henk Barendregt <henk at cs.kun.nl>
>DEFINITION
>A foundation of mathematics (F.O.M.) is a formal system such that
>1. Enough mathematics is derivable.

Mathematicians may not agree with you.  In order for me to argue this
I'll first have to go through a bit of a warmup, which I hope people
will bear with.

Your definition seems to assume that you have some notion of proposition,
e.g.  equation, first-order formula, etc.  Let P be any such class
of propositions.

What isn't so clear is whether it also assumes some notion of universe
in or about which the propositions are stated, e.g.  algebra, relational
structure, etc.  The thought of a formal system as pure propositions
that are not about anything is not very appealing.  It is therefore very
reasonable to suppose that your foundation also has a class of universes
in mind, call it U.

But propositions about or in universes aren't worth a hill of beans
if you can't assess the truth of that proposition in that universe.
So let |= be a binary relation of *satisfaction* between universes
and propositions, with u |= p ("u satisfies p") asserting the truth of
proposition p in universe u.

So our data at this point consist of U, |=, and P.  Collect this data as
the triple (U,|=,P).  There will be no further data.

Any subclass Q of P, as *axioms* of a theory, induces a subclass W_Q of
U called the *models* of Q, consisting of those universes in which all
the axioms in Q hold.  Conversely any subclass V of U, which might be
a singleton such as {2} consisting of the two-element Boolean algebra,
or the class of all torsion-free abelian groups, induces a subclass R_V
of P consisting of those propositions holding of every universe in V.

Now it is well known that R_{W_Q}, as a function of Q, is a closure
operator on the subclasses of P ordered by inclusion.  A natural name for
this operator is *deductive closure*, yielding all *consequences* of Q.

But the situation is entirely symmetric, and it should therefore be
equally well-known (but sadly isn't) that W_{R_V}, as a function of V,
is a closure operator on the subclasses of U ordered by inclusion.
A natural name for this operator is *constructive closure*, yielding
all *homologues* (universes resembling) all universes of V.

For example when U consists of all algebras of a given signature,
and P consists of all equations in terms of that signature, and u|=p
asserts that equation p holds identically in algebra u, then deductive
closure is the usual one for equational logic, extending Q to the least
substitutive congruence on the terms of the language that contains Q.
Or for first order logic it is the deductive closure operation given by
the axioms and rules of the pure predicate calculus.

Dually constructive closure for equational logic is closure under the
constructions of homomorphism, subalgebra, and direct product.  For first
order logic it is closure under the constructions of isomorphism,
substructure, and ultraproduct.

The point is that to *every* framework (U,|=,P), however tame or wild, is
associated not only a deductive closure but also a constructive closure.
Birkhoff's theorem and the model theory of elementary classes are just
two well-known instances of this very general but surprisingly less
well-known phenomenon.  Surprising because it is simpler to prove and
also admits appealingly simple elaborations.

---------

Now for my question.  When you say that "a foundation of mathematics is
a formal system such that enough mathematics is derivable", which if
anything is more important to you: derivability on the P side of the
framework, or constructibility on the U side?  And if the former, how
do you convince a platonist who does his mathematics with constructions
rather than deductions that your foundation is of what *he* thinks of
as mathematics, and not merely of a formal system that he does not care
about, the interchangeability of the two notwithstanding?

Vaughan Pratt