arXiv subjects
Publications and source records attributed to Alexei Muravitsky.
This is the text of my speech at the Logica Universalis webinar, which took place on May 11, 2022. I discuss two ways to implement a semantic approach to nonmonotonic consequence relations in an arbitrary propositional language. For one particular language, we also discuss the proof-theoretic framework that we connect with this semantic approach.
We show that the modalized Heyting calculus~\cite{esa06} admits a normal axiomatization. Then we prove that in this calculus the inference rule $\squareα/α$ is admissible (Proposition 5.6), but the rule $\squareα\rightarrowα/α$ is not (Proposition 6.1). Finally, we show that this calculus and intuitionistic propositional calculus are assertorically equipollent, which leads to a variant of limited separation property for the modalized Heyting calculus.
The book is devoted to the study of the field of application of the method, which arose from the concept of the Lindenbaum matrix by A. Lindenbaum and the Lindenbaum theorem, within the framework of the concept of a consequence relation by A. Tarski and in the context of the conception of separating tools by A. Kuznetsov. The unifying term Tarski-Lindenbaum method is intended to refer to the first two headings as the key topics of this study. Our implementation of the Tarski-Lindenbaum method aims to emphasize the role of the conception of separating tools.
These results are a contribution to the model theory of matrix consequence. We give a semantic characterization of uniform and couniform consequence relations. These properties have never been treated individually, at least in a semantic manner. We consider these notions from a purely semantic point of view and separately, introducing the notion of a uniform bundle/atlas and that of a couniform class of logical matrices. Then, we show that any uniform bundle defines a uniform consequence; and if a structural consequence is uniform, then its Lindenbaum atlas is uniform. Thus, any structural consequence is uniform if, and only if, it is determined by a uniform bundle/atlas. On the other hand, any couniform set of matrices defines a couniform structural consequence. Also, the Lindenbaum atlas of a couniform structural consequence is couniform. Thus, any structural consequence is couniform if, and only if, it is determined by a couniform bundle/atlas. We then apply these observations to compare structural consequence relations that are defined in different languages when one language is a primitive extension of another. We obtain that for any structural consequence defined in a language having (at least) a denumerable set of sentential variables, if this consequence is uniform and couniform, then it and the \emph{ Wójcicki's consequence} corresponding to it, which is defined in any primitive extension of the given language, are determined by one and the same atlas which is both uniform and couniform.
The paper is devoted to an algebraic interpretation of Kuznetsov's theorem which establishes the assertoric equipollence of intuitionistic and proof-intuitionistic propositional calculi. Given a Heyting algebra, we define an enrichable Heyting algebra, in which the former algebra is embedded. Moreover, we show that both algebras generate one and the same variety of Heyting algebras. This algebraic result is equivalent to the Kuznetsov theorem. The proposed construction of the enrichable `counterpart' of a given Heyting algebra allows one to observe that some properties of the original algebra are preserved by this embedding in the counterpart algebra.
During his brief life, the Polish mathematician and logician Adolf Lindenbaum (1904--1941) contributed to mathematical logic, among other things, by several significant achievements. Some results of Lindenbaum's, which bear his name, were published without proofs by other people from the Lvov--Warsaw School and the proofs later were provided by some others, though the authorship of Lindenbaum has never been challenged. Many may have heard about Lindenbaum's lemma, asserting the existence of Lindenbaum's extension, and Lindenbaum-Tarski algebra; less known is Lindenbaum's logical matrix. This tutorial is devoted to the two last concepts rather than the first one. However, the latter can be understood in a purely algebraic fashion, if one employs the notion of Lindenbaum-Tarski algebra. In general, the notions of Lindenbaum matrix and Lindenbaum-Tarski algebra have paved a way to further algebraization of logic, which had been begun by George Boole in the 19th century, as well as to a new branch of logic, model theory. For this reason, the present tutorial is also a gentle introduction to algebraic logic. A uniting idea of the aforementioned concepts is a special view on the formal judgments of a formal language. It is this view we call the Lindenbaum method. Although Lindenbaum expressed merely a starting viewpoint in the tradition of Polish logic of the time, this viewpoint became a standard ever since and its development goes on until this day, continuing to shape the field of algebraic logic. Our main objective is to demonstrate how this view gave rise to formulating the aforementioned concepts and how it opens door to unexplored paths.
Following A. Kuznetsov's outline, we restore Kuznetsov's syntactic proof of the assertoric equipollence of the intuitionistic propositional calculus and the proof-intuitionistic calculus KM (Kuznetsov's Theorem). Then, we show that this property is true for a broad class of modal logics on an intuitionistic basis, which includes, e.g., the modalized Heyting calculus mHC. The last fact is one of two key properties necessary for the commutativity of a diagram involving the lattices of normal extensions of four well-known logics. Also, we give an algebraic interpretation of the assertoric equipollence for subsystems of KM.
Lindenbaum method is named after the Polish logician Adolf Lindenbaum who prematurely and without a clear trace disappeared in the turmoil of the Second World War at the age of about 37. The method is based on the symbolic nature of formalized languages of deductive systems and opens a gate for applications of algebra to logic and, thereby, to Abstract algebraic logic.