ABSTRACT. This talk is on a project aiming to explore the concept of ultimate ignorance of an agent, depending on the underlying logic of knowledge. By "ultimate ignorance" we formally mean a modal operator obtained by iterating (possibly transfinitely) the ignorance operator I, where Iϕ intuitively says that "The agent is ignorant whether ϕ is true", until stabilisation up to logical equivalence, if that stabilisation ever occurs. In the talk I will explore the logical behaviour of the finite hierarchy of iterated ignorance I, I²,... and its first limit operator I^ω and will demonstrate that, contrary to common expectation, that behaviour is generally rather complex, both in terms of the valid consequences between these operators and in terms of the semantic conditions corresponding to the respective implications between them, over relatively weaker underlying logics of knowledge. More specifically, I will focus on the expressiveness of the language L(I, I^ω) involving both I and I^ω and will first discuss frame correspondences of some simple formulas involving iterated ignorance over some natural frame classes. I will then demonstrate that over reflexive models I is not expressible in monadic second-order logic (MSO) and that the hierarchy of iteration does not stabilize at ω over such models. I will conclude with a brief discussion of some metalogical properties of L(I, I^ω) on some natural classes of frames.

ABSTRACT. Hamkins and Löwe described modal logic S4.2 through the notion of sets of independent buttons — statements that are possibly necessary — and switches — possibly necessary statements. In this article we investigate logics intermediate between S4.2 and S4.3 that are defined through a different notion of independence. We provide an axiomatic description of such logics, state some basic facts and prove various completeness and decidability results.

ABSTRACT. A new approach to information-based logics using many-logic modal structures (MLMSs) was recently proposed by Martins et al. In such a setting, it is possible to have worlds with different underlying logics within the same frame, all anchored to a base lattice that contains the semantics of each logic as a down-complete sublattice. In this paper, we take the lattice L6, defined by the six-valued semantics of the logic of evidence and truth LET+ K , as our base lattice. We also consider four-, three-, and two-valued formal systems associated with down-complete sublattices of L6. These logics are capable of representing paracomplete, paraconsistent, and classical contexts with six, four, three, and two informational scenarios, respectively. As applications of MLMSs, we will discuss the merging and temporal evolution of databases whose underlying logics are two-, three-, four-, and six-valued. We will also investigate inconsistency measures in this context.

ABSTRACT. Quantum logic has developed in various directions since its inception. However, many existing logical approaches either focus only on pure states, or use Hilbert-space models in which the abstract relationship between pure states, mixed states, and probabilities is not made explicit. In this work, we introduce a kripke model designed to handle quantum mixed states abstractly. Furthermore, we construct a proof system for the proposed logic and establish its completeness with respect to the intended semantics.

ABSTRACT. In this paper, we propose fuzzy topological semantics for Łukasiewicz valued modal logic, based on the standard Łukasiewicz algebra. Within this setting, formulas are interpreted as fuzzy sets of truth values, while the modal operators are realized through fuzzy interior and closure operators. We define a Kripke-induced fuzzy Alexandroff topology and establish a precise correspondence between Łukasiewicz fuzzy Kripke semantics and its topological counterpart. The proposed topological semantics validates the S4 modal axioms that include reflexivity, transitivity, monotonicity, normality, and the necessitation of truth.

ABSTRACT. Orthomodular logic has long been studied as a fundamental logical framework within quantum logic. In addition to its lattice-theoretic foundations, various formulations have been proposed that incorporate specialized implication connectives and more complex logical operators. In this study, we reconstruct orthomodular logic by introducing an operator referred to as restricted negation, which has received comparatively little attention in the existing literature. We demonstrate that this operator provides a natural and expressive basis for formulating the core principles of orthomodular logic. Furthermore, as a main result, we construct new proof system for orthomodular logic founded on this operator.

ABSTRACT. This paper provides arithmetical characterizations of the logical rules Ex Falso Quodlibet ($\mathsf{ECQ}$) and Absorption of Negation ($\mathsf{An}$). To this end, we introduce $\mathbf{NA}^{PR}$, a system of subminimal arithmetic, over which Heyting Arithmetic ($\mathbf{HA}$) is shown to be a conservative extension for positive formulas. Based on this subminimal arithmetic, we prove that $\mathsf{ECQ}$ is equivalent to the definability of disjunction. In addition, that $\mathsf{An}$ is equivalent to a variant of the least number principle. Furthermore, using the constant domain neighbourhood semantics, we show that the systems $\mathbf{NA}^{PR}$, $\mathbf{NA}^{PR}+\mathsf{An}$ written as $\mathbf{MA}^{PR}$, and $\mathbf{NA}^{PR}+\mathsf{An}+\mathsf{ECQ}$ written as $\mathbf{HA}^{PR}$ form a strictly increasing hierarchy of strength. Finally, we demonstrate the essential role of primitive recursive functions in weak arithmetic using classical countermodels.

