# Mathematical logic

**Mathematical logic** is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics.

Although the layperson may think that mathematical logic is the *logic of mathematics*, the truth is rather that it more closely resembles the *mathematics of logic*. It comprises those parts of logic that can be modelled mathematically. Earlier appellations were symbolic logic (as opposed to philosophical logic), and metamathematics, which is now restricted as a term to some aspects of proof theory.

## Contents

## History

*Mathematical logic* was the name given by Giuseppe Peano to what is also known as symbolic logic. In essentials, it is still the logic of Aristotle, but from the point of view of notation it is written as a branch of abstract algebra.

Attempts to treat the operations of formal logic in a symbolic or algebraic way were made by some of the more philosophical mathematicians, such as Leibniz and Lambert; but their labors remained little known and isolated. It was George Boole and then Augustus De Morgan, in the middle of the nineteenth century, who presented a systematic mathematical (of course non-quantitative) way of regarding logic. The traditional, Aristotelian doctrine of logic was reformed and completed; and out of it developed an adequate instrument for investigating the fundamental concepts of mathematics. It would be misleading to say that the foundational controversies that were alive in the period 1900-1925 have all been settled; but philosophy of mathematics was greatly clarified by the 'new' logic.

While the traditional development of logic (see list of topics in logic) put heavy emphasis on *forms of arguments*, the attitude of current mathematical logic might be summed up as *the combinatorial study of content*. This covers both the *syntactic* (for example, sending a string from a formal language to a compiler program to write it as sequence of machine instructions), and the *semantic* (constructing specific models or whole sets of them, in model theory).

Some landmark publications were the Begriffsschrift by Gottlob Frege, Studies in Logic by Charles Peirce, Principia Mathematica by Bertrand Russell and Alfred North Whitehead, and On Formally Undecidable Propositions of Principia Mathematica and Related Systems by Kurt Godel.

## Topics in mathematical logic

The main areas of mathematical logic include model theory, proof theory and recursion theory (often now referred to as computability theory). Axiomatic set theory is sometimes considered too. There are many overlaps with computer science, since many early pioneers in computer science, such as Alan Turing, were mathematicians and logicians.

The study of programming language semantics derives from model theory, as does program verification, in particular model checking.

The Curry-Howard isomorphism between proofs and programs relates to proof theory; intuitionistic logic and linear logic are significant here. Calculi such as the lambda calculus and combinatory logic are nowadays studied mainly as idealized programming languages.

Computer science also contributes to logic by developing techniques for the automatic checking or even finding of proofs, such as automated theorem proving and logic programming.

## Some fundamental results

Some important results are:

- The set of valid first-order formulas is recursively enumerable. This follows from Gödel's completeness theorem (which establishes the equivalence of validity and provability), because the set of proofs for first-order logic formulas is recursively enumerable ("semi-decidable"). Therefore, there is a procedure that behaves as follows: Given a first-order formula as its input, the procedure eventually halts if the formula is valid or not valid, and runs forever otherwise. Some first-order theorem provers have this completeness property.

- The set of valid first-order formulas is
*not*recursive, i.e., there is no algorithm for checking for universal validity. This follows from Gödel's incompleteness theorem.

- The set of all universally valid second-order formulas is not even recursively enumerable. This is also a consequence of Gödel's incompleteness theorem.

- The independence of the continuum hypothesis, proved by Paul Cohen in 1963.

## Technical reference

### First-order languages and structures

**Definition.** A **first-order language** is a collection of distinct typographical symbols classified as follows:

- The
**equality symbol**; the**connectives**, ; the**universal quantifier**and the**parentheses**, . - A countable set of
**variable symbols**. - A set of
**constant symbols**. - A set of
**function symbols**. - A set of
**relation symbols**.

Thus, in order to specify a language, it is often sufficient to specify only the collection of constant symbols, function symbols and relation symbols, since the first set of symbols is standard. The parentheses serve the only purpose of forming groups of symbols, and are not to be formally used when writing down functions and relations in formulas.

These symbols are just that, *symbols*. They don't stand for anything. They do not *mean* anything. However, that deviates further into semantics and linguistic issues not useful to the formalization of mathematical language, yet.

*Yet*, because it will indeed be necessary to get some meaning out of this formalization. The concept of *model* over a language provides with such a semantics.

**Definition.** An -**structure** over the language , is a bundle consisting of a nonempty set , the universe of the structure, together with:

- For each constant symbol from , an element .
- For each -ary function symbol from , an -ary function .
- For each -ary relation symbol from , an -ary relation on , that is, a subset .

Often, the word *model* is used for that of *structure* in this context. However, it is important to understand perhaps its motivation, as follows.

### Terms, formulas and sentences

**Definition.** An -**term** is a nonempty finite string of symbols from such that either

