SOME PROPERTIES OF SEVERAL PROOF SYSTEMS FOR INTUITIONISTIC, JOHANSSON’S AND MONOTONE PROPOSITIONAL LOGICS

Chubaryan Anahit¹⁺ --- Karabakhtsyan Arman ² --- Petrosyan Garik³

¹ Doctor of Physical and Mathematical Sciences, Full Professor of Yerevan State University and Russian-Armenian University, Armenia

² Master Student of Department of Applied Mathematics and Informatics of Russian-Armenian University, Armenia

³Master Student of Department of Informatics and Applied Mathematics of Yerevan State University, Armenia

Keywords:Strongly equal tautology, Minimal tautology, Sequent proof systems, Frege systems, Proof complexity measures, Monotonous system.

ARTICLE HISTORY: Received: 19 December 2017, Revised: 19 January 2018, Accepted: 23 January 2018, Published: 30 January 2018

1. INTRODUCTION

The traditional assumption that all tautologies as Boolean functions are equal to each other is not fine-grained enough to support a sharp distinction among tautologies. The authors of An and Arm [1] have provided a different picture of equality for classical tautologies. The notion of “determinative conjunct” is introduced in Chubaryan [2] on the basis of which the notion of strong equality of classical tautologies was suggested in An and Arm [1]. The idea to revise the notion of equivalence between tautologies in such way that is takes into account an appropriate measure of their “complexity”.  

The relations between the proof complexities of strongly equal classical tautologies in some proof systems are investigated in [3-5]. It was proved that the strongly equal tautologies have the same proof complexities in some “weak” proof systems, but the measures of proof complexities for strongly equal tautologies can be essentially different in the most traditional proof systems of Classical Logic (Frege systems, substitution Frege systems, sequent systems with and without cut rule). As the set of classical tautologies is co-NP-complete, the theory of proof complexity for classical proof systems is motivated by the conjecture NP ≠ co-NP. The set of tautologies, being intuinistically valid is PSPACE-complete, thus the PSPACE ≠ NP conjecture motivates an analogous research program as in classical case. In this work we introduce the notions of strongly equal non-classical valid sequents (non-classical tautologies) and show that the proof complexities of strongly equal non-classical valid sequents ( non-classical tautologies)  can be also essentially different in some sequent propositional systems of Intuitionistic, Johansson’s and Monotone logics, therefore in corresponding Frege systems as well..

The second theme of our investigation is connected with relation between the proof complexities of minimal tautologies, i.e. tautologies, which are not a substitution of a shorter tautology, and results of a substitution in them. The minimal tautologies play main role in proof complexity area. Really all “hard” propositional formulaes, proof complexities of which are investigated in many well known papers, are minimal tautologies. There is traditional assumption that minimal tautology must be no harder than any substitution in it. We introduce for the propositional proof systems the notions of monotonous by lines and monotonous by sizes of proofs. In [4, 6] it is proved that many traditional classical proof systems of 2-valued and many-valued logics are no monotonous neither by lines nor by size. Here we prove the analogous result for some systems of non-classical propositional logic as well. This work consists from 4 main sections. After Introduction we give the main notion and notations as well as some auxiliary statements in Preliminaries. The main results are given in 3-th section and in  the last  section we give some problem for discussion.

2. PRELIMINARIES

We will use the current concepts of a propositional formula, a classical tautology and non-classical tautologies,  sequent, sequent systems for non-classical propositional logics [7-9] Frege systems for Intuitionistic and Johansson’s logics [10, 11] and proof complexity [12]. Let us recall some of them.

2.1. The Considered Sequent Systems

Follow Kleene [7] we give the definition of main systems, which are considered in this point. The particular choice of a language for presented propositional formulas is immaterial in this consideration. However, because of

Sometimes we’ll use term tautology (valid sequent)for all types of above mentioned tautology (valid sequent)  further. 

2.2. Some Properties of Tautologies (Valid Sequents)

