Main Page

logic4free started (back in 2017) shortly after one of us, Thomas, had found out that some publishers offer online textbooks only in bundles, which means a university needs to buy a licence for an entire collection of textbooks even if they are only interested in a single textbook. In Thomas' case it meant he would have had to pay more than 30000 Euro just to have a textbook on logic in computer science online available for his students. Read more about this wiki ...

Introduction

This is the home page of a course on logic, more specifically, on logic for computer science: you, as the learner, take your first steps in mathematical logic in the realm of computer science. In the end, you may say: "Wow, I didn't know that logic can be so useful in computer science. Now, I know. Now, I know how to use logic in computer science."

In general, logic for computer science is quite similar to mathematics in engineering disciplines. It is a means to model situations and, at the same time, provides tools to analyze the situations modeled. At best, a practical problem is modeled in logic and then solved using logical tools.

This page guides you through the different units of this course. Individual competencies that you are supposed to acquire are spelled out: for every student (to pass the course); for advanced students (to obtain better grades). Some general competencies are recurring: students ...

• define sets and function by induction,
• prove facts by induction,
• prove elementary relations between fundamental notions such as satisfiability and entailment,
• answer simple questions about fundamental notions and facts,
• reproduce and illustrate definitions, and
• reconstruct basic to medium complex proofs.

Top students should, in addition, be capable of solving problems that require abstract thinking and creativity and reconstruct complex proofs.

There are two parts to this course: the first one is about propositional logic; the second part is about first-order logic.

Propositional logic

The first part of this course is on propositional logic, a simple logic, yet extremely useful in computer science.

Syntax and semantics

The first thing to learn is what a propositional formula looks like—you learn the so-called syntax of propositional logic. Note that connectives and inductive definitions and proofs are part of this.

At this point, every student

• gives an inductive definition of the set of all propositional formulas ⬀,
• tells formulas and other objects apart,
• reads and writes formulas in different notation ⬀ ⬀,
• transforms a formula from one notation into another one ⬀ ⬀.

An advanced student

• provides grammars for the set of all propositional formulas in different notation when viewed as strings ⬀ ⬀.

The next thing to learn is what a propositional formula means—you learn the so-called semantics of propositional logic. Note that truth values and boolean functions and, again, connectives and inductive definitions and proofs are part of this.

At this point, every student

• gives an inductive definition of the value of a propositional formula with respect to a variable assignment ⬀,
• evaluates given propositional formulas with respect to given variable assignments (in two different ways) ⬀ ,
• defines functions on the set of all propositional formulas ⬀ ,
• proves simple properties of forumulas by induction ⬀ ,
• comes up with formulas expressing simple boolean functions ⬀.

An advanced student

• defines new connectives (syntax and semantics) ⬀ ⬀,
• comes up with (small) formulas expressing more complicated boolean functions ⬀.

There is an important issue concerning variable assignments that needs to be clarified, once and for all. In many situations, it is good to assume that there is an (countably) infinite supply of variables and define a variable assignment as a function that assigns a truth value to each variable in the infinite supply. But, clearly, the truth value of a formula under an assignment only depends on the variables occurring in the formula. This is known as the coincidence lemma.

Every student

• defines the variables occurring in a formula by induction,
• states the coincidence lemma formally,
• determines whether a partial assignment is fitting or tightly fitting,
• evaluates formulas under partial assignments ⬀ ⬀.

An advanced student

• gives a proof of the coincidence lemma. ⬀

Modeling

Now that we know how propositional formulas look like and what they mean, we can use them in practice, for modeling. In general, modeling means that we represent objects we are interested in by variable assignments and describe properties of such objects by formulas. Good examples are colorability and sudoku. A more complex example are computations.

At this point, every student

• models simple situtations (problems) in propositional logic ⬀, in particular,
• finds variables, designs formulas, and explains representations of objects by 1-assignments. ⬀

An advanced student

• models more complicated situations.

What remains to be answered is the question how we can find 1-assignments. This is the most important question from a practical point of view, since finding 1-assignments corresponds to finding solutions to the problems modeled, for instance, filling in sudoku instances or checking for colorability and finding colorings.

This topic is postponed.

Equivalence

Algorithms for finding 1-assignments often require the input to be in a certain form, more precisely, the respective software does not accept any propositional formula, but only ones of a particular shape. So it is important to know how arbitrary formulas can be converted accordingly.

