# All Science Fair Projects

## Science Fair Project Encyclopedia for Schools!

 Search    Browse    Forum  Coach    Links    Editor    Help    Tell-a-Friend    Encyclopedia    Dictionary

# Science Fair Project Encyclopedia

For information on any area of science that interests you,
enter a keyword (eg. scientific method, molecule, cloud, carbohydrate etc.).
Or else, you can start by choosing any of the categories below.

# 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 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 and Bertrand Russell's Principia Mathematica.

## Topics in mathematical logic

The main areas of mathematical logic include model theory, proof theory and recursion 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:

• Putative proofs of universal validity of first-order formulas can be checked for validity, algorithmically. In technical language, the set of proofs is primitive recursive. Essentially, this is Gödel's completeness theorem, although that theorem is usually stated in a way that does not make it obvious that it has anything to do with algorithms.
• The set of valid first-order formulas is not computable, i.e., there is no algorithm for checking for universal validity. There is, however, an algorithm that behaves as follows: Given a first-order formula as its input, the algorithm eventually halts if the formula is universally valid, and runs forever otherwise. If the algorithm has been running for a trillion years, the answer remains unknown. In other words, this set is "recursively enumerable", or, as it is sometimes more suggestively put, "semi-decidable".

## Technical Reference

Necessarily temporary. The aim of this page really is not to become a crash course in mathematical logic, but we have to start somewhere irrªtiºnal 14:32, 21 Apr 2005 (UTC)

### Basic Definitions

Definition. Let $\mathfrak{L}\,$ be a first order language. Given a formula $\phi\,$, a term $t\,$ is said to be substitutable for a $x\,$ in $\phi\,$ where $x\,$ is a variable in $\mathfrak{L}\,$, if any of the following cases holds:

• φ is atomic
• φ is of the form $\lnot(\alpha)$ and t is substitutable for x in α
• φ is of the form $(\alpha \lor \beta)$ and t is substitutable for x in both α and β
• φ is of the form $(\forall y)(\alpha)$ and either
• x is not a free variable in φ
• y does not occur in t and t is substitutable for x in α

## 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.