- is a variable symbol.
- is a constant symbol.
- is a string of the form where is an -ary function symbol and , ..., are terms of .

**Definition.** An -**formula** is a nonempty finite string of symbols from such that either

- is a string of the form where and are terms of .
- is a string of the form where is an -ary relation symbol and , ..., are terms of .
- is of the form where is an -formula.
- is of the form where both and are -formulas.
- is of the form where is a variable symbol from and is an -formula.

**Definition.** An -formula that is characterized by either the first or the second clause is called an **atomic**.

**Definition.** Let be an -formula. A variable symbol from is said to be **free** in if either

- is atomic and occurs in .
- is of the form and is free in .
- is of the form and is free in or .
- is of the form where and are not the same variable symbols and is free in .

**Definition.** A **sentence** is a formula with no free variables.

### Assignment functions

Hereafter, will denote a first-order language, will be an -structure with underlying universe set denoted by . Every formula will be understood to be an -formula.

**Definition.** A **variable assignment function** (v.a.f.) into is a function from the set of variables of into .

**Definition.** Let be a v.a.f. into . We define the **term assignment function** (t.a.f.) , from the set of -terms into , as follows:

- If is the variable symbol , then .
- If is the constant symbol , then .
- If is of the form , then .

**Definition.** Let be a v.a.f. into and suppose that is a variable and that . We define the v.a.f. , referred to as an -**modification of the assignment funtion** , by

### Logical satisfaction

**Definition.** Let be formula and suppose is a v.a.f. into . We say that **satisfies** **with assignment** , and write , if either:

- is of the form and .
- is of the form and .
- is of the form and .
- is of the form and or .
- is of the form and for each element , .

**Definition.** Let be formula and suppose that for every v.a.f. into . Then we say that **models ** , and write .

**Definition.** Let be a set of formulas and suppose that for every formula then we say that **models** , and write .

In the case that is a sentence, that is, a formula with no free variables, the existence of a single v.a.f. for which immediately implies that .

**Definition.** Let be a sentence and suppose that . Then we say that is **true in** .

### Logical implication and truth

**Definition.** Let and be sets of formulas. We say that **logically implies** , and write , if for every structure , implies .

As a shortcut, when dealing with singletons, we often write instead of .

**Definition.** Let be a formula and suppose that . Then we say that is **universally valid**, or simply valid, and in this case we simply write .

To say that a formula is valid really means that every -structure models .

**Definition.** Let be a sentence and suppose that . Then we say that is **true**.

### Variable substitution

**Definition.** Let be a term and suppose is a variable and is another term. We define the term , read **with** **replaced by** , as follows:

- If is the variable symbol , then is defined to be the term .
- If is a variable symbol other than , then is defined to be the term .
- If is a constant symbol, then is defined to be the term .
- If is of the form , then is defined to be the term .

**Definition.** Let be a formula and suppose is a variable and is a term. We define the formula , read **with** **replaced by** , as follows:

- If is of the form , then is defined to be the formula .
- If is of the form , then is defined to be the formula .
- If is of the form , then is defined to be the formula .
- If is of the form , then is defined to be the formula .
- If is of the form , then
- if and are the same variable symbol, is defined to be the formula .
- else, is defined to be the formula .

### Substitutability

**Definition.** Let be a formula and suppose is a variable and is a term. We say that **is substitutable for** **in** , if either:

- is atomic.
- is of the form and is substitutable for in .
- is of the form and is substitutable for in both and .
- is of the form and either
- is not a free variable in .
- does not occur in and is substitutable for in .

The notion of substitutability of terms for variables corresponds to that of the preservation of truth after substitution is carried out in terms or formulas. Strictly speaking, substitution is always allowed, but substitutability will be imperative in order to yield a formula which meaning was not deformed by the substitution.

## References

- A. S. Troelstra & H. Schwichtenberg (2000).
*Basic Proof Theory*(Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0521779111. - George Boolos & Richard Jeffrey (1989).
*Computability and Logic*(3rd ed.). Cambridge University Press. ISBN 0521007585. - Elliott Mendelson (1997).
*Introduction to Mathematical Logic*(4th ed.) Chapman & Hall. - A. G. Hamilton (1988).
*Logic for Mathematicians*Cambridge University Press.

## External links

## See also

- Logic
- Model theory
- Computability logic
- Game semantics
- Provability logic
- Interpretability logic
- Sequent calculus
- Intuitionistic logic
- Predicate logic
- Theory of institutions
- Table of mathematical symbols
- Infinitary logicde:Mathematische Logik

es:Lógica matemática fr:Logique mathématique it:Logica matematica ja:数理論理学 ru:Математическая логика sl:Matematična logika sq:Logjika Matematikore sv:Matematisk logik th:คณิตตรรกศาสตร์ tl:Matematikal na lohika tr:Sembolik Mantık zh:数理逻辑