In an introductory logic course, we looked at the language of First-Order Logic (FOL) and its components informally. We illustrated the practical purpose of symbols such as variables, constants, function/prepositional/predicate symbols, boolean connectives and quantifiers, and look at the expressive power of our language as a whole. We became loosely acquainted with interpreting terms and formulas, and covered some higher semantic concepts such as first-order validities, logical consequence and logical equivalence. We also spent a considerable amount of time doing proofs inside our language.
In a second logic course, however, we are concerned primarily with the metatheorems, or theorems about the language itself. Put it slightly differently, we develop a mathematical theory about our language, and doing so requires precise definitions of its various components. In this handout, we focus on giving inductive definitions to terms, formulas and valuations, thereby illustrating how the meaning of an expression depends solely on the meaning of its components. After taking care of the semantical components of our language, we go over briefly some theoretical consequences of our definitions.