Section 2.1: FirstOrder Languages
We are given the following infinite set of symbols:
logical symbols  sentential connective symbols  (negation symbol) 
(conditional symbol)  
punctuation symbols  (left parenthesis)  
(right parenthesis)  
variables  (for each )  
equality symbol  (optional)  
parameters  quantifier symbols  (universal quantifier symbol) 
predicate symbols  For each , some set of symbols, called place predicate symbols.  
constant symbols  Some set of symbols (a.k.a. place function symbols).  
function symbols  For each , some set of symbols, called place function symbols. 
The firstorder languages differ in (a) the presence of the equality symbol (which is a logical symbol rather than a parameter), and (b) parameters.
An expression is a finite sequence of symbols. There are special types of expressions:

Terms. For each
place function symbol
we define an
place termbuilding operation
. We define a term to be built up from the constant symbols and variables by applying zero or more times
place termbuilding operations.
 Terms form objects from constants and variables inductively, by taking functions of already constructed objects.

Atomic formulas. An atomic formula is an expressions of the form
where
is an
place predicate symbol (or
) and each
is a term.
 Atomic formulas are the smallest parts of formulas that are assigned truth values, they are formed as predicates of terms. They play a role similar to that of sentence symbols in sentential logic.
 Wellformed formulas. A wellformed formula (wff) is an expression that can be built up from the atomic formulas by applying zero or more times the following formulabuilding operations:
A variable
is said to occur free in a wff
(
is a free variable of
) iff one of the following holds: (a)
is atomic and
occurs in
, (b)
and
occurs free in
, (c)
and
occurs free in
and/or
, and (d)
and
occurs free in
.
 Alternatively, we define where is atomic to be the set of all its variables, and extend it to defined on the set of all wffs as follows: , , and .
 is a sentence iff .
Conventions
 abbreviates .
 abbreviates .
 abbreviates .
 abbreviates .
 abbreviates (similarly, for some other place predicate and function symbols).
 abbreviates (similarly, for some other place predicate and function symbols).
 The outermost parentheses can be dropped.
 , and apply to as little as possible.
 and apply to as little as possible subject to the previous point.
 Parentheses can be added or changed to etc. for readability.
 Right precedence: is understood as .
Alphabets used
 Variables: lowercase italic letters , , , , , .
 Predicate symbols: uppercase italic letters, and specific symbols such as , etc.
 Constant symbols: lowercase italic letters , , , , and specific symbols such as etc.
 Function symbols: lowercase italic letters , , , and specific symbols such as , etc.
 Terms: lowercase italic letters , .
 Formulas: lowercase Greek letters , , , .
 Sentences: lowercase Greek letters , .
 Sets of formulas: uppercase Greek letters.
 Structures (not yet introduced): uppercase German (Fraktur) letters.