ABSTRACT. Cyclic proof theory provides finitary representations of inductive and fixpoint reasoning via non-wellfounded derivations. Provability logics, such as the Gödel–Löb logic GL and its reflexive counterpart Grz, are a natural arena for cyclic methods; yet, although intuitionistic logic embeds into both systems, a fully syntactic (derivation-transforming) proof of faithfulness for the GL embedding has been missing.

We introduce a cyclic sequent calculus for intuitionistic logic and prove, by a direct proof-theoretic argument, that cyclic reasoning is conservative over the standard intuitionistic system. Using cyclic calculi for GL and Grz that eliminate diagonal modal formulas, we then exploit the resulting structural alignment to give uniform, purely syntactic proofs of faithfulness of the provability interpretation of intuitionistic logic into both GL and Grz, avoiding any detour through semantics.

The talk is based on a joint work with Matteo Tesi.

ABSTRACT. We study three paraclassical propositional logics with two weak negations, obtained by combining the one-negation systems CLuN, CLaN, and CLoN. The negation ∼u is glut-tolerant and paraconsis- tent, while ∼a is gap-tolerant and paracomplete. We define the mixed systems CLoaN, CLouN, and CLauN, and provide sound and complete two-valued non-deterministic semantics for each of them. We then focus on CLauN, the system containing the primitive dual pair (∼a, ∼u). In this setting, clas- sical negation is recovered by a deterministic formula, while the interaction between the two weak negations is controlled by a formula-sensitive boundary parameter. We use this parameter to obtain a classical translation, local and finite forms of classical recapture, and a duality result for CLauN.

ABSTRACT. The constructive logic JP' is known to be the weakest logic between intuitionistic and minimal logic that satisfies Glivenko's theorem. In spite of this natural and desirable formal property, the motivation for its notion of negation remains rather elusive: it is characterised by the double negation of the law of explosion, which is not the most intuitive. In order to have an alternative perspective on this negation, we study in this paper a couple of natural deduction systems for JP'. We first present a system that is normalisable and satisfies a restricted form of the subformula property. Then a modification of this system is introduced, whose rules satisfy the separation of connectives and the full subformula property. Afterwards we turn our attention to a typed lambda-calculus, with respect to which our natural deduction enjoys the Curry-Howard correspondence, followed by a concluding discussion.

ABSTRACT. We introduce a uniform non-deterministic semantics for the hierarchy of paraconsistent systems mbC^n introduced by Ciuciura. The proposed construction generalizes Omori’s three-valued semantics for mbC^1 to all systems of the hierarchy. We prove soundness and completeness of the semantics with respect to the corresponding axiomatizations and show that the consequence relations of the systems mbC^n cannot be characterized by finite deterministic matrices with unrestricted valuations.

ABSTRACT. Cyclic Linear Logic (CyMALL) is a compromise between Commutative Linear Logic (MALL) and Noncommutative Linear Logic (Bilinear Logic). We do not admit commutativity of the tensor, but we still admit only one De Morgan negation. MALL and its variants are natural extensions of Full Lambek Calculus (FL). Abrusci proved that CyMALL is not a conservative extension of FL, if we admit additive constants in these logics. In this paper we show that Cyclic Nonassociative Bilinear Logic with both additive constants is a strongly conservative extension of Full Nonassociative Lambek Calculus with only one additive constant: the upper bound.

ABSTRACT. In this paper, we present a natural deduction system for a strong Kleene-based neutral free logic with definite descriptions. The system combines a three-valued propositional basis with free quantification, identity, existence, and rules for definite descriptions. The main result of the paper is the proof of the normalisation theorem.

