3.1.1  Title

 

WEAK ARITHMETICS

 

3.1.2     Objectives

 

In three years :

 

To construct Nonstandard Models of Buss Arithmetic to establish some bounds on the class NP inter co-NP.

 

To solve the problem of existence of end extensions of countable models of bounded collection.

 

To explore further the additive theory of infinite sets of prime numbers, both with absolute results and its links with number theory via the Schinzel's hypothesis.

 

To code natural numbers, complex numbers, and quadratic integers by automata accepting numbers (written in non-classical systems).

 

To prove results for ultra-linear unary recursive schemata (with individual constants).

 

To obtain decidability results for S2S[P]  theories.

 

To build formal constructive theories with (from Grzegorczyk hierarchy) with applications to databases. To investigate the power of counting in very small complexity classes and in the corresponding logical or arithmetical settings.

 

To explore the relation between Infinite games, automata, and arithmetic.

 

To study the fine structure of the BSS recursive enumerable sets.

 

To investigate concurrent processes in distributed conveyer systems and their relation with corresponding weak arithmetics.

 

To construct Diophantine representations of recursively enumerable sets of particular interest.

 

To show the cofinality of primes in D0 (P), where P is the function which counts the primes below x.

 

To study subsystems of Goodstein’s Arithmetic (without quantifiers).

 

To develop families of formalized languages for presenting arithmetical texts.

 

 

 

 

 

 

 

 

3.1.3          Background & Justification for Undertaking the Project

 

Weak arithmetic is the study of problems of Number theory and Computer Science using methods of mathematical logic, just as Algebraic Number Theory or Analytic Number Theory use Algebra and Analysis.

 

Weak arithmetic was born in the 1930’s, then really emerged with a famous paper of Julia Robinson in 1949 ; Weak arithmetic has known its most famous result with the (negative) solution of Hilbert’s tenth problem in 1970 by Yuri Matiyasevich, and is involving more and more topics.

 

Works in weak arithmetic are founded on a common field of mathematical interest, a common set of questions and logical methods to investigate problems, and  a general culture within computer science. Basically, a scientist interested in weak arithmetics knows some mathematical logic, likes Peano Arithmetic and the two Gödel Theorems, works or has been working on decision problems, on algorithms and their complexities, and uses all kinds of abstract machines.

 

****

Five of the main sources of results in weaks arithmetics are undecidability of the field of rational numbers, Matiyasevich-Davis-Robinson-Putnam theorem, solving Hilbert’s tenth problem, Erdös-Woods conjecture, Buss arithmetic and study of the real exponential field.

 

**

For a first-order structure M, one denotes by DEF(M) the set of constants, functions and relations which are first-order definable within M. Following Church and Turing's proof in 1936 that the theory of natural integers equipped with addition, multiplication, and identity is not decidable, one obtains a method for proving the undecidability of the theory of a structure M which consists in showing DEF(M) = DEF(N,+, x, =). Julia Robinson has proved in 1949 than the set N of natural numbers is definable in the structure (Q,+,x,=), hence undecidability of the first-order theory of the field of rational numbers. There exist many other results in this vein. At the origin, these results were important for speculation but now we need analog result for Computer Science.

 

**

The most famous questions to have been solved in the framework of arithmetical definability is Hilbert's tenth problem; it asks for an algorithm to determine whether a given diophantine equation has a solution or, in other words whether there exists a program such that given a polynomial P(x1, … , xn) with integer coefficients as input, we can say whether the set of integer solutions of P(x1, … , xn) = 0 is nonempty. In 1970, Y. Matiyasevich proved the key-results leading to a negative answer to this  problem: exponentiation is definable by a diophantine equation, i.e. by a S1-formula within Peano Arithmetic. Of course, this result was obtained after years of research and collaboration with M. Davis, H. Putnam, J. Robinson who provide many classical theorems and conjectures.

 

This result has many generalisations for various number fields. The main question is to know whether there exists a program such that given a polynomial P(x1, … , xn) with integer coefficients as input, we can say whether the set of rational solutions of P(x1, … , xn) = 0 is nonempty. Matiyasevich and his team look at this question thirty years later.

 

**

The question of whether first-order arithmetic on the set of nonnegative integers is definable in terms of the successor function S and the coprimeness predicate ^ is a typical problem of Weak Arithmetics and perhaps, historically speaking, one of the first to be posed in this modern framework. It was raised in 1949 by Julia Robinson in her thesis, when she investigated the axiomatizability of different theories of elementary structures on numbers. More precisely, Julia Robinson stated: We might also try to improve the theorem by replacing divisibility by the relation of relative primeness. However I have not been able to determine whether x is arithmetically definable in terms of ^ and S or even in terms of ^ and +. This question, and some others of the same
nature such as the definability of all arithmetical relations in terms of addition and
coprimeness, were neglected for decades. In the eighties, Alan Woods returned
to these problems. He was the first to realize that the question of definability within mathematical logic is equivalent to the following conjecture of Number Theory: there is an integer k such that for every pair (x,y) of integers, the equality x = y holds if and only if x+i and y+i have the same prime divisors for 0
£ i £ k. This number-theoretical form of Julia Robinson’s question is itself very closely linked to some open questions proposed by Paul Erdös and for which he had conjectured a positive answer. In the book by Richard Guy entilted Unsolved Problems of Number Theory, the question is attributed to Alan Woods, but due to its close relation with conjectures of Erdös which were known to A. Woods, it is called the Woods-Erdös conjecture, or WE. This problem has been and is the subject of works from team 8.

 

**

