Theorem Proving:
Enumeration, Computation, Deduction
Goals
Computer-Assisted proof components
Automated Deduction
Limits of Set theory and First-order Logic
Goals
- Goal: Use computers to greatly increase our ability to discover and prove
mathematical results across areas of mathematics.
- Why?
- How?
Learn to search for, construct and recognize useful mathematical objects.
What?
- There are infinitely many prime numbers.
- There are arbitrarily long arithmetic progressions all of whose elements are prime numbers.
- There are infinitely many natural numbers $n$ such $n$ and $n+2$ are both primes.
Computer-Assisted proof components
- Computers have been used in various ways to provide a component of a proof:
- Enumeration,
- Symbolic algebra,
- Exact real number arithmetic,
- Linear programming,
- SAT solvers.
- Some examples:
- Four colour theorem,
- Kepler conjecture,
- Boolean Pythagorean triples problem.
First-order logic: languages
- A first-order language, which describes a domain of discourse (e.g. $\mathbb{N}$) has vocabulary consisting of
- Variables - can be taken to be a fixed countable set.
- Constants (e.g. $0$, $1$).
- Functions (e.g. $+$).
- Predicates (e.g. $<$, $=$).
- Special symbols $\Rightarrow$, $\iff$, $\wedge$, $\vee$, $\forall$, $\exists$, ...
- We form two kinds of expressions from these, terms (e.g. $1+1$, $n + 3$)
and formulas (e.g. $n + 1 < 2$, $4 < 3$).
- Terms and formulas may depend on variables.
- Terms represent objects in the domain of discourse.
- Formulas are either true or false.
Deduction and theories
- We can deduce formulas from other formulas using the rules of deduction.
- The main deduction rule is Modus Ponens : given $P$ and $P\Rightarrow Q$ we deduce $Q$.
- A theory is a language together with a collection of formulas, called axioms in the language.
- A formula is deducible in a theory if it can be
obtained from the axioms by the rules of deduction.
Universal deducer?
- A universal deducer is a computable function (algorithm) which, given a proposition (formula),
returns a proof if it is deducible and otherwise returns failure.
- By results of Turing, there is no such algorithm.
- We can enumerate proofs and check if they prove either the given proposition or its negation.
This does not always work as there are statements that are true but not provable.
- Practically, we can conclude that there is no best deducer,
as any given proof can be found by some deducer but no deducer can find all proofs.
Resolution theorem proving: Conjunctive normal form
- To prove a proposition $P$ from axioms, we can derive a contradiction from $\neg P$ and the axioms.
- We can rewrite $\implies$, $\wedge$ etc in terms of $\vee$ and $\neg$.
- Suppose a variable is existentially quantified,
- e.g. $\delta$ in $\forall \epsilon \exists \delta\ |x| < \delta \implies |x|^2 < \epsilon$,
- we can regard the variable $\delta$ as a function $\delta(\epsilon)$,
- we extend the language with additional functions (or constants)
for existentially quantified variables.
- In the extended language we no longer need $\exists$,
$\forall \epsilon\ |x| < \delta(\epsilon) \implies |x|^2 < \epsilon$.
- Variables without explicit quanitification are regarded as universally quantified.
Resolution theorem proving
- By the above process, we reduce to
- A list of statements all of which are true, i.e., a conjunction of clauses.
- Each clause consists of atomic formulas and their negations combined by $\vee$,
i.e., a disjunction of literals.
- From these we seek a contradiction - an empty clause.
- Resolution is the rule by which if two clauses are of the form
$P\vee Q_1\vee\dots\vee Q_n$ and $\neg P \vee R_1\vee \dots\vee R_m$, we deduce
$Q_1\vee\dots\vee Q_n\vee R_1\vee \dots\vee R_m$.
- Combined with unification - substituting expressions for variables to make literals equal, this is refutation complete.
- To handle equality efficiently, paramodulation is used.
First-order logic deducers; machine learning
- Theorem proving is thus reduced to a search for the empty clause,
starting with a given collection of clauses and using moves such as resolution and paramodulation.
- Various search heuristics can be used.
- We can also add premises corresponding to theorems in a formal library
(Mizar has been used for this).
- Machine learning has been used to select both strategies and premises.
Robbins conjecture
- Robbins conjecture was a conjectural characterization of Boolean algebras in terms of
associativity and commutativity of $\vee$ and the Robbins equation
$\neg(\neg(a\vee b)\vee \neg(a \vee \neg b)) = a$.
- This was conjectured in the 1930s, and finally proved in 1996 using the
automated theorem prover EQP.
- So far, this seems to be the only major success of deductive theorem provers.
- First-order logic theorem provers are, however, used in interactive proof systems
(hammer tactics).
Real-life mathematics
- A proof in real-life mathematics consists of:
- definitions, axioms, assumptions, notation;
- assertions;
- hints about which assertions, definitions etc. are used in the proof of a given assertion.
- The reader is expected to deduce all assertions based on the hints
(or at least believe that he/she can do so).
- In particular, there is no objective sense in which a proof is complete or correct.
- Interactive proof systems modelled on human proofs, such as Mizar and Naproche,
follow a similar approach.
“ Since the first half of the 20th century mathematics has been presented as a science based on
ZFC and ZFC was introduced as a particular theory in Predicate Logic.
“ Therefore someone who wanted to get to the bottom of things in mathematics had a simple
road to follow - learn what Predicate Logic is, then learn a particular theory called ZFC, then
learn how to translate propositions about a few basic mathematical concepts into formulas of
ZFC, and then learn to believe, through examples, that the rest of mathematics can be reduced
to these few basic concepts.”
Vladimir Voevodsky
Why new foundations?
- In the usual foundations of mathematics, $sin(3)$ and $3(sin)$ are syntactically equally valid.
- We need additional (run-time) conditions for being well-defined.
- We do have types, i.e., syntactic restrictions, in Category theory and Higher-order logic.
- However, proofs are still not first class, so not composable.
- We instead have patterns of proof (such as induction) in mathematics,
and tactical meta-language in formal proof systems (which are then implicitly part of the foundations).
“ The roadblock that prevented generations of interested mathematicians and computer scientists
from solving the problem of computer verification of mathematical reasoning was the
unpreparedness of foundations of mathematics for the requirements of this task.”
“ Formulating mathematical reasoning in a language precise enough for a computer to follow
meant using a foundational system of mathematics not as a standard of consistency applied only
to establish a few fundamental theorems, but as a tool that can be employed in everyday
mathematical work. ”
Vladimir Voevodsky