ABSTRACT. While Russell's theory of definite descriptions, expressions of the form `the F', is almost incontrovertible in classical logic, in free logic matters stand differently. Several alternative theories have been proposed by Lambert and others, and the present paper adds two new ones by looking at Hintikka's work. I'll present tableaux calculi for five theories that form a linear hierarchy. The weakest theory is Lambert's minimal free theory of definite descriptions (MFD), which only says that anything is the F iff it is the unique existing F, the strongest one is a chosen object theory in which all improper definite descriptions refer to the same object, Lambert (FD2). Intermediate theories are Lambert's $FD1$, which adds t=ix(x=t) as an axiom to MFD, and the two new theories, in which this principle is provable. One is based on the idea that t is the F iff t is the unique existing F, which is taken from Hintikka's work (FDH), the other an amalgamate (FDA) of this theory and MFD. I'll briefly indicate their motivation in proof-theoretic semantics.

ABSTRACT. In the dissertation "Investigations into Logical Deduction", Gentzen introduced systems for logic based on ‘introduction’ and ‘elimination’ rules, and left a remark: "introductions represent the ‘definitions’ of the symbols concerned, and eliminations are no more than the consequences of these definitions." This idea of Gentzen was developed further by Prawitz who added that the introduction rule "may now be taken as the ‘meaning’ of the logical constant," and also explicitly acknowledged that the question arises how to make Gentzen's idea precise since the idea is quite vague. Against this background, the aim of this paper is to have a fresh look at Gentzen's idea from the perspective of non-deterministic semantics, an elegant and natural generalization of many-valued semantics. This is a project with a strong exploratory nature, with interesting implications for both proof-theoretic and model-theoretic semanticists, and I will try to present them without assuming any familiarity with non-deterministic semantics. [Ongoing joint work with Sara Ayhan]

ABSTRACT. A logic $\mathcal{L}$ is a logic of formal inconsistency ($LFI$) \textit{iff} the following conditions are satisfied for $\mathcal{L}$:

(1) the logic $\mathcal{L}$ is paraconsistent; that is, there exist formulas $\alpha$ and $\beta$ such that $\{\alpha, {\sim}\alpha\}\not\vdash_{\mathcal{L}}\beta$;

(2) For some $\alpha$ and $\beta$, we have $\{{\circ}\alpha, \alpha\}\not\vdash_{\mathcal{L}}\beta$ and $\{{\circ}\alpha, {\sim}\alpha\}\not\vdash_{\mathcal{L}}\beta$;

(3) $\{{\circ}\alpha, \alpha, {\sim}\alpha\}\vdash_{\mathcal{L}}\beta$ for every $\alpha$ and $\beta$.

\noindent The third condition is known as the principle of gentle explosion. The symbol `${\circ}$' is a unary connective representing the concept of consistency within the object language. When `${\circ}$' precedes a formula $\alpha$, it indicates that $\alpha$ is consistent.

In my talk, I discuss some results concerning strongly paraconsistent variants of Logics of Formal Inconsistency ($LFI$s). A logic $\mathcal{L}$ is considered strongly paraconsistent if it allows contradictions to be explicitly expressed within its own language without collapsing into triviality. We focus on extensions of $LFI$s obtained by adding certain contra-classical (more precisely, connexive) theses to the postulates of $LFI$s; i.e.,

$(AT)$ ${\sim}({\sim}\alpha\rightarrow\alpha)$

$(AT^{\star})$ ${\sim}(\alpha\rightarrow{\sim}\alpha)$

$(ATa)$ $\alpha\rightarrow{\sim}({\sim}\alpha\rightarrow\alpha)$

$(ATb)$ ${\sim}\alpha\rightarrow{\sim}(\alpha\rightarrow{\sim}\alpha)$.

\noindent The formulas $(AT)$ and $(AT^{\star})$ are commonly known as Aristotle's theses. The schemata $(ATa)$ and $(ATb)$ can be regarded as alternative formulations of these theses. This proposal carries significant philosophical implications, particularly from the perspective of da Costa’s philosophy underlying the hierarchy of C-systems. Da Costa’s approach involves a distinction within the object language between well-behaved and not well-behaved formulas--that is, those for which the principle of explosion holds and those for which it fails. This idea is generalized in $LFI$s, where the operator ${\circ}$ is assumed to express consistency, and the ${\circ}$-free fragment of $LFI$s considered a subsystem of classical propositional calculus. In contrast, the approach we discuss does not aim for the $\circ$-free fragment to coincide with classical propositional logic but rather with a contra-classical logic. Given that any contra-classical logic containing classical logic is trivial, da Costa’s original idea does not apply in this context. From the standpoint we adopt, no philosophical assumptions about the meaning of the operator ${\circ}$ are initially implied.