Buss arithmetic was introduced by Buss in 1985. He considers a first-order logical language L(BA) which contains symbols for successor, addition, multiplication, constant 0, integer part of x/2, length of x, written in binary form, the  function 2|x |.|y |, identity and natural order. In this language, Buss defines a special induction-schema on certain subset of formulas providing a Weak Arithmetical theory S such that a subset A of the set N of natural integer is in the complexity class P (we may determine wether an integer belongs to A in polynomial time) if and only if it is S-provably in NP Ç co-NP. In doing so, Buss provides a promising method to prove a set A to be in P since, according to this result, it is sufficient to prove it is both NP and co-NP in some explicitly known and specific (weak) theory. Practically, if we know a set is both NP and co-NP, then the method used to prove this result certainly is not too abstract and the proof can be formalized in such a theory. However, up to now, no set has been shown in P by such a method. The main reason is that bounded arithmetics are still not widely developed. For instance we do not know which classical theorems of Number Theory are true in these Weak Arithmetics. The length of proof of any classical theorem increases greatly with weakness of the arithmetical theory in which this proof takes place. For instance, a proof of Dirichlet theorem on (infinity of) primes in arithmetical sequences in primitive recursive arithmetic PRA, a result of Cegielski in 1990, is one hundred pages long. More such results would help to apply Buss'results.

 

**

Tarski has proved in the 1920’s than the first-order theory of the structure (R,+,x,=), where R is the set of real numbers, is decidable, hence the elementary geometry is decidable. He asks the question of the status of (R,+,x,exp,=), where exp is the exponential. Recently very substantial results about this structure and this question have been obtained by Wilkie, Macintyre and others : decidability assuming Shammel’s conjecture, quantifier elimination and « o-minimality ».

 

 

 

3.1.4          Scientific/Technical Description

3.1.4.1              RESEARCH PROGRAMME

 

The proposed research consists of five tasks.

 

Task 1.- Construction of Nonstandard Models of first-order Arithmetics

The objective is to construct Nonstandard Models of first-order Arithmetics in order to investigate:

- 1) which functions and sets cannot be defined in the Arithmetic axiomatizations of subtheories of Peano Arithmetic (denoted PA) in which induction schemata are restricted to a special subset of formulas;

- 2) and what is the algorithmic complexity of those who can be defined.

This theme is closely linked, on the one hand, to the study of induction schemata which are respectively called logarithmic, open, parameter free, Sk-induction, etc. In this theme, logicians try to construct (nonstandard) models having specific properties (for example an ordered field without an integer part (Boughattas in 1996)). One tries also to prove (or disprove) some axiomatizability properties such as the fact that open-induction in normal rings is not finitely axiomatisable (Boughattas in 1996). Algorithmic Complexity theory is also connected to this theme because computability in polynomial time corresponds to some specific axiomatisations one can characterize: for instance P. Pudlak, Takeuti and Krajicek proved the equivalence between the provability in bounded arithmetic of the collapsing of the strict polynomial time hierarchy and the finite axiomatizability of this arithmetical theory in the language of addition, multiplication and x|x|.

 

Subtask 1-1.- Jean-Pierre Ressayre, Sedki Boughattas, from team 1, want to build non standard models of Buss Arithmetic and of related axiom systems. The aim is to extend the theorem of Buss and to establish some bounds on the class of NP inter co-NP which these theorems allow to solve in deterministic polynomial time. To this end they start using non standard models of the structure (R,+,.,exp,=) and the recent developments about this structure, including those of Ressayre which rely on formal power series of transfinite length.

 

          Subtask 1-2.- Members of the team 9 will work towards, which was posed by J. Paris and L. Kirby (1978) and studied by A. Wilkie and J. Paris (1989). This problem is related to the question whether or not bounded induction proves the so-called MDRP theorem.

 

Task 2.- Definability and decidability of weak substructures of the Standard Model of Peano.

In the present theme, usually one considers an arithmetical substructure M of the standard model and one tries to prove that either the whole arithmetical standard model is definable within M, or M is decidable and in this case we investigate the complexity of the considered structure. This is not an alternative: there are undecidable weak substructure of Peano where addition and multiplication are not simulteneously definable and which are undecidable. Arithmetical definability is closely related to Number Theory and, in a sense, sheds new light on its classical results. Weak Arithmetics therefore also include arithmetical decision problems such as decidable extensions of Presburger (additive) arithmetic and Skolem (multiplicative) arithmetic. The decision problem for additive prime number theory is adressed both  within Number Theory and the Theory of Automata.

 

Subtask 2.1.- There are conditional results in this field (mostly due to A. Woods and M. Boffa) under Shinzel's Hypothesis on primes. Boffa, from team 7, will explore further the additive theory of infinite sets of prime numbers and its links with number theory via the Schinzel's hypothesis. He will investigate the conjecture that this theory is undecidable in any case. Also there exists absolute results recently proved by Cegielski, Richard and Vsemirnov. The last authors (from team 1, team 2 and team 8) and the Ph.D. student Francois Heroult (from team 8) will continue to explore this way.

 

Subtask 2.2.- The directions of research of a part of team 7, in Mons University, are concerned with extensions and  generalizations of the theories of <N,+> and <N,£>. In this context, V. Bruyère, A. Maes, C. Michaux, and F. Point already have obtained definability and decidability results thanks to codings by finite automata accepting numbers written in non-classical systems. The coding problem of the addition by an automaton is not completely settled as well as the relationship between two different systems of numbers. Extensions to complex numbers and quadatric integers will be considered with a study of possible axiomatizations of the theories.

 

Subtask 2.3.- Systems of Diophantine Linear Equations and Applications.

Members of team 5 are going to develop the method of a semi-linear reservoir. Using this method, the decidability of the problem of equivalence for the meta-linear unary recursive schemata with individual constants has been already proved. They plan to prove even more strong result for ultra-linear unary recursive schemata (with individual constants), namely to show that the problem above can be expressed in the Presburger Arithmetic.

They hope to find new applications of the decidability of the universal theory of addition and decidability in the automata theory and schematology. (Namely, for two-way automata with one finite-turned counter this result can be generalized to the models connected with the calculations over infinite labeled trees.)

They also plan to obtain results on undecidability for finite substitutions over regular languages. The equivalence problem of finite substitutions on regular languages is undecidable (L. Lisovik). They will investigate this problem over bounded regular languages, for instance over the language ab*c.

 

Subtask 2-4.- Decidability results for S2S[P]  theories.

Members of team 5 plan to obtain the decidability results for S2S[P]  theories (i.e. for monadic second order arithmetic of  two successors with extra unary predicate).

 

Subtask 2-5.- Formal constructive theories.

