Propositional and Predicate Logic

Abstract

Propositional logic is the study of propositions, where a proposition is a statement that is either true or false. Propositionallogic may be used to encode simple arguments that are expressed in natural language, and to determine their validity. The validity of an argument may be determined from truth tables, or using the inference rules such as modus ponens to establish the conclusion via deductive steps. Predicate logic allows complex facts about the world to be represented, and new facts may be determined via deductive reasoning. Predicate calculus includes predicates, variables and quantifiers, and a predicate is a characteristic or property that the subject of a statement can have. The universal quantifier is used to express a statement such as that all members of the domain of discourse have property P, and the existential quantifier states that there is at least one value of x has property P.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

FormalPara Key Topics

• Propositions

• Truth Tables

• Semantic Tableaux

• Natural Deduction

• Proof

• Predicates

• Universal Quantifiers

• Existential Quantifiers

15.1 Introduction

Logic is the study of reasoning and the validity of arguments, and it is concerned with the truth of statements (propositions) and the nature of truth. Formal logic is concerned with the form of arguments and the principles of valid inference. Valid arguments are truth preserving, and for a valid deductive argument the conclusion will always be true if the premises are true.

Propositional logic is the study of propositions, where a proposition is a statement that is either true or false. Propositions may be combined with other propositions (with a logical connective) to form compound propositions. Truth tables are used to give operational definitions of the most important logical connectives, and they provide a mechanism to determine the truth values of more complicated logical expressions.

Propositional logic may be used to encode simple arguments that are expressed in natural language, and to determine their validity. The validity of an argument may be determined from truth tables, or using the inference rules such as modus ponens to establish the conclusion via deductive steps.

Predicate logic allows complex facts about the world to be represented, and new facts may be determined via deductive reasoning. Predicate calculus includes predicates, variables and quantifiers, and a predicate is a characteristic or property that the subject of a statement can have. A predicate may include variables, and statements with variables become propositions once the variables are assigned values.

The universal quantifier is used to express a statement such as that all members of the domain of discourse have property P. This is written as (∀x) P(x), and it expresses the statement that the property $P\left( x \right)$ is true for all x. The existential quantifier states that there is at least one member of the domain of discourse that has property P. This is written as (∃x)P(x).

15.2 Propositional Logic

Propositional logic is the study of propositions where a proposition is a statement that is either true or false. There are many examples of propositions such as ‘1 + 1 = 2’ which is a true proposition, and the statement that ‘Today is Wednesday’ which is true if today is Wednesday and false otherwise. The statement x > 0 is not a proposition as it contains a variable x, and it is only meaningful to consider its truth or falsity only when a value is assigned to x. Once the variable x is assigned a value it becomes a proposition. The statement ‘This sentence is false’ is not a proposition as it contains a self-reference that contradicts itself. Clearly, if it the statement is true it is false, and if is false it is true.

A propositional variable may be used to stand for a proposition (e.g. let the variable P stand for the proposition ‘2 + 2 = 4’ which is a true proposition). A propositional variable takes the value or false. The negation of a proposition P (denoted ¬P) is the proposition that is true if and only if P is false, and is false if and only if P is true.

A well-formed formula (wff) in propositional logic is a syntactically correct formula created according to the syntactic rules of the underlying calculus. A well-formed formula is built up from variables, constants, terms and logical connectives such as conjunction (and), disjunction (or), implication (if… then…), equivalence (if and only if) and negation. A distinguished subset of these well formed formulae is the axioms of the calculus, and there are rules of inference that allow the truth of new formulae to be derived from the axioms and from formulae that have already demonstrated to be true in the calculus.

A formula in propositional calculus may contain several propositional variables, and the truth or falsity of the individual variables needs to be known prior to determining the truth or falsity of the logical formula.

Each propositional variable has two possible values, and a formula with n-propositional variables has 2ⁿ values associated with the n-propositional variables. The set of values associated with the n variables may be used derive a truth table with 2ⁿ rows and n + 1 columns. Each row gives each of the 2ⁿ truth values that the n variables may take, and column n + 1 gives the result of the logical expression for that set of values of the propositional variables. For example, the propositional formula W defined in the truth table above (Table 15.1) has two propositional variables A and B, with 2² = 4 rows for each of the values that the two propositional variables may take. There are 2 + 1 = 3 columns with W defined in the third column.

Table 15.1 Truth table for formula W

A rich set of connectives is employed in the calculus to combine propositions and to build up the well-formed formulae. This includes the conjunction of two propositions (A ∧ B), the disjunction of two propositions (A ∨ B) and the implication of two propositions (A → B). These connectives allow compound propositions to be formed, and the truth of the compound propositions is determined from the truth values of its constituent propositions and the rules associated with the logical connective. The meaning of the logical connectives is given by truth tables.¹

Mathematical Logic is concerned with inference, and it involves proceeding in a methodical way from the axioms and using the rules of inference to derive further truths. The rules of inference allow new propositions to be deduced from a set of existing propositions. A valid argument (or deduction) is truth preserving: i.e. for a valid logical argument if the set of premises is true then the conclusion (i.e. the deduced proposition) will also be true. The rules of inference include rules such as modus ponens, and this rule states that given the truths of the proposition A, and the proposition A → B, then the truth of proposition B may be deduced.

The propositional calculus is employed in reasoning about propositions, and it may be applied to formalize arguments in natural language. Boolean algebra is used in computer science, and it is named after George Boole, who was the first professor of mathematics at Queens College, Cork.² His symbolic logic (discussed in Chap. 14) is the foundation for modern computing.

15.2.1 Truth Tables

Truth tables give operational definitions of the most important logical connectives, and they provide a mechanism to determine the truth values of more complicated compound expressions. Compound expressions are formed from propositions and connectives, and the truth values of a compound expression containing several propositional variables is determined from the underlying propositional variables and the logical connectives.