ABSTRACT. Logical bilateralism challenges traditional concepts of logic by treating assertion and denial as independent yet opposed acts. While initially devised to justify classical logic, its constructive variants show that both acts admit intuitionistic interpretations. We will present a bilateral system where a formula cannot be both provable and refutable without contradiction, offering a framework for modelling mathematical proofs and refutations that exclude inconsistency. We formalise the logic via a bilateral natural deduction system with the desirable proof-theoretic properties of normalisation, subformula property and consistency, together with a base-extension semantics grounded in explicit proofs and refutations. Refutation is shown to coincide with Nelson's constructive falsity, extending intuitionistic logic for constructive epistemic reasoning. Finally, we will show how to obtain a well behaved bilateral sequent system and extend the work for the first-order setting.

This is a joint work with Victor Barroso-Nascimento and Maria Osório and Carlos Olarte.

ABSTRACT. This abstract explores the constructive thoroughly linear modal logic (CTLML). We establish a hypersequent calculus of CTLML with cut-elimination, decidability, disjunction property, and algebraic completeness. By enriching CTLML with some appropriate structural rules, we show that CTLML is the thoroughly linear core of the intuitionistic counterpart of S5, i.e., known as MIPC in the intuitionistic modal logic literature.

ABSTRACT. In 2015, the propositional logic of change LCBox was formulated [15]), drawing on the Aristotelian and Leibniz's reductionist conceptions of time. A crucial assumption in both of these approaches concerns the nature of time: time is considered secondary to change, i.e., without change in the world, time does not pass. LCBox is expressed in the propositional A-language containing two primitive modal operators: C, read "it changes whether", and Box for "it is constant that". It is interpreted in the Kripkean semantics of B-series, in which a discrete set of the world states is linearly ordered by succession relation. A sublogic of LCBox with the only one modal operator C was studied already in [12] and [14]. In [16] the extension of LCBox into a two-dimensional propositional logic was axiomatized and in [3] LCBox was used as a basis for an epistemic logic. In [13], LCBox was extended to a first-order logic. Weak completeness proofs were provided for all the constructed systems corresponding to the aforementioned logics.

Research on LCBox has shown that its definitional extension by the Next operator is equivalent to the Until-free fragment of LTL extended by an appropriate definition of the C operator. Thus, one can say that LCBox and the mentioned fragment of LTL originally formulated by D. Scott [7], are the reverse and obverse of the same coin. LTL without Until was later introduced into computer science by Pnueli [6] and investigated in [4] for program verification.

The project of formalizing logics with a primitive operator C is rooted in philosophical ideas, which are also related to formal issues. One of them is dealt with in the paper proposed here. We begin with the observation that, starting with LCBox, all original systems for its aforementioned extensions incorporate the so-called omega-rules. The latter allow one to infer that the formula A has a constant value from the fact that A never changes; they have infinitely many premises. It is known that infinite rules lend a deductive strength to the system, but in the case of the mentioned systems for logics of change, this has not yet been exploited. The proofs of only weak completeness theorems have been given for them, although, because they have infinite inference rules, a stronger result can be obtained. When a logical system satisfies the strong completeness theorem, it is possible to provide a formal proof whenever a conclusion is a semantic consequence of some extra-logical premises. In our case, the strong completeness theorem thus opens the perspective of applying logic LCBox and its extensions to extralogical theories that may be attractive in the framework of formal philosophy of time. Here, we prove a strong completeness for a certain infinitary system for LCBox. The result applies to all the mentioned extensions of LCBox.

