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.

ABSTRACT. Monoidal closed categories are standard categorical models of NMILL, non-commutative multiplicative intuitionistic linear logic: the monoidal unit and tensor model the multiplicative unit and conjunction; the internal hom models linear implication. In recent years, the weaker notion of (left) skew monoidal closed category has been proposed by Ross Street, where the three structural laws of left and right unitality and associativity are not required to be invertible, they are merely natural transformations with a specific orientation. A question arises naturally: is it possible to find deductive systems which are naturally modelled by skew monoidal closed categories? We answer positively by introducing a cut-free sequent calculus for a skew version of NMILL that serves this purpose. We study the proof-theoretic semantics of the sequent calculus by identifying a calculus of derivations in normal form, obtained from an adaptation of Andreoli's focusing technique to the skew setting. The resulting focused sequent calculus peculiarly employs a system of tags for keeping track of new formulae appearing in the antecedent and appropriately reducing non-deterministic choices in proof search. Focusing solves the coherence problem for skew monoidal closed categories by exhibiting an effective procedure for deciding equality of canonical maps in all models.

ABSTRACT. The syntactic calculus of Lambek is a deductive system for the multiplicative fragment of intuitionistic non-commutative linear logic. As a fine-grained calculus of resources, it has many applications, mostly in formal computational investigations of natural languages. This paper introduces a calculus of $\beta\eta$-long normal forms for derivations in the Lambek calculus with multiplicative unit and conjunction among its logical connectives. Reduction to normal form follows the normalization by evaluation (NbE) strategy: (i) evaluate a derivation in a Kripke model of Lambek calculus; (ii) extract normal forms from the obtained semantic values. The implementation of the NbE algorithm requires the presence of a strong monad in the Kripke interpretation of positive formulae, in analogy with the extension of intuitionistic propositional logic with falsity and disjunction. The NbE algorithm can also be instantiated with minor variations to calculi for related substructural logics, such as multiplicative and dual intuitinistic linear logic.

ABSTRACT. In the Polish tradition, a (propositional) logic L = L_A 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 U₂ 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 L_A 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 K₀ be Grothendieck's functor and Γ the categorical equivalence between unital lattice-ordered abelian groups and MV-algebras. Combining K₀ and Γ, from Elliott's classification [1] it follows that for every AF C*-algebra C with lattice-ordered K₀(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 K₀(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 A_m,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 θ = ¹/_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.

ABSTRACT. The notion of non-deterministic logical matrix (where connectives are interpreted as multi-functions) preserves many good properties of traditional semantics based on logical matrices (where connectives are interpreted as functions) whilst finitely characterizing a much wider class of logics, and has proven to be decisive in a myriad of recent compositional results in logic. Crucially, when a finite non-deterministic matrix satisfies monadicity (distinct truth-values can be separated by unary formulas) one can automatically produce an axiomatization of the induced logic. Furthermore, the resulting calculi are analytical and enable algorithmic proof-search and symbolic counter-model generation.

For finite (deterministic) matrices it is well known that checking monadicity is decidable. We show that, in the presence of non-determinism, the property becomes undecidable. As a consequence, we conclude that there is no algorithm for computing the set of all multi-functions expressible in a given finite Nmatrix. The undecidability result is obtained by reduction from the halting problem for deterministic counter machines.

ABSTRACT. On the one hand, classical logic is an extremely successful theory, even if not being perfect. On the other hand, intuitionistic logic is, without a doubt, one of the most important non-classical logics. But, how can proponents of one logic view the other logic? In this paper, we focus on one of the directions, namely how classicists can view intuitionistic logic. To this end, we introduce an expansion of positive intuitionistic logic, both semantically and proof-theoretically, and establish soundness and strong completeness. Moreover, we discuss the interesting status of disjunction, and the possibility of combining classical logic and minimal logic. We also compare our system with the system of Caleiro and Ramos

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.