The conjunction of A and B (denoted A ∧ B) is true if and only if both A and B are true, and is false in all other cases (Table 15.2). The disjunction of two propositions A and B (denoted A ∨ B) is true if at least one of A and B are true, and false in all other cases (Table 15.3). The disjunction operator is known as the ‘inclusive or’ operator as it is also true when both A and B are true; there is also an exclusive or operator that is true exactly when one of A or B is true, and is false otherwise.

Table 15.2 Conjunction

Table 15.3 Disjunction

Example 15.1

Consider proposition A given by “An orange is a fruit” and the proposition B given by “2 + 2 = 5” then A is true and B is false. Therefore

• (i) A ∧ B (i.e. An orange is a fruit and 2 + 2 = 5) is false

• (ii) A ∨ B (i.e. An orange is a fruit or 2 + 2 = 5) is true

The implication operation (A → B) is true if whenever A is true means that B is also true; and also whenever A is false (Table 15.4). It is equivalent (as shown by a truth table) to ¬A ∨ B. The equivalence operation (A ↔ B) is true whenever both A and B are true, or whenever both A and B are false (Table 15.5).

Table 15.4 Implication

Table 15.5 Equivalence

The not operator (¬) is a unary operator (i.e. it has one argument) and is such that ¬A is true when A is false, and is false when A is true (Table 15.6).

Table 15.6 Not operation

Example 15.2

Consider proposition A given by ‘Jaffa cakes are biscuits’ and the proposition B given by ‘2 + 2 = 5’ then A is true and B is false. Therefore

• (i) A → B (i.e. Jaffa cakes are biscuits implies 2 + 2 = 5) is false

• (ii) A ↔ B (i.e. Jaffa cakes are biscuits is equivalent to 2 + 2 = 5) is false

• (iii) ¬B (i.e. 2 + 2 ≠ 5) is true.

Creating a Truth Table

The truth table for a well-formed formula W(P ₁, P ₂, …, P _n ) is a table with 2ⁿ rows and n + 1 columns. Each row lists a different combination of truth values of the propositions P ₁, P ₂, …, P _n followed by the corresponding truth value of W.

The example above (Table 15.7) gives the truth table for a formula W with three propositional variables (meaning that there are 2³ = 8 rows in the truth table).

Table 15.7 Truth table for W(P, Q, R)

15.2.2 Properties of Propositional Calculus

There are many well-known properties of the propositional calculus such as the commutative, associative and distributive properties. These ease the evaluation of complex expressions, and allow logical expressions to be simplified.

The commutative property holds for the conjunction and disjunction operators, and it states that the order of evaluation of the two propositions may be reversed without affecting the resulting truth value: i.e.

$$ \begin{aligned} {\text{A}} \wedge {\text{B}} &= {\text{B}} \wedge {\text{A}}\\ {\text{A}} \vee {\text{B}} &= {\text{B}} \vee {\text{A}}\end{aligned} $$

The associative property holds for the conjunction and disjunction operators. This means that order of evaluation of a sub-expression does not affect the resulting truth value, i.e.

$$ \begin{aligned} (A \wedge B) \wedge C &= A \wedge (B \wedge C) \\ (A \vee B) \vee C &= A \vee (B \vee C) \end{aligned} $$

The conjunction operator distributes over the disjunction operator and vice versa.

$$ \begin{aligned} A \wedge (B \vee C) &= (A \wedge B) \vee (A \wedge C) \\ A \vee (B \wedge C) &= (A \vee B) \wedge (A \vee C)\end{aligned} $$

The result of the logical conjunction of two propositions is false if one of the propositions is false (irrespective of the value of the other proposition).

$$ A \wedge {\text{F}} = {\text{F}} \wedge A = {\text{F}} $$

The result of the logical disjunction of two propositions is true if one of the propositions is true (irrespective of the value of the other proposition).

$$ A \vee {\text{T}} = {\text{T}} \vee A = {\text{T}} $$

The result of the logical disjunction of two propositions, where one of the propositions is known to be false is given by the truth value of the other proposition. That is, the Boolean value ‘F’ acts as the identity for the disjunction operation.

$$ A \vee {\text{F}} = A = {\text{F}} \vee A $$

The result of the logical conjunction of two propositions, where one of the propositions is known to be true, is given by the truth value of the other proposition. That is, the Boolean value ‘T’ acts as the identity for the conjunction operation.

$$ A \wedge {\text{T}} = A = {\text{T}} \wedge A $$

The ∧ and ∨ operators are idempotent. That is, when the arguments of the conjunction or disjunction operator are the same proposition A the result is A. The idempotent property allows expressions to be simplified.

$$ A \wedge A = A $$

$$ A \vee A = A $$

The law of the excluded middle is a fundamental property of the propositional calculus. It states that a proposition A is either true or false: i.e. there is no third logical value.

$$ A \vee \neg A $$

We mentioned earlier that A → B is logically equivalent to ¬A ∨ B (same truth table), and clearly ¬A ∨ B is the same as ¬A ∨ ¬¬B = ¬¬B ∨ ¬A which is logically equivalent to ¬B → ¬A. Another words, A → B is logically equivalent to ¬B → ¬A, and this is known as the contrapositive.

De Morgan was a contemporary of Boole in the nineteenth century, and the following law is known as De Morgan’s law.

$$ \begin{aligned} \neg (A \wedge B) \equiv \neg A \vee \neg B \hfill \\ \neg (A \vee B) \equiv \neg A \wedge \neg B \hfill \\ \end{aligned} $$

Certain well-formed formulae are true for all values of their constituent variables. This can be seen from the truth table when the last column of the truth table consists entirely of true values. A proposition that is true for all values of its constituent propositional variables is known as a tautology. An example of a tautology is the proposition A ∨ ¬A (Table 15.8)

Table 15.8 Tautology B ∨ ¬B

A proposition that is false for all values of its constituent propositional variables is known as a contradiction. An example of a contradiction is the proposition A ∧ ¬A.

15.2.3 Proof in Propositional Calculus

Logic enables further truths to be derived from existing truths by rules of inference that are truth preserving. Propositional calculus is both complete and consistent. The completeness property means that all true propositions are deducible in the calculus, and the consistency property means that there is no formula A such that both A and ¬A are deducible in the calculus.