Members of team 3 and Henri-Alex Esbelin, from team 8, want to develop a method of building formal constructive theories with the following properties:

1. The task of finding proofs in these theories is tractable ;

2. The algorithms that can be extracted from these proofs belong to some known small subrecursive classes (from Grzegorczyk hierarchy) and to some analogs of these classes for word and tree functions ;

3. with applications to databases.

Also Esbelin, from team 8, searches properties of reals definable by subrecursive classes, particularly rudimentary reals.

 

 

 

 

 

 

 

Task 3.- Abstract Machines, Automata and Words.

Any program in a specified language which we use in a computer has a corresponding abstract machine, for instance a Turing machine. Actually, we can formalize any program because with addition and multiplication we can define (or simulate) all recursive schemata. Now if we  consider only some Weak Arithmetics (for instance Presburger Arithmetic) then a corresponding abstract machine computing functions and relations definable in this theory, or in a model of this one, is of course weaker than a Turing Machine (for instance it is a finite automaton for Presburger Arithmetic). In this way, it is natural to associate abstract machines (Finite Automata, Pushdown Automata, Cellular Automata, Beltiukov Machines, Alternating Turing Machines, etc) with  different weak arithmetical theories and to the models we investigate.

To this theme also belong general coding theory and all problems of weak arithmetical structures consisting of the usual integers with pairing functions (such as Cantor pairing polynomial) or codings of n-tuples (using for example the well-known beta-function of Godel). Machines as tools for solving problems of definability or decidability were used by I. Korec, from Slovakia, A. Bès, V. Bruyère, C. Michaux, from Belgium, J.E. Pin, J. Tomasik, etc. Machines are not only tools but are themselves the objects of investigation such as for instance the Matiyasevich machines introduced to solve problems of trace monoid.

 

          Subtask 3-1.- Ressayre and Finkel, from team 1, want to explore the relation between Infinite games, automata, and arithmetic. For various classes of machines (for instance push down and blind counter automata), they study which infinite games accepted by a machine have winning strategies that can be performed by a machine of the same class. This has applications to processor synthesis, and to the decidability of extensions of monadic second order arithmetic.

 

          Subtask 3-2.- BSS model of computation A part of team 7, explores the Blum, Shub, and Smale model of computation for which strong links with weak arithmetics and relative complexity questions were proved (S. Smale, H. Fournier, P. Koiran). A first research plan is the study of the fine structure of the BSS recursive enumerable sets. This work was initiated by C. Michaux and C. Troestler with a characterization of the isomorphism type of these sets. A second research project is the continuation of the work of J.-S. Gakwaya on the extension of the Grzegorczyk hierarchy to BSS recursive functions and relations. Separation of some small classes of complexity for this hierarchy in relation to the classical open problem for small classes of the Grzegorczyk hierarchy will be studied. A third theme is related to works of C. Michaux on the P=NP problem. It is planned to investigate how some notions of classical complexity for polynomials are related to the P=NP question. This will begin by a study of some differential structures for the solutions of liouvillian differential equations (as a part of future PhD work by C. Rivière).

 

          Subtask 3-3.- Yuri Shoukourian and K. V. Shakhbazyan, from team 4, are in charge of investigating concurrent processes in distributed conveyer systems and their relation with corresponding weak arithmetics.

 

          Subtask 3-4.- D. Beauquier and A. Slissenko, from team 1, will work on verification of real-time distributed systems in a logical framework in several directions:
- development of efficient heuristic algorithms for a practical verification and its implementation (a russian PhD student will work on this topic with a fellowship given by  french government for a joint supervision) ;

- extension of the logical framework in order to include the treatment of system’s behavior uncertainty.


Subtask 3-5.- Classification of real functions.

Members of team 5 were going to explore the classification of real functions according to the type of the memory of "optimal" machines, which define the functions, particularly, to obtain new results about the connections between the memory structure of a transducer and differentiability of the corresponding function. The finite transducers defining the nowhere differentiable functions and Peano curve with the overlapping coefficient 3 already have been constructed. It has been shown that the class of functions differentiable on a given interval and defined by a push-down binary transducer is included in the class of functions linear on the interval. They plan to generalize this fact to the stack transducers and explore the situation for the k-nested stack transducers.

 

Subtask 3-6.- Counting classes

A. Durand (from team 1), H.A. Esbelin and M. More (both from team 8) investigate the power of counting in very small complexity classes and in the corresponding logical or arithmetical settings. Counting is a basic natural algorithmic operation, and the counting ability of a small class of predicates or problems is a good measure of its expressive or computing power. More precisely, on the one hand, these researchers look for robust and convenient abstract machine characterizations of closure under counting of weak arithmetical classes (such as the rudimentary relations). On the other hand, they also intend to determine logical counterparts of small complexity classes involving counting (such as #TC0, the closure under counting of the class of circuits families with bounded height with majority gates). Finally, they study the possible closure of various weak arithmetical classes under various weakened forms of counting (eg. modular counting).

 

Subtask 3-7.- Jerzy Tomasik and Malika More, from team 8, will investigate methods from classical model theory, fusion theory and multihead automata in order to improve some lower bounds in circuit complexity and examine their links with small
complexity classes.

 

Subtask 3-8.- Purposes of members of team 2 is

1) To study definability and decidability problems for weak theories of integers and polynomial rings. For this purpose both number-theoretic and logical methods will be used (Vsemirnov).

2) To construct Diophantine representations of recursively enumerable sets of particular interest (Vsemirnov, Matiyasevich).

3) To study properties of sets of pseudoprimes defined by formulas with small number of quantifiers (Eterevsky).

4) To construct universal self-delimiting exponential Diophantine equation; such equations are of interest in algorithmic infomation theory developed by G. J. Chaitin (Matiyasevich).

Task 4.- Elementary proofs of classical Number Theory results.

