Investigation of Monotonous Properties for Frege Systems
DOI:
https://doi.org/10.51408/1963-0048Keywords:
Minimal tautology, Frege systems, Proof lines, Monotonous and strong monotonous of proof systems.Abstract
In this paper, we investigate the relations between the Frege proof lines of minimal tautologies and the results of substitutions in them. We show that there is a sequence of tautologies ψn, each of which has a unique minimal tautology ϕn, such that for every n the Frege proof lines of ϕn are an order more than the Frege proof lines for ψn.
References
А. С. Аникеев, О некоторой классификации выводимых пропозициональных формул, Математические заметки, т. 11, н. 2, сс. 165-174, 1972.
Г. М. Зограбян, С. М. Саядян и А. А. Чубарян, Исследование свойства монотонности некоторых пропозициональных систем выводов классической и неклассических логик, ДНАН РА, т. 119, н. 1, сс. 33-39, 2019.
A . Chubaryan, A . Karabakhtsyan and G. Petrosyan, Some Properties of Several Proof Systems for Intuitionistic, Johanssons and Monotone Propositional Logics" , Journal of Asian Scienti¯c Research, vol. 8, no. 2, pp. 61-72, 2018.
A. A. Aмбарцумян, Г. А. Гаспарян, С.А. Ованнисян и А. А. Чубарян, О количестве минимальных тавтологий и свойствах их выводов в ряде систем классической и неклассических логик,Математические вопросы кибернетики и вычеслительной техники, т. 52, сс. 66-73, 2019.
А. А. Чубарян, A. A. Aмбарцумян, Г. А. Гаспарян и С.А. Ованнисян, О некоторых свойствах минимальных тавтологий классической и неклассических логик, Доклады НАН РА, т. 120, н. 1, сс. 4-5, 2020.
S. A . Cook and R. A .Reckhow, The relative effciency of propositional proof systems" , The journal of symbolic logic, vol. 44, no. 1 , pp. 36-50, 1979.
S. C. Kleene, Introduction to Metamathematics, Van Nostrand New York, 1952.
A . A . Chubaryan, H . A . Tamazyan and A . S. Tshitoyan, Some improvement of lower bounds for steps and sizes of proofs in frege systems" , Sciences of Europe, vol. 1 , no. 37, pp. 39-44, 2019.
Downloads
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
