An FOL Language

An FOL language is a finite set of symbols and a description of what role they play in writing expressions of the language. In addition, a program, wff, (a recognizer) that determines if an object is a well formed expressions of the language. Using recognizers to represent 'sets' and to be the interpretations of sorts is the strategy we use to reduce the notion of language, meaning an infinite set of expressions, to a collection of finite structures. The different roles of the symbols of a language are organized using the mathematical notion of signature (a finite structure).

Requirements: What is a minimal language?

In representational terms it needs to contain

1. names for things
2. names for sorts that deliniate the type of a thing
3. names for operations on things both
   to construct 'new' things out of old ones and
   to be able to mention the parts of things
4. names for the relations between things (which form atomic expressions)
5. propositional connectives on expressions and
6. the quantifiers 'forall' and 'exists'

We represent objects as finite structures and predicates, P, as programs that can recognize which structures are examples of P. The representation of functions are programs that take objects as arguments and return an object as a value. Relations are represented as programs whose arguments are objects and which will tell us (if it can) whether the relation holds or not on its arguments.

Why traditional programing languages do not satisfy our requirements and describe what is needed to facilitate this.

and we call this map 'interp'. Signatures and a definition of 'interp' is described in detail below.