On the completeness properties of the systems of symmetric construstive and three-valued logic
by
I..D. Zaslavsky
Institute for Informatics and Automation Problems, National Academy of Sciences of Armenia

On the completeness properties of the systems of symmetric constructive and three-valued logic Zaslavsky I.D. Institute of Informatics and Automation Problems of ANAS and YSU EXTENDED ABSTRACT Formal systems HS (symmetric constructive predicate calculus), HL (three-valued predicate calculus) and the corresponding arithmetical systems HSA, HLA are defined as in [1]; the system HSAD is defined as in [2]. It was proved in [2] that the system HSAD is equivalent to the system HSAR+ considered in [1]. The list of systems (HS, HL, HSA, HLA, HSAD) will be denoted below as the main list. For every system in this list we define the corresponding extended system as follows: the propositional symbol E is added to the language of the given system and the axiom (E contains not E) ( not E contains E) is added to the set of its axioms. The list of systems (HSE, HLE, HSEA, HLEA, HSEAD) obtained by such extending will be denoted below shortly as Extlist. The union of the main list and the Extlist will be denoted as Genlist; it contains 4 logical (HS, HL, HSE, HLE) and 6 arithmetical systems (HSA, HLA, HSAD, HSEA, HLEA, HSEAD). The calculi HLE and HLEA were considered in [3], [4], [5]. Below denotes one of the systems belonging to Genlist. The notion of Luk-completeness is defined as in [5]; a formal system of the kind mentioned above is said to be Luk-complete if for every closed formula F the following statement holds: either F, or not F, or (F contains not F) ( not F contains F) is deducible in . In the opposite case is said to be Luk-incomplete. The notion of consistency is interpreted in an usual way: the system is said to be consistent if no formula F is deducible in simultaneously with not F; in the opposite case is said to be inconsistent. A system is said to be effectively Luk-incomplete if for every recursively enumerable consistent extension of a closed formula F can be effectively constructed such that neither F, nor not F, nor (F contains not F) ( not F contains F) is deducible in . The notion of essential undefinability is defined as in [1]. Namely, the formula F is said to be essentially undefinable in the system if the adding of the universal closure of F to as a new axiom gives an inconsistent system as well as the adding of the universal closure of not F. It was proved in [1] that such formulas exist in HSAR+ (hence they exist in HSAD). Lemma. A formula F is essentially undefined in a system if and only if (F contains not F) ( not F contains F) is deducible in . Corollary. All the formulas essentially undefined in are equivalent. Note. It is easily to seen that essentially undefined formulas exist in all the systems belonging to Extlist and, besides, in HSAD; they are absent in other systems belonging to the main list. Theorem 1. All the arithmetical systems belonging to Genlist are effectively Luk-incomplete. This theorem includes as partial cases the theorem formulated in [6] and the theorem 5 in [5]. The systems HLEP and HSEP are defined as systems obtained from, correspondingly HLEA and HSEA by dropping all the functional symbols out of M. Presburger's ([7], [8]) signature (=, 0, ', +). The system HLEP is considered in [5]. Theorem 2. The systems HLEP and HSEP are equivalent. Corollary. The system HSEP is Luk-complete. References 1. I.D. Zaslavsky. Symmetric constructive logic. Publ. House of Acad. Sci. Arm. SSR, Yerevan (1978) (in Russian). 2. I.D. Zaslavsky. Dual realizability in symmetric logic. Annals of Pure and Applied Logic, 113, pp. 389-397 (2002). 3. I.D. Zaslavsky. On a 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). 4. I.D. Zaslavsky. On three-valued arithmetic. Proceedings of the Conference ``Computer Science and Information Technologies'', CSIT-01, Yerevan, pp. 133-136 (2001). 5. I.D. Zaslavsky. On three-valued logical models and their applications to arithmetical theories. Submitted to Denis Richard 60th Birthday Conference, Clermont-Ferrand, France (2002). 6. I.D. Zaslavsky. On the symmetric constructive arithmetic. 9th All-Union Conference on Mathematical Logic, Abstracts of Reports, Leningrad, p. 59 (1988). 7. S.C. Kleene. Introduction of Metamathematics. D. van Nostrand Comp., Inc. (1952). 8. M. Presburger. Ueber die Vollstaendigkeit eines gewissen System der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Sprawozdanie z I Kongresu Matematikow Krajow Slowianskich (Comptes rendudu I Congres des Mathematiciens des Pays Slaves), Warszawa, pp. 92-101 (1930).

Footnotes: This research is supported by INTAS grant "Weak Arithmetics" 2000-447.

Date received: April 16, 2002

Copyright © 2002 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cail-19.