An argument in propositional logic consists of a sequence of formulae that are the premises of the argument and a further formula that is the conclusion of the argument. One elementary way to see if the argument is valid is to produce a truth table to determine if the conclusion is true whenever all of the premises are true.

Consider a set of premises P ₁, P ₂, … P _n and conclusion Q. Then to determine if the argument is valid using a truth table involves adding a column in the truth table for each premise P ₁, P ₂, … P _n , and then to identify the rows in the truth table for which these premises are all true. The truth value of the conclusion Q is examined in each of these rows, and if Q is true for each case for which P ₁, P ₂, … P _n are all true then the argument is valid. This is equivalent to P ₁ ∧ P ₂ ∧ … ∧ P _n → Q is a tautology.

An alternate approach to proof with truth tables is to assume the negation of the desired conclusion (i.e. ¬Q) and to show that the premises and the negation of the conclusion result in a contradiction (i.e. P ₁ ∧ P ₂ ∧ … ∧ P _n ∧ ¬Q) is a contradiction.

The use of truth tables becomes cumbersome when there are a large number of variables involved, as there are 2ⁿ truth table entries for n propositional variables.

Procedure for Proof by Truth Table

• (i) Consider argument P ₁, P ₂, …, P _n with conclusion Q

• (ii) Draw truth table with column in truth table for each premise P ₁, P ₂, …, P _n

• (iii) Identify rows in truth table for when these premises are all true.

• (iv) Examine truth value of Q for these rows.

• (v) If Q is true for each case that P ₁, P ₂, … P _n are true then the argument is valid.

• (vi) That is P ₁ ∧ P ₂ ∧ … ∧ P _n → Q is a tautology

Example 15.3

(Truth Tables) Consider the argument adapted from [1] and determine if it is valid.

If the pianist plays the concerto then crowds will come if the prices are not too high.

If the pianist plays the concerto then the prices will not be too high

Therefore, if the pianist plays the concerto then crowds will come.

Solution

We will adopt a common proof technique that involves showing that the negation of the conclusion is incompatible (inconsistent) with the premises, and from this we deduce the conclusion must be true. First, we encode the argument in propositional logic:

Let P stand for ‘The pianist plays the concerto’; C stands for ‘Crowds will come’; and H stands for ‘Prices are too high’. Then the argument may be expressed in propositional logic as

$$ \begin{aligned} & P \to (\neg H \to C) \\ & P \to \neg H \\ & P \to C \\ \end{aligned} $$

Then we negate the conclusion P → C and check the consistency of P → (¬H → C) ∧ (P → ¬H) ∧ ¬ (P → C)* using a truth table (Table 15.9).

Table 15.9 Proof of argument with a truth table

It can be seen from the last column in the truth table that the negation of the conclusion is incompatible with the premises, and therefore it cannot be the case that the premises are true and the conclusion false. Therefore, the conclusion must be true whenever the premises are true, and we conclude that the argument is valid.

Logical Equivalence and Logical Implication

The laws of mathematical reasoning are truth preserving, and are concerned with deriving further truths from existing truths. Logical reasoning is concerned with moving from one line in mathematical argument to another, and involves deducing the truth of another statement Q from the truth of P.

The statement Q maybe in some sense be logically equivalent to P and this allows the truth of Q to be immediately deduced. In other cases the truth of P is sufficiently strong to deduce the truth of Q; in other words P logically implies Q. This leads naturally to a discussion of the concepts of logical equivalence (W ₁ ≡ W ₂) and logical implication (W ₁ ├ W ₂).

Logical Equivalence

Two well-formed formulae W ₁ and W ₂ with the same propositional variables (P, Q, R …) are logically equivalent (W ₁ ≡ W ₂) if they are always simultaneously true or false for any given truth values of the propositional variables.

If two well-formed formulae are logically equivalent then it does not matter which of W ₁ and W ₂ is used, and W ₁ ↔ W ₂ is a tautology. In Table 15.10 above we see that P ∧ Q is logically equivalent to ¬(¬P ∨ ¬Q).

Table 15.10 Logical equivalence of two WFFs

Logical Implication

For two well-formed formulae W ₁ and W ₂ with the same propositional variables (P, Q, R …) W ₁ logically implies W ₂ (W ₁ ├ W ₂) if any assignment to the propositional variables which makes W ₁ true also makes W ₂ true (Table 15.11). That is, W ₁ → W ₂ is a tautology.

Table 15.11 Logical implication of two WFFs

Example 15.4

Show by truth tables that (P ∧ Q) ∨ (Q ∧ ¬R) ├ (Q ∨ R).

The formula (P ∧ Q) ∨ (Q ∧ ¬R) is true on rows 1, 2 and 6 and formula (Q ∨ R) is also true on these rows. Therefore (P ∧ Q) ∨ (Q ∧ ¬R) ├ (Q ∨ R).

15.2.4 Semantic Tableaux in Propositional Logic

We showed in example 15.3 how truth tables may be used to demonstrate the validity of a logical argument. However, the problem with truth tables is that they can get extremely large very quickly (as the size of the table is 2ⁿ where n is the number of propositional variables), and so in this section we will consider an alternate approach known as semantic tableaux.

The basic idea of semantic tableaux is to determine if it is possible for a conclusion to be false when all of the premises are true. If this is not possible, then the conclusion must be true when the premises are true, and so the conclusion is semantically entailed by the premises. The method of semantic tableaux is a technique to expose inconsistencies in a set of logical formulae, by identifying conflicting logical expressions.

We present a short summary of the rules of semantic tableaux in Table 15.12, and we then proceed to provide a proof for Example 15.3 using semantic tableaux instead of a truth table.

Table 15.12 Rules of semantic tableaux

Whenever a logical expression A and its negation ¬A appear in a branch of the tableau, then an inconsistency has been identified in that branch, and the branch is said to be closed. If all of the branches of the semantic tableaux are closed, then the logical propositions from which the tableau was formed are mutually inconsistent, and cannot be true together.

