1.2.3 Building Formulas

Terms

Let's suppose we've composed a certain vocabulary. How do we mix these ingredients together? That is, what is the syntax of first-order languages? First of all, we define a first-order term to be any constant or any variable. Roughly speaking, terms are the noun phrases of first-order languages: constants can be thought of as first-order counterparts of proper names, and variables as first-order counterparts of pronouns.

Atomic Formulas

We can then combine our ``noun phrases'' with our ``predicates'' (meaning, the various relation symbols in the vocabulary) to form what we call atomic formula s:

If is a relation symbol of arity , and are terms, then is an atomic formula.

Intuitively, an atomic formula is the first-order counterpart of a natural language sentence consisting of a single clause (that is, a simple sentence). So what does a formula like actually mean? As a rough translation, we could say that the entities that are named by the terms stand in a relationship that is named by the symbol . An example will clarify this point:

What's meant by this formula is that the entity named stands in the relation denoted by to the entity named - or more simply, that Peter loves Anna.

Complex Formulas

Now that we know how to build atomic formulas, we can define more complex ones as well. The following inductive definition tells us exactly what kinds of well-formed formula s (or wffs, or simply formulas) we can form.

  1. All atomic formulas are wffs.

  2. If and are wffs then so are , , , and .

  3. If is a wff, and x is a variable, then both and are wffs. (We call the matrix or scope of such wffs.)

  4. Nothing else is a wff.

Roughly speaking, formulas built using , , and correspond to the natural language expressions ``... and ...'', ``if ... then ...'', ``... or ...'', and ``it is not the case that ...'', respectively. First-order formulas of the form and correspond to natural language expressions of the form ``some...'' or ``all...''.


Aljoscha Burchardt, Alexander Koller and Stephan Walter
Version 1.2.5 (20030212)