nach oben

2012 | Buch

Kapitel lesen Erstes Kapitel lesen

Logic: A Brief Course

verfasst von: Daniele Mundici

Verlag: Springer Milan

Buchreihe : UNITEXT

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This short book, geared towards undergraduate students of computer science and mathematics, is specifically designed for a first course in mathematical logic. A proof of Gödel's completeness theorem and its main consequences is given using Robinson's completeness theorem and Gödel's compactness theorem for propositional logic. The reader will familiarize himself with many basic ideas and artifacts of mathematical logic: a non-ambiguous syntax, logical equivalence and consequence relation, the Davis-Putnam procedure, Tarski semantics, Herbrand models, the axioms of identity, Skolem normal forms, nonstandard models and, interestingly enough, proofs and refutations viewed as graphic objects. The mathematical prerequisites are minimal: the book is accessible to anybody having some familiarity with proofs by induction. Many exercises on the relationship between natural language and formal proofs make the book also interesting to a wide range of students of philosophy and linguistics.

Inhaltsverzeichnis

Frontmatter

Propositional Logic

Frontmatter

Introduction

Abstract

Have a look at the following drawing: The problem C is to colour the vertices 1, ..., 5 with one of two available colours, in such a way that vertices of the same edge have different colours. The answer is simple, but think of the same problem, denoted by C ⁺, to colour a complex graph with 1000 vertices, 10000 edges and a palette of 7 colours. The search for efficient methods of solving a problem like C ⁺, so either finding an explicit solution or proving that no solution exists, forms a central challenge for contemporary mathematics.

Daniele Mundici

2. Fundamental Logical Notions

Abstract

Following the convention of the previous chapter, we use capital letters to denote variables. We need infinitely many variables, but by analogy with the keyboard of our computer we want to maintain our symbol apparatus, called the alphabet, finite. Therefore we represent officially the variables as

$$X,XI,XII,XIII,...$$

Daniele Mundici

3. The Resolution Method

Abstract

Let F be a CNF formula. We will describe a method of transforming F into a formula equivalent to F and richer in clauses. This method then decides whether F is unsatisfiable, and whenever F is satisfiable it finds an assignment that satisfies F.

Daniele Mundici

4. Robinson’s Completeness Theorem

Abstract

As we have seen, after a number of steps t ^* not exceeding the number of variables in S ₀, DPP terminates producing as output a set S _t* of clauses without variables. S _t* can have only one of two possible forms: S _t* = □ or S _t* = ø

Daniele Mundici

5. Fast Classes for DPP

Abstract

In some cases DPP proceeds fast, also with sets K of clauses having thousands of variables, whereas other procedures (e.g., the “truth table method”, in which one tries all assignments) would take geological time to decide whether K is satisfiable and to find an assignment if any.

Daniele Mundici

6. Gödel’s Compactness Theorem

Abstract

So far we have considered only finite sets of clauses. But as we will see in the second part of this course, infinite sets play an important rôle. Therefore we extend the notion of satisfiability as follows: Satisfaction of an infinite set of clauses. Let S be a (finite or infinite) set of clauses. Let V ar (S) denote the set of variables that occur in the clauses of S. Then an assignment α is suitable for S if the domain of α contains V ar (S). We say that α satisfies S, and write

$$\alpha \vDash S,$$

if it satisfies each clause of S; S is unsatisfiable if no assignment satisfies it.

Daniele Mundici

7. Propositional Logic: Syntax

Abstract

We now study a language, known as (Boolean, or classical) propositional logic. While it is more extended than the language of clauses considered so far, as we will see, it is not more expressive. For this language it is still possible to define precisely the concepts of satisfiability, logical equivalence and logical consequence.

Daniele Mundici

8. Propositional Logic: Semantics

Abstract

Having completed the syntactic definitions we now pass on to the semantic definitions.

Daniele Mundici

9. Normal Forms

Abstract

We now list some logical equivalences. Their proofs follow immediately from the definitions of the previous chapter. To facilitate the reading, outer parentheses are omitted throughout:

