The list of confirmed invited speakers includes:
Patrick Blackburn (University of Roskilde, Denmark)
Talk title: Temporal Reference and Temporal Indexicals
Abstract: I sketch an approach to logic and indexicality, which I illustrate using hybrid tense logic and temporal indexicals. I have chosen temporal indexicals because they are probably the easiest natural language indexicals to model in a propositional logic. I have chosen hybrid tense logic because while it is rooted in the Priorean tradition of taking the internal perspective on time seriously, it also allows us to incorporate both Reichenbach's approach to temporal reference, and (as we shall see) a Kaplan-style character approach to indexicality. This will enable us to view "now" as a bridge that leads us to the logic(s) of "yesterday," "today", "tomorrow," and indeed other indexicals.
Janusz Czelakowski (University of Opole, Poland)
Talk title: On the Collatz Conjecture
Abstract: We start with an arbitrary but fixed positive integer n. If n is even, we divide it by 2 and get n/2. If n is odd, we multiply n by 3 and add 1 to obtain the even number 3n + 1. Then we repeat the procedure indefinitely. Each sequence defined in this way is referred to as a Collatz sequence. The Collatz conjecture says that no matter what number n we start with, we will always eventually reach 1. For example, if one starts with 5, one gets
5, 3 · 5 + 1 = 16, 8, 4, 2, 1.
The number 7 yields the sequence:
7, 3 · 7 + 1 = 22, 11, 3 · 11 + 1 = 34, 17, 3 · 17 + 1 = 52, 26, 13, 3 · 13 + 1 = 40, 20, 10, 5, 3 · 5 + 1 = 16, 8, 4, 2, 1.
The Collatz conjecture is an old problem in number theory, named after Lothar Collatz, who proposed it in 1937.
In the talk we show that the Collatz conjecture is unprovable in the elementary Peano arithmetic PA. The proof refers to the general approach to first-order logic based on Rasiowa-Sikorski Lemma and the derived notion of a Rasiowa-Sikorski set. The central idea consists in constructing countable models from individual variables by means of appropriate Rasiowa-Sikorski sets. This idea is developed and applied to the language of Peano arithmetic.
Advanced methods borrowed from the contemporary mathematical logic are applied. Such a ``logical'' methodology is a useful addition to the dominant approach to number theory based on analytical methods.
Stéphane Demri (CNRS, Paris, France)
Talk title: Logics with Concrete Domains: An Introduction
Abstract: In this talk, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These mainly include temporal/description logics with concrete domains. For the simple concrete domain (ℕ,<), we present known proof techniques to handle satisfiable (infinite) symbolic models, sometimes at the cost of going beyond omega-regularity. The talk is freely inspired from [1].
References:
[1] Stéphane Demri & Karin Quaas (2021): Concrete Domains in Logics: A Survey. ACM SIGLOG News 8(3), pp. 6–29, doi:10.1145/3477986.3477988.
Rajeev Goré (Australian National University, Australia)
Talk title: CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-learning and SAT
Abstract: We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal encodings into SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using ``satisfiability under unit assumptions'', we can iterate rather than ``backtrack'' over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude. It can now also handle all of the 15 logics in the modal cube as well as multimodal tense logic Kt(n) (AKA description logic ALCI). We believe that in the future, all tableaux calculi implementations will use CEGAR-Tableaux.
Joanna Grygiel (University of Social Sciences and Humanities, Warsaw, Poland)
Talk title: Some Aspects of Lattice Tolerances
Abstract: The idea of tolerance relations seen as a formalization of the intuitive notion of resemblance was formalized by E. C. Zeeman in 1960s. In mathematics, as a natural generalization of congruences, tolerances appeared to be a very useful tool, especially in universal algebra.
Tolerances of a lattice L are reflexive, symmetric relations compatible with lattice operations of L. They form a lattice denoted by Tol(L).
A block of a tolerance T ∊ Tol(L) is a maximal set X ⊆ L satisfying X2 ⊆ T. Blocks are convex sublattices of L, and it was shown by G. Czédli that they form a lattice (denoted by L/T), called the factor lattice of L modulo T. Although this construction generalizes the notion of a factor lattice L/φ defined by means of a congruence φ ∊ Con(L), properties of factor lattices modulo tolerances are significantly different. For instance, L/φ belongs to the same equational class as L, however, the lattice L/T does not belong to it, in general.
It is known that for any φ ∊ Con(L), the congruence lattice of the factor lattice L/φ is isomorphic to the principal filter [φ) of φ in Con(L) (homomorphism theorem). Moreover, any ψ ∊ Con(L), ψ ≥ φ induces the congruence ψ/φ on the factor lattice L/φ such that (L/φ)/(ψ/φ) ≅ L/ψ holds (second isomorphism theorem).
In this talk we formulate analogous results for tolerance factors defining a new partial order ⊑ on the lattice Tol(L) such that for any S ∊ Tol(L) with T ⊑ S, the tolerance S/T is induced on the factor lattice L/T. We also discuss the philosophical background of tolerances and their significance in lattice theory.
References:
[1] Ivan Chajda (1991): Algebraic Theory of Tolerance Relations. Univerzita Palackého Olomouc, Olomouc.
[2] George Grätzer (2011): Lattice Theory: Foundation. Springer, Basel, doi:10.1007/978-3-0348-0018-1.
[3] Joanna Grygiel (2019): Many faces of lattice tolerances. Bulletin of the Section of Logic 48(4), pp. 285–298, doi:10.18778/0138-0680.48.4.03.
[4] Joanna Grygiel & Sándor Radeleczki (2013): On the tolerance lattice of tolerance factors. Acta Mathematica Hungarica 141(3), pp. 220–237, doi:10.1007/s10474-013-0340-x.
[5] Eric Christopher Zeeman (1962): The topology of the brain and visual perception. In Marion Kirkland Fort, editor: Topology of 3-Manifolds and Related Topics, Dover Publications, New Jersey.
Jacek Malinowski (Polish Academy of Sciences)
Talk title: Connexive Logics via Relating Semantics
Abstract: There is a common agreement that each connexive logic should satisfy the Aristotles and Boethian Theses (AB). However, the sole AB theses don't guarantee any common content or other form of "connexions" as they are true in binary matrix {0,1} with distinguished value of 1, with classical material implication and negation defined as ~1 = ~0 = 1. Similarly, AB are true in a binary matrix with classical negation and implication defined as x ⇒ y = 1 iff x = y.
Counterexamples above show that the sole AB theses are very weak and should be strengthen in some way. We can eliminate the first counterexample by assuming that negation behaves in a classical way. We did it in [6] and [7]. It brings us to the notion of Boolean connexive logic. Boolean algebras are defined in terms of ∧, ∨, ¬. In Boolean connexive logic these connectives behave in classical way. It made us to refer to George Boole here.
We can eliminate a second counterexample and consider connexive logics with material implication. It is not known whether that could lead to a promising research area. Anyway we could call such logics `material connexive logics'. Obviously we could eliminate both the counterexamples. It would bring us to connexive logics which are neither Boolean not material.
In this lecture we concetrate on Boolean connexive logics. We indicate a numer of possible desiderata strengthening Aristotle and Boethius' theses. We investigate them by means of relating semantics.
A relating semantics has its origins in Epstein and Walton papers. However in its full generality it has been proposed by Jarmużek and Kaczkowski in [4]. It is extensively studied among others in [3], [5], [10]. The general idea of relating semantics is based on the relating relation R. The fact that ARB – sentences A and B relate with respect to R – could be interpreted in many ways depending on the motivations of a given logical system. For example, A and B could be related causally, they could be related in the sense of time order, they could have a common content. Generally, two sentences are related because they have something in common.
In Boolean connexive logics only implication depends on a relating relation R. The truth conditions for the propositional letters and ∧, ∨, and ¬ remain standard, i.e. as in classical logic. Only implication → has an intensional nature, it depends on a relation R: 〈v,R〉 ⊨ A → B iff [〈v,R〉 ⊭ A or 〈v,R〉 ⊨ B] & ARB.
By a minimal Boolean connexive logic we mean the least set of sentences containing all classical tautologies expressed by means of ∧, ∨, ¬, (A1), (A2), (B1), (B2), (A → B) ⊃ (A ⊃ B) and closed under substitutions and modus ponens with respect to ⊃. ⊃ denotes material implication. Let JT denote a class of all relations R such that R is (a1), (a2), (b1), (b2). Let JT¬ denote a class of all relations from JT satisfying (c1), where:
- R is (a1) iff for all A ∈ ForCF, AR̃~A;
- R is (a2) iff for all A ∈ ForCF, ~AR̃A;
- R is (b1) iff for all A,B ∈ ForCF, if ARB, then AR̃~B and (A →w B)R~(A →w ~B);
- R is (b2) iff for all A,B ∈ ForCF, if ARB, then AR̃~B and (A →w ~B)R~(A →w B);
- R is (c1) iff for all A,B ∈ ForCF, if ARB then ~AR~B.
In [6] we characterized Boolean connexive logics by means of relating semantics. Then Mateusz Klonowski (forthcoming) made this result stronger. Klonowski proved that the class JT determines minimal Boolean connexive logics. The class JT¬ determines the least Boolean connexive logics satisfying the following two axioms: (A → B) ⊃ (¬¬A → ¬¬B) (A → B) ⊃ ((¬A → ¬B) ∨ (¬A ∧ B)).
In [2] Estrada-González and Ramírez-Cámara consider a number of properties added to AB. They used terms hyper-connexive and totally connexive logics. Malinowski and Nicolás-Francisco in [9] analyzed it in terms of relating semantics for Boolean connexive logcs. In particular they show that Minimal Boolean Connexive Logic (or alternatively the logic determined by JT) is Abelardian, strongly consistent, Kapsner strong and antiparadox. They also construct examples showing that it is not simplificative, neither conjunction-idempotent nor strongly inconsistent logics. Malinowski and Nicolás-Francisco also describe in terms of relating semantics an interrelation between hyper-connexive logics and JT logic.
In the last part we remind less known Barbershop paradox published by Lewis Carrol in 1894 [1], see also [8], [10]. We show that if interpreted by means of material implication paradox reduces to simple paralogism. Then we interpret it by means of connexive implication. We develop relating semantics for Boolean connexive logics to eludicate Barbershop paradox.
References:
[1] Lewis Carroll (1894): A logical paradox. Mind 3(11), pp. 436–438, doi:10.1093/mind/III.11.436.
[2] Luis Estrada-González & Elisngela Ramírez-Cámara (2016): A Comparison of Connexive Logics. The If- CoLog Journal of Logics and their Applications 3(3), pp. 341–355.
[3] Tomasz Jarmużek (2021): Relating semantics as fine-grained semantics for intensional propositional logics. In Alessandro Giordani & Jacek Malinowski, editors: Logic in High Definition. Trends in Logical Semantics, Trends in Logic 56, Springer, Cham, pp. 13–30, doi:10.1007/978-3-030-53487-5_2.
[4] Tomasz Jarmużek & Bartosz J. Kaczkowski (2014): On some logic with a relation imposed on formulae: Tableau system F. Bulletin of the Section of Logic 43(1/2), pp. 53–72.
[5] Tomasz Jarmużek & Mateusz Klonowski (2021): Some intensional logics defined by relating semantics and tableau systems. In Alessandro Giordani & Jacek Malinowski, editors: Logic in High Definition. Trends in Logical Semantics, Trends in Logic 56, Springer, Cham, pp. 31–48, doi:10.1007/978-3-030-53487-5_3.
[6] Tomasz Jarmużek & Jacek Malinowski (2019): Boolean Connexive Logics: Semantics and tableau approach. Logic and Logical Philosophy 28(3), pp. 427–448, doi:10.12775/LLP.2019.003.
[7] Tomasz Jarmużek & Jacek Malinowski (2019): Modal Boolean Connexive Logics: Semantics and tableau approach. Bulletin of the Section of Logic 48(3), pp. 213–243, doi:10.18778/0138-0680.48.3.05.
[8] Jacek Malinowski (2019): Barbershop Paradox and Connexive Implication. Ruch Filozoficzny (Philosophical Movement) 75(2), pp. 109–115, doi:10.12775/RF.2019.023.
[9] Jacek Malinowski & Ricardo Arturo Nicolás-Francisco: Relating semantics for hyper-connexive and totally connexive logics. Forthcoming.
[10] Jacek Malinowski & Rafał Palczewski (2021): Relating Semantics for Connexive Logic. In Alessandro Giordani & Jacek Malinowski, editors: Logic in High Definition. Trends in Logical Semantics, Trends in Logic 56, Springer, Cham, pp. 49–65, doi:10.1007/978-3-030-53487-5_4.
María Manzano (University of Salamanca, Spain)
Talk title: Many-sorted logic
Abstract: Many-sorted logic is not only a natural logic for reasoning about more than one sort of objects, but also a unifying logic, the best target logic in translation issues, due to its efficient proof theory, flexibility, naturalness and versatility to adapt to reasoning about a variety of objects.
Translations can be seen as the path to completeness in three possible stages: abstract completeness at the first stage, weak and strong completeness at the other two. The case of second-order logic can act as the source of inspiration for translations of other logical systems. The idea is to include in the many-sorted structure obtained by direct conversion of the logic being translated a domain for sets (and relations); namely, for all sets and relations defined in the original logic with their own formulas. And so, we are somehow shifting to second-order logic. In these structures, the Comprehension Schema restricted to formulas which are translations is always true. The idea of restricting CS to obtain new logics is taken from Henkin [1].
References:
[1] Leon Henkin (1953): Banishing the rule of substitution for functional variables. Journal of Symbolic Logic 18(3), pp. 201–208, doi:10.2307/2267403.
Uwe Meixner (University of Augsburg, Germany)
Talk title: A Paradox for the Existence Predicate
Abstract: In this paper, a paradox is shown to arise from prima facie highly plausible assumptions for the existence predicate as applied to definite descriptions. There are several possibilities to evade the paradox; all involve modifications in first-order logic with identity, existence, and definite descriptions; some stay within classical logic, others leave it. The merits of the various "ways out" are compared. It is proposed, and supported by argument, that the most attractive "way out" is within classical logic and has the consequence that there is a new logical truth: "There is at least one nonexistent object." But this "exit" will certainly not be to everyone's taste and liking. Thus, the paradox defies complete resolution (as every good paradox should).
Daniele Mundici (University of Florence, Italy)
Talk title: Łukasiewicz logic and approximately finite-dimensional C*-algebras
Abstract: In the Polish tradition, a (propositional) logic L = LA arises from a structure (matrix) A on a universe U equipped with operations and constants, often including a top (designated) element 1. To take care of the fundamental notion of "consequence", A is usually equipped with an U-valued operation → on U2 satisfying conditions (a) x → y = 1 iff x ≤ y, and (b) x → (y → z) = y → (x → z). For instance, when U = {0,1} and ¬ x is the derived operation x → 0, the only algebra A = (U, ¬, →) satisfying condition (a) is the two-element boolean algebra, (b) automatically follows from (a), and LA is boolean logic. When U = [0,1] ⊆ ℝ, and → is a continuous function satisfying conditions (a)–(b), then ([0,1], ¬, →) is the standard Wajsberg algebra, [3]. Wajsberg algebras, like their term-equivalent MV-algebras, provide algebraic counterparts of infinite-valued Łukasiewicz logic Ł∞.
Let K0 be Grothendieck's functor and Γ the categorical equivalence between unital lattice-ordered abelian groups and MV-algebras. Combining K0 and Γ, from Elliott's classification [1] it follows that for every AF C*-algebra C with lattice-ordered K0(C), every Ł∞-formula φ codes a Murray-von Neumann equivalence class [p] = [p]φ,C of projections of C. Conversely, for every projection p of C there is an Ł∞-formula coding p. The logic algorithmic machinery of Ł∞ can be now applied to decision problem for AF C*-algebras. For instance: Is p a central projection of A? Is p = 0? Does [p] precede [q] in the Murray-von Neumann order of C? In [2] and [4] polytime reductions are constructed among these problems in any fixed AF algebra C such that K0(C) is lattice-ordered – a property of most AF algebras in the literature. The complexity of all these problems turns out to be polytime for many relevant AF algebras, including the Behncke-Leptin algebras Am,n, the CAR algebra, the Farey-Stern-Brocot algebra, Glimm's universal UHF algebra, and every Effros-Shen algebra Fθ for θ a real algebraic integer, or θ = 1/e, with e Euler's constant.
References:
[1] George A. Elliott (1976): On the Classification of Inductive Limits of Sequences of Semisimple Finite- Dimensional Algebras. Journal of Algebra 38, pp. 29–44, doi:10.1016/0021-8693(76)90242-8.
[2] Daniele Mundici (2018): Word problems in Elliott monoids. Advances in Mathematics 335, pp. 343–371, doi:10.1016/j.aim.2018.07.015.
[3] Daniele Mundici (2020): What the Łukasiewicz axioms mean. The Journal of Symbolic Logic 85(3), pp. 906–917, doi:10.1017/jsl.2020.74.
[4] Daniele Mundici (2021): Bratteli diagrams via the De Concini-Procesi theorem. Communications in Contemporary Mathematics 23(7), doi:10.1142/S021919972050073X. Article No. 2050073.
Hanamantagouda P. Sankappanavar (State University of New York at New Paltz, USA)
Talk title: Gautama and almost Gautama algebras and their associated logics
Abstract: The varieties of regular double Stone algebras and regular Kleene Stone Algebras are fairly well-known and well studied. The amazing similarity in their structures led me to introduce a new variety as a common generalization of the two varieties. The algebras in this new variety are called "Gautama algebras'" in memory and honor of the founders of Indian Logic: Medhatithi Gautama and Akshapada Gautama. It turns out that the variety G of Gautama algebras is the join of the variety of regular Stone algebra and regular Kleene Stone algebras and also that the variety G is the equivalent algebraic semantics of a new logic (in the sense of Blok and Pigozzi).
More recently, the variety G has been further generalized to "Almost Gautama algebras." It turns out that this new variety also has a corresponding logic.
In this lecture, I wish to present results about these new varieties and their corresponding logics.
Renate Schmidt (The University of Manchester, UK)
Talk title: Forgetting and Consequence-Based Knowledge Extraction for Description Logic Ontologies
Abstract: This presentation will give an overview of our ongoing work in developing knowledge extraction methods for description logic-based ontologies. Because the stored knowledge is not only given by axioms stated in an ontology but also by the knowledge that can be inferred from these axioms, knowledge extraction is a challenging problem. Forgetting creates a compact and faithful representation of the stored knowledge over a user-specified signature by performing inferences on the symbols not in this signature. After an introduction of the idea of forgetting, an overview of our forgetting tools and some applications we have explored, I will discuss recent work we have done in collaboration with SNOMED Intl to use our tools on the medical ontology SNOMED CT. Building on these experiences, we have developed a new consequence-based approach for computing self-contained subontologies that satisfy the SNOMED modelling guidelines. Such subontologies make it easier to reuse and share content, assist with ontology analysis, and querying and classification is faster.
The research was undertaken in several projects spanning several years funded by the UKRI/EPSRC (research, Doctoral awards, IAA), the University of Manchester and IHTSDO (SNOMED Intl).
Peter Schroeder-Heister (University of Tübingen, Germany)
Talk title: Contraction-free Logics and the Idea of an Intensional Proof-theoretic Semantics
Abstract: When we talk about intensional proof-theoretic semantics, we normally mean an approach, which takes into account not only whether something has been proved, but also how it has been proved and whether several ways of proving it should be considered different or not. Terefore its central concept is that of identity of proofs. However, there are other topics where intensionality comes in, which I would like to discuss. Using as an example the rule of contraction, I argue that we must distinguish between different ways the same formula is given to us (to use Frege's terminology). In the context of the paradoxes there are contexts where two occurrences of a formulas cannot plausibly contracted into one, as they are given to us in different ways. As another example I consider inductive definitions and argue that an alteration of their form, which does not alter their deductive strength, nevertheless affects which information can be extracted from them.
Yaroslav Shramko (Kryvyi Rih State Pedadogical University, Ukraine)
Talk title: Structural reasoning and four-valued logic: A case study
Abstract: Structural reasoning is reasoning that is governed exclusively by structural rules. In this context a proof system can be said to be structural if all of its proper inference rules are structural. A logic is considered to be structuralizable if it can be equipped with a sound and complete structural proof system. In my talk I will provide a general formulation of the problem of structuralizability, giving specific consideration to a family of logics that are based on the Dunn-Belnap four-valued semantics. It is shown how sound and complete structural proof systems can be constructed for a spectrum of logics within different logical frameworks.