Arithmetical Proof Theory stems from the work Erdös and Selfridge who were the first to ask for what they called elementary proofs (i.e. in the framework of real analysis instead of complex analysis) of results such as the Dirichlet Theorem on the infinity of primes in arithmetical sequences. Logicians such as Takeuti, Kreisel and Simpson (with his reverse mathematics) have contributed to the subject but in a general way. P. Cegielski and O. Sudac have constructed proofs for specific classical theorems (such as the Prime Number Theorem of De La Vallée Poussin). They have also  constructed some first order denumerable structures modelling a version of Peano Analysis to provide proofs within Peano Arithmetic models or even within the standard model of weaker arithmetical theories (e.g. PRA, the Primitive Recursive Arithmetic). It is clear that this work should be continued in order to strengthen the tools developed by Buss.

 

Subtask 4-1.- Let D0 be the subsystem of Peano Arithmetic (PA) where induction is applied only to formulas with bounded quantifiers. It is well known that in D0 the exponential function is not provably total. This is the main obstacle in reproducing elementary number theory in D0, whose interest is motivated by its connections with complexity theory.

The study of classical results of number theory in D0 requires a fine analysis of the classical proofs and gives many computational information. In some cases new proofs are required and functions of exponential growth are substituted by some combinatorial principles of pigeon hole type. This principle is available in the theory D0 + W1, where the axiom W1 guarantees the totality of the function xlog2 y. The following classical results where proved in th D0 + W1:

1) cofinality of primes, proved by Woods ;

2) Lagrange’s theorem, proved by Berarducci and Intrigila;

3) existence and uniqueness of an extension of every finite degree for a residue field of a model of D0 + W1, proved by D'Aquino and Macintyre.

Team 6 and team 9 plan to improve Woods result by showing the cofinality of primes in the system theory D0 (P) which is obtained by adding a new function symbol P to the language of arithmetic (which has to be thought as the function which counts the primes below x) and considering D0 -induction in the expanded language. A partial result towards proving the conjecture is due to Cornaros (1996).

The quadratic reciprocity law is one of the most celebrated theorems of classical number theory. There exist many proofs of this classical result but all of them seem to require functions which grow exponentially. Analysis of Gauss'second proof, in which he uses quadratic forms of given discriminant and finiteness of class number, is under way. For primes p,q equiv 3 (mod 4) we have already a proof in D0 + W1. It appears one can obtain a local result relating correctness of quadratic reciprocity law for p,q to solvability of Pell equation x2 – d.y2 =1,where d is one of p,pq, or a small multiple of them.

In connection with 3) above team 6 plan to study curves over residue fields of models of D0 + W1, in order to show that they are pseudofinite, i.e. perfect, they have a unique extension of each degree and every absolutely irreducible curve has a point in it. (This was proved by Macintyre for residue fields of models of PA.) In this context we plan also to study Chevalley theorem over models of D0 or D0 + W1.

 

Subtask 4-2.- Subsystem and Modifications of Goodstein’s Arithmetics; their application to the Logical Programming

The objective is the study of subsystems of R.L.Goodstein’s Arithmetic (without quantifiers) based on the A.Grzegorczyk’s scheme of bounded recursion and on the modified scheme of bounded recursion relating to the words in a fixed alphabet, the study of the arithmetical systems based on the corresponding classes of functions and predicates with some restrictions to the induction scheme, the comparison of the possibilities of such systems and of the complexity of logical deductions in them, the comparison of these systems with the systems based on the rudimentary and s-rudimentary predicates of R.M. Smullyan, the study of corresponding systems of Logical Programming, and the study of the modifications of these systems based on many-valued logic.

Team 4 and Esbelin, from team 8, are in charge of this task

 

Task 5.- Weak arithmetics, Pure and Computational Logic.

 

          Subtask 5-1.- Nezondet's p-destinies.

It is mainly concerned with Nezondet's p-destinies which are a general tool founded on trees for deciding closed sentences within theories consisting of a set of sentences in a relational language which have a bounded number of quantifiers. When applied to weak arithmetical theories, this promising new method gives rise to many interesting new questions in Number Theory (M. Guillaume, JeLei Yin, D. Richard). In addition, the computation of a p-destiny, when successfully carried out, effectively generates a finite structure, namely a set of labelles trees. This structure exactly encodes the necessary and sufficient information for deciding the sentences of the considered theory. The decision algorithms such obtained are expected to be efficient and useful in databases theory as well as in descriptive complexity. Denis Richard and Annie Château, from team 8, intend to develop the applications of p-destinies to weak arithmetical theories, as well in its number theoretic implications as in its connexions with theoretical Computer Science.


Subtask 5-2.- Computational Logic.

Members of team 5 and K. Verchinine, from team 1, will investigate:

- development of families of formalized languages for presenting mathematical texts in a form the most appropriate for a user: the languages must be used as  tools to write and verify mathematical publications and as the universal interfaces of declarative mathematical knowledge;

- formalization and evolutionary development of computer-made prover: computer-oriented sequent methods will be constructed for classical and intuitionistic logics, which will be reflect linguistic peculiarities of declarative mathematical knowledge and will use results of Computational Logic and Arithmetic; these methods should satisfy the following requirements: syntactical form of the initial problem should be preserved; deduction should be done in the signature of initial theory, proof search should be goal oriented, definition and lemma applications should be incorporated in deductions as unique rules, equality handling should be separated from deductive processes;

- combining deduction steps with arithmetical calculations and symbolic transformations.

 

 


3.1.4.2              REPORTING, EXPLOITATION & DISSEMINATION OF RESULTS

 

Of course normal discussions from distant members of different teams will be by e-mail but we expect a workshop every year to present results and, mainly, lively discussions. Normal dissemination will consist of papers in reviews (Journal of Symbolic Logic, Theoretical Computer Science, Annals of Pure and Applied Logic…). Also we expect to publish communications either in a special issue of a review or as a Lecture Note in Mathematics (Springer).

 

 

 


 

3.1.5         Description of the Consortium

3.1.5.1         RESEARCH TEAMS

 

TEAM 1: Université de Paris (France)

 