The method of proof is to negate the conclusion, and to show that all branches in the semantic tableau are closed, and that therefore it is not possible for the premises of the argument to be true and for the conclusion to be false. Therefore, the argument is valid and the conclusion follows from the premises.

Example 15.5

(Semantic Tableaux) Perform the proof for Example 15.3 using semantic tableaux.

Solution

We formalized the argument previously as

$$ \begin{array}{*{20}c} {\left( {{\text{Premise}}\, 1} \right)} & {P \to (\neg H \to C)} \\ {\left( {{\text{Premise}}\, 2} \right)} & {P \to \neg H} \\ {\left( {\text{Conclusion}} \right)} & {P \to C} \\ \end{array} $$

We negate the conclusion to get ¬(P → C) and we show that all branches in the semantic tableau are closed, and that therefore it is not possible for the premises of the argument to be true and for the conclusion false. Therefore, the argument is valid, and the truth of the conclusion follows from the truth of the premises.

We have showed that all branches in the semantic tableau are closed, and that therefore it is not possible for the premises of the argument to be true and for the conclusion false. Therefore, the argument is valid as required.

15.2.5 Natural Deduction

The German mathematician, Gerhard Gentzen (Fig. 15.1), developed a method for logical deduction known as ‘Natural Deduction’, and his formal approach to natural deduction aimed to be as close as possible to natural reasoning. Gentzen worked as an assistant to David Hilbert at the University of Göttingen, and he died of malnutrition in Prague at the end of the Second World War.

Fig. 15.1

Gerhard gentzen

Natural deduction includes rules for ∧, ∨, → introduction and elimination and also for reductio ab absurdum. There are ten inference rules in the Natural Deduction system, and they include two inference rules for each of the five logical operators—∧, ∨, ¬, → and ↔. There are two inference rules per operator (an introduction rule and an elimination rule), and the rules are defined in Table 15.13:

Table 15.13 Natural deduction rules

Natural deduction may be employed in logical reasoning and is described in detail in [1, 2].

15.2.6 Sketch of Formalization of Propositional Calculus

Truth tables provide an informal approach to proof and the proof is provided in terms of the meanings of the propositions and logical connectives. The formalization of propositional logic includes the definition of an alphabet of symbols and well-formed formulae of the calculus, the axioms of the calculus and rules of inference for logical deduction.

The deduction of a new formulae Q is via a sequence of well-formed formulae P ₁, P ₂, … P _n (where P _n  = Q) such that each P _i is either an axiom, a hypothesis or deducible from an earlier pair of formula P _j , P _k , (where P _k is of the form P _j ⇒ P _i ) and modus ponens. Modus ponens is a rule of inference that states that given propositions A, and A ⇒ B then proposition B may be deduced. The deduction of a formula Q from a set of hypothesis H is denoted by H ├ Q, and where Q is deducible from the axioms alone this is denoted by ├ Q.

The deduction theorem of propositional logic states that if H ∪ {P} ├ Q, then H ├ P → Q, and the converse of the theorem is also true: i.e. if H ├ P → Q then H ∪ {P} ├ Q. Formalism (this approach was developed by the German mathematician, David Hilbert) allows reasoning about symbols according to rules, and to derive theorems from formulae irrespective of the meanings of the symbols and formulae.

Propositional calculus is sound; i.e. any theorem derived using the Hilbert approach is true. Further, the calculus is also complete, and every tautology has a proof (i.e. is a theorem in the formal system). The propositional calculus is consistent: (i.e. it is not possible that both the well-formed formula A and ¬A are deducible in the calculus).

Propositional calculus is decidable: i.e. there is an algorithm (truth table) to determine for any well-formed formula A whether A is a theorem of the formal system. The Hilbert style system is slightly cumbersome in conducting proof and is quite different from the normal use of logic in mathematical deduction.

15.2.7 Applications of Propositional Calculus

Propositional calculus may be employed in reasoning with arguments in natural language. First, the premises and conclusion of the argument are identified and formalized into propositions. Propositional logic is then employed to determine if the conclusion is a valid deduction from the premises.

Consider, for example, the following argument that aims to prove that Superman does not exist.

If Superman were able and willing to prevent evil, he would do so. If Superman were unable to prevent evil he would be impotent; if he were unwilling to prevent evil he would be malevolent; Superman does not prevent evil. If superman exists he is neither malevolent nor impotent; therefore Superman does not exist.

First, letters are employed to represent the propositions as follows:

• a: Superman is able to prevent evil

• w: Superman is willing to prevent evil

• i: Superman is impotent

• m: Superman is malevolent

• p: Superman prevents evil

• e: Superman exists

Then, the argument above is formalized in propositional logic as follows:

Premises
P 1	(a ∧w) → p
P 2	(¬a → i) ∧ (¬w → m)
P 3	¬p
P 4	e → ¬ i ∧¬ m
————————————
Conclusion	P 1 ∧ P 2∧ P 3 ∧ P 4 ⇒ ¬ e

Proof that Superman does not exist

1.	a ∧ w → p	Premise 1
2.	(¬ a →i) ∧ (¬ w →m)	Premise 2
3.	¬p	Premise 3
4.	e→ (¬ i ∧ ¬ m)	Premise 4
5.	¬p → ¬(a ∧ w)	1, Contrapositive
6.	¬(a ∧ w)	3, 5 Modus Ponens
7.	¬a ∨ ¬w	6, De Morgan’s Law
8.	¬ (¬ i ∧ ¬ m) → ¬e	4, Contrapositive
9.	i ∨ m → ¬e	8, De Morgan’s Law
10.	(¬ a → i)	2, ∧ Elimination
11.	(¬ w → m)	2, ∧ Elimination
12.	¬ ¬a ∨ i	10, A→ B equivalent to ¬A∨ B
13.	¬ ¬a ∨ i ∨ m	11, ∨ Introduction
14.	¬ ¬a ∨ (i ∨ m)
15.	¬a → (i ∨ m)	14, A → B equivalent to ¬A∨ B
16.	¬ ¬w ∨ m	11, A → B equivalent to ¬A∨ B
17.	¬ ¬w ∨ (i ∨ m)
18.	¬w → (i ∨ m)	17, A → B equivalent to ¬A∨ B
19.	(i ∨ m)	7, 15, 18 ∨Elimination
20.	¬e	9, 19 Modus Ponens