As a starting point, it is good to know what it means that one formula is as good as another one. This is captured by the notion of equivalence.

At this point, every student

• determines the equivalence of formulas by drawing on the definition ⬀,
• proves basic properties of equivalence. ⬀

Deriving equivalences

The (algorithmic) question whether two given formulas are equivalent is an obvious one. A partial answer is given by a list of fundamental and known equivalences. These can be used to establish equivalences between propositional formulas. To this end it is crucial to know how formulas can be substituted for variables. In other words, a formal notion of substitution is needed.

At this point, every student

• lists the laws of propositional logic,
• applies substitutions and finds suitable ones, Todo: Aufgabe.
• gives a formal statement of the congruence lemma (simple and generalized variant),
• derives the equivalence between propositional formulas using the congruence lemma and the laws of propositional logic. ⬀⬀

An advanced student

• proves complicated equivalences involving connectives with multiple arities, Todo: Aufgabe.
• derives fundamental laws from the base axioms. Todo: Aufgabe.

Normal forms

The syntax of propositional formulas allows many different connectives and does not restrict where these connectives occur in a formula. It is, however, sometimes useful when formulas have a certain form or shape. One generally speaks of normal forms.—In fact, as pointed out above some algorithms for finding 1-assignments require their input to be in certain normal forms.

There are three normal forms we take a look at:

• boolean normal form,
• negation normal form,
• conjunctive normal form.

The last one can also be written in a special notation, called clausal notation.

At this point, every student

• gives definitions of the three normal forms,
• explains algorithms converting arbitrary propositional formulas into equivalent formulas in the different normal forms ⬀,
• explains upper bounds on the complexity of these conversions ⬀,
• knows the exponential lower bound for the conversion of BNF into CNF,
• converts formulas in CNF into clausal notation and vice versa. ⬀

A better student

• explains lower bounds for the conversion algorithms.
• knows formulas that establish the exponential lower bound for the conversion of BNF into CNF.

SAT Solving

One thing is to model situations in propositional logic, another thing is to exploit such models. More concretely, it is important to have algorithms at hand that take a propositional formula as input and produce 1-assignments of this formula as ouputs if there are any. Such algorithms are called SAT solvers.—We distinguish between SAT solvers and SAT tests; the latter simply check whether there is a 1-assignment for a given formula.

There are four more or less simple SAT solvers:

• the naive SAT solver,
• the backtracking SAT solver,
• the DP algorithm (not covered in the course), and
• the DPLL algorithm.

The last two algorithms only work with formulas in CNF and really exploit the fact that their input is in CNF; the first two are quite generic. Assuming the input to be in CNF seems like a severe restriction, but in many cases modeling in CNF is not much more complicated than in full propositional logic.

SAT tests are related to SAT solvers: every SAT solver is, in some sense, a SAT test; conversely, every SAT test can be turned into a SAT solver with only a polynomial overhead (self-reducing SAT solver).

At this point, every student

• explains how the naive SAT solver, the backtracking SAT solver, and the self-reducing SAT solver work,
• phrases, proves, and explains the self-reducibility lemma,
• explains how the DPLL algorithm works,
• explains how the individual steps of the DPLL algorithm correspond to the statements of the corresponding lemma (which amounts to a correctness argument),
• applies the DPLL algorithm to small instances ⬀ ⬀

An advanced student

• explains why there would be a polynomial-time SAT solver if there was a polynomial-time SAT test.

Entailment

Given a set of formulas, one may want to know what its conclusions are, that is, which formulas follow from the given set and which do not. This is captured by the entailment relation.

There is a simple, but fundamental connection between entailment and satisfiability.

At this point, every student

• gives a definition of entailment,
• checks whether or not a formula is entailed by a set of formulas, drawing on the definition, ⬀
• gives a proof of the lemma about satisfiability and entailment,
• mutually reduces instances of the satisfiability problem to the entailment problem.

Clearly, it is important to have tools which allow to deal with entailment. Fortunately, there are several of them and some of them are dealt with in what follows.

A natural proof system

There are certain logical arguments that show up over and over again in mathematical proofs. That gives rise to the question whether these arguments can be formalized and whether they are sufficient to produce each formula entailed by a given set of formulas.

There is, in fact, a so-called natural proof system which gives a positive anwer to the two questions.

At this point, every student

• lists all the proof rules of the natural proof system,
• carries out proofs in the natural proof system ⬀, and
• explains what it means that the natural proof system is sound and complete.