The idea of formulating an infinitary system for Until-free fragment of LTL was taken up by Segerberg, who drew inspiration from von Wright’s "Always" (cf. [9]). Segerberg's intention was to give a proof of the strong completeness theorem for his system, however, the result was not entirely correct, and it was refined by Sundholm in [11]. Independently of Segerberg's approach infinite rules had already been applied in algorithmic logic by Salwicki [8] and Mirkowska [5]. Following them, Goldblatt began research concerning the application of infinitary rules in computational logic. Inv [1], he provided a strong completeness proof for an infinitary system for first-order dynamic logic. Then, he gave a general procedure for proving strong completeness for systems with infinitary rules that characterize various normal modal logics [2] (applied also to the Until-free fragment of LTL). Segerberg also formulated a general strategy for constructing strong completeness proofs for a certain class of normal logics in [10]. Mentioned strategies differ, but the core of the completeness proofs is the same: it always concerns the construction of a canonical model, which is based on an appropriate version of Lindenbaum's lemma. The point is that the procedure for extending any consistent set of formulas to a maximally consistent set, on which Lindenbaum's lemma is based, requires a kind of finitization of the infinite rules of the given system. In view of the results from [10] and [2], our outcome for LCBox is not surprising. However, LCBox is not normal, and this forces us to move slightly beyond the scope of known methodologies.

The presented results are included in [17].

[1] R. Goldblatt (1992): Logics of Time and Computation, 2nd edition. CSLI.

[2] R. Goldblatt (1993): Mathematics of Modality, 1st edition. CSLI.

[3] M. Łyczak (2021): The Modal Logic LEC for Changing Knowledge, Expressed in the Growing Language. Logic and Logical Philosophy 30(1), pp. 39–59.

[4] Z. Manna & A. Pnueli (1979): The modal logic of programs. In Hermann A. Maurer, editor: Automata, Languages and Programming, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 385–409.

[5] G. Mirkowska (1971): On formalized systems of algorithmic logic. Bulletin de l’Académie Polonaise des Sciences. Série des Sciences Mathématiques 19, pp. 421–428.

[6] A. Pnueli (1978): The Temporal Semantics of Concurrent Programs. Technical Report, Tel-Aviv University.

[7] A. Prior (1967): Past, Present and Future. Oxford University Press.

[8] A. Salwicki (1970): On the Predicate Calculi With Iteration Quantifiers. Bulletin de l’Académie Polonaise des Sciences. Série des Sciences Mathématiques 18(6), pp. 279–285.

[9] K. Segerberg (1989): Von Wright’s Tense Logic. In Paul Arthur Schilpp & Lewis Edwin Hahn, editors: The Philosophy of Georg Henrik von Wright, The Library of Living Philosophers 19, Open Court, pp. 603–635. Written in 1974.

[10] K. Segerberg (1994): A Model Existence Theorem in Infinitary Propositional Modal Logic. Journal of Philosophical Logic 23(4), pp. 337–367.

[11] G. Sundholm (1977): A Completeness Proof for an Infinitary Tense-Logic. Theoria 43, pp. 44–51.

[12] K. Świętorzecka (2008): Classical Conceptions of the Changeability of Situations and Things Represented in Formalized Languages. CSWU Publishing House.

[13] K. Świętorzecka (2024): First-order Logic of Change. Logic Journal of the IGPL 32(1), pp. 35–46.

[14] K. Świętorzecka & J. Czermak (2012): Some Calculus for a Logic of Change. Journal of Applied Non-Classical Logics 22(1), pp. 1–8.

[15] K. Świętorzecka & J. Czermak (2015): A Logic of Change with Modalities. Logique et Analyse 232, pp. 511–527.

[16] K. Świętorzecka & M. Łyczak (2022): Leibnizian Logic of Possible Laws: A Formal Framework Motivated by Hintikka That Blocks the Lovejoy’s Plenitude. Logic and Logical Philosophy 32(1), pp. 119–140.

[17] Kordula Świętorzecka (2026): A Strongly Complete Infinitary System for a Logic of Change. Submitted.

ABSTRACT. The short abstract is uploaded.

ABSTRACT. In Proof-Theoretic Semantics (PTS), meaning validity are explained through proof-conditions rather than truth-conditions. This approach relies on the techniques introduced by Prawitz in his normalization theory for Natural Deduction. In my talk, I am to propose an interpretation of PTS as a "double-model" semantics, arguing that validity of derivation-structures (the core-notion of PTS which that of validity of formulas is based on) is determined by the interplay between two distinct components: language models and computation models.

Language models are what Prawitz calls "atomic bases", i.e., sets of atomic rules that fix the behavior of the non-logical constants by showing how they behave at the level of atomic derivability (similarly to models in model-theoretic or Kripke semantics).

Computational models are given by mappings for the manipulation of derivation-structures which "interpret" non-introduction inferences by showing how they evaluate relative to introduction rules (the latter being constitutive of the meaning of the logical constants, along the lines of a famous suggestion by Gentzen).