Second Proof

1.	¬p	P 3
2.	¬(a ∧w) ∨ p	P 1 (A → B ≡ ¬A ∨ B)
3.	¬(a ∧w)	1, 2 A ∨ B, ¬B ├ A
4.	¬a ∨ ¬w	3, De Morgan’s Law
5.	(¬a → i)	P 2 (∧-Elimination)
6.	¬a → i ∨ m	5, x → y ├ x → y ∨ z
7.	(¬w → m)	P 2 (∧-Elimination)
8.	¬w → i ∨ m	7, x → y ├ x → y ∨ z
9.	(¬a ∨ ¬w) → (i ∨ m)	8, x → z, y→ z ├ x ∨ y → z
10.	(i ∨ m)	4, 9 Modus Ponens
11.	e → ¬(i ∨ m)	P 4 (De Morgan’s Law)
12.	¬e ∨ ¬ (i ∨ m)	11, (A → B ≡ ¬A ∨ B)
13.	¬e	10, 12 A ∨ B, ¬B ├ A

Therefore, the conclusion that Superman does not exist is a valid deduction from the given premises.

15.2.8 Limitations of Propositional Calculus

The propositional calculus deals with propositions only. It is incapable of dealing with the syllogism ‘All Greeks are mortal; Socrates is a Greek; therefore Socrates is mortal’. This would be expressed in propositional calculus as three propositions A, B therefore C, where A stands for ‘All Greeks are mortal’, B stands for ‘Socrates is a Greek’ and C stands for ‘Socrates is mortal’. Propositional logic does not allow the conclusion that all Greeks are mortal to be derived from the two premises.

Predicate calculus deals with these limitations by employing variables and terms, and using universal and existential quantification to express that a particular property is true of all (or at least one) values of a variable. Predicate calculus is discussed in the next section.

15.3 Predicate Calculus

Predicate logic is a richer system than propositional logic, and it allows complex facts about the world to be represented. It allows new facts about the world to be derived in a way that guarantees that if the initial facts are true then the conclusions are true. Predicate calculus includes predicates, variables, constants and quantifiers.

A predicate is a characteristic or property that an object can have, and we are predicating some property of the object. For example, “Socrates is a Greek” could be expressed as G(s), with capital letters standing for predicates and small letters standing for objects. A predicate may include variables, and a statement with a variable becomes a proposition once the variables are assigned values. For example, G(x) states that the variable x is a Greek, whereas G(s) is an assignment of values to x. The set of values that the variables may take is termed the universe of discourse, and the variables take values from this set.

Predicate calculus employs quantifiers to express properties such as all members of the domain have a particular property: e.g., (∀x)P(x), or that there is at least one member that has a particular property: e.g. (∃x)P(x). These are referred to as the universal and existential quantifiers.

The syllogism ‘All Greeks are mortal; Socrates is a Greek; therefore Socrates is mortal’ may be easily expressed in predicate calculus by

$$ \begin{aligned} & (\forall x)(G\left( x \right) \to M\left( x \right)) \\ & G(s) \\ & - - - - - - - - - - - - - - - - \\ & M\left( s \right) \\ \end{aligned} $$

In this example, the predicate G(x) stands for x is a Greek and the predicate M(x) stands for x is mortal. The formula G(x)→ M(x) states that if x is a Greek then x is mortal, and the formula (∀x)(G(x)→ M(x)) states for any x that if x is a Greek then x is mortal. The formula G(s) states that Socrates is a Greek and the formula M(s) states that Socrates is mortal.

Example 15.6

(Predicates) A predicate may have one or more variables. A predicate that has only one variable (i.e. a unary or 1-place predicate) is often related to sets; a predicate with two variables (a 2-place predicate) is a relation; and a predicate with n variables (a n-place predicate) is a n-ary relation. Propositions do not contain variables and so they are 0-place predicates. The following are examples of predicates:

• (i) The predicate Prime(x) states that x is a prime number (with the natural numbers being the universe of discourse).

• (ii) Lawyer(a) may stand for a is a lawyer.

• (iii) Mean(m, x, y) states that m is the mean

• (iv) of x and y: i.e. m = ½(x + y).

• (iv) LT(x, 6) states that x is less than 6.

• (v) G(x, π) states that x is greater than π (where is the constant 3.14159)

• (vi) G(x, y) states that x is greater than y.

• (vii) EQ(x, y) states that x is equal to y.

• (viii) LE(x, y) states that x is less than or equal to y.

• (ix) Real(x) states that x is a real number.

• (x) Father(x, y) states that x is the father of y.

• (xi) ¬(∃x)(Prime(x) ∧ B(x, 32, 36)) states that there is no prime number between 32 and 36.

Universal and Existential Quantification

The universal quantifier is used to express a statement such as that all members of the domain have property P. This is written as (∀x)P(x) and expresses the statement that the property P(x) is true for all x. Similarly, (∀x ₁, x ₂, …, x _n ) P(x ₁, x ₂, …, x _n ) states that property P(x ₁, x ₂, …, x _n ) is true for all x ₁, x ₂, …, x _n . Clearly, the predicate (∀x) P(a, b) is identical to P(a, b) since it contains no variables, and the predicate (∀y ∈ℕ) (x ≤ y) is true if x = 1 and false otherwise.

The existential quantifier states that there is at least one member in the domain of discourse that has property P. This is written as (∃x)P(x) and the predicate (∃x ₁, x ₂, …, x _n ) P(x ₁, x ₂, …, x _n ) states that there is at least one value of (x ₁, x ₂, …, x _n ) such that P(x ₁, x ₂, …, x _n ) is true.

Example 15.7

(Quantifiers)

