Predicate LogicIntroductionTerminologyTermPredicateQuantifierWFF (of First-Order Logic)WFFNotation: Seven Kinds of SymbolsApplication: Parse TreeFree and Bound VariablesApplication: Determining Free or Bound using Parse TreeSubstitutionMotivationFormal DefinitionInterpretationsValues of Variable-Free TermsTotal FunctionsValues of Formulas Containing Only Variable-Free TermsEnvironmentsMeaning of TermsQuantified FormulasValues of Quantified FormulasValidity and SatisfiabilityExercise: Give an Interpretation and an environment such that ...Overall RemarksSemantic EntailmentRelevance LemmaSemantic EntailmentExercise: Semantic EntailmentNatural DeductionTrivial: Forall-eliminationTrivial: Exists-introductionChallenging: Forall-introduction Challenging: Exists-elimination

Predicate logic generalizes propositional logic with the following new things:

A*Definition.***domain**is a*non-empty*set of objects.A*Definition.***constant**is a concrete object in the domain.A*Definition.***variable**is a place holder for a concrete object; it lets us refer to an object without specifying which particular object it is.A*Definition.***function symbol**is denoted by , where is the function name and denotes its arity.

** Definition.** A

**Atom**: each constant symbol and variable term is a term.**Function application**: if are terms and is a function symbol of arity , then is a term.**Nothing else is a term**.

** Definition.** A

** Remark.** We can think of a predicate as a function mapping from into .

- Universal quantifier
- Existential quantifier

** Definition.** The set of

**Atom**: A*predicate*(atomic formula) is a formula.**Unary Connectives**:If is a formula, is a formula.**Binary Connectives**: If are formulas and is a binary connective, is a formula.**Quantifiers**: If is a formula and is a variable, then each of and is a formula.**Nothing else is a formula.**

- Constant symbols:
- Variables:
- Function symbols:
- Predicate symbols:
- Connectives:
- Quantifiers:
- Punctuations:
*parentheses*and*comma*

** Remarks.** Function symbols and predicate symbols have assigned

- Quantifiers and have one subtree, behaves like the unary connective .
- A predicate symbol has a parent node labeled with a subtree for each of the term .
- A function symbol has a parent node labeled with a subtree for each of the term .

** Definition.** There are two types of variables in a formula:

- A variable may be
**free**. To evaluate the formula, we need to replace a free variable by an object in the*domain*. - A variable may be
**bound**by a quantifier. The*quantifier*tells us how to evaluate the formula.

*Definition.*

In a formula or , the

**scope**of a quantifer is the formula ; the quantifier**binds**its variable within its scope.An occurrence of a variable in a formula is

**bound**if it lies in the scope of some quantifier of the same variable. Otherwise the occurrence of this variable is**free**.- If a variable occurs multiple times, we need to consider each occurrence of the variable separately.
- The variable symbol immediately after or is neither free nor bound.

A formula with

*no*free variables is called a**closed formula**or**sentence**.

To determine whether a variable is free or bound, we can use a parse tree:

- Draw the parse tree for the formula
- Choose the leaf node for an occurrence of a variable
- Walk up the tree. Stop as soon as we
*encounter a quantifier for this variable*or*we reach the root of the tree*. - If we reach the root of the tree which is not a quantifier for the variable, this occurrence of the variable is
*free*.

** Definition.** For a variable , a term , and a formula , denotes the resulting formula by replacing each

** Remark**.

*Example.*

Let , then

- .

If , then , because has no free occurrence of so the substitution does nothing.

** Definition.** Let be a variable and a term.

For a term , the term is with each occurrence of replaced by .

For a formula ,

- If is a predicate, recursively substitute each with .

- If can be splitted into other formulas, recursively apply rule 1.

- If is bounded in , then substituting into does nothing.

- If contains no bounded variable, leave the quantifier alone and do substituion.

- If contains a bounded variable, we need to find a new variable with no name clash and do the substitution.

*Exercise.*

, then is?

Note that the term contains a bounded variable. To resolve the name clash, we first replace every occurrence of in by , i.e. , and then substitute by , so that .

To write this formally, we need the following steps:

- Let , so that .
- Let and . Since occurs in , select a new variable, say .
- Then .
- Thus .

** Definition.** Fix a set of constant symbols, function symbols, variable symbols and predicate symbols. An