An advanced student

• explains in a mathematical fashion how a proof in the natural proof system is structured in detail and
• explains how one goes about proving the correctness of the proof system.

The resolution proof system

On one hand, the natural proof system is a proof system that can be applied to almost arbitrary propositional formulas; there is only a minor restriction as far as the allowed connectives are concerned. On the other hand, it is not so easy to find proofs, simply because there are many different rules. As pointed out earlier, when formulas in strict normal forms are considered, things become easier. This is true for proof systems as well.

When formulas in conjunctive normal form are considered and the only question is whether $\bot$ follows (or, equivalently, whether the given set of formulas is unsatisfiable), then the situation becomes fairly easy in the sense that one proof rule is sufficient: the resolution rule.

At this point, every student

• phrases the resolution proof rule,
• gives a formal definition of the set of all resolution proofs (by induction or not) ⬀,
• carries out proofs in the resolution proof system ⬀,
• identifies problems which are best modeled using entailment, models them appropriately, and solves them ⬀,
• explains what is special about the situation where formulas are in 2CNF ⬀,
• explains what it means that resolution is sound and complete (as a refutation proof system),
• proves the correctness of resolution,
• mimicks the completeness proof, and
• uses completeness ⬀.

An advanced student

• proves the completeness of resolution.

Compactness

Many situations, when modeled appropriately, involve only a single formula or a finite set of formulas (which can be replaced by a single formula). Still, in some situations the only option is to use an infinite set of formulas. The question then is whether satisfiability and entailment can be reduced to the finite case (and how).

The answer is "yes" in a certain sense, which is called compactness of propositional logic.

Compactness has concrete implications for recursively enumerable (r.e.) sets of formulas: the satisfiability of such sets is co-recursively enumerable (co-r.e.); the entailment problem for such sets is recursively enumerable (r.e.).

At this point, every student

• phrases the comptactness theorem,
• uses it to reduce questions about infinite objects to questions about finite objects ⬀, and
• uses it to derive algorithms for working with recursively enumerable sets of formulas.

An advanced student

• proves the compactness theorem.

NP-completeness of satisfiability

It is one thing to develop good SAT solvers. It is another thing to know what limits there are for solving the satisfiability problem. An established way of doing so is to determine its worst-case complexity, in other words, to answer the question which complexity classes it is complete for.

Unfortunately, the satisfiability problem is not known to be solvable in polynomial time. Rather, it is known that satisfiability is NP-complete. This definitely depends on which formulas are considered as inputs, but for many normal forms NP-completeness holds: BNF, CNF, and even $k$-CNF for every $k \geq 3$.

At this point, every student

• explains the relation between NP-completeness of SAT and SAT solvers ⬀,
• reproduces the reductions in the NP-completeness of SAT ⬀ ⬀,
• illustrates these reductions.

An advanced student

• gives a formal explanation of the relation between solutions of NP-complete problems and 1-assignments of propositional formulas.

First-order logic

The only thing that propositional logic does for us is to formalize (model!) the mechanics of truth values. (It does it in a perfect manner though!) In many situations, however, it would be good to have formal means to describe how truth values result from the circumstances. First-order logic provides such means in a systematic fashion: it allows to describe truth values in circumstances which can be captured by looking at elements of a given universe, relations between them, and functions on them. An instructive example is given in the introductory article on logic.

Syntax and semantics

A starting point for modeling how truth values result from concrete situations is to choose the right vocabulary. This is captured by the formal notion of signature; the 'situations' are captured by the notion of structure.

At this point, every student

• chooses signatures for modeling situations Todo:Aufgabe.,
• gives examples of structures over a certain signature, and
• explains common signatures and structures.

The syntax of first-order logic in a certain vocabulary is defined in two stages: first, terms are defined; second, formulas are defined.

At this point, every student

• gives an inductive definition of the set of all terms and formulas over a given signature,
• tells terms, formulas and objects from other syntactic categories (such as variables and symbols for relations) apart,
• reads and writes formulas in different notation,
• transforms a formula from one notation into another one.

The semantics brings two things together: structures and formulas. It defines what it means for a first-order formula to be true in a structure (under a variable assignment), that is, it assigns a truth value to a formula in a given context. To this end, it is necessary to assign values to terms (in a given context).

At this point, every student