• (i) (∃p) (Prime(p) ∧ p > 1,000,000) is true

  It expresses the fact that there is at least one prime number greater than a million, which is true as there are an infinite number of primes.

• (ii) (∀x) (∃ y) x < y is true

  This predicate expresses the fact that given any number x we can always find a larger number: e.g. take y = x + 1.

• (iii) (∃ y) (∀x) x < y is false

  This predicate expresses the statement that there is a natural number y such that all natural numbers are less than y. Clearly, this statement is false since there is no largest natural number, and so the predicate (∃ y) (∀x) x < y is false.

Comment 15.1

It is important to be careful with the order in which quantifiers are written, as the meaning of a statement may be completely changed by the simple transposition of two quantifiers.

The well-formed formulae in the predicate calculus are built from terms and predicates, and the rules for building the formulae are described briefly in Sect. 15.3.1. Examples of well-formed formulae include

$$ \begin{aligned} & (\forall x)\left( {x > 2} \right) \\ & (\exists x)x^{ 2} = 2\\ & (\forall x)\,(x > { 2} \wedge x < 10) \\ & (\exists y)x^{ 2} = y \\ & (\forall x)\,(\forall y)\,Love\left( {y,x} \right)\quad \quad \left( {{\text{everyone}}\,{\text{is}}\,{\text{loved}}\,{\text{by}}\,{\text{someone}}} \right) \\ & (\exists y) \, (\forall x)Love\left( {y,x} \right)\quad \quad \,\left( {{\text{someone}}\,{\text{loves}}\,{\text{everyone}}} \right) \\ \end{aligned} $$

The formula (∀x)(x > 2) states that every x is greater than the constant 2; (∃x) x ² = 2 states that there is an x that is the square root of 2; (∀x) (∃y) x ² = y states that for every x there is a y such that the square of x is y.

15.3.1 Sketch of Formalization of Predicate Calculus

The formalization of predicate calculus includes the definition of an alphabet of symbols (including constants and variables), the definition of function and predicate letters, logical connectives and quantifiers. This leads to the definitions of the terms and well-formed formulae of the calculus.

The predicate calculus is built from an alphabet of constants, variables, function letters, predicate letters and logical connectives (including the logical connectives discussed in propositional logic, and universal and existential quantifiers).

The definition of terms and well-formed formulae specifies the syntax of the predicate calculus, and the set of well-formed formulae gives the language of the predicate calculus. The terms and well-formed formulae are built from the symbols, and these symbols are not given meaning in the formal definition of the syntax.

The language defined by the calculus needs to be given an interpretation in order to give a meaning to the terms and formulae of the calculus. The interpretation needs to define the domain of values of the constants and variables, provide meaning to the function letters, the predicate letters and the logical connectives.

Terms are built from constants, variables and function letters. A constant or variable is a term, and if t ₁, t ₂, …, t _k are terms, then f ^k _i (t ₁, t ₂, …, t _k ) is a term (where f ^k _i is a k-ary function letter). Examples of terms include

$$ \begin{aligned} x^{ 2} \quad \quad & {\text{where}}\,x\,{\text{is}}\,{\text{a}}\,{\text{variable}}\,{\text{and}}\,{\text{square}}\,{\text{is}}\,{\text{a}}\, 1- {\text{ary}}\,{\text{function}}\,{\text{letter}} \\ x^{ 2} + y^{ 2} \quad & {\text{where}}\,x^{ 2} + y^{ 2} \,{\text{is}}\,{\text{shorthand}}\,{\text{for}}\,{\text{the}}\,{\text{function}}\,{\text{add}}\left( {{\text{square}}\left( x \right),\,{\text{square}}\left( y \right)} \right) \\ & {\text{where}}\,{\text{add}}\,{\text{is}}\,{\text{a}}\, 2- {\text{ary}}\,{\text{function}}\,{\text{letter}}\,{\text{and}}\,{\text{square}}\,{\text{is}}\,{\text{a}}\, 1- {\text{ary}}\,{\text{function}} \\ \end{aligned} $$

The well-formed formulae are built from terms as follows. If P ^k _i is a k-ary predicate letter, t ₁, t ₂, …, t _k are terms, then P ^k _i (t ₁, t ₂, …, t _k ) is a well-formed formula. If A and B are well-formed formulae then so are ¬A, A ∧ B, A ∨ B, A → B, A ↔ B, (∀x)A and (∃x)A.

There is a set of axioms for predicate calculus and two rules of inference used for the deduction of new formulae from the existing axioms and previously deduced formulae. The deduction of a new formula Q is via a sequence of well-formed formulae P ₁, P ₂, … P _n (where P _n  = Q) such that each P _i is either an axiom, a hypothesis or deducible from one or more of the earlier formulae in the sequence.

The two rules of inference are modus ponens and generalization. Modus ponens is a rule of inference that states that given predicate formulae A, and A ⇒ B then the predicate formula B may be deduced. Generalization is a rule of inference that states that given predicate formula A, then the formula (∀x)A may be deduced where x is any variable.

The deduction of a formula Q from a set of hypothesis H is denoted by H ├ Q, and where Q is deducible from the axioms alone this is denoted by ├ Q. The deduction theorem states that if H ∪ {P} ├ Q then H ├ P → Q³ and the converse of the theorem is also true: i.e. if H ├ P → Q then H ∪ {P} ├ Q.

The approach allows reasoning about symbols according to rules, and to derive theorems from formulae irrespective of the meanings of the symbols and formulae. Predicate calculus is sound: i.e. any theorem derived using the approach is true, and the calculus is also complete.

Scope of Quantifiers

The scope of the quantifier (∀x) in the well-formed formula (∀x)A is A. Similarly, the scope of the quantifier (∃x) in the well-formed formula (∃x)B is B. The variable x that occurs within the scope of the quantifier is said to be a bound variable. If a variable is not within the scope of a quantifier it is free.

Example 15.8

(Scope of Quantifiers)

• (i) x is free in the well-formed formula ∀y (x ² + y > 5)

• (ii) x is bound in the well-formed formula ∀x (x ² > 2)

