Semantics of Predicate Logic

We can use the rules of Natural Deduction (as augmented with the new rules for quantifiers) to prove the validity of a sequent in predicate logic.  However, it is not clear how we might find a general method to show that a sequent is not valid (i.e. it cannot be proved, by any possible proof).

If we think about propositional logic, we remember that we can demonstrate that semantic entailment holds by constructing a truth table.  In predicate logic, we can see that if we have an instance where a formula PSI evaluates to False even when PHI1 to PHIn all evaluate to True, then semantic entailment cannot hold.  However, to show that semantic entailment does hold (i.e. that if a set of formulas PHI1 to PHIn all evaluate to True, then some other formula PSI also evaluates to True) we seem to need to evaluate infinitely many domains, function definitions and predicate definitions.

To summarize, within the proof system, positive results are easily demonstrated, but negative results are not.  Within the semantic entailment domain, positive results are very difficult, but negative results are easily demonstrated.  Thus, even more than in propositional logic, in order to deal successfully with logical arguments we need to combine proof techniques with sophisticated methods for evaluating semantic entailment.

Soundness and Completeness

Though we will not prove this result, predicate logic has exactly the same relationship that propositional logic has, between things that are provable and things that are "true":  the set of provable sequents is exactly the same as the set of valid semantic entailments - that is, both soundness and completeness apply to predicate logic.

Semantic Entailment

We turn now to a more detailed examination of semantic entailment in predicate logic.  This begins with the precise definition of a model and a look-up table.

Model definition:  Given a set FF of functions, and a set PP of predicates, a model M consists of
a)  a non-empty set A of objects (this is the domain)
b) for each nullary function f in FF, a specific value in A that f returns
c) for each function f in FF of arity k >= 1, a mapping from k-tuples from A, to A
d) for each predicate P in PP of arity k, a subset of all possible k-tuples from A.  This subset defines the set of combinations of arguments for which P is true.

If a predicate formula contains any free variables, having a model is not enough to allow us to evaluate whether the formula is True or False.  We also need a mechanism for assigning values to the free variables.  We call this a look-up table or environment.  The name look-up table pretty much tells the story - a look-up table l simply assigns a value to each free variable in the formula.

Note that if a formula has no free variables, we do not need a look-up table.