We begin by adding contra-classical theses to the axioms of $Ci$, then subsequently expand the set of axioms for other, stronger $LFI$s. Since some of the strongly paraconsistent logics defined over da Costa's $C_{\omega}$ fail to validate the principle of gentle explosion, two strategies are proposed as solutions:

(1) an alternative set of criteria for classifying a logic as an $LFI$--this leads to the introduction of \textit{Logics of Formal quasi-Inconsistency} ($LFqI$s), representing a more general concept of $LFI$s;

(2) an alternative approach to defining strongly paraconsistent logics, based on the requirement that each calculus must admit the principle of gentle explosion. Unlike the original $LFI$s, the logics presented here are not defined over da Costa's $C_{\omega}$ but over its weaker variant $C_{\omega}^{\sim}$. This approach produces a class of strongly paraconsistent calculi that not only satisfy the criteria for $LFI$s but also preserve the original axioms of $LFI$s while employing contra-classical theses.

ABSTRACT. This paper investigates Okada’s purely constructive implication. Gentzen (1936) pointed out the circularity in the intuitionists' justification of modus ponens, which Okada (1987) interpreted as the impredicativity of intuitionistic implication. Okada relegated this impredicative part to second-order intuitionistic propositional logic while weakening its propositional fragment to a subsystem called WLJ—a sequent calculus for strict implication S4I. Although Okada introduced the notion of validity based on “constructive interpretations of logical connectives" to provide semantics for WLJ, it was shown that derivability implies validity but not vice versa. Consequently, syntactically characterizing Okada’s validity has remained an open question. This paper makes progress toward resolving this question. We first demonstrate that for formulas whose main connective is implication, Okada’s validity coincides with the admissibility of the corresponding rule in S4I. Furthermore, we prove that characterizing Okada’s validity in general requires an additional condition beyond admissibility in S4I. These results highlight key issues to fully solve this open question.