$$\begin{gathered} F \vee G \equiv G \vee F \hfill \\ \left( {F \vee G} \right) \vee H \equiv F \vee \left( {G \vee H} \right) \hfill \\ F \vee F \equiv F \hfill \\ \neg \neg F \equiv F \hfill \\ F \vee O \equiv F for each unsatisfiable formula O \hfill \\ F \vee \neg O \equiv \neg O for each unsatisfiable formula O \hfill \\ \neg \left( {\neg F \vee G} \right) \vee G \equiv \neg \left( {\neg G \vee F} \right) \vee F. \hfill \\ \end{gathered}$$

Daniele Mundici

10. Recap: Expressivity and Efficiency

Abstract

Recall the example on page 3, in which we transcribed in clauses the problem of checking whether a graph G with n vertices is k-colourable. We used n × k variables with the intention that each variable X _ij abbreviates the phrase “vertex i has colour j”. Each variable X _ij also represents the question “does vertex i have colour j?”, and intends to contain the yes-no answer to this question.

Daniele Mundici

Predicate Logic

Frontmatter

11. The Quantifiers “There Exists” and “For All”

Abstract

The fundamental notions of natural number, zero and successor are sufficiently clear to us. Addition and multiplication are then defined inductively, using zero and successor together with the equality predicate =, as is done on the next page of this course. More complicated arithmetic relations and operations such as x ≤ y, “x divides y”, “x is the minimum of y and z”, “x is a prime number”, are definable using these fundamental notions.

Daniele Mundici

12. Syntax of Predicate Logic

Abstract

Following the same procedure as for propositional logic, we prepare now the necessary material for writing expressions upon which the logical calculus will act. In a first phase we will only work with formulas that are similar to the clauses of propositional logic. Then the calculus will be extended to all formulas.

Daniele Mundici

13. The Meaning of Clauses

Abstract

The discovery of a non-Euclidean geometry ended a two thousand-year-old search for a refutation of the set of statements obtained by adding the negation of the Fifth Postulate (about parallel lines) to the remaining Euclidean axioms. This is an important example of a general fact: if there exists a possible world in which a set of statements is true, then there does not exist a refutation of this set of statements. The reverse implication is a fundamental result of logic, the completeness theorem of Gödel, for the proof of which we cannot content ourselves with a generic intuition. Instead, we have to learn to work with some fundamental concepts that will be defined in this chapter.

Daniele Mundici

14. Gödel’s Completeness Theorem for the Logic of Clauses

Abstract

This fundamental theorem shows the equivalence of two at first sight different properties of a set of clauses S:

satisfiability, or the existence of a model of S;
coherence (= irrefutability = consistency), i.e., the impossibility of obtaining the empty clause when applying DPP to a finite subset of S/H _S.

Daniele Mundici

15. Equality Axioms

Abstract

The possibility of enriching the logical calculus with the equality symbol is not a trifling matter. This symbol is found everywhere in mathematics, and makes sense in every Tarskian model. This is not the case for the other mathematical relations. For example, the relation “is bigger than” makes no sense for lines, the relation “belongs to” makes no sense for natural numbers, etc.

Daniele Mundici

16. The Predicate Logic L

Abstract

In this chapter, a bit more dense than the other ones, we describe a logic, denoted by L, and known as “predicate logic” or “elementary logic”, or also “first-order logic.” The syntax of L is perfectly tailored for the language of mathematics, which usually avoids clauses.

Daniele Mundici

17. Final Remarks

Abstract

We have prepared a formidable symbolic apparatus, with its logical calculus, and we can now launch it in the vast field of mathematics for which it was constructed. For example, if we wish to dedicate ourselves to the study of the problem of twin prime numbers p, p + 2 introduced on page 57, we cannot do anything else than accept the axioms for natural numbers, or for sets, and subsequently get down to calculate the consequences of the axioms — mentally, or with the help of lemmas and theorems previously obtained, or even with the help of a computer that generates for us pairs of twin primes with more than hundred thousand digits, hence suggesting that there are infinitely many of such pairs. The completeness theorem assures us that no consequence of the axioms will escape the logical calculus.

Daniele Mundici

Backmatter

Titel: Logic: A Brief Course
verfasst von: Daniele Mundici
Verlag: Springer Milan
Electronic ISBN: 978-88-470-2361-1
Print ISBN: 978-88-470-2360-4
DOI: https://doi.org/10.1007/978-88-470-2361-1