[FOM] Concerning definition of formulas

[Francois G. Dorais]

B. Sidney Smith wrote:
> None of the responses I've seen on this thread seem to me to do
> justice to the central worry, which is the semantics of predicate
> logic.  If the quantifiers are understood in the usual set-theoretic
> way, how are we justified in formulating set theory in predicate
> logic?

Alex Blum replied:
> It would be helpful to have a problematic example. After all, the rules 
> of English are formulated in  English.

Indeed, it would be interesting to look at similar situations with a
richer set of examples.  One such situation is that of programming
languages.  The semantics of such a language are usually provided by a
compiler (or interpreter, or translator, or some other variant) for the
language.  (Hardware is also a component here, but it doesn't seem to be
that relevant.)  Issues in compiler design are very similar to the
foundation issues for predicate logic.  Here are brief points that may
be worth investigating.

1. Before the compiler, the programming language, and its intended
semantics, are usually described in some human-readable document, e.g.
the ISO 9899:1999 standard that describes the most recent evolution of
the C programming language.  Relying on human language is not a major
issue here since most such languages are designed with the human coder
in mind.  This issue is much more important for foundations of mathematics.

It is a common belief that mathematics transcends humanity, to a certain
extent.  Perhaps a standard description of predicate logic and it's
intended semantics is not acceptable to some, but I am perfectly happy
with that --- I'm not sure I really need an actual implementation of
predicate logic (in set theory or elsewhere) to continue my work.  I am
sure many will disagree with me here...

2. A compiler for a given programming language is usually itself written
in a programming language.  This could be the same or a different
language.  If different, this reduces the semantics problem for the
given language to another (previously solved) problem.  The situation is
more interesting when the same language is used.  Perhaps there already
exists a compiler for the given language, but how can we trust that
compiler to have correct semantics.  This is a very real issues in
compiler design since compilers tend to be very buggy.

We have a clear (human language) description of predicate logic.  We
have a clear description of set theory in predicate logic and how to
interpret (the syntax and semantics of) predicate logic within set
theory.  This is a lot like writing a compiler in the language that it
accepts.  Without a compiler for the language, we cannot compile the
compiler.  Is it still a compiler?  It is certainly more concrete than a
human-language description.

3. Many compilers are written partly in their own language and partly in
another.  Moreover, the compilation process for a compiler sometimes
involves some bootstrapping where sequence of compilers for small
subsets of the language each, except for the first, compiled using the
previous one until the final product is reached.  This is a very
interesting solution to the problem that other compilers cannot be
relied on for correct semantics.

Can there be a similar compromise for predicate logic?  Is it possible
to bootstrap predicate logic on fragments of itself?  Can we use this to
build sturdy semantics for predicate logic on top of weaker ones?

Mathematicians (especially logicians) tend to be purists and idealists,
I don't think such compromises have been thoroughly investigated.

4. There are probably many more comparison points.  Can we learn
something from computer scientists?  Is it worth pursuing this
comparison?  Are there other similar situations?

-- 
François G. Dorais
Department of Mathematics
Cornell University