ABSTRACT. This talk presents a geometric semantics for the logic KR (relevant logic R extended with the Duns Scotus axiom) and its variant $KR^-$ (KR without the axiom $[p \rightarrow (p \rightarrow q)] \rightarrow (p \rightarrow q)$, building on Urquhart's ternary-relational semantics for relevant logics, in which R(x,y,z) is read as "x, y and z lie on the same line" but did not pursue its connection to concrete finite geometries. We take up that connection directly and ask: what do the geometric structures corresponding to KR and $KR^-$look like?

\textbf{Framework.} We define a KR-structure as a tuple $\langle U,R,a \rangle$, where U is a non-empty universe, $a \in U$ is a distinguished element, and $R \subseteq U \times U \times U $ satisfies reflexivity-type conditions, a symmetry condition, and the Veblen–Young axiom $R(a,b,c) \wedge R(c,d,e) \Rightarrow \exists t (R(a,d,t) \wedge R(t,b,e))$. Reading R as a collinearity relation on a finite point set, we translate these algebraic conditions into axioms of an incidence geometry $\langle L, P, | \rangle$ (lines, points, incidence). Projective geometry is examined first as a candidate model but rejected as too strong, since it imposes duality (equal numbers of points and lines) and forces every line to carry the same number of points — constraints not implied by the KR-axioms themselves.

\textbf{Main results (Part I).} Treating the Veblen–Young axiom as a genuine implication — vacuously satisfied whenever two lines fail to meet — dissolves the duality requirement and permits "parallel" lines. This yields a three-tier classification: \begin{itemize} \item 3KR geometry: figures composed entirely of length-3 lines; we show that every such figure decomposes into copies of the three-point degenerate line and the Fano plane, and that 3KR geometry coincides with the class of Steiner Triple Systems S(2,3,n) together with the Fano plane. \item $KR^-$ geometry: subsumes 3KR geometry, projective planes, general Steiner systems, and mixed-length-line ("m,n-") geometries, in which lines are defined as unions of ternary R-relations over their points. \item KR geometry ($KR^+$): structures whose shortest lines have length $\geq 4$, obtained by adding the axiom $[p \rightarrow (p \rightarrow q)] \rightarrow (p \rightarrow q)$ ; the Fano plane and five-point model cannot occur here. \end{itemize} \textbf{Main results (Part II).} The second part of the talk introduces two structural operations for generating new KR structures and establishes their closure properties. \begin{itemize} \item Point-adjunction: adding an odd number of new points to a non-dualistic KR structure — lengthening existing lines and, when more than one point is added, introducing one further line consisting solely of new points — always yields a new KR structure with lines of varying length. Structures satisfying duality (the Fano plane, Steiner systems) cannot absorb such additions while remaining finite. \item Line-adjunction: attaching an entire new line of length $\geq 3$ to an KR structure, via a substructure decomposition, is shown always to preserve the KR-structure property, demonstrated on the Fano plane (yielding a 15-point, 35-line 3KR structure, proved by two independent methods) and on a 3,4-geometry (34 points, 124 lines). \item Point-elimination: the converse "gluing" operation $a \rightarrow b$ is shown to be admissible only within $KR^+$ structures (minimum line length 4), since eliminating a point from a length-3 line collapses it below the minimum required by the second KR axiom. Elimination may be iterated until a line would be reduced to two points, at which stage it must stop; moreover, no sequence of eliminations from an $KR^+$ structure can produce a 3KR structure. \end{itemize}

\textbf{Significance.} The results answer, for the first time, Urquhart's open question of which geometries correspond to KR and $KR^-$, situate the Fano plane and Steiner triple/quadruple systems within a unified geometric hierarchy for relevance logic, and provide constructive operations — adjunction and elimination — for building and reducing models within this hierarchy, laying groundwork for algebraic theory of KR geometries.

\begin{thebibliography}{9} \bibitem{andersonbelnap1975} Alan Ross Anderson and Nuel D. Belnap (1975) \emph{Entailment}, Vol. 1, Princeton University Press, Princeton. \bibitem{urquhart1996} Alasdair Urquhart (1996) \emph{Duality for Algebras of Relevant Logics}, \emph{Studia Logica}, Vol. 56, pp. 277--290. \bibitem{urquhart2017} Alasdair Urquhart (2017) \emph{The Geometry of Relevant Implication}, \emph{IFCoLog Journal of Logics and their Applications}, Vol. 4, No. 3, pp. 591--604. \end{thebibliography}

ABSTRACT. A pseudo-Heyting algebra generalizes the notion of a Heyting algebra. In the finite case, it can be viewed as a join-semidistributive lattice equipped with an additional operation $\leadsto$, which generalizes the relative pseudocomplement. We characterize the $\leadsto$-irreducible elements. We investigate the problem of determining which elements of a given pseudo-Heyting lattice can be represented as $\leadsto$-combinations of $\leadsto$-irreducible elements. We solve this problem for finite planar pseudo-Heyting algebras.

ABSTRACT. In this work, we present a novel paradox that affects most of the available contenders for an adequate semantic theory. Semantic paradoxes are commonly addressed through structural and substructural approaches. Such approaches leave certain principles outside the scope of what an adequate logic would be; the first renders invalid certain principles governing the logical operators, whereas the second excludes some features characteristic of the consequence relation.

Arguably, such approaches rest on the idea that logic is understood as the discipline that studies valid inference, and that specific logics are identified by the inferences they validate. However, this approach to defining logic has some shortcomings. In the present work, we provide several reasons for considering anti-valid inferences, discuss their significance, and outline the benefits of taking them into account. We motivate the adoption of a hybrid system that includes both valid and anti-valid inferences and show that expanding one's language with an antivalidity predicate leads to expressive limitations for the most promising accounts of developing semantic theories.

ABSTRACT. A semantics for a language is a relating semantics iff at least for one con- nective ci the valuation of all complex propositions of the form c(A₁, . . . , A_j), where j is the arity of c, in a world w requires not only valuations of pairs (A₁, w), . . . , (A_j , w), but also a valuation of j-tuples ((A₁, . . . , A_j ), w). A valuation of j-tuples ((A₁, . . . , A_j), w) can in a formal semantics represent various logical or non-logical relationships between A1, . . . , Aj in a world w, for example: content relationships (like relatedness relation), analytical relationships, causalities, temporal orderings, preference orderings, logical consequences of some logic, etc [1], [7].

During the 1st Workshop of Relating Logic, the following problem was posed:

Problem α: axiomatization of logics defined by relating semantics [4].

In the presentation we try to answer the problem of how to algorithmically provide adequate axiomatic systems for relating logics. We concentrate only on the fragments of mono-relating language with at least one relating connective (so, the logic is two-valued, its language is formed with a functionally complete set of classical connectives and one relation in a model is employed). We consider so called positive as well as negative relating properties of relations in models. However, even this approach allows us to define interesting systems of logic, both sub-classical and contra-classical [5], [6], [8], [3].

In the presentation we discuss two sub-problems of axiomatization: (a) relat- ing logics determined by positive conditions imposed on relations (already done in the paper [2]), (b) relating logics defined by arbitrary conditions imposed on relations, including negative conditions (an open problem). We also discuss the limitations of this method and the limitations of axiom- atizing relating semantics structures in general.

At the end, we will also demonstrate some connection between the presented metatheory and systems of sequent calculi. This will be a preliminary step toward a theory of sequent calculus for relating logics.

This work was prepared as part of a proposal funded by the National Science Centre (NCN, proposal number 2023/51/B/HS1/02983, "Relation based semantics: axiomatic and tableaux proof-calculi").

References

[1] Tomasz Jarmużek. Relating semantics as fine-grained semantics for inten- sional logics. In A. Giordani and J. Malinowski, editors, Logic in High Definition, volume 56 of Trends in Logic, pages 13–30. Springer, 2021. doi:10.1007/978-3-030-53487-5_2.

[2] Tomasz Jarmużek and Mateusz Klonowski. Axiomatization of BLRI deter- mined by limited positive relational properties. Logic and Logical Philosophy, pages 1–17, 2022. doi:0.12775/LLP.2022.003.

[3] Tomasz Jarmużek and Mateusz Klonowski. Tableaux for logics of content relationship and set-assignment semantics. Logica Universalis, 16:195–219, 2022. doi:10.1007/s11787-022-00293-w.

[4] Tomasz Jarmużek and Francesco Paoli. Relating logic and relating seman- tics. History, philosophical applications and some of technical problems. Logic and Logical Philosophy, 30(4):563–577, 2021.

[5] Tomasz Jarmużek and Jacek Malinowski. Boolean connexive logics: Seman- tics and tableau approach. Logic and Logical Philosophy, 28(3):427–448, 2019. doi:10.12775/LLP.2019.003.

[6] Mateusz Klonowski. Axiomatization of some basic and modal Boolean connexive logics. Logica Universalis, 15:517–536, 2021. doi:10.1007/ s11787-021-00291-4.

[7] Mateusz Klonowski. History of relating logic. The origin and research direc- tions. Logic and Logical Philosophy, 30(4):579–629, 2021. doi:10.12775/ LLP.2021.021.

[8] Mateusz Klonowski and Luis Estrada-Gonzalez. Boolean connexive logic and content relationship. Studia Logica, 112:207–248, 2024. doi:10.1007/ s11225-023-10058-1