Indeed `université de Paris’ is used for three universities. Members are Patrick Cegielski, Danièle Beauquier, Anatole Slissenko, and Konstantin Verchinine, Professors at université Paris XII, Arnaud Durand and Tristan Crolard, lecturers at université Paris XII, Irène Guessarian, Professor at université Paris VI, Jean-Pierre Ressayre, Directeur de recherche (analog of Professor at CNRS) at université Paris VII, Serge Grigorieff, Professor at université Paris VII, Sedki Boughattas, lecturer at université Paris VII, Olivier Finkel, Eugenio Chinchilla, and A. Rambaud, from université Paris VII.

 

Team 1 is involved in subtasks 1-2, 2-1, 3-1, 3-4, 3-6, and 5-2.

 

TEAM 2: Saint-Petersburg (Russia)

 

Members are Yuri Matiyasevich (doctor of science) and Maxim Vsemirnov (candidate, researcher, born in 1972), from Steklov Institute of Mathematics at St.Petersburg, Russia, and Oleg Eterevsky, student at St.Petersburg State University, born in 1981.

 

Team 2 is involved in subtasks 2-1 and 3-8.


TEAM 3: Udmurt University (mathematics faculty, software chair), Russia.

 

Members are Anatoly Petrovich Beltiukov, Professor, Vyacheslav Viktorovich Pupyshev, born in 1970, senior lecturer, Tatiana Gennadievna Azhimova, born in 1964, senior lecturer, and Evgeny Valerievich Fadeev, born in 1977, postgraduate student.

 

Team 3 is involved in subtask 2-5.

 

TEAM 4: Yerevan (Armenia)

 

Members are Yuri Shoukourian, doctor of sciences, Professor, head of department, director of IIAP (Institute for Informatics and Automation Problems), Igor Zaslavsky, doctor of sciences, Professor, head of department, deputy director of IIAP, Karine Shakhbazyan, candidate of sciences, senior scientific researcher at IIAP, Mikael Khachatryan, candidate of sciences, senior scientific researcher at IIAP, Seda Manukian, candidate of sciences, senior scientific researcher at IIAP, Vahagn Khachatryan, born in 1978, post-graduate student (magistrant) at Yerevan State University, junior scientific researcher at IIAP, and Karen Hambartzumyan, born in 1972, candidate of sciences, junior researcher at IIAP.

 

Team 4 is involved in subtasks 3-3 and 4-2.

 

 

 

 

 

TEAM 5: Kiev (Ukraine)

 

Members are Alexander Lyaletski, senior research scientist at Kiev University, Leonid Lisovik,  Professor at Kiev University, Marina Morochovets, senior research scientist at  Glushkov Institute of Cybernetics, Olga Shkaravskaya, assistant-professor at Kiev University (born in 1969), and Andrei Paskevych, MSc student at Kiev University (born in 1979).

 

Team 5 is involved in subtasks 2-3, 2-4, 3-5, and 5-2.

 

TEAM 6: Naples (Italy)

 

Members are Paola D’Aquino, senior researcher at Second University of Naples, Alessandro Berarducci, Professor at University of Pisa, Domenico Zambella, senior researcher at University of Torino, and Andrea Vietri, graduate student at University of Roma, "La Sapienza" (31 year old).

 

Team 6 is involved in subtask 4-1.

 

TEAM 7: Université de Mons-Hainaut (Belgium)

 

Members are Maurice Boffa, Véronique Bruyère, and Christophe Troestler (29 year old), both Professor at université de Mons, Christian Michaux, associate Professor, Francoise Point, Senior Research Associate, Jean-Sylvestre Gakwaya (29 year old) and Arnaud Maes (27 year old), both Post-Doctoral researcher, and Cédric Rivière (22 year old), PhD Student.

 

Team 7 is involved in subtasks 2-1, 2-2, and 3-2.

 

TEAM 8: Université de Clermont-Ferrand (France)

 

Members are Denis Richard (Professor), Jersy Tomasik (senior lecturer), Henri-Alex Esbelin (lecturer), Malika More (lecturer), Annie Château, and François Heroult.

 

Team 8 is involved in subtasks 2-1, 5-1, 2-5, 3-6, 3-7, and 4-2.


TEAM 9: University of Athens (Greece)


Members are Constantinos Dimitracopoulos, Associate professor at University of Athens, Michael Mytilinaios, Associate professor at Athens University of Economics and Business, Thanases Pheidas, Associate professor at University of Crete, Konstantinos Hatzikiriakou, Assistant professor at University of Thessaly, Charalampos Cornaros, Researcher at University of Athens, and Chrysovalantis Verykios, Graduate student at University of Athens, born in 1974.

 

Team 9 is involved in subtasks 1-2 and 4-1.

 

 

 

 


 

3.1.5.2              SCIENTIFIC REFERENCES

 

TEAM 1

 

1. Danièle Beauquier and Anatole Slissenko, A., A First Order Logic for Specification of Timed Algorithms: Basic Properties and a Decidable Class, to appear in Annals of Pure and Applied Logic.

 

2. Sedki Boughattas, L'induction ouverte dans les anneaux discrets ordonnés et  normaux n'est pas finiment axiomatisable (French) [Open induction in ordered and normal discrete rings is not finitely axiomatizable], J. London Math. Soc. (2) 53 (1996), no. 3, 455-463.

 

3. Patrick Cegielski, Definability, decidability and complexity, Annals of Mathematics on Artificial Intelligence 111, 1996,  pp. 311-341.

 

4. Eugenio Chinchilla, A model of R_2_# inside a subexponential time resource, Notre Dame J. Formal Logic 39 (1998), no. 3, 307-324.

 

5. Arnaud Durand, Claus Lauteman, and Thomas Schwentick, Subclasses of Binary-NP, Journal of Logic and Computation, vol. 8(2), 1998, pp. 189-207.


6. Olivier Finkel and Jean-Pierre Ressayre, Stretchings, J. Symbolic Logic 61 (1996), no. 2, 563-585.


7. Jean-Pierre Ressayre, Polynomial time uniformization and non-standard methods, Ann. Math. Artificial Intelligence 16 (1996), no. 1-4, 75-88.

 

See also joint works in team 2 (papers 4, 7, 8) and 8 (papers 1, 2).

 

TEAM 2

 

1. M.A. Vsemirnov, Infinite sets of primes that admit Diophantine representations in eight
variables
, Zapiski Naychnukh Seminarov POMI, 220 (1995), pp. 36-48. (in Russian).
English translation: Journal of Mathematical Sciences. 87 (1997), no.1, pp. 3200-3208.

2. M.A. Vsemirnov, Diophantine representations of linear recurrent sequences. I, Zapiski Naychnukh Seminarov POMI, 227 (1995), pp. 52-60. (in Russian). English translation: Journal of Mathematical Sciences, 89 (1998), no.2, pp.1113-1118.


3. M.A. Vsemirnov, Diophantine representations of linear recurrent sequences. II,
Zapiski Naychnukh Seminarov POMI, 241(1997), pp.5-29. (in Russian). English translation: Journal of Mathematical Sciences.

 

4. Patrick Cegielski, Denis Richard, and Maxim A. Vsemirnov, On the additive theory of primes. LLAIC, Universite d'Auvergne - Clermont 1, Preprint No. 78 (1999), to appear in The Journal of Symbolic Logic.


5. M.A. Vsemirnov, Woods-Erdos conjecture for polynomial rings, to appear in Annals of Pure and Applied Logic.


6. Yu. Matiyasevich, A new technique for obtaining Diophantine representations via elimination of bounded universal quantifiers, Zapiski Nauchnykh Seminarov POMI, vol. 220, pp. 83-92, 1995.


7. Patrick Cegielski, Yuri Matiyasevich, and Denis Richard, Definability and decidability is­sues in extensions of the integers with the divisibility predicate, The Journal of Symbolic Logic, vol. 61,  June 1996, pp.515-540.


8. Luc Boasson, Patrick Cegielski, Irène Guessarian, and Yuri Matiyasevich, Window-Accumulated Subsequence matching Problem is linear, PODS’99 (Principle Of Databases Systems), ACM Press, pp. 327-336.


9. Yuri Matiyasevich, Hilbert's tenth problem: A two-way bridge between number theory and computer science, People and Ideas in Theoretical Computer Science, C. S. Calude, editor, Springer-Verlag, Singapore, 1999, pp. 177-204.


10. Maurice Margenstern and Yuri Matiyasevich, A binomial representation of the 3x+1 problem, Acta Arithmetica, vol.
XCI.4, 1999, pp. 367-378.

 

TEAM 3

 

1. A.P. Beljtjukov, Tractable tasks of deductive algorithms synthesis, Abstracts of second international conference "Mathematical algorithms", NNSU publishers, Nizhni Novgorod, 1995, pp.9-10.


2. A.P. Beljtjukov, Word stack register machines, Logic Colloquium'95 Abstracts, Finite Model Theory and Computer Science, Haifa, Technion, 1995, p.31.


3. A.P. Beljtjukov, Hierarchy of Small Subrecursive Classes Based on Bounded Simultaneous Recursion, Logic Colloquium'96, San-Sebastian,1996, p. 98.


4. A.P. Beltiukov, Hierarchy of Small Subrecursive Operator Classes Based on Bounded Recursion, Logic Colloquium'97, University of Leeds, 6th-13 July, 1997, Abstracts, 1997, p.11.


5. A.P. Beltiukov, Intuitionistic formal theories with realizability in subrecursive classes, Annals of Pure and Applied Logic, 89, 1997, p. 3-15.


6. A.P. Beltiukov, One-way one-dimensional cellular automata and small subrecursive classes, Proceedings of JAF'15 (Fifteenth Days of Weak Arithmetic), University of Mons-Hainaut, December 11-12, 1997, Mons, Belgium, 1998, pp. 21-27.


7. A.P. Beltiukov, Alternating time complexity bounds for protothetics, Logic Colloquium'98 The 1998 ASL European Summer Meeting, August 9-15, 1998, Prague, Chech Republic, 1998, p.81.

 
8. A.P. Beltiukov, Smullyan Rudimentary Predicates and Skolem Elementary Functions on Trees, Logic Colloquium 2000, Paris 2000.

 

 

 

 

TEAM 4

 

1. Y. Shoukourian and K. Schakbazyan, On the recognition of languages in free semilattices, Kibernetika, vol. 2, Kiev, 1996, pp. 179-182.

 

2. Y. Shoukourian, Parallelization of Automata, Cybernetics and System Analysis, vol. 34, n° 4, 1998, pp. 540-544 [translation of Kibernetika I Sistemnyi Analiz, n° 4, pp. 78-84].

 

3. Y. Shoukourian and K. V. Shakhbazyan, On process Languages in Finite Graphs, Proceedings of Sci. Seminar of Petersburg Branch of Math. Institute, vol. 248, 1998, pp. 205-215.

 

4. Y. Shoukourian and K. Shakhbazyan, Distributed Conveyor Processing of Data Streams, Proceedings of the Conference CSIT-99, Yerevan, 1999, pp. 9-12.

 

5. I.D. Zaslavsky, Dual realizability in symmetric logic, to appear in Annals of Pure and Applied Logic.


6. I.D. Zaslavsky, On the theory of constructive reducibility, Proceedings of Intern. Conference on Computer Science and Information Technologies (CSIT`97), Yerevan, pp.10-11 (1997).

 

