୯ҥᆵεᏢႝᐒၗૻᏢଣၗૻπำᏢس ᅺγፕЎ
Department of Computer Science and Information Engineering College of Electrical Engineering and Computer Science
National Taiwan University Master Thesis
ᅇᔆᅟႥၡ৩ୢᚒӧ๏ۓᚐѦॊຒ಄ဦϐΒ໘ᡄᒠΠޑ߄Ңݤ
A Study on Expressing the Hamiltonian Path Problem in Second-Order Logic with Some Additional Predicate Symbols
ֆॡᓄ Wei-Lin Wu
ࡰᏤ௲Ǻᇳڷप റγ
Advisor: Kun-Mao Chao, Ph.D.
ύ҇୯ 98 ԃ 6 Д
June, 2009
ᇞᖴ
ҁጇፕЎޑፍғǴаךঁߚ࣬ᜢሦୱङඳޑᏢғٰᇥǴঁΓᐱΚֹԋࢂόёૈޑҺ
୍Ƕჹܭ܌ԖමഉՔךǵᔅշךޑӚՏǴךᙣа೭ጇፕЎٰ߄ၲჹգॺޑགᖴ!
२ӃǴךाགᖴޑࢂךޑࡰᏤ௲ᇳڷपԴৣǶᇳԴࡉᓨ॥፪ǵᒃϪکᝰޑᄊࡋǴۈಖ ᡣךӑຝుڅǶซளךಃԛѠൔޑ߄όࣗགྷǴԴৣϝฅ๏ךӭ҅य़ຑሽǴᡣ ךૈӧௗΠٰ൳ԛൔޑ߄ߞЈΜى٠Ъ߄ளຫٰຫӳǶӧᅺγғఱޑٿԃ္Ǵך ਔதᄊࡋණᅐǵόޕᆒᆒǶฅԶԴৣࠅૅᛸቨεǴаႴᓰжඹೢഢǶ٠Ъӧךᎁख़ε
שǵЈեዊޑਔংǴਔਔ๏ϒᜢᚶکྕཪǶќБय़ǴךΨགᖴԴৣӧךॺޑࣴز፟
ϒཱུεޑԾҗǴ٬ךૈӧԾρགᑫ፪ޑሦୱ---ኧᡄᒠکीᆉፕ---ǴᅰӦวචǴ٠
๏ϒࡰᏤکޭۓǶԴৣޑৱǴך҉ғᜤב!
ௗǴךΨགᖴځдٿՏα၂ہ---৪ᅜ଼ԴৣکඁԴৣǶᖴᖴٿՏԴৣӧα၂ਔǴ
๏ךӭࡌکࡰᏤǴ٬ךޑፕЎૈঅႬள׳ӳǴևளᅰ๓ᅰऍǶӕਔΨགᖴாॺǴჹ ܭךޑࣴزЬᚒޑᢌ፞ᆶޭۓǴ࣬ߞӧௗΠٰޑࣴزύǴךૈ׳ԖߞЈ٠Ъ߄ߝ!
ฅࡕǴךाགᖴҁس௲ዅԴৣǴаϷণᏢس௲ླྀߎᑊԴৣǶᖴᖴٿՏԴৣਔதኘ ޜᆶךፋ၉Ǵᙚᆶךࣴز࣬ᜢޑਜᝤѦǴᗋόჇځྠӦှเךޑ֚ൽǴ٬ךૈӧኧᡄ ᒠޑᇡ׳Ƕ೭ጇፕЎૈֹԋǴӭᖝٿՏԴৣޑڐշ!
ќѦǴགᖴҁسֺࡏܻӕᏢǴᖴᖴգᙚ๏ךޑ࣬ᜢਜᝤǴ೭ჹךޑࣴزБӛԖᜢᗖ
܄ޑቹៜ! ᗋԖ݅٫ቼӕᏢǴᖴᖴգதᆶךϩ٦ፕᄽᆉݤ! Ψགᖴҁჴᡍ࠻ςԋࢫ ඵ៕ᏢߏǴаϷণᏢسᏢྤ๔ӕᏢǴᆶٿՏޑፋ၉ਔதᐟวрך٤ཥޑགྷݤǴჹךޑ
ࣴزԖࡐεޑᔅշ! ٿՏޑᖃܴᐒඵǵϸᔈᡫ௵ΨзךӑຝుڅǶ
ᅺγғఱޑ೭ٿԃǴӧ ACB ჴᡍ࠻೭ঁεৎ܌ԖԋޑڐշΠǴךωૈԖϞВޑԋ
݀Ƕᖴᖴ Roger ᏢߏǵεޚᏢۆᗋԖܴԢᏢߏǴᖴᖴգॺᆶךϩ٦۶ԜޑЈ٣! ᖴᖴӼமᏢ ߏǴᖴᖴգததᖐᒤநࢲǴᡣךӧࣴزϐᎩૈԖ଼நޑু(ݽξਓၯ); Ψᖴᖴ߷ӹ ᏢߏᗋԖࣿᏢۂǴᖴᖴգॺததᆶךӕୖᆶӼமᏢߏޑࢲ! ᖴᖴ wasabe ᏢۆǴᖴᖴی தගٮךӭڐշ٠Ъᗎፎךଆࠔऍ१! ᖴᖴঢᗋԖบঢٿՏᏢߏǴၟٿՏಠ٤Ԗ
፪၉ᚒޑਔংࡐ! ᖴᖴጩᏢۂǴᖴᖴیਔதکךፕаϷϩ٦ኧᏢ၉ᚒǴیޑགྷݤத தᡣךளࡐձ! ᖴᖴҺᏢߏǵՙҺᏢߏᗋԖᑉᏢǴᗨฅךکգॺޑௗਔ໔όӭǴ όၸךᕴࢂགڙډգॺޑᒃϪǴᖴᖴգॺѳத๏ךޑ٤ᔅԆ! ΨᖴᖴλۏӕᏢǴգࡐ cool ΨࡐԖૈΚǶךᕴࢂಉЈεཀǴᖴᖴգਔதඹךೀӭεୢᚒǴࡐଯᑫૈၟգԋࣁӕᏢ!
നࡕǴךाགᖴךޑР҆ৎΓǵךޑבԃϐҬѯሌǴᗋԖӳ϶ΪউǶᖴᖴգॺޔаٰ
ჹךޑЍᗋԖᜢЈǴ٠Ъӧךᎁၶख़εשਔǴႴᓰך٠Ъ๏ךྕཪکྣ៝Ƕգॺࢂךङ ࡕനεޑΚٰྍ! ΨགᖴමഉՔךǵᔅշךᗋԖངךޑܻ϶ॺ!
ύЎᄔा
ᡄᒠࢂኧᏢ္ߐ௶ॊޑᄽᛢޑঁϩЍǴᇡۓࣁޑࣴزǶҗܭኧᏢޑ ҁ፦ࢂҗᜢܭኧᏢނҹޑ௶ॊаϷᡍ೭٤௶ॊޑܴ܌ᄬԋǴӢԜǴঁኧᏢሦୱёаҔ ᡄᒠуаϩǶԶፕႝတࣽᏢޑਡЈϩ---ᄽᆉݤǴځᢀۺޑ୷ᘵ൩ࢂीᆉޑᢀۺǴΨࢂ
ঁኧᏢނҹǴёҗᡄᒠϩϐǶӧ೭ጇፕЎ္ǴךॺගٮΑᡄᒠޑ୷ҁ܄፦Ǵ٠ЪճҔ೭٤
܄፦ٰࣴز٤ीᆉୢᚒǴձࢂᅇᔆᅟႥၡ৩(Hamiltonian Path)೭ঁკࠠፕޑୢᚒǶ
ᜢᗖӷǺڮᚒᡄᒠ(propositional logic)Ǵॊຒᡄᒠ(predicate logic)Ǵ໘ᡄᒠ(first-order logic)Ǵ Ӹӧ܄Β໘ᡄᒠ(existential second-order logic)ǴᅇᔆᅟႥၡ৩Ƕ
Abstract
Logic is a branch of mathematics that investigates the deductions about statements and is rec- ognized as the study of reasoning. Because of this, the whole mathematics can be investigated by logic and is even governed by it since the essentials of mathematics consist of statements about mathematical objects and the proofs that verify these statements. Since the underlying concept of algorithms, the critical part of theoretical computer science, is that of computation, which is also a mathematical object, it can aslo be analyzed by logic. In this thesis we provide the basic properties of logic, and then use them to investigate some computational problems, especially the graph-theoretic problem hamiltonian path.
Key Words: Propositional logic, predicate logic, first-order logic, existential second-order logic, Hamiltonian path.
Contents
1 Introduction 1
1.1 Prolog . . . 1
1.2 Categories inside Logic . . . 2
1.2.1 Computational Problems . . . 2
2 Topics on Propositional Logic 4 2.1 Preliminaries . . . 5
2.2 Syntax . . . 6
2.3 Semantics . . . 9
2.3.1 Equvalence between Propositions . . . 12
2.4 Deduction Systems . . . 15
3 Topics on Predicate Logic 19 3.1 First-order Logic . . . 20
3.1.1 Syntax . . . 20
3.1.2 Semantics . . . 23
3.1.3 Deduction Systems . . . 26
3.1.4 Weakness of First-Order Logic . . . 29
3.2 Second-Order Logic . . . 29
3.3 Remarks . . . 30
4 Graph-Theoretic Problems as Expressed in Logical Formulae 31 4.1 Prolog . . . 31
4.2 The Successor Function in Graph-Theoretic Problems . . . 32
5 Concluding Remarks 37
Bibliography 39
Chapter 1 Introduction
1.1 Prolog
Logic has long been considered the study of reasoning and thoughts, and the study of it can be traced back to the time of Aristotle, a philosopher of ancient Greece, who gave a collection of deduction rules for rationally thinking and governing knowledge. Among these deduction rules, the most well-known is syllogism.
It was not until the seventeenth century, however, that the investigations of logic grew mature, through the contributions of many excellent mathematicians and philosophers, among whom especially the German mathematician Leibnitz was the first one to investigate logic after the time of Aristotle, followed by the British mathematician Boole, whose work mainly concerned the so-called Boolean operations (which is now stated as Boolean algebras), then the American logician Peirce, who introduced quantifiers, and the German logician Frege and mathematician Hilbert, who resorted to laying the foundations of mathematics on logic (known as Hilbert’s program), etc.
In 1930s, the famous Austrian logician G¨odel proved an incompleteness theorem which put a devastating end to Hilbert’s program. On the other hand, the English mathematician Turing proposed the Halting problem, which led to the undecidability of first-order logic. Both of these results best demonstrated the fatal flaws of the formal method.
Nevertheless, the progress of the researches in mathematics and logic continued on, and several marvelous results have been discovered in recent decades.
1.2 Categories inside Logic
Because of the wealth of the study of logic, it is often divided into two facets: mathematical logic and philosophical logic. The former is more relevant to our study of computer science and is further divided into a number of categories: propostional logic (or sentential logic, Boolean logic), predicate logic (including first-order, second-order, etc.), both of which are classical studies, and intuitionistic logic (whose most apparent feature is the absence of the law of excluded-middle, one of the constituents of classical logic), which is the modern trend. We shall always refer to the classical one in this thesis.
There are four theories intimately related to the study of logic: proof theory, model theory, set theory and recursion theory. Proof theory and model theory, respectively, represent the studies of the two most fundamental notions about logic — that of syntax and of semantics.
Set theory was proposed by the German mathematician Cantor. It is by and large considered the most fundamental theory in mathematics since the whole mathematics can be based on the notion of sets.
Finally, in the view point concerning theoretical computer science, recursion theory is usually considered part of computation theory, and hence is often called computability theory, with the other part of computation theory being (computational) complexity theory. The American mathematician Church proposed the so-called λ-calculus, which is one of the formal notions of computations, proved to be equivalent to other notions such as Turing machine.
1.2.1 Computational Problems
Logic is powerful in expressing statements in symbolic fashion since its expressibilty is its raison d’ˆetre. It has the ability to express all the mathematical statements and therefore it is natural to express computational problems in logic.
In computation theory, a problem is said to be in P if there is a deterministic Turing machine that decides it in polynomial time, whereas a problem is in NP if the same happens except for a nondeterministic Turing machine. The problem P = NP is well-known in this field.?
Essentially, every computational problem (which can be seen as a set of strings, i.e. a language) can be taken as one in graph theory, as the encoding of every string in it can be
regarded as the first row of the adjacency matrix of a graph.
According to Fagin [1], all the graph-theoretic problems in NP can be characterized as formulae in existential second-order logic. Moreover, Kolaitis and Vardi [2] showed the powerful zero-one law, which implies that the set of problems expressible in Horn existential second-order logic is only a restricted proper subset of P.
However, with an additional predicate symbolS which is interpreted as the successor func- tion in advance, the problems that are precisely in P can be characterized as Horn formulae in existential second-order logic. This result was independently discovered in [3, 4, 5, 7]. We shall later give another illustration of the requirement that the predicate symbol of successor function should be given in advance.
Chapter 2
Topics on Propositional Logic
Generally speaking, in the investigations of logic we quite often concern ourselves to those objects called logical statements. Informally, a logical statement is one that is declarative, i.e.
one that we can decide whether is true or false — the so-called truth value. For example,
1. “1 + 1 = 2,”
2. “J. K. Rowling is the author of the series of novels Harry Potter,” and 3. “D. E. Knuth is one of the greatest computer scientists ever,”
etc.
But more importantly, the truth value of a logical statement or, equivalently, whether it holds or not, should be independent of one’s own opinion, i.e. it should be clear and universally accepted. If we re-examine the three examples listed above, it should be clear that the first two are logical statements while the last is not in the sense that whether it is true depends on our own opinions (though almost all people of our time accept it with no doubt).
As mentioned earlier, we restrict our interest to classical logic, one feature of which is binary truth value (either true or false, or either 0 or 1 for another notation), whereas in modern logic there is one area called multivalued logic, in which truth values between 0 and 1 are allowed.
2.1 Preliminaries
Natural languages, such as everday English or Chinese, abound with plenty of connectives:
‘and,’ ‘or,’ ‘not,’ ‘but,’ ‘if . . . then,’ ‘if . . . then . . . else,’ ‘since,’ ‘unless,’ ‘while,’ etc. Actually, some of them are redundant, for example:
1. “Fried chicken is delicious but unhealthy.”: we could say “fried chicken is delicious and fried chicken is not healthy,” though that seems somewhat garrulous.
2. “If P = NP, then there are efficient algorithms to solve those NP-complete problems; else they are considered to be intractable.”: we could say “if P = NP, then there are efficient algorithms to solve NP-complete problems; else NP-complete problems are considered to be intractable.”
And at the same time, there is often temporal ordering with the usage of ‘and’:
1. “The police came in and the thief ran away.”
2. “The thief ran away and the police came in.”
In such statements, ‘and’ is in place of ‘and then.’
Moreover, we use ‘or’ sometimes in inclusive sense such as “that girl is slim or she is smart,”
in which one of both constituents of the statement is the case, and the case can be both; other times in exclusive sense such as “the manufacturer of this CPU is Intel or AMD,” in which one of both constituents of the statement is the case but it cannot be both. Occasionally, we even use ‘or’ to describe the situation resulted from that some criterion fails to hold, e.g. “you should hurry up or you would miss the bus.”
Moreover, some of them somewhat implicitly show our feelings about the events. For ex- ample, “that machine seems broken but it works,” in which the use of ‘but’ shows our surprise that the machine in question still works.
As we have seen, these examples illustrate the ambiguities and vagueness that often arise in our daily languages. What we need as a tool in studying mathematics as well as logic, is a formal and artificial language that contains preciseness and exactness while excluding those uncertainties.
Fortunately, for our purpose it is sufficient to use only a restricted part of the connetives mentioned above: ‘and,’ ‘or,’ ‘not,’ ‘if . . . then,’ and additionally ‘if and only if.’ In order to be precise, in logical statements we shall limit ourselves to the usage of the connectives just mentioned, and it is no loss with this restriction. In particular, we shall stipulate that
1. There is no temporal ordering with ‘and’;
2. There is no causal relation between the two statements connected by ‘or,’ it is merely used to indicate that one (or more) statement is the case;
3. ‘If . . . then’ is always used for implications; and finally 4. ‘If and only if’ is always used for bi-implications.
2.2 Syntax
The language we shall adopt here is the language of propositional logic. We shall give precise definitions of terminologies in the following:
Definition 2.1: [10] The alphabet of the language of propositional logic is the set that consists of
(a) propositional variables: p0, p1, . . . ; (b) propositional constants: true, false;
(c) logical connectives: ∧, ∨, ¬, →, ↔;
(d) parentheses: (, ).
We shall use the terms “variables,” “constants” and “connectives” for short when there are no ambiguities.
In the following we list the name of each connective and the way to pronounce them: [10]
symbol name pronunciation
∧ conjunction and
∨ disjunction or
¬ negation not
→ implication if . . . then
↔ equivalence . . . if and only if . . .
The objects in this language, propositions, are defined recursively in the following:
Definition 2.2: [10]
(a) true, false and pn for all n ∈ N, are propostions;
(b) If ϕ is a proposition, then so is ¬ϕ;
(c) If ϕ and ψ are propositions, then so are (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ) and (ϕ ↔ ψ). In fact, the symbols ϕ and ψ above are there merely to serve the purpose to denote some propositions, i.e. they are metavariables. They themselves are not propositions, actually. See [10]. In some viewpoint, the language we are investigating here (i.e. the language of proposi- tional logic) is so-called object language, and the language we use to describe it (i.e. English) is so-called metalanguage. See [6, 10]. The notions of object language and of metalanguage should not be unfamiliar to us: for the study of programming, the object language is of course the programming language itself, while the metalanguage is our daily language; for linguistics such as the research on Latin, the object language is Latin, whereas our daily language (English or some other) plays the role of metalanguage. In fact, the famous liar’s paradox
“This statement is false,”
which is an instance of self reference, arises from our confusion with object languages and metalanguages. This discrimination between them is essential to theory of truth, in which field the Polish logician Tarski contributed much. For a more thorough treatment about this, see [8].
On the other hand, the notation we adopt here is in infix form, i.e. we place the binary connectives (all except ‘¬,’ which is unary) between two propositions. In fact, we could adopt the notation in prefix form, i.e. binary connetives precede their two arguments, the so-called Polish notation. For example, the proposition in our ordinary notation
((p0∧ p1)→ p2) would become
→ ∧p0p1p2.
Interestingly, in Polish notation parenthese are eliminated. See [8, 9].
Now we are ready to convert those colloquial statements to those in our formal language.
For example,
“e is irrational and e is transcendental”
can be converted to
(p0∧ p1),
if we use p0 to represent “e is irrational” and p1 to represent “e is transcendental.”
Actually, “propositions” are just one of the synonyms for “logical statements” in propos- tional logic, others being “sentence,” “Boolean expressions” (named after Boole), etc. Similarly,
“propositional logic” is sometimes refered to as “sentential logic” or “Boolean logic.” We shall use “propositions” and “propositional logic” in the sequel.
Definition 2.3: [6] A proposition ϕ is in conjunctive normal form iff it is of the form 1
i
Ci,
where each Ci is a proposition, called a clause, that consists of only (perhaps negated) variables and ‘∨.’
1By the big ‘
’ we mean ‘∧’ applied several times, and there is no ambiguity since ‘∧’ is associative. (See the table of laws for equivalent propositions listed in subsection 2.3.1.)
Note that in our alphabet the variables are indexed on natural numbers. It is clear that our alphabet is a countable set. And since the set of all propositions are defined as strings over the alphabet according to the formation mentioned above, we have the following lemma:
Lemma 2.1: The set of all propositions is countable.
2.3 Semantics
So far, we have only defined the syntactic aspect of propositional logic, i.e. its superficial structure. We shall introduce its semantic aspect or its meaning.
Definition 2.4: [6] A truth assignment T is a mapping X → {0, 1}, where X is a finite subset of the set of all proposition variables {p0, p1, . . .}. (Recall that 1 and 0 are truth values that represents “true” and “false,” respectively.) We say that T is appropriate to ϕ iff the domain X of T contains all the variables appearing in ϕ as its elements.
Definition 2.5: [6] Let T be a truth assignment appropriate to ϕ. We define the notion of satisfaction of T to ϕ (written T |= ϕ) inductively as follows:
(a) T |= true; T |= false;2 (b) T |= pi :iffT (pi) = 1;
(c) T |= ¬ψ :iff T |= ψ;
(d) T |= (ψ ∧ χ) :iff both T |= ψ and T |= χ;
(e) T |= (ψ ∨ χ) :iff T |= ψ or T |= χ (inclusively);
(f) T |= (ψ → χ) :iff if T |= ψ then T |= χ;
(g) T |= (ψ ↔ χ) :iff T |= ψ if and only if T |= χ, where pi, ψ, and χ are all consituents of ϕ.
2Note thattrue and false always serve as logical constants.
For a more concise definition, we refer the reader to [6].
We are ready to define the truth value ofϕ, specifically, under a particular truth assignment T :
Definition 2.6: [6] The truth value of ϕ under T is 1 if T |= ϕ and 0 otherwise.
A truth table is a sysmatic way to exhaustively list the truth values of a proposition ϕ, where the truth assignments that involved are those of which the domain consists of precisely the variables appearing in ϕ.
Example 2.1: The following is the truth table for ((p → q) → (¬p → ¬q)):
p q ¬p ¬q (p → q) (¬p → ¬q) ((p → q) → (¬p → ¬q))
0 0 1 1 1 1 1
0 1 1 0 1 0 0
1 0 0 1 0 1 1
1 1 0 0 1 1 1
Observe in the above example that, we have four rows in the truth table. Generally speaking, for a propostion that involvesn variables, there are 2nrows in its truth table. Since each variable takes the value either 0 or 1, there are 2n possible combinations in total. Furthermore, if we regard a proposition with n variables as a mapping {0, 1}n → {0, 1} or, formally speaking, Boolean function, then there are totally 22n possible mappings from {0, 1}n to{0, 1}. Thus we have:
Lemma 2.2: There are 2n rows in the truth table of a proposition with n variables. There are 22n n-ary Boolean functions.
In the following we list the truth tables for ¬p0, (p0∧ p1) and (p0∨ p1):
p0 ¬p0
0 1
1 0
2. (p0∧ p1)
p0 p1 (p0 ∧ p1)
0 0 0
0 1 0
1 0 0
1 1 1
3. (p0∨ p1)
p0 p1 (p0 ∧ p1)
0 0 0
0 1 1
1 0 1
1 1 1
Example 2.2: The following is the truth table of (p0∨ ¬p0):
p0 ¬p0 (p0∨ ¬p0)
0 1 1
1 0 1
As shown in the above example, we have all 1’s in the last column (which corresponds to the truth values of the proposition (p0∨ ¬p0)). This kind of propositions have a special name
— tautologies.
Definition 2.7: [6] A proposition is a tautology iff it maps all appropriate truth assignments
to 1.
For a tautology ϕ, we write |= ϕ since T |= ϕ for all T appropriate to it (See [6].). A proposition that maps all appropriate truth assignments to 0 is usually called a contradiction.
(A contradiction is equivalent to the negation of a tautology, — actually, any tautology, — see the discussion below.)
2.3.1 Equvalence between Propositions
If we write down the truth tables for both (p0 → p1) and (¬p0∨ p1) (as shown below:
p0 p1 ¬p0 (p0 → p1) (¬p0∨ p1) ((p0 → p1)↔ (¬p0∨ p1))
0 0 1 1 1 1
0 1 1 1 1 1
1 0 0 0 0 1
1 1 0 1 1 1
where they share the same table), we find that they are essentially the same mappings (notice the fourth and fifth columns above). In such a case, we say that these propositions are equiva- lent. (We write ϕ ≡ ψ to denote that ϕ and ψ are equivalent.) More interestingly, if we apply
‘↔’ to two equivalent propositions (as we did in the above table, see the last column), then we find that it only has truth value 1 over all rows of the truth table, i.e. it is a tautology (hence the name “equivalence” of the connective ↔).
Lemma 2.3: Two propositions ϕ and ψ are equivalent iff (ϕ ↔ ψ) is a tautology.
Hence we know that implication ‘→’ can be replaced with ‘¬’ and ‘∨.’ On the other hand, it is easy to verify that equlvalence ‘↔’ itself can be replaced with other connectives. For example, (p0 ↔ p1) is equivalent to
((p0 → p1)∧ (p1 → p0)), which in turn is equivalent to
It is not hard to see that each Boolean function can be desribed by a proposition which involves only ‘¬,’ ‘∧’ and ‘∨,’ with constants true and false replaced by, say, (p0∨ ¬p0) and (p0∧ ¬p0), respectively. In this situation, we say the set of connectives {¬, ∧, ∨} is functionally complete, i.e. it is sufficient to express all Boolean functions. For a more complete treatment of the notion of functionally complete. See [9].
Lemma 2.4: {¬, ∧} and {¬, ∨} are functionally complete.
Proof: ‘∨’ is redundant in the sense that (ϕ ∨ ψ) is equivalent to (¬ϕ ∧ ¬ψ). (cf. De Morgan’s law.) The other is similar.
There are two binary connectives (which we eliminate here) that are both functionally complete by themselves: | (nand) and ↓ (nor), i.e. (ϕ | ψ) and (ϕ ↓ ψ) are equivalent to
¬(ϕ ∧ ψ) and ¬(ϕ ∨ ψ), respectively.
Laws for Equivalent Propositions
The method of truth table to decide whether two propositions are equivalent works well as we have seen earlier. However, with the growing of the number n of variables appearing in them, this method would become inefficient and physically impractical for lack of space since the size (i.e. the total number of rows) of the truth table for a proposition with n variables is in exponential of n (see Lemma 2.2).
If we look deeper into those equivalent propositions, we should find some useful rules. We list some laws for equivalent propositions below: 3
form name
(1) ¬¬ϕ ≡ ϕ law of double neqation (2) ¬(ϕ ∨ ψ) ≡ (¬ϕ ∧ ¬ψ) De Morgan’s laws
¬(ϕ ∧ ψ) ≡ (¬ϕ ∨ ¬ψ)
(3) (ϕ ∨ ψ) ≡ (ψ ∨ ϕ) commutative laws (ϕ ∧ ψ) ≡ (ψ ∧ ϕ)
3Those listed here are taken from [11]. And the name for item (11) (negation laws) is undetermined.
form name
(4) (ϕ ∨ (ψ ∨ χ)) ≡ ((ϕ ∨ ψ) ∨ χ) associative laws (ϕ ∧ (ψ ∧ χ)) ≡ ((ϕ ∧ ψ) ∧ χ)
(5) (ϕ ∨ (ψ ∧ χ)) ≡ ((ϕ ∨ ψ) ∧ (ϕ ∨ χ)) distributive laws (ϕ ∧ (ψ ∨ χ)) ≡ ((ϕ ∧ ψ) ∨ (ϕ ∧ χ))
(6) (ϕ ∨ ϕ) ≡ ϕ idempotent laws
(ϕ ∧ ϕ) ≡ ϕ
(7) (ϕ ∨ false) ≡ ϕ identity laws
(ϕ ∧ true) ≡ ϕ
(8) (ϕ ∨ ¬ϕ) ≡ true inverse laws
(ϕ ∧ ¬ϕ) ≡ false
(9) (ϕ ∨ true) ≡ true domination laws
(ϕ ∧ false) ≡ false
(10) (ϕ ∨ (ϕ ∧ ψ)) ≡ ϕ absorption laws (ϕ ∧ (ϕ ∨ ψ)) ≡ ϕ
(11) ¬true ≡ false negation laws
¬false ≡ true
(continued)
By the associative laws, we shall often write (ϕ∧ψ∧χ) and (ϕ∨ψ∨χ) instead of ((ϕ∧ψ)∧χ) and ((ϕ ∨ ψ) ∨ χ), as no ambiguities should arise.
Example 2.3: The inference rule modus ponens 4 is a tautology:
((ϕ ∧ (ϕ → ψ)) → ψ)
≡ (¬(ϕ ∧ (¬ϕ ∨ ψ)) ∨ ψ)
≡ (¬((ϕ ∧ ¬ϕ) ∨ (ϕ ∧ ψ)) ∨ ψ) (distributive law)
≡ (¬(false ∨ (ϕ ∧ ψ)) ∨ ψ) (inverse law)
≡ (¬(ϕ ∧ ψ) ∨ ψ) (identity law)
≡ ((¬ϕ ∨ ¬ψ) ∨ ψ) (DeMorgan’s law)
≡ (¬ϕ ∨ (¬ψ ∨ ψ)) (associative law)
≡ (¬ϕ ∨ (ψ ∨ ¬ψ)) (commutative law)
≡ (¬ϕ ∨ true) (inverse law)
≡ (¬ϕ ∨ ¬false) (negation law)
≡ ¬(ϕ ∧ false) (DeMorgan’s law)
≡ ¬false (domination law)
≡ true (negation law)
On the other hand, every proposition can be transformed into an equivalent proposition in conjunctive normal form (Definition 2.3). See [6, 10].
2.4 Deduction Systems
As mentioned in the beginning, we recognize logic as a tool for analyzing thoughts and realizing truths. But what is truth? Philosophers, and even mathematicians, have sought the answer for centuries. For a satisfactory answer, at least in propositional logic, the concept of truth coincides with that of tautology. If we take a deeper look at tautologies, we conceive that their truth values are 1 (true), independent of any particular truth assignments. Hence it suits perfectly with our feelings about truth — always true.
More precisely, in the process of discovering truth or deduction, we usually assume that certain conditions (possibly none), called premises, hold. Then we successively get the result or conclusion that follows from such assumptions by those justified inference rules. Symbolically, it states
(ϕ0 ∧ . . . ∧ ϕn−1)⇒ ϕ,
where those ϕi, 0≤ i ≤ n − 1, are premises, and ϕ is the conclusion. The conjuction 5 of those
5From the associative laws there is no ambiguity to write propositions in conjuntion without parentheses.
premises is called hypothesis. We use ‘⇒’ to denote that ϕ is deduced from ϕi’s.
For a set Δ of propositions, we write Δ |= ϕ to denote that ϕ is a conclusion given the propositions in Δ as premises and we say that ϕ is a consequence of Δ.
Actually, given ϕi’s and ϕ, there is a simple method to decide whether the argument, i.e.
the equation shown above, is correct (in which case we say the argument is valid). What we need to do is to show that the implication
((ϕ0∧ . . . ∧ ϕn−1)→ ϕ)
is a tautology. This method is justified by Tarski’s deduction theorem. Intuitively, it is not hard to see the correctness of this method: Since we assume those premises to hold, if the conclusion holds as well, then the truth value of the implication evaluates to 1; if otherwise some premise fails to hold, then the truth value of the implication also evaluates to 1, no matter whether the conclusion holds or not. This reminds us of tautology in some way.
It is not hard to decide whether a given proposition is a tautology, as we have seen: the truth table method, which suffices to decide all tautologies. Thus in the viewpoint of computer science, concerning the language tautology that consists of all tautologies in propositional logic, we have
Lemma 2.5: tautology is decidable.
However, the drawback of the method of truth table is apparent: it is a tedious work and is inefficient and impractical for large number of variables appearing in the proposition. (See Lemma 2.2.)
Fortunately, we are equipped with useful rules discussed earlier (the laws for equivalent propositions), which reduce a great deal of effort of constructing the truth table most of the time, since they can be used to transform a complicated proposition into a simplified equivalent one.
A subtlety is in order: Let an implicationχ be equivalent to a proposition ψ. If we added ψ as an additional premise, then the new implication χ would be a tautology, i.e. the argument would be valid. The reason is clear: Whether χ is valid depends on whether or not the truth value ofψ is 1, if we assume that to be 1 as our additional premise, then the augument is valid.
Lemma 2.6: Let ((ϕ0 ∧ . . . ∧ ϕn−1)→ ϕ) be an implication equivalent to some proposition ψ. Then ((ϕ0∧ . . . ∧ ϕn−1∧ ψ) → ϕ) is a tautology.
Proof:
(((ϕ0∧ . . . ∧ ϕn−1)→ ϕ) ∨ ¬ψ)
≡ ((¬ϕ0∨ . . . ∨ ¬ϕn−1∨ ϕ) ∨ ¬ψ) (DeMorgan’s law applied several times)
≡ ((¬ϕ0∨ . . . ∨ ¬ϕn−1∨ ¬ψ) ∨ ϕ) (associative law and commutative law)
≡ (¬(ϕ0∧ . . . ∧ ϕn−1∧ ψ) ∨ ϕ) (DeMorgan’s law applied several times)
≡ ((ϕ0∧ . . . ∧ ϕn−1∧ ψ) → ϕ).
On the other hand, there is an alternative method which provides ‘formal’ proofs that are reminiscent of mathematical proofs for valid arguments: deduction system. There are four common deduction systems: axiom system, sequent calculus, natural deduction and analytic tableau. The method of deduction system is highly syntactic and more machine-oriented, and is suitable for valid arguments only, i.e. it cannot determine those invalid arguments. We shall briefy introduce axiom system, which is purely syntactic.
First of all, the term “axiom” should not be strange to us: it is fundamental to the study of mathematics and even physics. Take Euclidean geometry for an example, one of its axioms states “given an (infinitely long) line on a plane, and a point on the same plane but not on this line, there is exactly one line on the same plane that passes through the given point and is parallel to the given line.” Another example arises from physics: That “the speed of light in absolute vacuum is a constant, independent of any frame of inertia” is an axiom in Einstein’s relativity theory.
Definition 2.8: [11] A proof for an argument
(ϕ0∧ . . . ∧ ϕn−1)⇒ ϕ is a sequence ψ0, . . . , ψm, ψ where
ψ := ((ϕ0∧ . . . ∧ ϕn−1)→ ϕ),
and each ψi, 0≤ i ≤ m is an axiom of the system or a proposition generated according to the inference rules of the system.
(Note that these axioms are just like premises of another argument where the conclusion is the original argument.)
If there is a proof for a proposition ϕ, then we say ϕ is a theorem and is derivable and we write ϕ.
Given a set Δ of propositions, if a proposition ϕ is derivable regarding those in Δ as additional axioms, then we say ϕ is a Δ-theorem and is derivable from Δ and we write Δ ϕ.
The notion Δ ϕ is the syntactic counterpart of Δ |= ϕ.
Definition 2.9: [6] A set Δ is consistent iff Δ false.
The following two theorems together state that the notion of consequence and that of derivability coincides in propositional logic:
Theorem 2.1: [soundness theorem], [10] If Δ ϕ, then Δ |= ϕ. Theorem 2.2: [completeness theorem], [10] If Δ|= ϕ, then Δ ϕ.
For more on axiom systems, see [12]. For more on soundness and completeness theorems, see [10].
Chapter 3
Topics on Predicate Logic
All is well so far. Propositional logic possesses many good properties as we have seen in previous chapter. But let us examine the implication below, Aristotle’s well-known syllogism:
1. (Premise) All humans are mortal.
2. (Premise) Socrates is a human.
3. (Conclusion) Socrates is mortal.
This implication is evidently correct, since the conclusion is just an instantiation of the first premise by the second premise. If we symbolize this implication as shown below, however, we will be surprised that it is not a tautology, which stands for truth in propositional logic:
((p0∧ p1)→ p2), where
(a) p0: “All humans are mortal,”
(b) p1: “Socrates is a human,”
(c) p2: “Socrates is mortal.”
We see from this example that there is a flaw in propositional logic: There is no way to express single objects (e.g. ‘Socrates’ in our previous implication), along with their attibutes
such as states and relations. Thus, we must enlarge our language with some additional elements to encompass such statements — hence predicate logic. In the next section, we shall introduce the simplest part, first-order logic.
3.1 First-order Logic
First-order logic is more complicated than propositional logic. Informally, First-order logical statements (so-called formulae) are similar to propositions: They can be decided to whether hold or not (just like propositions can be decided to be whether true or false) and can be connected by logical connectives just like propositions. But additionally, they can be preceded by the so-called quantifiers (‘∀’ and ‘∃,’ hence we sometimes refer to predicate logic as quan- tificational logic) and, more importantly, the basic parts of them, i.e. the atomic formulae (analogous to propositional variables), consist of statements about single objects — a com- bination of predicate symbol and terms, — which in contrast are the key improvements on propositional logic. (Recall that propositional variables cannot be further divided into smaller parts.)
3.1.1 Syntax
Definition 3.1: [6, 8] The alphabet of the language of first-order logic is the set that consists
of
(a) first-order variables: v0, v1, . . . ;
(b) (i) a (possibly empty) set K of constant symbols: c0, c1, . . . ;
(ii) a (possibly empty) set Φn of n-ary function symbols for each n ∈ Z+; (iii) a (possibly empty) set Πn of n-ary relation symbols for each n ∈ Z+; (c) quantifiers: ∀, ∃;
(d) logical connectives: ∧, ∨, ¬, →, ↔;
We shall denote Φ :=
n∈Z+Φn and Π :=
n∈Z+Πn. Note that Π= ∅ as the equality symbol
‘=’ (a binary relation symbol) is a member of Π. Relation symbols are often called predicate symbols, or predicate for short. And some regard constants as nullary functions. Also, the language of first-order logic as well as of others in predicate logic, may or may not contain the binary predicate ‘=,’ depending on the topics we are speaking about. (Predicate logic without
‘=’ is sometimes called specialized predicate logic, whereas that with it is sometimes callled generalized logic. For more topics on this, see [9, 10].) We shall include it in our language.
Definition 3.2: [8]
(a) Each variable (v0, v1, . . . , or x, y, . . . ) is a term;
(b) Each constant symbol is a term;
(c) If t0, . . . ,tn−1 are terms and f is an n-ary function symbol, then so is ft0. . . tn−1. We shall often write f(t0, . . . , tn−1) for ft0. . . tn−1.
Definition 3.3: [8]
(a) If t0, . . . ,tn−1 are terms and R is an n-ary relation symbol, then Rt0. . . tn−1 is an (atomic) formula;
(b) If ϕ is a formula, then so is ¬ϕ;
(c) If ϕ and ψ are formulae, then so are (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ) and (ϕ ↔ ψ);
(d) If ϕ is a formula and x is a variable, then ∀xϕ and ∃xϕ are also formulae.
In the following, we list the name of each quantifier and the way to pronounce them: [10]
symbol name pronunciation
∀ universal quantifier for all, for any, . . .
∃ existential quantifier there exists . . . such that, there is . . . such that, . . .
We shall often writeR(t0, . . . , tn−1) forRt0. . . tn−1. In particular, for binary predicate, we often write t0Rt1 (infix form) instead of Rt0t1 (prefix form). Note that these alternative forms of terms and formulae are just for ease of reading, by definition they are not terms and formulae, respectively.
The polish notation applies to first-order logic (actually, predicate logic) as well, just re- gard each atomic formula or quantified formula (those that are preceded by quantiers) as a propositional variable.
Now we are ready to convert those colloquial statements to ones in our formal language.
For example,
“For every pair x, y, if x < y then f(x) < f(y).”
can be converted to
∀x∀y(x < y → f(x) < f(y)).
We say an occurrence of a variable x is bound in ϕ iff it is quantified, i.e. there is ‘∀x’ or
‘∃x’ that applies to it; otherwise it is called free. More precisely, in the following formula:
(∀xx = x ∧ x = f(y)),
the first two occurrences of x (in ‘x = x’) are bound (we do not recognize the x in ‘∀x’ as an occurrence of x as it is part of the package ‘∀x’), whereas the third occurrence of x (in
‘x = f(y)’) is free. Note that quantifiers only apply to the formula that immediately follows.
Likewise, they in the above formula is also free. A variable is bound if it has no free occurrences, otherwise it is free. A formula without free variable is called a sentence. Sincex and y are free in the above formula, i.e. they have free occurrences, this formula is not a sentence.
Definition 3.4: [6] A formula ϕ is in prenex normal form iff it is of the form Q0. . . Qn−1ψ,
where Qi’s are packages of the form ‘∀x’ or ‘∃x’ and ψ is a quantifier-free formula, called the ϕ.
It is clear that our new alphabet is also countable, though we add some elements to it.
Since the set of all formulae are defined as strings over the alphabet according to the formation mentioned above, we have the following lemma, analogous to Lemma 2.1:
Lemma 3.1: The set of all formulae is countable.
3.1.2 Semantics
Until now, terms and formulae are merely strings (of special kinds) over the alphabet. We shall introduce their meanings. The semantic aspect of predicate logic is somewhat complicated.
First, we are given a nonempty set D, called domain (or universe), of which we map each variable x in our alphabet to some element. It is similar to {0, 1} given in propositional logic.
Furthermore, we map each constant, function symbol and relation symbol to actual element, function and relation, respectively, over the domain D, except that ‘=’ is always mapped to {(e, e)|e ∈ D}. We shall denote the mapping from variables to elements in D (called an assignment) as β, and denote the mapping from constants, function symbols and relation symbols to those actual objects over D (called a structure) as A. We shall often write fA (or fD), cA (or cD), and RA (or RD) instead of A(f), A(c) and A(R), respectively. We have the following definition:
Definition 3.5: [8] An interpretation I for a given domain D is a pair (A, β) that consists of a structure A and an assignment β.
Intuitively, an interpretation in predicate logic is the counterpart of a truth assignment in propositional logic. For the meanings of terms, given an interpretationI, we have the following definition:
Definition 3.6: [the meaning of a term], [6]
(a) For a variable x, I(x) := β(x);
(b) For a constant c, I(c) := cA;
(c) For an n-ary function symbol f applied to n terms t0, . . . , tn−1, I(ft0. . . tn−1) :=fA(I(t0), . . . , I(tn−1)).
Hence the meanings of terms and atomic formulae (for Rt0. . . tn−1, its meaning is thus RA(I(t0), . . . , I(tn−1)), given I) are well-defined. Just as in propositional logic, we shall define the notion of satisfaction of I to a formula ϕ below:
Definition 3.7: [8]
(a) For atomic formula Rt0. . . tn−1,I |= Rt0. . . tn−1 :iff RA(I(t0), . . . , I(tn−1));
(Note that we stipulate that “=A:={(e, e)|e ∈ D},” so “I |= t0 =t1 :iff I(t0) = I(t1).”) (b) I |= ¬ϕ :iff I |= ϕ;
(c) I |= (ϕ ∧ ψ) :iff both I |= ϕ and I |= ψ;
(d) I |= (ϕ ∨ ψ) :iff I |= ϕ or I |= ψ (inclusively);
(e) I |= (ϕ → ψ) :iff if I |= ϕ then I |= ψ;
(f) I |= (ϕ ↔ ψ) :iff I |= ϕ if and only if I |= ψ.
(g) I |= ∀xϕ :iff for all e ∈ D, Ix→e |= ϕ; 1
(h) I |= ∃xϕ :iff there exists e ∈ D such that Ix→e |= ϕ.
An interpretation I is said to be a model of a formula ϕ iff I |= ϕ. Moreover, for a set Δ of formulae, I is a model of Δ (written I |= Δ) iff I |= ϕ for every ϕ ∈ Δ.
If for Δ and ϕ, every interpretation I which is a model of Δ (I |= ϕ) is also a model of ϕ (I |= ϕ), then we write Δ |= ϕ and say that ϕ is a consequence of Δ. Specifically, if ∅ |= ϕ, i.e. ϕ is satisfied by all interpretations, then we write |= ϕ and say ϕ is a valid formulae (a situation analogous to tautologies in propositional logic). If a formula ϕ is unsatisfiable, i.e. it has no models, then it is equivalent to the negation of a valid formula.
Example 3.1: Let K := ∅, Φ := ∅ and Π := {R, =}, where R is binary. Let I0 and I1 be two interpretations such that:
1Ix→e is justI with the variable x mapped to e
I0 I1
domain {0, 1, 2} {1, 2, 3}
x 0 1
y 1 2
z 2 3
R {(0, 1), (0, 2), (1, 2)} {(1, 2), (1, 3), (2, 3), (3, 2), (3, 1), (2, 1)}
(The mappings of other variables are irrelevant to this example.)
Let
ϕ0 :=R(x, y), and
ϕ1 :=∀x∀y(¬x = y → R(x, y)), then we have:
Is I0 a model? Is I1 a model?
ϕ0 Yes Yes
ϕ1 No Yes
Equivalent Formulae
Analogous to propositional logic, we have the following definition:
Definition 3.8: [8] Two formulae ϕ and ψ are equivalent (written: ϕ ≡ ψ) iff {ϕ} |= ψ and {ψ} |= ϕ.
The laws for equivalent formulae are the same to those for equivalent propositions (without, of course, those that involve true or false), regarding a formulae as a proposition. And additionally, [6, 10]
form note
¬∀xϕ ≡ ∃x¬ϕ generalized DeMorgan’s law for ‘∀’
¬∃xϕ ≡ ∀x¬ϕ generalized DeMorgan’s law for ‘∃’
∀x(ϕ ∧ ψ) ≡ (∀xϕ ∧ ∀xψ) -
∀x(ϕ ∧ ψ) ≡ (∀xϕ ∧ ψ) x does not appear free in ψ
∀x(ϕ ∨ ψ) ≡ (∀xϕ ∨ ψ) x does not appear free in ψ
∀xϕ ≡ ∀yϕ[x ← y] y does not appear in ϕ
(ϕ[x ← y] is ϕ with those free occurrences of x replaced by occurrences of y) We see that ‘∀’
and ‘∃’ are similar to ‘∧’ and ‘∨,’ respectively.
On the other hand, every formula can be transformed into an equivalent formula in prenex normal form (cf. Definition 3.4). See [6, 10].
3.1.3 Deduction Systems
As mentioned in section 2.4, there are four common methods to deduce conclusions given some premises. Note that the method of truth table does not work here, since there are infinitely many possible interpretations. (Recall that in propositional logic, there are only finitely many truth assignments that matter.)
The following definitions are all analogous to those in propositional logic:
Definition 3.9: A proof for an argument2
(ϕ0∧ . . . ∧ ϕn−1)⇒ ϕ
is a sequence ψ0, . . . , ψm, ψ where
ψ := ((ϕ0∧ . . . ∧ ϕn−1)→ ϕ),
and each ψi, 0 ≤ i ≤ m is an axiom of the system or a formula generated according to the inference rules of the system.
2The argument for first-order logic is defined similarly.
(Note that these axioms are just like premises of another argument where the conclusion is the original argument.)
If there is a proof for a formulaϕ, then we say ϕ is a first-order theorem and ϕ is derivable, and we also write ϕ.
Given a set Δ of formulae, if a formula ϕ is derivable regarding those in Δ as additional axioms, then we say ϕ is a Δ-first-order theorem and ϕ is derivable from Δ, and we also write Δ ϕ. Note that a theorem ϕ is also a Δ-first-order theorem by definition. The set Θ of all Δ-first-order theoremsϕ (which are sentences) is called a theory, given Δ. The notation Δ ϕ is the syntactic counterpart of Δ|= ϕ.
There is an interesting application to the research of artificial intelligence: the knowledge base plays the role of Δ, while ϕ denotes the representation of some knowledge. The process for the knowledge base to deduce ϕ (reasoning) is indeed the same as that for Δ ϕ. For more on this issue, see [20].
Definition 3.10: [8] A set Δ is consistent iff there is no contradiction ϕ such that Δ ϕ.
The axiom system given in [6] is shown below:
item form
AX0 Any formula whose propositional form is a tautology.
AX1 Any formula of the following forms:
AX1a t = t, where t is a term.
AX1b ((t0 =t0∧ . . . ∧ tn−1=tn−1)→ ft0. . . tn−1=ft0. . . tn−1), whereti’s are terms and f is an n-ary function symbol.
AX1c ((t0 =t0∧ . . . ∧ tn−1=tn−1)→ (Rt0. . . tn−1 → ft0. . . tn−1)), whereti’s are terms and R is an n-ary relation symbol.
AX2 Any formula of the form (∀xϕ → ϕ[x ← t]).
AX3 Any formula of the form (ϕ → ∀xϕ), with x not free in ϕ.
AX4 Any formula of the form (∀x(ϕ → ψ) → (∀xϕ → ∀xψ)).
(ϕ[x ← t] is ϕ with those free occurrences of x replaced by occurrences of the term t). The formulae shown above are basic axioms. The axiom system contains besides these all those formulae that are preceded by any number of prefixes of the form ‘∀x.’ It is not hard to see that the axioms are valid formulae. The only one inference rule is modus ponens. (See Example 2.3.) Schematically, it states:
ϕ (ϕ → ψ)
ψ .
Here we give an example illustrating the proof under axiom systems:
Example 3.2: The formal proof of the theorem ∃y(x = y) is:
ψ0 :=x = x
(an axiom from group AX1a), ψ1 := (∀y¬x = y → ¬x = x)
(an axiom from group AX2),
ψ2 := ((∀y¬x = y → ¬x = x) → (x = x → ∃yx = y)) (an axiom from group AX0),
ψ3 := (x = x → ∃yx = y)
(from ψ1 and ψ2 by modus ponens), ψ4 :=∃yx = y
(from ψ0 and ψ3 by modus ponens).
In proving a theorem, we often divide it into two or more parts. The correctness of this technique can be justified by the following lemma. (Note that we prove it in the level of metalanguage.)
Lemma 3.2: Let ϕ and ψ be two formulae. Then
( ϕ and ψ) if and only if (ϕ ∧ ψ).
Proof: Suppose that ϕ and ψ, i.e. there are proofs Sϕ andSψ for them. Notice thatϕ and ψ are the last elements of Sϕ and Sψ, respectively. Then Sϕ, Sψ, (ψ → (ϕ → (ϕ ∧ ψ))), (ϕ →
Conversely, suppose that there is a proofS(ϕ∧ψ) for (ϕ∧ψ). Then S(ϕ∧ψ), ((ϕ∧ψ) → ϕ), ϕ and S(ϕ∧ψ), ((ϕ ∧ ψ) → ψ), ψ are proofs for ϕ and ψ, respectively. Hence ϕ and ψ.
Analogous to propositional logic, the following two theorems together state that the notion of consequence and that of derivability coincides in first-order logic:
Theorem 3.1: [soundness theorem], [6] If Δ ϕ, then Δ |= ϕ.
Theorem 3.2: [G¨odel’s completeness theorem], [6] If Δ|= ϕ, then Δ ϕ.
The following theorem, which is a consequence of G¨odel’s completeness theorem, is critical to our main result (Theorem 4.3):
Theorem 3.3: [L¨owenheim-Skolem theorem], [6] If a sentence ϕ has finite models of arbitrary large cardinality (i.e. the size of the domain), then it has an infinite model.
For more complete treatment about this, see [6, 8, 10].
For more on the axiom system, see [6]. [8, 10] are excellent references for other deduction systems. [6, 8, 10] all discuss the theorems above. (However, the proofs of Theorem 3.2 in all of them adopt the one by [13]. For G¨odel’s own proof, see [14].)
3.1.4 Weakness of First-Order Logic
Note that first-order variables are only mapped to the simplest or the individual objects (hence the name first-order) in a structure, whereas the concepts such as functions and relations are objects in second-order. Because of this, there are many (computational) problems that cannot be expressed in first-order logic (our result in the next chapter, for instance). It is the need to represent these complex objects that provokes second-order logic.
3.2 Second-Order Logic
In fact, second-order logic is very much similar to first-order logic, except for addtional variables
— so-called the second-order variables, — which map to relations over the domain.
A formula in second-order is the same as in first-order, except that it can be formed using second-order variable P as ordinary relation symbol in the alphabet (e.g. P t0. . . tn−1, where P is an n-ary second-order variable) and that second-order variables can be quantified in it (e.g. ∀P (t0 = tn−1 → ¬P t0. . . tn−1) or ∃XXt0t1). In this aspect, the relation symbols in the alphabet can be regarded as second-order constants.
A specialized part of second-order logic — existential second-order logic — concerns only those formulae of the form
∃P ϕ,
where P is a second-order variable, and ϕ is a first-order formula regarding P as given in the alphabet. We shall focus our effort to this in the next chapter.
3.3 Remarks
In the view point of algebra, propositional logic is characterized by Boolean algebras, whereas predicate logic is characterized by cylindric algebras. [16]
G¨odel’s incompleteness theorem [15] states that there is some statement about elementary arithmetic that is neither provable nor refutable provided that our axiom system is consistent, which manifests the limit of our formal method. This is a devastating result to Hilbert’s program, of which the ultimate goal is to totally axiomatize mathematics. [6, 8, 10] are all good references for this topic.
Chapter 4
Graph-Theoretic Problems as Expressed in Logical Formulae
4.1 Prolog
Graphs are a widely-used data structure in computer science, and they have many applications.
The first use of graphs dates back to 1736, when the Swiss mathematician Euler used them to solve the problem of seven bridges of K¨onigsberg, thereby built the foundations of graph theory.
Definition 4.1: [17] A directed graph G is a pair (V, E), where V is a finite set and E is a binary relation defined over V . V is called the set of vertices of G (its elements are called vertices) and E is called the set of edges of G (its elements are called edges).
Note that there is another kind of graphs called undirected graphs, in which E contains subsets of cardinality exactly 2 of V as its elements. However, we shall focus on directed graphs. In the sequel we use graph for short.
A subgraph G = (V, E) of G = (V, E) is a graph (hence E ⊂ V× V) such that V ⊂ V andE ⊂ E. If (u, v) is an edge of G, then we say that (u, v) is incident from u and it is incident to v and v is adjacent to u. The in-degree of a vertex v is the number of edges incident to v, while its out-degree is the number of edges incident from it.
A path from a vertex u to a vertex v is a sequence v0, . . . , vn of vertices in V such that v0 = u, vn = v, and there is an edge in the graph for each pair of consecutive vertices in the sequence. A path is simple if each vertex in this path appears exactly once. If there is a path from u to v, we say that v is reachable from u. A directed graph is strongly connected if every vertex in the graph is reachable from others.
A cycle is a path such that the first and the last vertices in the path coincide and there is at least one vertex other than the first and the last ones in this path.
For more thorough treatment, see [11, 17, 18].
Hamiltonian Path
A problem “Does a graph contain a Hamiltonian path?” which is named after the Irish math- ematician Hamiltonian is defined below:
Definition 4.2: [17] A Hamiltonian path of a graph G = (V, E) is a simple path in which exactly all vertices inV appear. The decision problem hamiltonian path asks, given a graph G, whether it contains a Hamiltonian path.
hamiltonian path is a well-known NP-complete problem. [6, 17] For more on the prop- erties and examples of Hamiltonian path, see [11].
4.2 The Successor Function in Graph-Theoretic Prob- lems
Let us return back to the perspectives of logic. In general, the alphabet concerning graph- theoretic problems is: KG := ∅, ΦG := ∅ and ΠG := {G, =}, where G is a binary relation symbol which is intuitively interpreted as “edges” in a graph, and = is a binary relation symbol which is “always” interpreted as the equality relation. (See Subsection 3.1.2.)
If we regard the set of verticesV of a graph G = (V, E) with n vertices as the set of numbers {0, 1, . . . , n − 1}, then the problem hamiltonian path can be expressed by the following existential second-order formula, where P is isomorphic to the usual is-less-than relation (‘<’)
over {0, 1, . . . , n − 1}: [6]
∃P ϕ,
where ϕ is the conjuction of the following three formulae:
∀x∀y(P (x, y) ∨ P (y, x) ∨ x = y),
∀x∀y∀z(¬P (x, x) ∧ ((P (x, y) ∧ P (y, z)) → P (x, z))), and
∀x∀y((P (x, y) ∧ ∀z(¬P (x, z) ∨ ¬P (z, y))) → G(x, y)).
Moreover, if we added to ϕ in conjunction the additional formula
∀x∀y(∀z(¬P (x, z) ∧ ¬P (z, y)) → G(x, y)),
then the resulting existential second-order formula would characterize the problem hamilto- nian cycle.
The following two theorems are critical:
Theorem 4.1: [Fagin’s theorem], [6] The class of all graph-theoretic properties expressible in
existential second-order logic is NP.
A formula∃P ϕ is said to be in Horn existential second-order logic iff ϕ is in prenex normal form with only universal first-order quantifiers (i.e. ‘∀’ that only applies to first-order variables), and its matrix is in conjunctive normal form where each clause contains at most one unnegated atomic formula that involves the second-order variable P . Horn existential second-order with successor is that with an additional binary relation symbolS given in our alphabet, i.e. ΠG :=
{G, S, =}, and additionally S is interpreted in advance as the successor function, i.e. a linear ordering over the vertices in a graph. More precisely,S(x, y) states that vertex y is the successor of vertexx, and S is isomorphic to {(0, 1), (1, 2), · · · , (n − 2, n − 1)} for a graph with n vertices.
Theorem 4.2: [6] The class of all graph-theoretic properties expressible in Horn existential second-order logic with successor is precisely P.
The reason of the requirement that S should be given in advance is according to [2], and might be well illustrated by our main result in the following (the proof technique is very much similar to that adopted in Corollary 6 to Theorem 5.7 from [6]):
Theorem 4.3 : Let ∃Sϕ be an existential second-order formula describing that S is the successor function. Then the part ϕ cannot be in first-order logic.
Proof: Suppose, for the sake of contradiction, that there were such a first-order formula ϕ.
Then, it must be a sentence, i.e. one that has no free (first-order) variables. The reason is clear: the subject of this formula is the relation S itself and this description applies to all pairs of vertices in the graph.
Next, consider the following first-order sentence:
ψ := ϕ ∧ ϕ0∧ ϕ1∧ ϕ2,
where
ϕ0 :=∃x∀y¬S(x, y)
states that there is a vertex x that has no successor, i.e. the “last” vertex exists, ϕ1 :=∀x∀y((S(x, y) ∨ ∀z(¬S(x, z) ∧ ¬S(z, y))) → G(x, y))
states that there is an edge from vertex x to vertex y if either y is the successor of x or y is the first vertex (vertex 0) and x is the last vertex (vertex n − 1), and
ϕ2 :=∀x∀y(G(x, y) → (S(x, y) ∨ ∀z(¬S(x, z) ∧ ¬S(z, y))))
states the converse of ϕ1. (ϕ1 and ϕ2 together states that there is an edge from vertex x to vertex y if and only if either y is the successor of x or y is the first vertex and x is the last vertex.)
ψ states that the graph G is a cycle itself, and ψ has arbitrarily large finite models. In other words, there are finite cycles that have as many vertices as desired. According to L¨owenheim- Skolem (cf. Theorem 3.3), the sentence ψ has an infinite model, call it G∞.
If we start from vertex 0 and follow the edge out of it, we reach vertex 1; and then follow the edge out of it we reach vertex 2; . . . , in this way, we will eventually meet all vertices reachable from vertex 0.
But since the graph is strongly connected, those vertices previously described include all vertices in the graph. At the same time, the graph is a cycle, so there must be a vertex,
