[FOM] Concerning definition of formulas

[Andrej Bauer]

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