|
Weak arithmetics and applications
Proving the existence of some meta-mathematical object
(e.g. a method for solving polynomial equations of degree 3 or 4)
does not need a mathematical definition of that object:
a general agreement about the correctness of each answer is achievable.
Proving the inexistence of some meta-mathematical object
(e.g., a method for solving polynomial equations of degree 5 or more)
needs a mathematical definition.
Among the inexistence problems inducing the main concepts of logic, let us start with the following two.
Problem 1. (Hilbert's tenth problem) Prove that there is no universal method correctly asserting wether any given diophatine equation has (at least) a solution or has no. Problem 2. Prove that there is some arithmetical statement that cannot be proved or disproved. These problems have no sense without a precise definition of an algorithm and of a proof. Together with the concept of algorithm formalizing the notion of method, it is possible to define a concept of complexity, also to define a formal proof and a strength scale for theories. Weak arithmetics study the statements needing a few axioms or weak rules of reasoning for proving them. Surprisingly, appear numerous links with the complexity of algorithms. This tutorial is intended to provide an introduction to the topic, its problems and its methods.
It will avoid both technical difficulties and ambiguity.
It will be divided in the following three sessions.
I. Decidable fragments of arithmetic
Peano arithmetic admits various equivalent families of axioms formalizing the properties of the successor function (and of addition and multiplication) together with a family of Induction Axioms formalizing the usual mathematical induction. It is not possible to algorithmically determine, for any sentence in its language, whether that sentence is provable from its axioms: the theory is undecidable. Presburger arithmetic is the well known first-order theory of the natural numbers with addition and equality. The axioms include the schema of induction. It is much weaker than Peano arithmetic and has been proved to be decidable. However the algorithms for decision require more than exponential run time. Stronger fragments than Presburger arithmetic have been proved to be decidable, e.g. the existential theory of addition and divisibility. Decidable fragments of Peano arithmetic are more and more involved in automatic reasoning. II. Definability
Let us consider a set on words on a finite alphabet with k letters denoted as digits {0, 1, 2, ..., k-1}. There is a natural correspondance between such words and natural numbers using base k representation. Let us now consider the set of words recognizable by a finite automaton. It turns out that the correspondant set of integers is definable by a formula of the langage (+;Vk), where z=Vk(x) is the relation "z is the greatest power of k dividing x". The converse is true. This correspondance provides insight in the area of complexity: a relation which is definable both in (+;Vk) and (+;Vk') for which there is no n and m such that kn=k'm is definable in Presburger arithmetic.
Other correspondance are sources of problem or of solutions!
The unary relation "x is not prime nor 0 nor 1" is definable using the formula
∃u<x∃v<x(x=u×v).
More generally, the Δ0-definability is essentially definability with a formula in the
langage of arithmetic where the quantified variables way bounded by terms.
Most of the natural notions have been proved to be Δ0-definable,
and classical diagonalization methods provide ad hoc non Δ0-definable ones.
A major open problem is to find a "natural" artithmetical relation which is NOT Δ0-definable.
The relation z=Card{i≤y; i is a prime number}
is not known to be Δ0-definable and is a candidate.
An answer could provide the strict inclusion LOGSPACE⊊LINSPACE.
|
 III. Provability Let E be a subset of ℕn for which there exists an algorithm that will ultimately halt when a member of the set is provided as input, but may continue indefinitely when the input is a non-member. There is a Δ0-formula φ such that E is defined by (∃y∈ℕm)(φ(x,y)=0). This very last formula is called a Σ1-formula. The fundamental step of the answer to problem 1 is the following theorem of Y. Matiyasevich, J. Robinson, M. Davis, and H. Putnam: Theorem. For all Σ1-formula ψ, there is two polynomials P and Q with natural coefficients such that forall a in ℕn, ψ(a) is true if and only if there exists b in ℕm such that P(a,b)=Q(a,b). Let us consider the following question: "What axioms are really useful in the proof of this theorem?". We say that a set of axioms T proves the MRDP-theorem for the following mathematical statement: For all Σ1-formula ψ, there is two polynomials P and Q with natural coefficients such that Theorem. If IΔ0 proves MRDP, then NP=co-NP. A much stronger theory is obtained if we add an axiom, denoted by EXP, which guarantees the totality of the exponential function: Theorem. IΔ0 + EXP proves MRDP. But EXP is not a theorem in IΔ0. A weaker axiom than EXP is the following axiom Ω1: We are very far from proving the premise of this theorem, but more and more parts of the natural arithmetic turn out to be formally proved to be in IΔ0 + Ω1. For example: Theorem. IΔ0 + Ω1 proves the infinity of the prime numbers. Bibliography
| ||||