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,
asserted “infinite” cycle is indeed finite.
Thus the formula expressing the successor function is
∃S∃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))) ↔ S(x, y)).
Note that it is similar to the formula that expresses hamiltonian path.
On the other hand, hamiltonian path can in turn be expressed in existential second-order logic with successor:
∃π(ϕ0∧ ϕ1∧ ϕ2∧ ψ), where
ϕ0 :=∀x∃xπ(x, x),
ϕ1 :=∀x∀x∀x((π(x, x)∧ π(x, x))→ x =x), (ϕ0 and ϕ1 together state that π is a function.)
ϕ2 :=∀x∃xπ(x, x),
(Additionally, ϕ2 states that the function π defined by ϕ0 and ϕ1 is surjective. Hence these three formulae together state that π is a permutation, since a surjective function defined over a finite set is a permutation over it.) and
ψ := ∀x∀x∀y∀y((π(x, x)∧ π(y, y)∧ S(x, y))→ G(x, y)).
At this point, ψ says that after the renumbering of all vertices according to the permutation π defined by ϕ0, ϕ1 and ϕ2, there is an edge between every pair of vertices with consecutive numbers, hence a Hamiltonian path exists.
Alternatively,ϕ2 can be replaced by
ϕ2 :=∀x∀x∀y∀y((π(x, x)∧ π(y, y)∧ x =y)→ x = y),
which states that the function π defined by ϕ0 and ϕ1 is injective. Again, all these three formulae together says that π is a permutation, since an injective function defined over a finite set is a permutation over it. Furthermore, if we added to ψ in conjunction the additional formula
ψ :=∀x∀x∀y∀y(∀z(π(x, x)∧ π(y, y)∧ ¬S(x, z) ∧ ¬S(z, y))→ G(x, y)),
then the resulting existential second-order formula would express hamiltonian cycle.
Finally, for an NP-complete problem such as hamiltonian path, it is least likely that it can be expressed in Horn existential second-order logic with successor, unless P = NP.
Chapter 5
Concluding Remarks
Logic is fundamental to mathematics in the sense that it governs the formulation of mathe-matical statements and its deductions. In this thesis we restrict ourselves to the classical part of logic, which underlies mathemtics. There are some interesting properties about nonclassical logic. For example, intuitionistic logic, which was developed by A. Heyting, L. Kronecker and L. E. J. Brouwer and which abandons the use of the law of excluded-middle, is even closer to our algorithmic approach, since for a proof it gives an algorithm to produce the required conclusion. Others find its applications to many fields.
With the fact that halting problem is undecidable, it can be shown that first-order logic is also undecidable, i.e. whether or not a given formula follows from axioms is undecidable. This in turn can be used to show that number theory cannot be axiomitized by a recursively enumerable set of axioms. [6] Therefore it is impossible to devise a machine that, given some premises, automatically proves or refutes each statement. On the other hand, Hilbert’s program, of which the ambitious goal is to completely axiomatize number theory and even the whole mathematics, was defeated by G¨odel’s imcompleteness theorem.
Moreover, the famous continuum hypothesis, proposed by G. Cantor, which assumes that the cardinality of R is |2N|, was proved independent of our axioms for set theory by K. G¨odel and P. Cohen. The “second” G¨odel’s incompleteness theorem (the one provided in the text is the “first” G¨odel’s incompleteness theorem) states that the consistency of set theory itself, provided that set theory is consistent, is not provable within (axiomatic) set theory itself. With this result, that the assertion “Mathematics is consistent, i.e. there is no contradiction that can
be derived within it” is also not provable, since the whole mathematics can be built upon the notion of set. This brings us to review the rudiments of the formal method, which has evolved since the time of Aristotle and Euclid.
On the other hand, besides logic there are many other characterizations of computational problems. The efforts to the problem P = NP keep on, and the investigations of logic as well.? (For more discussions on the logical characterization about this problem, see [19].)
Bibliography
[1] R. Fagin “Generalized first-order spectra and polynomial-time recognizable sets,” pp. 43–
73 in Complexity of Computation, edited by R. M. Karp SIAM-AMS Proceedings, vol. 7, 1974.
[2] P. Kolatis and M. Vardi “0 – 1 laws and decision problems for fragments of second-order logic,” Proc. 3rd IEEE Symp. on Logic In Comp. Sci, pp. 2–11, 1988.
[3] N. Immerman “Relational queries computable in polynomial time,” Information and Con-trol, 68, pp. 86–104, 1986.
[4] M. Y. Vardi “The complexity of relational query languages,” Proceedings of the 14th ACM Symp. on the Theory of Computing, pp. 137–146, 1982.
[5] C. H. Papadimitriou “A note on the expressive power of PROLOG,” Bull. of the EATCS, 26, pp. 21–23, 1985.
[6] C. H. Papadimitriou Computational complexity, second edition, Addison-Wesley Long-man.
[7] E. Gr¨adel “The expressive power of second-order Horn logic,” Proc. 8th Symp. on Theor.
Aspects of Comp. Sci., vol. 480 of Lecture Notes in Computer Science, pp. 466–477, 1991.
[8] H.-D. Ebbinghaus, J. Flum, and W. Thomas Mathematical logic, second edition, Springer.
[9] H. B. Enderton A Mathematical Introduction to Logic, Academic Press.
[10] D. van Dalen Logic and Structure, fourth edition, Springer.
[11] R. P. Grimaldi Discrete and Combinatorial Mathematics, an Applied Introduction, fifth edition, Pearson Addison-Wesley.
[12] E. Mendelson Introduction to Mathematical Logic, fourth edition, Chapman & Hall/CRC.
[13] L. Henkin “The completeness of first-order functional calculus,” J. Symb. Logic, 14, pp.
159 – 166, 1949.
[14] K. G¨odel “Die Vollst¨andigkeit der Axiome der Logischen Funktionenkalk¨uls” (The com-pleteness of the axioms of the logical function calculus), Monat, Math. Physik, 37, pp. 349 – 360, 1930.
[15] K. G¨odel “ ¨Uber formal unentscheidbare S¨atze der Principia Mathematica und verwandter Systeme” (“On formally undecidable theorems in Principia Mathematica and related sys-tems), Monatschefte f¨ur Mathematik und Physik, 38, pp. 173 – 198, 1931
[16] L. Henkin, J. D. Monk and A. Tarski Cylindric Algebras, North Holland, 1971 – 1985.
[17] T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein Introduction to Algorithms, second edition, MIT Press, Cambridge, Massachusetts, 2001
[18] E. Horowitz, S. Sahni, D. Mehta Fundamentals of Data Structures in C++, Computer Science Press, An imprint of W. H. Freeman and Company, New York, 1995.
[19] S. Hedman A first course in logic : an introduction to model theory, proof theory, com-putability, and complexity, Oxford, New York, Oxford University Press, 2004.
[20] S. Russell, P. Norvig Artificial Intelligence, a Modern Approach, second edition, Prentice Hall Series in Artificial Intelligence, 2003.