# Logic for CS

`Logic For CS - Foundations of Automatic Theorem Proving` - Jean Gallier, 2003

## Introduction

Logic is concerned mainly with two concepts: _truth_ and _provability_.

We'll focus on a mathematically well-defined logical system known as _first-order logic_ (FOL) and _many-sorted logic_, and try to prove some basic properties of these systems. In particular, we focus on _algorithmic methods for proving theorems_, often referred to as _automatic theorem proving_.

Every _logical system_ consists of a _language_ used to write _statements_, which are also called _propositions_ or _formulas_.

Normally, every formula has some intended _interpretation_. For example, a formula may assert a true property about the natural numbers.

This implies that a formula has a well-defined _semantics_. But how do we define this meaning precisely? In logic, we usually define the meaning of a formula as its _truth value_. A formula can be either true, i.e. _valid_, or false.

Defining rigorously the notion of truth is actually not as obvious as it appears. We shall present a concept of truth due to Tarski. Roughly speaking, a formula is true if it is _satisfied_ in _all possible interpretations_.

So far, we have used the intuitive meaning of such words as interpretation, truth, and similar, but we must define these terms rigorously when dealing with FOL.

The branch of logic in which _abstract structures_ and the properties true in these structures are studied is known as _model theory_.

Once the concept of truth has been defined rigorously, the next question is to investigate whether it is possible to find methods for deciding in a finite number of steps whether a formula is _valid_ (i.e. true). Due to Church, there is no such general method for first-order logic. However, there is another familiar method for testing whether a formula is true: to give a _proof_ of this formula. Of course, to be of any value, a _proof system_ should be _sound_, which means that _every provable formula is true_.

We also need to rigorously define _the notion of proof_, and _proof system_ for FOL. The branch of logic concerned with the study of proof is known as _proof theory_. Now, if we have a sound proof system, we know that every provable formula is true. Is the proof system strong enough that it is also possible to prove every true formula (of FOL)? A major theorem due to Godel shows that there are logical proof systems in which every true formula is provable. This is referred to as the _completeness_ of the proof system.

To summarize the situation, if one is interested in algorithmic methods for testing whether a FOL formula is valid, there are two logical results of central importance: one positive, _Godel's completeness theorem_, and one negative, _Church's undecidability of validity_.

Roughly speaking, Godel's completeness theorem asserts that there are logical calculi in which every true formula is provable, and Church's theorem asserts that there is no decision procedure (which always terminates) for deciding whether a formula is true/valid. Hence, any algorithmic procedure for testing whether a formula is true (or equivalently, by Godel's completeness theorem, provable, in a complete system) must run forever when given certain non-true formulae as input.

We'll investigate Godel's positive result and its applications to automatic theorem proving (ATP), following thw main thread of _Gentzen-like sequent calculi_. Despite the theoretical limitation imposed by Church's result, the goal of ATP is to find efficient algorithmic methods for finding proofs of valid formulas.

A fairly intuitive method for finding such algorithms is the _completeness proof for Gentzen-like sequent calculi_. This approach yields a complete search procedure for proving valid formulae of FOL. However, it is not very practical so we'll try to improve it or find more efficient ones. And for that, we'll need to analyze the structure of proofs carefully.

Fundamental results of Gentzen and Herbrand show that, if a formula is provable, then the proof has a particular form, called the _normal form_. The existence of such normal forms can be exploited to reduce the size of the proof search space.

The existence of normal forms is also fundamental because it reduces the problem of finding a proof of a _first-order formula_ to the problem of finding a proof of a simpler type of formula, called a proposition. _Propositions_ are much simpler than first-order formulae. There are efficient algorithms for deciding their truth value - one of them, based on the reduction technique, is the _resolution method_.

Besides looking for general methods applying to the class of all true first order formulae, it is interesting to consider subclasses for which simpler or more efficient proof procedures exist. Some subclasses even have _decision procedures_. This is the case for propositions, and for quantifier-free formulae.

Unfortunately, even in cases in which algorithms exist, another difficulty emerges. A decision procedure may take too much time and space to be practical. For example, even testing whether a proposition is true may be very costly.

ATP techniques can be used to _axiomatize_ structures and prove the properties of programs working on these structures. Logic is also used in CS to model computations and as a PL. _Prolog_ programs are specified by sets of assertions, a computation is a proof, and the output of a program is the extracted proof. Since programs are essentially logical formulae, establishing their correctness is claimed to be trivial. This is not quite so, because the concept of _correctness_ is relative, and the semantics of a Prolog program needs to be expressed in a language other than Prolog.