7. I.D. Zaslavsky, The realization of three-valued logical functions by recursive and Turing operators, Selecta Mathematic Sovetica, Vol.7, N1, Birkhäuser Verlag, pp. 15-22 (1988).

 

8. I.D.Zaslavsky, On logically but not functionally complete calculus in three-valued logic, The Tbilisi Symposium on Logic, Language and Computation, Selected papers, CSLI Publications, Stanford, California, pp.309-313 (1998).

 

9. M.A. Khachatryan, Sequent calculus with restricted antecedent and succedent, Proceedings of the Intern. Conference on Comp.Science and Informational Technologies (CSIT’97), Yerevan, pp.12-14 (1997).

 

10. S.N.Manukian, On the structure of the recursive enumerable fuzzy sets, Proceedings of IIAP of  National Acad. Sci. Armenia and Yer. State University, vol.17, pp.86-91 (1997). (in Russian).

 

TEAM 5

 

1. Lyaletski, A., A sequent formalism and deductive systems for 1st-order classical logic, Proc. of Intern. Conf. ``Logic and Applications'', Novosibirsk, Russia (2000).


2. A. Lyaletski and M. Morokhovets, On principles of proof search and  construction of mathematical knowledge bases in the Evidence, Algorithm, Proc. of the International Congress IMACS'2000, Switzerland, 2000.

 

