Proof theory

Proof theory is a special area of study that belongs to both mathematical logic and theoretical computer science. In proof theory, mathematicians study proofs. Proofs are the steps we use to show that something is true. They look at proofs like they are math objects, such as numbers or shapes, and study them in detail.

Proofs in this area are seen as special structures, like lists or trees, that follow strict rules. These rules start from basic ideas called axioms. They also include ways to build new statements from old ones, called rules of inference. This way of thinking helps experts learn more about how logic works.

Proof theory has many areas to explore, such as structural proof theory, ordinal analysis, and automated theorem proving. It is useful in computer science, linguistics, and philosophy, showing how important this way of thinking is in many fields.

History

Proof theory started with work by mathematicians like Gottlob Frege, Giuseppe Peano, Bertrand Russell, and Richard Dedekind. It grew because of David Hilbert, who began Hilbert's program to keep math safe and sure.

Later, Kurt Gödel showed that some theories could not prove they were right. This brought new ideas to proof theory, such as provability logic and self-verifying theories. At this time, Jan Łukasiewicz, Stanisław Jaśkowski, and Gerhard Gentzen found new ways to see how proofs work, like natural deduction and the sequent calculus. These ideas helped make proofs simpler to learn and study.

Structural proof theory

Main article: Structural proof theory

Structural proof theory is a part of proof theory that studies different ways to write down logical proofs, called proof calculi. The three most famous styles are Hilbert calculi, natural deduction calculi, and sequent calculi. These methods help us understand many kinds of logic, including basic propositional and predicate logic, as well as more complex logics.

Researchers in this area focus on a special type of proof called analytic proofs. These proofs have special features that make them easier to study. They help show that the logic system works correctly. There are also links between structural proof theory and type theory, showing how different parts of mathematics and logic connect.

Ordinal analysis

Main article: Ordinal analysis

Ordinal analysis is a special way to check that math rules work well and don’t create mistakes. It helps us learn how much “infinity” we need to prove these rules are good. For example, a famous mathematician named Gentzen used this method to show that Peano Arithmetic—a system for basic number facts—is correct by using a special type of counting called transfinite induction.

This method is used to study many math ideas. It can show that some ideas are only true if we think of certain endless patterns in a neat way. It also helps mathematicians sort out which math facts and patterns can be proven using these systems.

Provability logic

Main article: Provability logic

Provability logic is a kind of special logic. In this logic, a special symbol means "it can be proven that." It helps us understand how we can talk about proofs using strict rules. One important system is called GL, and it matches what can be proven in Peano Arithmetic.

Researchers have discovered many interesting things using provability logic. For example, GL shows that if a mistake cannot be proven, then it also cannot be proven that a mistake cannot be proven. People have also studied how to make provability logic more complex and how proofs are related to each other.

Reverse mathematics

Main article: Reverse mathematics

Reverse mathematics is a part of mathematical logic that looks at which basic rules, or axioms, are needed to prove big math ideas. It was started by Harvey Friedman.

Instead of starting with rules and proving theorems, reverse mathematics works backward — from theorems to the rules needed to prove them.

In this area, mathematicians start with a basic set of rules that is too weak to prove many theorems. They then find out which stronger rules are needed to prove each theorem. Research in reverse mathematics often uses ideas from recursion theory.

Functional interpretations

Functional interpretations help us understand theories that do not use construction by changing them into theories that do. This happens in two steps. First, a classical theory is changed into an intuitionistic theory. This means finding a way to translate the ideas of the classical theory into a more structured form. Second, the intuitionistic theory is made even simpler, turning it into a theory without quantifiers, and focusing only on functions.

These interpretations support Hilbert's program by showing that classical theories are consistent when compared to constructive ones. They also help us find useful, constructive information from proofs. For example, they can show that some recursive functions can be written as simple terms. One famous method, known as the Dialectica interpretation, was developed by Kurt Gödel to connect intuitionistic arithmetic with a theory of functionals.

Formal and informal proof

Main article: Formal proof

Informal proofs are how mathematicians usually share their ideas. They are like rough outlines that experts can understand. Most mathematicians don’t write full formal proofs because they take a lot of time and are very detailed.

Formal proofs are like clear, step-by-step instructions that computers can help make and check. While it is easy for a computer to check these formal proofs, finding them can be very hard. Checking informal proofs, however, often takes many weeks of careful review by other mathematicians, and sometimes mistakes are still found.

Proof-theoretic semantics

Main articles: Proof-theoretic semantics and Logical harmony

In language studies, ideas from proof theory help us understand how we give meaning to words and sentences. This is used in types of grammar like type-logical grammar, categorial grammar, and Montague grammar.