• gives an inductive definition of the value of a term in a structure under a variable assignment,
• gives an inductive definition of the truth value of a formula in a structure under a variable assignment,
• evaluates terms and formulas in a given structure under a given variable assignment ⬀⬀,
• gives a definition of a model of a formula, and
• verifies whether given structures and variable assignments are models of simple formulas ⬀.

Quantifications are an important syntactic feature of first-order logic. When a formula is interpreted in a structure under an assignment, the variables which are quantified are not relevant, but the others (potentially) are. The latter variables are the free variables; the aformentioned fact is formalized in the coincidence lemma.

At this point, every student

• gives an inductive definiton of the set of free variables in a formula,
• determines the set of free variables in a formula, and
• justifies the use of partial assignments in the definition of the semantics on the basis of the coincidence lemma.

Modeling

Defining relations and SQL queries

A key application of first-order logic is to use it as a language to describe objects in a rigorous way. One particular application in this respect is to use formulas to define relations in structures. This is very similar to using database queries to define tables.

At this point, every student

• defines relations in classes of structures and in individual structures, in particular, the natural numbers ⬀,
• transforms simple formulas into SQL queries and vice versa ⬀.

An advanced student

• defines complex relations in classes of structures and in individual structures ⬀ and
• argues on an informal level why certain relations are not definable Todo: Aufgabe..

Describing computations and satisfiability

One of many good examples how things are modeled in first-order logic is concerned with computations of Turing machines. It is a good exercise to show that for a given Turing machine and a given word, a first-order formula can be constructed in such a way that the models of the formula represent the infinite computations of the given machine on the given word.

At this point, every student

• explains how (infinite) computations can be viewed as structures over a specific signature Todo: Verlinken.,
• converts an infinite computation into a structure (and a variable assignment) Todo: Aufgabe.,
• reconstructs the formula that describes the structures which represent infinite computations Todo: Verlinken..

An advanced student

• reconstructs infinite computations from models of the formula, both for concrete models and in general,
• proves that these reconstructions are correct (and, in particular, well-defined).

The formula that describes the infinite computations of a given Turing machine on a given word is uniform in the sense that this formula can be computed from an encoding of the Turing machine and the word. As a consequence, satisfiability of first-order formulas is undecidable. In first-order logic, a formula is satisfiable if it has a model.

At this point, every student

• argues, by using the semantics of first-order logic, why simple formulas are satisfiable or unsatisfiable Todo: Aufgabe.,
• explains what it means that satisfiability is undecidable,
• explains why satisfiability is undecidable using the result on modeling computations Todo: Verlinken., and
• draws conclusions from the fact that satisfiability is undecidable Todo: Aufgabe.

An advanced student

• reduces satsifiability to other undecidable problems.

Equivalence

Equivalence between first-order formulas is defined in complete analogy to equivalence between formulas of propositional logic. As a consequence, the laws of propositional logic apply in first-order logic, but they do not capture all aspects of equivalence. Most importantly, the laws of propositional logic do not say anything about quantifiers, which are a crucial syntactic ingredient of first-order logic.

Laws, derivations, and substitution

There are specific laws for quantifiers, most of which are derived from propositional laws along the analogy that existential quantification is similar to disjunction and universal quantification is similar to conjunction. One important law explains what it means to rename bound variables. In this context, it is important to understand the scope of quantifiers and what term substitution is about.

At this point, every student

• names and phrases all laws,
• derives the equivalence of formulas using laws of propositional logic and quantifier laws,
• gives an inductive definition of the variables in the scope of a quantifier,
• gives an inductive definition of the application of a substitution,
• applies substitutions to formulas and identifies name clashes ⬀,
• phrases the substitution lemma, and
• describes situations in which the substitution lemma is applied.

An advanced student

• proves the substitution lemma.

Normal forms

Just as with propositional logic, it is good to have normal forms in first-order logic. We consider three of them:

• boolean normal form,
• prenex normal form,
• conjunctive normal form.

Unlike in propositional logic, conjunctive normal form is not complete in the sense that every first-order formula is equivalent to a formula in conjunctive normal form.

At this point, every student

• gives definitions of the three normal forms,
• explains algorithms converting arbitrary propositional formulas into equivalent formulas in the different normal forms ⬀,
• converts formulas in CNF into clausal notation and vice versa Todo:Aufgabe..

Modeling cont'd: axiomatizing classes of structures