3. A. Lyaletski and M. Morokhovets, On linguistic aspects of integration of computer mathematical knowledge, CALCULEMUS Workshop, Trento, Italy, 1999, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 23, issue 3, 1999, p. 165-178.


4. A.I. Degtyarev, A.V. Lyaletski, and M.K. Morokhovets, On the EA-style integrated processing of self-contained mathematical texts, Proc. of the International Workshop CALCULEMUS'2000, Great Britain, 2000.


5. A.I. Degtyarev, A.V. Lyaletski, and M.K. Morokhovets, Evidence Algorithm and Sequent Logical Inference Search, Springer, Lecture Notes in Artificial Intelligence, Vol.1705, 1999, pp.44-61.

 

6. A.I. Lyaletski, On Herbrand theorem, Proc. of the European Congress of the Association for Symbolic Logic of the millennium, Sorbonne, Paris, 2000, to appear in Bulletin of Symbolic Logic.

 

7. L.P. Lisovik, Hard sets methods and semilinear reservoir method, with application (Review), Springer, Lecture Notes in Computer Science, Vol. 1099, 1996, pp. 219-231.

 

8. L.P. Lisovik, Nondeterministic systems and finite substitutions on regular laguages, Bulletin of European Association for Theoretical Computer Science, v. 63, 1997, pp. 156-160.

 

9. J. Karhumaki and L.P. Lisovik, On the equivalence of finite substitutions and transducers, Jewels are Forever  (dedicated to the 65th anniversary of A. Salomaa), Springer, 1999, pp.  97-108.

 

10. L.P. Lisovik and O.Yu. Shkaravskaya, On the Real Functions Defined by Transducers, Kibernetika i Sistemny Analiz, No 1, 1998, pp. 82-93.

 

TEAM 6

 

1. Alessandro Berarducci and Benedetto Intrigila, Linear recurrence relations are D0-definable, Logic and Foundations of Mathematics, Selected contributed papers, LMPS '95 (A.Cantini, E.Casari, P.Minari editors), Kluwer Academic Publishers, Dordrecht, The Netherlands, 1999, 67-81.

 

2. Alessandro Berarducci, Factorization in generalized power series, Transactions of AMS, Vol. 352, N. 2 (1999) 553-557.

 

3. Alessandro Berarducci and Margarita Otero, Intersection theory for o-minimal manifolds, to appear in Annals of Pure and Applied Logic.

 

4. Paola D’Aquino, Towards the limits to the Tennenbaum phenomenon, Notre Dame Journal of Formal Logic, 38, 1997, pp. 81-92.

 

5. Paola D’Aquino, Solving Pell equations locally in models of ID0, Journal of Symbolic Logic, vol 63, 1998, pp. 402-410.

 

6. Paola D’Aquino and Angus Macintyre, Non standard finite fields over ID0+W1, Israel Journal of Mathematics 117 (2000), pp. 311-333.

 

7. Paola D’Aquino, Quotient fields of a model of ID0+W1, to appear in Mathematical Logic Quarterly.

 

8. D. Zambella, Foundation versus induction in Kripke-Platek set theory, Journal of Symbolic Logic 63 (1998), no.4, pp. 1399-1403.

 

9. D. Zambella, End extensions of models of linearly bounded arithmetic, Annals of Pure and  Applied Logic  88  (1997), no.2-3, pp. 263-277.

 

10. D. Zambella, Algebraic methods and bounded formulas, Notre Dame J. Formal Logic 38 (1997), no. 1, pp. 37-48.

 

TEAM 7

 

1. M. Boffa, More on a undecidability result of Bateman, Jockusch and Woods, Journal of Symbolic Logic 63 (1998), p. 50.


2. A. Maes, An automata theoretic decidability proof for the first-order theory of <N;<,P> with morphic predicate P, Journal of Automata, Languages and Combinatorics, 4 (1999), p. 229-245.


3. A. Maes, Revisiting Semënov's results about decidability of extensions of Presburger Arithmetic, Definabillity in Arithmetics and Computability, Cahiers du Centre de Logique 11 (2000) p. 11-59.

 

4. V. Bruyère and G. Hansel, Bertrand numeration systems and recognizability, Theoret. Comput. Sci. 181 (1997) 17-43.


5. S. Ben-David, K. Meer, and C. Michaux, A note on Non-Complete Problems in NPR, The Journal of Complexity 16 (2000), p. 324-332.

 

6. J.-S. Gakwaya, Extended Grzegorczyk's Hierarchy in the BSS model of computability, FoCM'97, F. Cucker - M. Shub Eds, Springer Verlag (1997), p. 127-151.

 

7. C. Michaux and R. Villemaire, Presburger arithmetic and recognizability of sets of natural numbers by automata: New proofs of Cobham's and Semenov's theorem, Annals of Pure and Applied Logic 77 (1996), p. 251-277.

 

8. C. Michaux and C. Troestler, Isomorphism Theorem for BSS Recursively Enumerable Sets over Real Closed Fields, Theoretical Computer Science 231 (2000), 253-273.


9. F. Point and V. Bruyère, On the Cobham-Semenov theorem, Theory Computer Systems, 30 (1997), p. 197-220.


10. F. Point, On decidable extensions of Presburger arithmetic: From A. Bertrand numeration systems to Pisot numbers, to appear in J. Symb. Logic.

 

TEAM 8

 

1. Patrick Cegielski and Denis Richard, Decidability of natural integers equipped with Cantor pairing function and successor, to appear in Theoretical Computer Science.

 

2. Patrick Cegielski and Denis Richard, On arithmetical first-order theories allowing encoding and decoding of lists, Theoretical Computer Science, vol. 222, 1999, pp. 55-75.

 

3. Henri-Alex Esbelin, Counting modulo semi-groups, to appear in Theoretical Computer Science.


4. Henri-Alex Esbelin and Malika More, Rudimentary relations and primitive recursion : a toolbox, Theoretical Computer Science 193 (1998) 129-148.

 