A well-formed formula is closed if it has no free variables. The substitution of a term t for x in A can only take place only when no free variable in t will become bound by a quantifier in A through the substitution. Otherwise, the interpretation of A would be altered by the substitution.

A term t is free for x in A if no free occurrence of x occurs within the scope of a quantifier (∀y) or (∃y) where y is free in t. This means that the term t may be substituted for x without altering the interpretation of the well-formed formula A.

For example, suppose A is ∀y (x ² + y ² > 2) and the term t is y, then t is not free for x in A as the substitution of t for x in A will cause the free variable y in t to become bound by the quantifier ∀y in A, thereby altering the meaning of the formula to ∀y (y ² + y ² > 2).

15.3.2 Interpretation and Valuation Functions

An interpretation gives meaning to a formula and it consists of a domain of discourse and a valuation function. If the formula is a sentence (i.e. does not contain any free variables) then the given interpretation of the formula is either true or false. If a formula has free variables, then the truth or falsity of the formula depends on the values given to the free variables. A formula with free variables essentially describes a relation say, R(x ₁, x ₂,.… x _n ) such that R(x ₁, x ₂,.… x _n ) is true if (x ₁, x ₂, … x _n ) is in relation R. If the formula is true irrespective of the values given to the free variables, then the formula is true in the interpretation.

A valuation (meaning) function gives meaning to the logical symbols and connectives. Thus, associated with each constant c is a constant c _Σ in some universe of values Σ; with each function symbol f of arity k, we have a function symbol f _Σ in Σ and f _Σ: Σ^k → Σ; and for each predicate symbol P of arity k a relation P _Σ ⊆ Σ ^k. The valuation function, in effect, gives the semantics of the language of the predicate calculus L.

The truth of a predicate P is then defined in terms of the meanings of the terms, the meanings of the functions, predicate symbols, and the normal meanings of the connectives.

Mendelson [3] provides a technical definition of truth in terms of satisfaction (with respect to an interpretation M). Intuitively a formula F is satisfiable if it is true (in the intuitive sense) for some assignment of the free variables in the formula F. If a formula F is satisfied for every possible assignment to the free variables in F, then it is true (in the technical sense) for the interpretation M. An analogous definition is provided for false in the interpretation M.

A formula is valid if it is true in every interpretation; however, as there may be an uncountable number of interpretations, it may not be possible to check this requirement in practice. M is said to be a model for a set of formulae if and only if every formula is true in M.

There is a distinction between proof theoretic and model theoretic approaches in predicate calculus. Proof theoretic is essentially syntactic, and there is a list of axioms with rules of inference. The theorems of the calculus are logically derived (i.e. ├ A) and the logical truths are as a result of the syntax or form of the formulae, rather than the meaning of the formulae. Model theoretical, in contrast is essentially semantic. The truth derives from the meaning of the symbols and connectives, rather than the logical structure of the formulae. This is written as ├ _M A.

A calculus is sound if all of the logically valid theorems are true in the interpretation, i.e. proof theoretic ⇒ model theoretic. A calculus is complete if all the truths in an interpretation are provable in the calculus, i.e. model theoretic ⇒ proof theoretic. A calculus is consistent if there is no formula A such that ├ A and ├ ¬A.

The predicate calculus is sound, complete and consistent. Predicate calculus is not decidable: i.e. there is no algorithm to determine for any well-formed formula A whether A is a theorem of the formal system. The undecidability of the predicate calculus may be demonstrated by showing that if the predicate calculus is decidable then the halting problem (of Turing machines) is solvable. We discussed the halting problem in Chap. 13.

15.3.3 Properties of Predicate Calculus

The following are properties of the predicate calculus.

$$ \begin{aligned} ({\text{i}})\quad & (\forall x)P\left( x \right) \equiv (\forall y)P\left( y \right) \\ ({\text{ii}})\quad & (\forall x)P\left( x \right) \equiv \neg (\exists x)\neg P\left( x \right) \\ ({\text{iii}})\quad & (\exists x)P\left( x \right) \equiv \neg (\forall x)\neg P\left( x \right) \\ ({\text{iv}})\quad & (\exists x)P\left( x \right) \equiv (\exists y)P\left( y \right) \\ ({\text{v}})\quad & (\forall x)(\forall y)P\left( {x,y} \right) \equiv (\forall y)\,(\forall x)P\left( {x,y} \right) \\ ({\text{vi}})\quad & (\exists x)(P\left( x \right) \vee Q\left( x \right)) \equiv (\exists x)P\left( x \right) \vee (\exists y)Q\left( y \right) \\ ({\text{vii}})\quad & (\forall x)P\left( x \right) \wedge Q\left( x \right)) \equiv (\forall x)\,P(x) \wedge \left( {\forall y} \right)Q(y) \\ \end{aligned} $$

15.3.4 Applications of Predicate Calculus

The predicate calculus is may be employed to formally state the system requirements of a proposed system. It may be used to conduct formal proof to verify the presence or absence of certain properties in a specification. It may also be employed to define piecewise defined functions such as f(x, y) where f(x, y) is defined by

$$ \begin{array}{*{20}l} {f(x,y) = x^{2} - y^{2} } \hfill & {{\text{where}}\,x \le 0 \wedge y < 0;} \hfill \\ {f(x,y) = x^{2} + y^{2} } \hfill & {{\text{where}}\,x > 0 \wedge y < 0;} \hfill \\ {f(x,y) = x + y} \hfill & {{\text{where}}\,x \ge 0 \wedge y = 0;} \hfill \\ {f(x,y) = x - y} \hfill & {{\text{where}}\,x < 0 \wedge y = 0;} \hfill \\ {f(x,y) = x + y} \hfill & {{\text{where}}x\, \le 0 \wedge y > 0;} \hfill \\ {f(x,y) = x^{2} + y^{2} } \hfill & {{\text{where}}\,x > 0 \wedge y > 0} \hfill \\ \end{array} $$

