Time: Monday, February 17, 4:10 PM
Place: SC 1312
Speaker: Adam Prenosil
Title: Medvedev’s logic of finite problems (continued)
Abstract: The idea of a constructive logic is often thought to be embodied by the so-called Brouwer–Heyting–Kolmogorov (BHK) interpretation, which describes the proofs of complex formulas in terms of the proofs of their subformulas. For example, in this interpretation a proof of an implication is an algorithm transforming proofs of the premise into proofs of the conclusion. The BHK interpretation is usually taken to underpin intuitionistic logic (the main “constructive” rival to classical logic). However, one natural formalization of the BHK principles yields a strictly stronger logic, introduced in 1966 by Medvedev. This logic is in many ways one of the most intriguing extensions of intuitionistic logic and several open problems relate to it. In this talk, I will cover some known facts as well as open problems concerning Medvedev’s logic.

Time: Monday, February 10, 4:10 PM
Place: SC 1312
Speaker: Adam Prenosil
Title: Medvedev’s logic of finite problems
Abstract: The idea of a constructive logic is often thought to be embodied by the so-called Brouwer–Heyting–Kolmogorov (BHK) interpretation, which describes the proofs of complex formulas in terms of the proofs of their subformulas. For example, in this interpretation a proof of an implication is an algorithm transforming proofs of the premise into proofs of the conclusion. The BHK interpretation is usually taken to underpin intuitionistic logic (the main “constructive” rival to classical logic). However, one natural formalization of the BHK principles yields a strictly stronger logic, introduced in 1966 by Medvedev. This logic is in many ways one of the most intriguing extensions of intuitionistic logic and several open problems relate to it. In this talk, I will cover some known facts as well as open problems concerning Medvedev’s logic.

Time: Monday, January 13, 4:10 PM
Place: SC 1312
Speaker: Adam Prenosil
Title: Four-valued logics and equality-free quasivarieties
Abstract: The subdirectly irreducible four-element De Morgan algebra DM4 consists of the elements t (True), f (False), n (Neither), and b (Both). This algebra generates the variety of De Morgan algebras DMA as a quasivariety, and it also forms a semantics for the four-valued Belnap–Dunn logic BD. These two facts can be formulated more uniformly as follows: the strict universal Horn theory of the algebra DM4 equipped with the binary equality predicate is axiomatized by the axioms of DMA, and the strict universal Horn theory of the algebra DM4 equipped with the unary truth predicate interpreted by {t, b} is axiomatized by the axioms of BD. We show how to axiomatize the strict universal Horn theory of DM4 in other relational signatures, for example truth and non-falsity ({t, n}) or truth and equality. Our intention is to primarily to provide reasonable examples of universal Horn classes worth considering which are not quasivarieties or logics in the narrow sense of abstract algebraic logic.