- A non-empty set or simply , called the
**domain**of . - For each constant symbol , a member .
- For each function symbol , an -ary function .
- For each predicate symbol , an -ary predicate .

** Definition.** Fix an interpretation . For each term containing no variables (only constants), the value of under interpretation , denoted , is as follows:

- If is a constant , the value is .
- If is , the value is .

** Remark.** The value of a term is always a member of the domain of .

** Motivation.** Recall that your function's interpretation must be defined on the entire domain. That is, for a function with arity , we need to define an interpretation such that the function satisfies

** Definition.** Functions capable of doing this (that is, the result is in domain) are called

** Example.** Let . The addition function is a total function since the sum of any two natural numbers gives another natural number. However, the subtraction function is not, as .

** Definition.** Fix an interpretation . For each formula containing no variables, the value of under interpretation , denoted , is as follows:

If is , then

If is or , then is determined by and in the same way as for propositional logic.

** Remark.** simply means evaluates to True under the interpretation .

** Definition.** An

An environment needs to be defined on*Warning.**all*variables.- Although environments will only be used to interpret free variables, they still need to be defined on all variables including bound variables.
- Bound variables will get their meaning primarily through the corresponding quantifier.

** Principle.** The combination of an

** Definition.** Fix an interpretation and an environment . For each term , the value of under and , dentoed , is as follows:

**Interpretations give constants meanings**: if is a constant , then .**Environments give variables meanings**: if is a variable , then .**Recursively extend to functions**: if is a function application , then .

** Example.** Let be where is a constant and let be where is a variable. Let be the interpretation with domain , and . Then but is undefined. To give a value, we must also specify an

** Definition.** For any environment and domain element , the environment " with maps to ", denoted , is given by

In other words, and for any other variable , .

** Remark.** is a new environment!

** Example.** Let for some and such that . Then .

** Definition.** The values of and are given by

** Remark.** The values of and do not depend on the values of ; only matters for free occurrences of but nontheless environments must be specified for all variables.

** Definition.** A formula is

**valid**if every interpretation and environment satisfy , that is, for every and .**satisfiable**if some interpretation and environment satisfy , that is, for some and .**unsatisfiable**if no interpretation and environment satisfy , that is, for every and .

** Remark.** The term "tautology" is not used in predicate logic.

** Remark.** If there is no need to specify an environment, then simply defining an interpretation and writing will suffice.

** Remark.** To show a formula is

**Template:**

- Define the domain.
- Map each constant to a domain element.
- Give each function a meaning.
- Give each predicate a meaning.
- Map each variable to a domain element.

Now use reduction to show the statement holds.

**Example I**. (with variables but no quantifier): Consider this language of predicate logic:

- Constant symbols:
- Variable symbols:
- Function symbols:
- Predicate symbols:

Give an interpretation and environment such that .

**Solution I:**

The interpretation and the environment are given below:

Given and , we can show that because

**Example II:** Use the same language as above, give an interpretation and environment such that .

**Remark II:** is free so its value is given by the environment; even though and do not appear in the formula, we need to define their mapping as part of . To make the statement true, there must be at least one tuple in the set of with second element being .

**Solution II:**

The interpretation and the environment are given below:

Given and , we can show that because

- Hence, by the satisfaction rules for , .

The constants get their meaning through and the variables through .

Map every constant to a domain element in and every variable to a domain element in , even if some of them do not appear in the formula.

The function and predicate must be able to every possible domain elements (or combinations of domain element, in the case its arity is greater than one).

To show , show that ; LHS gets its value from only if there is no free variable.

Use the satisfaction rules precisely

** Lemma.** Let be a well-formed predicate formula, be an interpretation, and be two environments such that for every that occurs free in . Then if and only if .

Let be a set of well-formed predicate logic formulas and is a well-formed predicate logic formula. For an interpretation and an environment , we write if and only if for every , we have that .

** Definition.** We say that

** Remark.** means that is valid (recall how we interpret this in propositional logic).

** Notes.** Suppose . Then means

- ... that every pair of interpretation and environment that makes true must also make true.
- ... that .
- ... that is valid.

Thus, to prove these, take an arbitrary interpretation and environment and show that if this satisified then it must also satisfy . You may also assume towards a contradiction that and proceed from there. To prove