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.