As stated earlier, a key application of first-order logic is to use it as a language to describe objects in a rigorous way, just as a programming language describes algorithms (in a certain sense) precisely. One application in this direction is to define relations in structures. Here, we are concerned with describing (axiomatizing) classes of structures, such as algebraic structures or graphs or orderings.

Todo: congruence relations.

As first-order logic has a rigorous semantics, this gives us a way to describe classes of structures in an unambiguous fashion. Second, once a class is axiomatized, it allows us to study it in detail, more precisely, we can deduce properties of the structures in the class via entailment.

At this point, every student

• finds axiomatizations of simple classes of structures described in ordinary mathematical language, in particular, algebraic and relational structures ⬀, and
• distinguishes between axiomatizations in general and finite axiomatizations.

An advanced student

• argues on an informal level why certain classes of structures are not (finitely) axiomatizable.⬀

Entailment

Just as with propositional logic, entailment is the most fundamental notion in first-order logic, simply because it captures logical deduction in a purely mathematical fashion. Similarly, proof systems capture the essence of reasoning.

Logic programming is an area of programming where entailment plays a crucial role, in fact, it initiated this programming paradigm.

Entailment itself is closely related to satisfiability, in fact, they are two sides of the same coin.

At this point, every student

• gives a definition of entailment,
• checks whether or not a formula is entailed by a set of formulas, drawing on the definition ⬀,
• gives a proof of the lemma about satisfiability and entailment,
• mutually reduces instances of the satisfiability problem to the entailment problem.

Modeling using entailment

Entailment is a good tool for modeling.

Modeling reachability demonstrates in a nice fashion how useful entailment is from an algorithmic perspective. Another example is satisfiability.

At this point, every student

• models simple situations as questions about entailment ⬀.

Proof systems

There are natural proof systems which try to model reasoning of mathematicians, in principle. There are proof systems such as resolution, which are basically meant to allow fully automated reasoning (or are, at least, a starting point for fully automated reasoning).

A natural proof system

Here is a particular natural proof system for first-order logic, which simply extends the one for propositional logic by rules for quantifiers and equality. This proof system is sound and complete, which immediately implies that entailment (for finite sets of formulas) is a recursively enumerable and satisfiability (for finite sets of formulas) is co-r.e. We already know that satisfiability and thus entailment are undecidable. This classifies the most important notion of logic with regard to its computational properties.

At this point, every student

• names and phrases all rules of the natural proof system,
• constructs simple proofs in the natural proof system ⬀, and
• explains what it means for the proof system to be sound and complete.

An advanced student

• explains concrete scenarios where weakening the assumptions for applying the quantifier rules lead to wrong proofs and
• constructs more complicated proofs, for instance in theories like Presburger arithmetic.

Resolution

Another proof system is resolution, which can, in its pure form, only be used as a refutation proof systems for sets of formulas in conjunctive normal form without equality. Resolution itself is based on unification.

In a setting with formulas with equality, resolution can be applied after equality has been replaced by a binary relation symbol and congruence axioms for this symbol have been added. In a setting with existential quantification, skolemization can be used. To understand how skolemization works it is helfpful to know what reducts and expansions are.

At this point, every student

• identifies unifiers and most general unifiers ⬀(5.),
• gives formal resolution proofs ⬀,
• gives formal resolution proofs when equality and existential quantification are present ⬀,
• applies resolution to determine whether a formula is a tautology or unsatisfiable Todo:Aufgabe., and
• explains what it means for the proof system to be sound and complete.

An advanced student

• explains the connection between resolution and logic programming.

Compactness and computational perspective

Just as with propositional logic, there is a fundamental question concerned with satisfiability. Is there a way to reduce the satisfiability for arbitrary sets of formulas to the satisfiability of finite sets of formulas or even single formulas? And just as with propositional logic, the answer is positive, which is called compactness.

Compactness can be applied in many contexts. One particular application yields the theorem that the set of all finite sets is not axiomatizable.

Entailment is undecidable, simply because satisfiability is undecidable. But entailment is recursively enumerable, which follows from the fact that there are sound and complete proof systems for first-order logic.

At this point, every student

• explains what it means that first-order logic enjoys the compactness property,
• sketches why the soundness and the completeness of the proof system imply that entailment is recursively enumerable for recursively enumerable sets of first-order formulas Todo:Aufgabe..

An advanced student

• uses compactness in simple contexts Todo:Aufgabe..