Here we give some properties of propositional formulas, which will be used for main results.

2.2.1. Determinative Disjunctive Normal Forms

Following the usual terminology we call the variables and negated variables   literals for classical logic. The conjunct K (clause) can be represented simply as a set of literals (no conjunct contains a variable and its negation simultaneously).

In [1, 2] the following notions were introduced for classical logic. Each of the under-mentioned trivial

Application of a replacement-rule to some word consists in the replacing of some its subwords, having the form of the left-hand side of one of the above identities, by the corresponding right-hand side.

3. MAIN RESULTS

3.1. Auxiliary Statements

Before we prove the main theorems, at first we must give some easy proved auxiliary statements. Let us consider the following sequences of sequents:

3.2. Results for Frege Systems of Intuitionistic and Johansson’s Logics

Here we recall the definitions of Frege systems for Intuitionistic and Johansson’s logics, which are given in Mints and Kozhevnikov [10] and Sayadyan and Chubaryan [11] correspondingly.

Definition 3.2.1

4. DISCUSSION

REFERENCES

[1]          C. An and C. Arm, "Definition of strong equality of tautologies and universal system for various propositional logics," Armenian Journal of Mathematics, vol. 1, pp. 30-35, 2008.View at Google Scholar 

[2]          A. A. Chubaryan, "On complexity of the proofs in Frege system," presented at the CSIT Conference, Yerevan, 2001

[3]          C. An, C. Arm, and A. Mnatsakanyan, "Proof complexities of strongly equal classical tautologies in some proof systems," Nauka i Studia, NR, vol. 42, pp. 92-98, 2013.

[4]          C. Anahit and P. Garik, "Frege systems are no monotonous, evolutio," Natural Sciences, Vyhn, vol. 3, pp. 12-14, 2016.

[5]          C. Anahit and P. Garik, "On some properties of several proof systems for 2-valued and 3-valued propositional logic," Fundamentalis Scientiam, Spain, vol. 8, pp. 70-73, 2017.

[6]          C. Anahit, N. Hakob, K. Arman, and P. Garik, "Propositional sequent systems of two valued classical logic and many valued logics are no monotonous," ASL, ESM, Logic Colloquium – 2017, Stockholm,  Abstracts, Programme and Abstracts, LC2017-Book, 98, 2017.

[7]          S. C. Kleene, Introduction to Metamathemics: D.Van Nostrand Company, INC, 1952.

[8]          A. Chubaryan and O. Bolibekyan, "On sequential systems of weak arithmetics," DNA of Armenia, Applied Mathematics, vol. 102, pp. 214-218, 2002.

[9]          A. Atserias, N. Galesi, and R. Gavalda, "Monotone proofs of the pigeon hole principle," Mathematical Logic Quarterly, vol. 47, pp. 461-474, 2001. View at Google Scholar | View at Publisher

[10]        G. Mints and A. Kozhevnikov, "Intuitionistic Frege systems are polynomially equivalent," Zapiski Nauchnykh Seminarov POMI, vol. 316, pp. 129-146, 2004.

[11]        S. Sayadyan and A. Chubaryan, On polynomially equivalence of minimal Frege systems vol. 27. Yerevan: Mathematical Problemsof Computer Science, 2007.

[12]        Y. Filmus, M. Lauria, J. Nordstrom, N. Thapen, and N. Ron-Zewi, "Space complexity in polynomial calculus," presented at the 2012 IEEE Conference on Computational Complexity (CCC), 2012.

[13]        A. Chubaryan, A. Chubaryan, H. Nalbandyn, and S. Sayadyan, "A hierarchy of resolution systems with restricted substituted rules," Computer Technology and Applications, vol. 3, pp. 330-336, 2012. View at Google Scholar 

[14]        A. S. Anikeev, "On some classification of deducible propositional formulas," Matematicheskie Zametki, vol. 11, pp. 165-174, 1972. View at Google Scholar