[FOM] Concerning definition of formulas
Andrej Bauer
Andrej.Bauer at fmf.uni-lj.si
Thu Sep 27 18:42:35 EDT 2007
Saurav wrote:
> So, by set theoretical tools it is not acceptable to define formulas
> because we need to think about set theories as well, and without set
> theoretical tools we are in this problem; then what should we do?
Set theory is only one way to think about inductive definitions. It may
be helpful to read more recent accounts of syntax that are based on
experience with writing parsers for programming languages. Old books on
logic tend to present formulas as strings of symbols, which obfuscates
their mathematically relevant structure (namely that formulas are
trees). For a presentation of syntax as it is done in the programming
languages community, have a look at, e.g., Bob Harper's "Practical
Foundations for Programming Languages". The draft of the book is
available from his home page http://www.cs.cmu.edu/~rwh/.
As the book explains, definitions of well formed formulas are just a
special case of inductive definitions. So another place to look is how
inductive types are defined in type theory. Instead of saying things like
> "nothing else is a formula" or "a string is a formula if and only if it
> is obtained in this way"
the idea is to give introduction rules that tell you how to build the
elements of an inductive type (in your case well-formed formulas) and
suitable elimination rules (induction principles) that tell you how to
prove their properties. _Roughly_ speaking, instead of saying something
like this
1) 0 and 1 are wffs
2) if x and y are wwfs then so is x /\ y
3) nothing else is a wff
we say instead
1') 0 and 1 are wffs
2') if x and y are wwfs then so is x /\ y
3') if P is a property of wwws such that P(0) holds, P(1) holds,
and P(x /\ y) holds whenever P(x) and P(y) hold, then P holds
for all wwfs.
Here 1') and 2') are introduction rules and 3') is an
elimination/induction rule. It is a replacement for rule 3) above that
makes it more precise and computationally useful.
Another way to understand syntax comes from category theory. The
well-formed terms of a language constitute the initial algebra for a
functor. (If you prefer algebra, you may think of the well-formed
formulas as the free algebra for a given signature.) A possible reading
material in this direction is R. Crole's "Basic Category Theory for
Models of Syntax", downloadable as [6] at
http://www.cs.le.ac.uk/people/rlc3/papers/roybib.html.
Best regards,
Andrej Bauer
More information about the FOM
mailing list