The predicate calculus may be employed for program verification, and to show that a code fragment satisfies its specification. The statement that a program F is correct with respect to its precondition P and postcondition Q is written as P{F}Q. The objective of program verification is to show that if the precondition is true before execution of the code fragment, then this implies that the postcondition is true after execution of the code fragment.

A program fragment a is partially correct for precondition P and postcondition Q if and only if whenever a is executed in any state in which P is satisfied and execution terminates, then the resulting state satisfies Q. Partial correctness is denoted by P{F}Q, and Hoare’s Axiomatic Semantics is based on partial correctness. It requires proof that the postcondition is satisfied if the program terminates.

A program fragment a is totally correct for precondition P and postcondition Q, if and only if whenever a is executed in any state in which P is satisfied then the execution terminates and the resulting state satisfies Q. It is denoted by {P}F{Q}, and Dijkstra’s calculus of weakest preconditions is based on total correctness [2, 4]. It is required to prove that if the precondition is satisfied then the program terminates and the postcondition is satisfied

15.3.5 Semantic Tableaux in Predicate Calculus

We discussed the use of semantic tableaux for determining the validity of arguments in propositional logic earlier in this chapter, and its approach is to negate the conclusion of an argument and to show that this results in inconsistency with the premises of the argument.

The use of semantic tableaux is similar with predicate logic, except that there are some additional rules to consider. As before, if all branches of a semantic tableau are closed, then the premises and the negation of the conclusion are mutually inconsistent, and all branches in the tableau are closed. From this, we deduce that the conclusion must be true.

The rules of semantic tableaux for propositional logic were presented in Table 15.12, and the additional rules specific to predicate logic are detailed in Table 15.14.

Table 15.14 Extra rules of semantic tableaux (for predicate calculus)

Example 15.9

(Semantic Tableaux) Show that the syllogism ‘All Greeks are mortal; Socrates is a Greek; therefore Socrates is mortal’ is a valid argument in predicate calculus.

Solution

We expressed this argument previously as (∀x)(G(x)→ M(x)); G(s); M(s). Therefore, we negate the conclusion (i.e. ¬M(s)), and try to construct a closed tableau.

Therefore, as the tableau is closed we deduce that the negation of the conclusion is inconsistent with the premises, and that therefore the conclusion follows from the premises.

Example 15.10

(Semantic Tableaux) Determine whether the following argument is valid.

• All lecturers are motivated

• Anyone who is motivated and clever will teach well

• Joanne is a clever lecturer

• Therefore, Joanne will teach well.

Solution

We encode the argument as follows

• L(x) stands for ‘x is a lecturer’

• M(x) stands for ‘x is motivated’

• C(x) stands for ‘x is clever’

• W(x) stands for ‘x will teach well’

We therefore wish to show that

$$ (\forall x)(L\left( x \right) \to M\left( x \right)) \wedge (\forall x)((M\left( x \right) \wedge C\left( x \right)) \to W\left( x \right)) \wedge L\left( {joanne} \right) \wedge C\left( {joanne} \right)\,{\models }W\left( {joanne} \right) $$

Therefore, we negate the conclusion (i.e. ¬W(joanne)) and try to construct a closed tableau.

Therefore, since the tableau is closed we deduce that the argument is valid.

15.4 Review Questions

• 1. Draw a truth table to show that ¬ (P → Q) ≡ P ∧¬ Q

• 2. Translate the sentence ‘Execution of program P begun with x < 0 will not terminate’ into propositional form.

• 3. Prove the following theorems using the inference rules of natural deduction

  • a. From b infer b ∨¬c

  • b. From b ⇒ (c ∧ d), b infer d

• 4. Explain the difference between the universal and the existential quantifier.

• 5. Express the following statements in the predicate calculus

  • a. All natural numbers are greater than 10

  • b. There is at least one natural number between 5 and 10

  • c. There is a prime number between 100 and 200.

• 6. Which of the following predicates are true?

  • a. $\forall i \in \{ 10, \ldots , 50\} .i^{ 2} < 2000 \wedge i < 100$

  • b. $\exists i \in {\mathbb{N}}.i > 5\wedge i^{ 2} = 2 5$

  • c. $\exists i \in {\mathbb{N}}.i^{ 2} = 2 5$

• 7. Use semantic tableaux to show that (A → A) ∨ (B ∧ ¬B) is true

• 8. Determine if the following argument is valid.

  If Pilar lives in Cork, she lives in Ireland. Pilar lives in Cork. Therefore, Pilar lives in Ireland.

15.5 Summary

This chapter considered propositional and predicate calculus. Propositional logic is the study of propositions, and a proposition is a statement that is either true or false. A formula in propositional calculus may contain several variables, and the truth or falsity of the individual variables, and the meanings of the logical connectives determines the truth or falsity of the logical formula.

A rich set of connectives is employed in propositional calculus to combine propositions and to build up the well-formed formulae of the calculus. This includes the conjunction of two propositions (A ∧ B), the disjunction of two propositions (A ∨ B), and the implication of two propositions (A ⇒ B). These connectives allow compound propositions to be formed, and the truth of the compound propositions is determined from the truth values of the constituent propositions and the rules associated with the logical connectives. The meaning of the logical connectives is given by truth tables.

Propositional calculus is both complete and consistent with all true propositions deducible in the calculus, and there is no formula A such that both A and ¬A are deducible in the calculus.

An argument in propositional logic consists of a sequence of formulae that are the premises of the argument and a further formula that is the conclusion of the argument. One elementary way to see if the argument is valid is to produce a truth table to determine if the conclusion is true whenever all of the premises are true. Other ways are to use semantic tableaux or natural deduction.

Predicates are statements involving variables and these statements become propositions once the variables are assigned values. Predicate calculus allows expressions such as all members of the domain have a particular property to be expressed formally: e.g., (∀x)Px, or that there is at least one member that has a particular property: e.g., (∃x)Px.

Predicate calculus may be employed to specify the requirements for a proposed system and to give the definition of a piecewise defined function. Semantic tableaux may be used for determining the validity of arguments in propositional or predicate logic, and its approach is to negate the conclusion of an argument and to show that this results in inconsistency with the premises of the argument.