By reframing PTS in this way, I show that PTS validity stems not just from the meaning of formulas, but from the "meaning" (i.e., the proof-rewriting behavior) of the non-introduction inferences. This "double-model" perspective provides a clearer account of why PTS validity is not always closed under the replacement of atoms, and highlights significant and overlooked connections to the finitist programs of Hilbert and Gentzen.

ABSTRACT. We consider a class of logics weaker than intuitionistic logic, commonly referred to in the literature as subintuitionistic logics, and investigate them with respect to the property of Halldén completeness.

ABSTRACT. A variety of proof systems for hybrid logics have been developed. In particular, hybrid logics formulated in languages with nominals, @, and ↓ were extended to infinitary proof systems for non-compact modal logics. The resulting system Khybω treats sequents Γ ⊢ φ as primitive and axiomatizes derivability directly by means of infinitary sequent rules, with the deduction theorem internalized as a rule on sequents. By adding countably many pure sequents, one obtains strongly complete calculi for non-compact classes of general frames, including reachability frames, finite-cycle frames, transitive-closure frames, and frames satisfying the bounded chain condition. Completeness is proved using named models generated from saturated sets closed under infinitary sequents and witness conditions.

In this paper, we study a hybrid temporal language with the temporal operator F and the hybrid operators @ and ↓, interpreted over discrete linear frames. We consider a non-compact logic and so strong completeness cannot be achieved by finitary methods. In our language, the next operator is definable:

◯φ := ↓x F ↓y @x(F(y ∧ φ) ∧ ¬FFy)

where F is interpreted as strong future. This yields non-compactness: {p, ◯p, ◯◯p, ...} ∪ {¬Gp} is unsatisfiable, while each of its finite subsets is satisfiable. Our aim is to construct a strongly complete quasi-Hilbert-style proof system with infinitary rules of inference.

Several general approaches to strong completeness for non-compact modal logics with infinitary rules have been developed in the literature, most notably by Goldblatt and Segerberg. Goldblatt defines derivability in terms of theories closed under infinitary rules, whereas Segerberg works within natural deduction systems. In both approaches, strong completeness relies on extending consistent sets to maximally consistent theories compatible with infinitary rules. In the infinitary setting, however, the standard Lindenbaum construction requires additional finitization conditions. Following Goldblatt and Świętorzecka, we formulate a quasi-Hilbert-style infinitary system in which derivability is defined via closure conditions on theories. This framework enables us to establish the deduction theorem and prove strong completeness. Unlike the systems considered by Kooi et al., our infinitary rules are not restricted to pure formulas.

ABSTRACT. In his seminal book Counterfactuals, David Lewis developed an account of counterfactual conditionals as variably strict conditionals [1]. The resulting systems are commonly known as V-logics. Although several tableau systems have been proposed in the literature for this interpretation of counterfactuals (see, for example, [2]), to the best of our knowledge no such system is available for V-logics formulated within the framework of sphere semantics (see also [3, p. 93]). In this talk, we address this gap. Building on the metatheory of tableau systems developed in [4], [5] and [6], we introduce tableaux for the base logic V and some of its extensions. The key technique we use here is tracing the origin of the expressions decomposed in the proof.

This work was prepared as part of a proposal funded by the National Science Centre (NCN, proposal number 2025/58/A/HS1/00472, "What if Connexive Implication Governed Inference? A Study in Theory and Motivation").

References

[1] David Lewis (1973): Counterfactuals. Blackwell, Malden, Mass., doi:10.2307/2273738.

[2] Daniel Rönnedal (2009): Counterfactuals and Semantic Tableaux. Logic and Logical Philosophy 18(1), pp. 71–91, doi:10.12775/llp.2009.006.

[3] Graham Priest (2008): An Introduction to Non-Classical Logic: From If to Is, 2nd edition. Cambridge University Press, Cambridge, doi:10.1017/CBO9780511801174.

[4] Tomasz Jarmużek (2023): Metatheory of tableau systems. Nicolaus Copernicus University Press, Toruń, 244 pp., ISBN 978-83-231-5239-2.

[5] Tomasz Jarmużek (2014): Tableau Metatheorem for Modal Logics. In Roberto Ciuni, HeinrichWansing and Caroline Willkommen, editors: Recent Trends in Philosophical Logic, Trends in Logic 41, Springer, Cham, pp. 103–126, doi:10.1007/978-3-319-06080-4_8.

[6] Tomasz Jarmużek and Rajeev Goré (2025): Tableau methodology for propositional logics. arXiv:2511.16781, doi:10.48550/arXiv.2511.16781