5. M. Kokar and Jerzy Tomasik, Towards a goal-driven autonomous fusion system,
Proc. International Conference on Information Fusion FUSION'99 July 6-8, 1999, Sunnyvale, CA (Org. NASA, IEEE, ISIF) Vol. 1, pp. 148-153.


6. M. Kokar, Jerzy Tomasik, and J. Weyman, A formal approach to information fusion, Proc. International Conference on Information Fusion FUSION'99 July 6-8, 1999, Sunnyvale, CA (Org. NASA, IEEE, ISIF) Vol. 1, pp. 133-142.


7. Rémy Malgouyres and Malika More, On the computational complexity of basic problems of 2D digital topology, to appear in Theoretical Computer Science.


8. Malika More and Frédéric Olive, Rudimentary languages and second-order logic, Mathematical Logic Quarterly 43 (1997) 419-426


9. Jerzy Tomasik, Discrete Dynamic approach to multisensory multirack fusion, Proc. AeroSense'2000, April 25-28, 2000, Orlando, Florida, Vol. 4051, pp. 369-379.


TEAM 9


1. Ch. Cornaros, On Grzegorczyk induction, Annals of Pure and Applied Logic 74 (1995), 1-21.

 

2. Ch. Cornaros & C. Dimitracopoulos, A note on end extensions, Arch. Math. Logic 39 (2000), 459-463.

 

3. K. Hatzikiriakou, WKL0 and Stone's separation theorem for convex sets, Ann. Pure Appl. Logic 77 (1996), 245-249.

 

4. M. J. Groszek, M. E. Mytilinaios & T. A. Slaman, The Sacks Density Theorem and S2-Bounding, J. Symbolic Logic 61 (1996), 450-467.

 

5. M. E. Mytilinaios & T. A. Slaman, On a question of Brown and Simpson, in "Computability, Enumerability, Unsolvability. Directions in Recursion Theory", Cambridge University Press, 1996, 205-218.

 

6. L. Lipshitz & Th. Pheidas, An analogue of Hilbert's Tenth Problem for p-adic functions, J. Symbolic Logic 60 (1995), 1301-1309.

 

 


 

3.1.6          Management

 

Main exchanges are by e-mail but we plan two workshops (a local one and a general) by year, two co-ordination meeting and exchanges of scientists (already are planned visits of a student of team 2 and one of team 5 in team 1).

 

 
3.1.6.1         PLANNING & TASKS ALLOCATION

 

Tasks
Teams
Months
1-6
Months
7-12
Months
13-18
Month
19-24
Months
25-30
Months
31-36
 
 
 
 
 
 
 
 
T1.1
Team 1
 
 
 
 
 
 
T1.2
Team 9
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
T2.1
Team 7,1,2,8
 
 
 
 
 
 
T2.2
Team 7
 
 
 
 
 
 
T2.3
Team 5
 
 
 
 
 
 
T2.4
Team 5
 
 
 
 
 
 
 
T2.5
Team 3,8
 
 
 
 
 
 
 
 
 
 
 
 
 
 
T3.1
Team 1
 
 
 
 
 
 
T3.2
Team 7
 
 
 
 
 
 
T3.3
Team 4
 
 
 
 
 
 
T3.4
Team 1
 
 
 
 
 
 
T3.5
Team 5
 
 
 
 
 
 
T3.6
Team 1,8
 
 
 
 
 
 
T3.7
Team 8
 
 
 
 
 
 

 

T3.8
Team 2
 
 
 
 
 
 
 
 
 
 
 
 
 
 
T4.1
Team 6,9
 
 
 
 
 
 
 
T4.2
Team 4,8
 
 
 
 
 
 
 
 

 

 
 
 
 
 
 
 
 
T5.1
Team 8
 
 
 
 
 
 
 
T5.2
Team 5,1
 
 
 
 
 
 
 
 

 

 

 

3.1.7 SUMMARY

 

 

Weak arithmetic is the study of problems of Number theory and Computer Science using methods of mathematical logic, just as Algebraic Number Theory or Analytic Number Theory use Algebra and Analysis. Five of the main sources of results in weaks arithmetics are undecidability of the field of rational numbers, Matiyasevich-Davis-Robinson-Putnam theorem, solving Hilbert’s tenth problem, Erdös-Woods conjecture, Buss arithmetic and study of the real exponential field.

 

The proposed project is constituted of nine teams from university of Paris, Steklov Institute of Mathematics at Saint-Petersburg (Russia), Udmurt University (Russia), Institute for Informatics and Automaton Problems at Yerevan (Armenia), Kiev University (Ukraine), University of Naples (Italy), university of Mons-Hainaut (Belgium), university of Clermont-Ferrand (France), and University of Athens (Greece).

 

Objectives for the three years were : to construct Nonstandard Models of Buss Arithmetic to establish some bounds on the class NP inter co-NP ; to solve the problem of existence of end extensions of countable models of bounded collection ; to explore further the additive theory of infinite sets of prime numbers, both with absolute results and its links with number theory via the Schinzel's hypothesis ; to code natural numbers, complex numbers, and quadratic integers by automata accepting numbers (written in non-classical systems) ; to prove results for ultra-linear unary recursive schemata (with individual constants); to obtain decidability results for S2S[P]  theories ; to build formal constructive theories with (from Grzegorczyk hierarchy) with applications to databases ; to investigate the power of counting in very small complexity classes and in the corresponding logical or arithmetical settings ; to explore the relation between Infinite games, automata, and arithmetic ; to study the fine structure of the BSS recursive enumerable sets ; to investigate concurrent processes in distributed conveyer systems and their relation with corresponding weak arithmetics; to construct Diophantine representations of recursively enumerable sets of particular interest ; to show the cofinality of primes in D0 (P), where P is the function which counts the primes below x ; to study subsystems of Goodstein’s Arithmetic (without quantifiers) ; to develop families of formalized languages for presenting arithmetical texts.

 

Main exchanges are by e-mail but it is planning two workshops (a local one and a general) by year, two co-ordination meeting and exchanges of scientists.