Mathematical Problems of Computer Science 53, 21--28, 2020. UDC 510.6 On Some Universal Propositional Proof Systems for Many-Valued Logic Artur A. Khamisyan Yerevan State University e-mail: khamisyam@gmail.com Abstract Some uniform Hilbert-like propositional proof system is suggested for all versions of many-valued logic to apply them to 3 versions of 3-valued logic, two of which have only one designated value, and the last one has two designated values. Keywords: Many-valued logic, Hilbert-like proof system, Uniform propositional proof system. 1. Introduction It is known that many-valued logic (MVL) as a separate subject was first created and developed by Łukasiewicz [1]. His intention was to use a third, additional truth value for “possible” (or “unknown”). In the meantime, many interesting applications of MVL were found in such fields as logic, mathematics, hardware design, artificial intelligence and some other areas of soft information technologies, therefore investigations in the area of many-valued logic are very actual. The main theoretical results concern several properties of formal systems, which can present different versions of MVL and, in particular, issues on logical completeness of such systems. The completeness of some types of proof systems is proved by hard, many-stepped operations of immersion into two-valued logic, and for the other systems itis proved by reducing tothe completeness of the first type. The generalization of Kalmar’s proof of deducibility for two-valued tautologies in classical propositional logic [2] enables us to suggest 1) a new method of proving the completeness of a propositional proof system (PPS) of some well-known MVL such that it is essentially simpler than other known proofs of completeness and can be easily modified even into a proof of completeness for fuzzy logic as well, 2) a method for defining of many traditional variants of PPS for MVL, the completeness of which is easily proved directly, without the usual immersion into two-valued logic. Several new PPS for two versions of MVL are introduced in [3-7]. The current research refers to the problem of constructing some uniform Hilbert-like PPS for all possible versions of MVL. 21 On Some Universal Propositional Proof Systems for Many Valued Logic 22 2. Main Definitions of k-Valued Logics Here we give the main notions and notations for different versions of MVL. Let Ek be the set �0, 1 k−1 , … , k−2 k−1 , 1�. We use the well-known notions of a propositional formula, which, as usual, are defined from propositional variables with values from Ek, (may be also propositional constants), parentheses (,), and logical connectives & , ∨ , ⊃ ,¬, each of which can be defined by a different mode. Additionally, we introduce several variants of the exponential function p .We use the well-known notion of a propositional formula and introduce an additional notion of a formula: for each formulas A and B, the expression 𝑨𝑨𝑩𝑩 is also a formula. In the considered logics, only 1 or each of the values 1 2 ≤ 𝑖𝑖 k−1 ≤ 1 can be fixed as designated values. Definitions of main logical functions are: 𝒑𝒑 ∨ 𝒒𝒒 = 𝑚𝑚𝑚𝑚𝑚𝑚(𝑝𝑝, 𝑞𝑞) (1) disjunction, 𝒑𝒑 ∨ 𝒒𝒒 = 𝑚𝑚𝑚𝑚𝑚𝑚(𝑝𝑝 + 𝑞𝑞, 1) (2) disjunction, 𝒑𝒑&𝑞𝑞 = 𝑚𝑚𝑚𝑚𝑚𝑚(𝑝𝑝, 𝑞𝑞) (1) conjunction, 𝒑𝒑&𝑞𝑞 = 𝑝𝑝𝑞𝑞(𝑚𝑚𝑚𝑚𝑚𝑚 𝑘𝑘)/(𝑘𝑘 − 1) (2) conjunction For implication, we have the following two versions: 𝒑𝒑 ⊃ 𝒒𝒒 = � 1, 𝑓𝑓𝑚𝑚𝑓𝑓 𝑝𝑝 ≤ 𝑞𝑞 1 − 𝑝𝑝 + 𝑞𝑞, 𝑓𝑓𝑚𝑚𝑓𝑓 𝑝𝑝 > 𝑞𝑞 (1) Łukasiewicz’s implication or p⊃ 𝒒𝒒 = � 1, 𝑓𝑓𝑚𝑚𝑓𝑓 𝑝𝑝 ≤ 𝑞𝑞 𝑞𝑞, 𝑓𝑓𝑚𝑚𝑓𝑓 𝑝𝑝 > 𝑞𝑞 (2) Gödel’s implication And for negation, there are also two versions: ¬𝒑𝒑 = 1 − 𝑝𝑝 (1) Łukasiewicz’s negation or ¬𝒑𝒑 = ((𝑘𝑘 − 1)𝑝𝑝 + 1)(𝑚𝑚𝑚𝑚𝑚𝑚 𝑘𝑘)/(𝑘𝑘 − 1) (2) cyclically permuting negation. Sometimes we can use the notation 𝒑𝒑� instead of ¬𝒑𝒑. For the propositional variable p and 𝛅𝛅= 𝑖𝑖 k−1 (0≤i≤k-1), we additionally define “exponent” functions: p as (𝑝𝑝 ⊃ δ)& (δ ⊃ 𝑝𝑝) with (1) implication (1) exponent, p as p with (k-1)–i(2) negations. (2) exponent. Note that both (1) exponent and (2) exponent are not new logical functions. If we fix “1” (each of the values 1 2 ≤ 𝑖𝑖 k−1 ≤ 1) as a designated value, then the formula φ with variables p1,p2,…pn is called a k-tautology if for every 𝛿𝛿 = (𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛) ∈ 𝐸𝐸𝑘𝑘 𝑛𝑛assigning 𝛿𝛿j (1≤j≤n) to each pj gives the value 1 (or some value 1 2 ≤ 𝑖𝑖 k−1 ≤ 1) of φ. 3. Uniform Hilbert-Like Propositional Proof System and Its Properties Here we suggest some uniform Hilbert-like PPS for all possible versions of MVL. For all formulas A, B, C of MVL, each 𝜎𝜎1, 𝜎𝜎2 from the set Ek and for ∗∈ {&,∨, ⊃} the following A. Khamisyan 23 formulas are axiom schemes of some PPS version: 1. 𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐴𝐴) 2. (𝐴𝐴 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐶𝐶)� ⊃ �𝐴𝐴 ⊃ 𝐶𝐶𝜑𝜑m.p.(𝐵𝐵,𝐶𝐶)�) 3.𝐴𝐴𝜎𝜎 ⊃ (¬𝐴𝐴)𝜑𝜑¬(𝐴𝐴,𝜎𝜎) 4.-6.𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ∗ 𝐵𝐵)𝜑𝜑∗(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 7.𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴𝐵𝐵)𝜑𝜑exp(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 8.(𝐴𝐴1 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 𝑘𝑘−1 𝑘𝑘−2� ⊃ 𝐵𝐵� ⊃ ⋯ ⊃ ��𝐴𝐴 1 𝑘𝑘−1 ⊃ 𝐵𝐵� ⊃ �(𝐴𝐴0 ⊃ 𝐵𝐵) ⊃ 𝐵𝐵�� … ), where many-valued functions 𝜑𝜑¬(𝐴𝐴, 𝜎𝜎), 𝜑𝜑∗(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2), 𝜑𝜑exp(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) must be defined individually for each version of MVL, such that axioms 3-7 will be a k-tautology in this version. Inference rule is a modification of modus ponens (m.m.p.) 𝐴𝐴,𝐴𝐴⊃𝐵𝐵 𝐵𝐵𝜑𝜑m.p.(𝐴𝐴,𝐵𝐵) , where many-valued functions 𝜑𝜑m.p.(𝐴𝐴, 𝐵𝐵) must be defined individually for each version of MVL, such that the formula 𝐴𝐴 ⊃ ((𝐴𝐴 ⊃ 𝐵𝐵) ⊃ 𝐵𝐵𝜑𝜑m.p.(𝐴𝐴,𝐵𝐵)) will also be a k-tautology in this version. We use the well-known notions of proof and proof from premises. For all defined systems, we first prove the well known deduction theorem using the first two axiom schemes, and then the generalization of Kalmar’s proof of deducibility for two valued tautologies inside the classical propositional logic gives us a possibility to directly prove completeness for the mentioned proof systems, without the usual loading into two-valued logic. Let Pk be one of the defined PPS for some version of MVL. The following statement can be proved as usual. Deduction theorem. Let Γ be a set of some formulas and 𝐴𝐴 and 𝐵𝐵 be some formulas. If the formula B is derived in the system Pk from the premises Γ and 𝐴𝐴 (Γ, 𝐴𝐴 ⊢𝑃𝑃𝑘𝑘 𝐵𝐵), then the formula𝐴𝐴 ⊃ 𝐵𝐵 is derived in the system Pk from the premises Γ(Γ ⊢𝑃𝑃𝑘𝑘 𝐴𝐴 ⊃ 𝐵𝐵). Lemma 1: Let 1 2= { , , , }nP p p p be the set of all variables of any formula A, then for every 𝛿𝛿 = (𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛) ∈ 𝐸𝐸3 𝑛𝑛 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢𝐶𝐶𝐶𝐶3 𝐴𝐴𝐴𝐴(𝛿𝛿1,𝛿𝛿2,…,𝛿𝛿𝑛𝑛). To simplify the proof, we demonstrate them only for P3 logic. Proof is given by induction on number n of logical connectives in the formula A. For n=1 we have: by 𝛿𝛿 = 0 𝑝𝑝0 ⊢ 𝑝𝑝0, by𝛿𝛿 = 1 2� 𝑝𝑝 1 2� ⊢ 𝑝𝑝 1 2� and by 𝛿𝛿 = 1 𝑝𝑝1 ⊢ 𝑝𝑝1. Suppose that the statement is valid for the number of logical connectives ˂n. If the number of logical connectives is n, then the formula A can be in one of the following forms: 1. 𝐴𝐴 = 𝐴𝐴1 ∗ 𝐴𝐴2, where ∗∈ {&,∨, ⊃}, 2. A=𝐴𝐴1 𝐴𝐴2, 3. 𝐴𝐴 = ¬𝐴𝐴1. For the case 1. 𝐴𝐴1�𝛿𝛿� = 𝜎𝜎1, 𝐴𝐴2�𝛿𝛿� = 𝜎𝜎2 => 𝐴𝐴�𝛿𝛿� = 𝜎𝜎1 ∗ 𝜎𝜎2 On Some Universal Propositional Proof Systems for Many Valued Logic 24 By induction hypothesis 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢ 𝐴𝐴1 𝜎𝜎1 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢ 𝐴𝐴2 𝜎𝜎2 Use one of the axiom schemes 4. – 6. we have 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢ 𝐴𝐴1 𝜎𝜎1 ⊃ (𝐴𝐴2 𝜎𝜎2 ⊃ (𝐴𝐴1 ∗ 𝐴𝐴2)𝜑𝜑∗(𝐴𝐴1,𝐴𝐴2,𝜎𝜎1,𝜎𝜎2)) And for 𝐴𝐴1 = 𝜎𝜎1, 𝐴𝐴2 = 𝜎𝜎2 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢ 𝐴𝐴1 𝜎𝜎1 ⊃ �𝐴𝐴2 𝜎𝜎2 ⊃ (𝐴𝐴1 ∗ 𝐴𝐴2)𝜑𝜑∗(𝐴𝐴1,𝐴𝐴2,𝜎𝜎1,𝜎𝜎2)� And (𝐴𝐴1 ∗ 𝐴𝐴2)𝜑𝜑∗(𝐴𝐴1,𝐴𝐴2,𝜎𝜎1,𝜎𝜎2) is derived after the double application of m.m.p. For the case 2. 𝐴𝐴1�𝛿𝛿� = 𝜎𝜎1, 𝐴𝐴2�𝛿𝛿� = 𝜎𝜎2 => 𝐴𝐴�𝛿𝛿�=�𝐴𝐴1 𝐴𝐴2� (𝝈𝝈𝟏𝟏 𝝈𝝈𝟐𝟐) and we must use the axiom scheme 7. For the case 3. 𝐴𝐴1�𝛿𝛿� = 𝜎𝜎 => 𝐴𝐴�𝛿𝛿� = ¬𝜎𝜎 we must use the axiom scheme 3. ⧠ Corollary 1: If A is a 3-tautology, then for every 𝛿𝛿 = (𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛) ∈ 𝐸𝐸3 𝑛𝑛 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢ 𝐴𝐴 Theorem 1: Any formula is derived in P3 iff it is a 3-tautology. Proof: It is obvious that every formula, derived in P3, is a 3-tautology. Let },,,{= 21 npppP  (n≥1) be the set of all variables of any tautology A. For every 𝛿𝛿 = (𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛) ∈ 𝐸𝐸3 𝑛𝑛 by the above corollary, we have 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛 𝛿𝛿𝑛𝑛 ⊢ 𝐴𝐴. For every 𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛−1 we take into consideration the following 3 truth values � 𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛−1, 0 𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛−1, 1 2� 𝛿𝛿1, 𝛿𝛿2, … , 𝛿𝛿𝑛𝑛−1, 1 , for which we have ⎩ ⎨ ⎧ 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1, 𝑝𝑝𝑛𝑛0 ⊢ 𝐴𝐴 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1, 𝑝𝑝𝑛𝑛 1 2� ⊢ 𝐴𝐴 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1, 𝑝𝑝𝑛𝑛1 ⊢ 𝐴𝐴 . By deduction theorem we have 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ 𝑝𝑝𝑛𝑛0 ⊃ 𝐴𝐴 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ 𝑝𝑝𝑛𝑛 1 2� ⊃ 𝐴𝐴 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ 𝑝𝑝𝑛𝑛1 ⊃ 𝐴𝐴. Then 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ (𝐴𝐴1 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 1 2� ⊃ 𝐵𝐵� ⊃ �(𝐴𝐴0 ⊃ 𝐵𝐵) ⊃ 𝐵𝐵�) /axiom 8./ 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ (𝑝𝑝𝑛𝑛 1 2� ⊃ 𝐴𝐴) ⊃ ((𝑝𝑝𝑛𝑛0 ⊃ 𝐴𝐴) ⊃ 𝐴𝐴) /m.m.p./ 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ (𝑝𝑝𝑛𝑛0 ⊃ 𝐴𝐴) ⊃ 𝐴𝐴 /m.m.p./ 𝑝𝑝1 𝛿𝛿1, 𝑝𝑝2 𝛿𝛿2, … , 𝑝𝑝𝑛𝑛−1 𝛿𝛿𝑛𝑛−1 ⊢ 𝐴𝐴 /m.m.p./ A. Khamisyan 25 So, the number of premises is now n-1. Repeating the above steps, we finally obtain the derivation of tautology A in P3 ⧠ Note that this proof is the complete analogy to proof of the corresponding theorem for the 2- valued logic [2]. Also note that after proving by analogy the corresponding Lemma 1. for any k- valued logic for k≥4, the proof of the corresponding theorem above can be given by analogy as well. Every such PPS can be easily transformed into Gentzen-like system as well. 4. Examples of Uniform PPS for Some Versions of MVL 4.1 The first of the constructed systems LNk(Łukasiewicz’s negation ) with fixed “1” as the designated value, uses conjunction, disjunction, (1) implication, (1) negation and (1) exponent, as well as constants 𝛅𝛅= 𝒊𝒊 𝒌𝒌−𝟏𝟏 (1≤i≤k-2) for using (1) exponent [3,5,7]. In particular, for all formulas A, B, C of 3-valued logic and each 𝜎𝜎1, 𝜎𝜎2 from the set {0,1/2,1}, the following formulas are axiom schemes of LN3. 1. 𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐴𝐴) 2. (𝐴𝐴 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐶𝐶)� ⊃ (𝐴𝐴 ⊃ 𝐶𝐶)) 3. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ⊃ 𝐵𝐵)𝜎𝜎1⊃𝜎𝜎2) 4. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ∨ 𝐵𝐵)𝜎𝜎1∨𝜎𝜎2) 5. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴&𝐵𝐵)𝜎𝜎1&𝜎𝜎2) 6. 𝐴𝐴𝜎𝜎 ⊃ (¬𝐴𝐴)¬𝜎𝜎 7. (𝐴𝐴1 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 1 2� ⊃ 𝐵𝐵� ⊃ �(𝐴𝐴0 ⊃ 𝐵𝐵) ⊃ 𝐵𝐵�) Inference rule is modus ponens /m.p./𝐴𝐴,𝐴𝐴⊃𝐵𝐵 𝐵𝐵 . 4.2. The second systems CNk (cyclically permuting negation) with fixed “1” as the designated value, use conjunction, disjunction, (2) implication, (2) negation and (2) exponent [4,6,7]. In particular, for all formulas A, B, C of 3-valued logic and each 𝜎𝜎1, 𝜎𝜎2 from the set {0,1/2,1,} the following formulas are axiom schemes of CN3 1. 𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐴𝐴) 2. (𝐴𝐴 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐶𝐶)� ⊃ (𝐴𝐴 ⊃ 𝐶𝐶)) 3. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ⊃ 𝐵𝐵)𝜑𝜑⊃(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 4. 𝐴𝐴𝜎𝜎1 ⊃ �𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ∨ 𝐵𝐵)𝜑𝜑∨(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)� 5. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴&𝐵𝐵)𝜑𝜑&(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 6.𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴𝐵𝐵)𝜑𝜑exp(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 7. 𝐴𝐴𝜎𝜎 ⊃ (¬𝐴𝐴)𝜎𝜎� 8. (𝐴𝐴 ⊃ 𝐵𝐵) ⊃ ((�̅�𝐴 ⊃ 𝐵𝐵) ⊃ ���̿�𝐴 ⊃ 𝐵𝐵� ⊃ 𝐵𝐵�), where the main role is played by the following exponents: On Some Universal Propositional Proof Systems for Many Valued Logic 26 𝜑𝜑⊃(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = (𝜎𝜎1 ⊃ 𝜎𝜎2)&(¬(𝐴𝐴⋁�̅�𝐴)⋁(𝐵𝐵� ⊃ 𝐵𝐵))⋁(¬�𝐴𝐴⋁�̿�𝐴�&¬(𝐵𝐵⋁𝐵𝐵�)), 𝜑𝜑∨(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = (𝜎𝜎1⋁𝜎𝜎2)⋁((𝐴𝐴 ⊃ �̅�𝐴)&¬(𝐵𝐵�⋁𝐵𝐵�))⋁(¬��̅�𝐴⋁�̿�𝐴�&(𝐵𝐵 ⊃ 𝐵𝐵�)), 𝜑𝜑&(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = (𝜎𝜎1&𝜎𝜎2)⋁((𝐴𝐴&�̿�𝐴)⋁(𝐵𝐵&𝐵𝐵�))⋁((𝐴𝐴&�̅�𝐴)⋁(𝐵𝐵&𝐵𝐵�) 𝜑𝜑exp(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = 𝜎𝜎1𝜎𝜎2⋁(¬(𝜎𝜎1𝜎𝜎2)&¬(¬(𝐴𝐴𝜎𝜎1&𝐵𝐵�𝜎𝜎2)⋁¬¬(𝐴𝐴𝜎𝜎1&𝐵𝐵�𝜎𝜎2))) Inference rule is modus ponens /m.p./𝐴𝐴,𝐴𝐴⊃𝐵𝐵 𝐵𝐵 . 4.3. For LN3,2 - Łukasiewicz’s logic with fixed “1/2” and “1” as the designated value, which use conjunction, disjunction, (1) implication, (1) negation and (1) exponent, as well as constants 0, ½ and 1 for using (1)exponent. In particular for all formulas A, B, C of 3-valued logic and each 𝝈𝝈𝟏𝟏, 𝝈𝝈𝟐𝟐 from the set {0,1/2,1}, the following formulas are axiom schemes of LN3,2: 1. 𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐴𝐴) 2. (𝐴𝐴 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 ⊃ (𝐵𝐵 ⊃ 𝐶𝐶)� ⊃ �𝐴𝐴 ⊃ 𝐶𝐶 1 2� �) 3. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ⊃ 𝐵𝐵)𝜑𝜑⊃(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 4. 𝐴𝐴𝜎𝜎1 ⊃ �𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴 ∨ 𝐵𝐵)𝜑𝜑∨(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)� 5. 𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴&𝐵𝐵)𝜑𝜑&(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 6.𝐴𝐴𝜎𝜎1 ⊃ (𝐵𝐵𝜎𝜎2 ⊃ (𝐴𝐴𝐵𝐵)𝜑𝜑exp(𝐴𝐴,𝐵𝐵,𝜎𝜎1,𝜎𝜎2)) 7. 𝐴𝐴𝜎𝜎 ⊃ (¬𝐴𝐴)𝜎𝜎� 8. (𝐴𝐴1 ⊃ 𝐵𝐵) ⊃ (�𝐴𝐴 1 2� ⊃ 𝐵𝐵� ⊃ �(𝐴𝐴0 ⊃ 𝐵𝐵) ⊃ 𝐵𝐵�), where 𝜑𝜑⊃(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = �̅�𝐴⋁𝐵𝐵⋁𝜎𝜎1���⋁𝜎𝜎2 𝜑𝜑⋁(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = 𝐴𝐴⋁𝐵𝐵⋁𝜎𝜎1⋁𝜎𝜎2 𝜑𝜑&(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = (𝐴𝐴⋁𝜎𝜎1⋁𝐵𝐵𝜎𝜎2�����)&(𝐵𝐵⋁𝜎𝜎2⋁𝐴𝐴𝜎𝜎1�����) 𝜑𝜑𝑒𝑒𝑒𝑒𝑒𝑒(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = 𝐴𝐴𝐵𝐵⋁𝜎𝜎1𝜎𝜎2 𝜑𝜑−(𝐴𝐴, 𝐵𝐵, 𝜎𝜎1, 𝜎𝜎2) = �̅�𝐴⋁𝜎𝜎1��� and inference rule is modification of modus ponens 𝑨𝑨,𝑨𝑨⊃𝑩𝑩 𝑩𝑩𝝋𝝋𝒎𝒎.𝒑𝒑.(𝑨𝑨,𝑩𝑩) , where 𝝋𝝋𝒎𝒎.𝒑𝒑.(𝑨𝑨, 𝑩𝑩)=1/2. The work with another version of MVL and for k =4 or k =8 is in progress. 5. Conclusion We suggest some Hilbert-like propositional proof system, which is universal for all versions of many-valued logic. Here we give also the application of the suggested system to 3 versions of 3- valued logic, two of which have only one designated value and the last one has two designated values. The investigation of the applications to the other versions of k-valued logics (k≥4) is in progress. A. Khamisyan 27 6. Acknowledgements This work was supported by the RA MES State Committee of Science, in the frames of the research project № 18T-1B034. I am grateful to my supervisor, Professor of YSU Anahit Chubaryan for her encouragement and fruitful discussions, and also for helpful suggestions, which enabled to improve and expand the results. References [1] J. Lukasiewicz, “O Logice Trójwartósciowej”, Ruch Filozeficzny English translation: On three valued-logic, vol. 5, pp. 169-171, 1920. [2] E. Mendelson, Introduction to Mathematical Logic, Van Nostrand, Princeton, 1975. [3] A. A. Chubaryan, A. S. Tshitoyan and A. A. Khamisyan, “On some proof systems for many-valued logics and on proof complexities in it”, (in Russian) Reports of NASA RA, vol. 116, no. 2, pp. 18-24, 2016. [4] A. Chubaryan and A. Khamisyan, “Generalization of Kalmar’s proof of deducibility in two valued propositional logic into many valued logic”, Pure and Applied Mathematics Journal, doi: 10.116448/j.pamj. 20170602.12, vol. 6, no. 2, pp. 71-75, 2017. [5] A. Chubaryan, A. Khamisyan and A. Tshitoyan, “On some systems for Łukasiewicz’s many-valued logic and its properties”,FundamentalisScientiam, vol. 8, no. 8, Spain, pp. 74-79, 2017. [6] А. Чубарян и А. Хамисян, Новый метод доказательства полноты пропозициональной системы трехзначной логики Лукасевича и его приложения, Evolutio, Естественные науки, Вып. 3, сс. 9-12, 2016. [7] A.Chubaryan, A.Khamisyan and G. Petrosyan, On Some Systems for Two Versions of Many-valued Logics and its Properties, Lambert Academic Publishing (LAP), 2017. Submitted 18.12.2019, accepted 09.03.2020. On Some Universal Propositional Proof Systems for Many Valued Logic 28 Բազմարժեք տրամաբանության ասույթային հաշվի որոշ համապիտանի համակարգերի մասին Արթուր Ա. Խամիսյան Երևանի պետական համալսարան e-mail: khamisyam@gmail.com Ամփոփում Սույն հոդվածում առաջարկվում է Հիլբերտյան տիպի համապիտանի արտածման համակարգ բազմարժեք տրամաբանության ասույթային հաշվի տարատեսակների համար, ինչպես նաև տրվում է այդ համապիտանի համակարգի ներկայացումը երեք տարբեր եռարժեք տրամաբանությունների համար, որոնցից երկուսը մեկ առանձնացված արժեքով են, իսկ վերջինը՝ երկու: Բանալի բառեր` բազմարժեք տրամաբանություն, Հիլբերտյան տիպի արտածման համակարգեր, ասույթային հաշվի համապիտանի արտածման համակարգ: О некоторых универсальных пропозициональных системах выводов для многозначных логик Артур А. Хамисян Ереванский государственный университет e-mail:khamisyam@gmail.com Аннотация В данной статье предлагается некоторая универсальная пропозициональная система Гильбертовского типа для всех версий многозначных логик и рассматриваются ее приложения для трех версий 3-значных логик, две из которых имеют одно выделенное значение, а последняя – два выделенных значения. Ключевые слова: многозначная логика, системы выводов Гильбертовского типа, универсальная пропозициональная система выводов.