Recent zbMATH articles in MSC 03Fhttps://www.zbmath.org/atom/cc/03F2021-04-16T16:22:00+00:00WerkzeugDialectica interpretation with marked counterexamples.https://www.zbmath.org/1456.030882021-04-16T16:22:00+00:00"Trifonov, Trifon"https://www.zbmath.org/authors/?q=ai:trifonov.trifon-aSummary: Goedel's functional ``Dialectica'' interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples. In the original interpretation decidability of atoms is required to compute the correct counterexample from a set of candidates. When combined with recursion, this choice needs to be made for every step in the extracted program, however, in some special cases the decision on negative witnesses can be calculated only once. We present a variant of the interpretation in which the time complexity of extracted programs can be improved by marking the chosen witness and thus avoiding recomputation. The achieved effect is similar to using an abortive control operator to interpret computational content of non-constructive principles.
For the entire collection see [Zbl 1391.03011].Relating sequent calculi for bi-intuitionistic propositional logic.https://www.zbmath.org/1456.030222021-04-16T16:22:00+00:00"Pinto, Luís"https://www.zbmath.org/authors/?q=ai:pinto.luis-f"Uustalu, Tarmo"https://www.zbmath.org/authors/?q=ai:uustalu.tarmoSummary: Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic.
In this paper, we compare three sequent calculi for bi-intuitionistic propositional logic: (1) a basic standard-style sequent calculus that restricts the premises of implication-right and exclusion-left inferences to be single-conclusion resp. single-assumption and is incomplete without the cut rule, (2) the calculus with nested sequents by \textit{R. Goré} et al. [in: Advances in modal logic. Vol. 7. Proceedings of the 7th conference (AiML 2008), Nancy, France, September 9--12, 2008. London: College Publications. 43--66 (2008; Zbl 1244.03157)], where a complete class of cuts is encapsulated into special ``unnest'' rules and (3) a cut-free labelled sequent calculus derived from the Kripke semantics of the logic. We show that these calculi can be translated into each other and discuss the ineliminable cuts of the standard-style sequent calculus.
For the entire collection see [Zbl 1391.03011].An applicative theory for \textsf{FPH}.https://www.zbmath.org/1456.030612021-04-16T16:22:00+00:00"Kahle, Reinhard"https://www.zbmath.org/authors/?q=ai:kahle.reinhard"Oitavem, Isabel"https://www.zbmath.org/authors/?q=ai:oitavem.isabelSummary: In this paper we introduce an applicative theory which characterizes the polynomial hierarchy of time.
For the entire collection see [Zbl 1391.03011].Superdeduction in \(\bar{\lambda}\mu\tilde{\mu}\).https://www.zbmath.org/1456.030862021-04-16T16:22:00+00:00"Houtmann, Clément"https://www.zbmath.org/authors/?q=ai:houtmann.clementSummary: Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. A proof-term language and a cut-elimination reduction already exist for superdeduction, both based on \textit{C. Urban}'s work on classical sequent calculus [Classical logic and computation. Cambridge: University of Cambridge (PhD Thesis) (2000)]. However the computational content of Christian Urban's calculus is not directly related to the (\(\lambda\)-calculus based) Curry-Howard correspondence. In contrast the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus is a \(\lambda\)-calculus for classical sequent calculus. This short paper is a first step towards a further exploration of the computational content of superdeduction proofs, for we extend the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. We also prove strong normalisation for this extension of the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus.
For the entire collection see [Zbl 1391.03011].Proof nets for multiplicative cyclic linear logic and Lambek calculus.https://www.zbmath.org/1456.030922021-04-16T16:22:00+00:00"Abrusci, V. Michele"https://www.zbmath.org/authors/?q=ai:abrusci.vito-michele"Maieli, Roberto"https://www.zbmath.org/authors/?q=ai:maieli.robertoSummary: This paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.Interactive learning based realizability and 1-backtracking games.https://www.zbmath.org/1456.030902021-04-16T16:22:00+00:00"Aschieri, Federico"https://www.zbmath.org/authors/?q=ai:aschieri.federicoSummary: We prove that interactive learning based classical realizability (introduced by the author and \textit{S. Berardi} for first order arithmetic [Log. Methods Comput. Sci. 6, No. 3, Paper No. 19, 22 p. (2010; Zbl 1201.03052)]) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. We also sketch some ongoing work about how to extend our notion of realizability in order to obtain completeness with respect to Coquand semantics, when it is restricted to 1-Backtracking games.
For the entire collection see [Zbl 1391.03011].Mackey-complete spaces and power series -- a topological model of differential linear logic.https://www.zbmath.org/1456.031002021-04-16T16:22:00+00:00"Kerjean, Marie"https://www.zbmath.org/authors/?q=ai:kerjean.marie"Tasson, Christine"https://www.zbmath.org/authors/?q=ai:tasson.christineSummary: In this paper, we describe a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted as bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we use a notion of power series between Mackey-complete spaces, generalizing entire functions in \(\mathbb{C}\). Finally, we get a quantitative model of Intuitionist Differential Linear Logic, with usual syntactic differentiation and where interpretations of proofs decompose as a Taylor expansion.Classical realizability and arithmetical formulæ.https://www.zbmath.org/1456.030262021-04-16T16:22:00+00:00"Guillermo, Mauricio"https://www.zbmath.org/authors/?q=ai:guillermo.mauricio"Miquey, Ètienne"https://www.zbmath.org/authors/?q=ai:miquey.etienneSummary: In this paper, we treat the specification problem in Krivine classical realizability
[\textit{J.-L. Krivine}, Panor. Synth. 27, 197--229 (2009; Zbl 1206.03017)], in the case of arithmetical formulæ. In the continuity of previous works from
[the first author, Jeux de réalisabilité en arithmétique classique. Paris: Université Paris 7 (PhD thesis) (2008);
the first author and \textit{A. Miquel}, Math. Struct. Comput. Sci. 26, No. 7, 1269--1303 (2016; Zbl 1425.03009)], we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first sections, we recall the definition of classical realizability, as well as a few technical results. In Section 5, we introduce in more details the specification problem and the intuition of the game-theoretic point of view we adopt later. We first present a game \(\mathbb{G}^1\), that we prove to be adequate and complete if the language contains no instructions `\texttt{quote}'
[\textit{J.-L. Krivine}, Theor. Comput. Sci. 308, No. 1--3, 259--276 (2003; Zbl 1169.03328)], using interaction constants to do substitution over execution threads. We then show that as soon as the language contain `\texttt{quote}', the game is no more complete, and present a second game \(\mathbb{G}^2\) that is both adequate and complete in the general case. In the last Section, we draw attention to a model-theoretic point of view and use our specification result to show that arithmetical formulæ are absolute for realizability models.Constructive forcing, CPS translations and witness extraction in interactive realizability.https://www.zbmath.org/1456.031092021-04-16T16:22:00+00:00"Aschieri, Federico"https://www.zbmath.org/authors/?q=ai:aschieri.federicoSummary: In Interactive realizability for second-order Heyting Arithmetic with \textsf{EM}\(_1\) and \textsf{SK}\(_1\) (the excluded middle and Skolem axioms restricted to \(\Sigma_1^0\)-formulas), realizers are written in a classical version of Girard's System \textsf{F}. Since the usual reducibility semantics does not apply to such a system, we introduce a constructive forcing/reducibility semantics: though realizers are not computable functionals in the sense of Girard, they can be forced to be computable. We apply this semantics to show how to extract witnesses for realizable \(\Pi_2^0\)-formulas. In particular, a constructive and efficient method is introduced. It is based on a new `(state-extending-continuation)-passing-style translation' whose properties are described with the constructive forcing/reducibility semantics.The conservation theorem for differential nets.https://www.zbmath.org/1456.031032021-04-16T16:22:00+00:00"Pagani, Michele"https://www.zbmath.org/authors/?q=ai:pagani.michele"Tranquilli, Paolo"https://www.zbmath.org/authors/?q=ai:tranquilli.paoloSummary: We prove the conservation theorem for differential nets -- the graph-theoretical syntax of the differential extension of Linear Logic (Ehrhard and Regnier's \textsf {DILL}). The conservation theorem states that the property of having infinite reductions (here infinite chains of cut elimination steps) is preserved by non-erasing steps. This turns the quest for strong normalisation (SN) into one for non-erasing weak normalisation (WN), and indeed we use this result to prove SN of simply typed \textsf {DILL} (with promotion).
Along the way to the theorem we achieve a number of additional results having their own interest, such as a standardisation theorem and a slightly modified system of nets, \textsf {DILL}\(_{\partial\varrho}\).Natural deduction for Post's logics and their duals.https://www.zbmath.org/1456.030472021-04-16T16:22:00+00:00"Petrukhin, Yaroslav"https://www.zbmath.org/authors/?q=ai:petrukhin.yaroslav-igorevichSummary: In this paper, we introduce the notion of dual Post's negation and an infinite class of Dual Post's finitely-valued logics which differ from Post's ones with respect to the definitions of negation and the sets of designated truth values. We present adequate natural deduction systems for all Post's \(k\)-valued \((k\geqslant 3)\) logics as well as for all Dual Post's \(k\)-valued logics.An explicit formula for the free exponential modality of linear logic.https://www.zbmath.org/1456.031022021-04-16T16:22:00+00:00"Melliès, Paul-André"https://www.zbmath.org/authors/?q=ai:mellies.paul-andre"Tabareau, Nicolas"https://www.zbmath.org/authors/?q=ai:tabareau.nicolas"Tasson, Christine"https://www.zbmath.org/authors/?q=ai:tasson.christineSummary: The exponential modality of linear logic associates to every formula \(A\) a commutative comonoid \(!A\) which can be duplicated in the course of reasoning. Here, we explain how to compute the free commutative comonoid \(!A\) as a sequential limit of equalizers in any symmetric monoidal category where this sequential limit exists and commutes with the tensor product. We apply this general recipe to a series of models of linear logic, typically based on coherence spaces, Conway games and finiteness spaces. This algebraic description unifies for the first time a number of apparently different constructions of the exponential modality in spaces and games. It also sheds light on the duplication policy of linear logic, and its interaction with classical duality and double negation completion.Jump from parallel to sequential proofs: exponentials.https://www.zbmath.org/1456.030962021-04-16T16:22:00+00:00"Di Giamberardino, Paolo"https://www.zbmath.org/authors/?q=ai:di-giamberardino.paoloSummary: In previous works, by importing ideas from game semantics (notably Faggian-Maurel-Curien's \textit{ludics nets}), we defined a new class of multiplicative/additive polarized proof nets, called \textit{J-proof nets}. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using \textit{jumps} (that is, untyped extra edges) as sequentiality constraints. Starting from this result, in the present work, we extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: More precisely, we replace the familiar linear logic notion of exponential box with a less restricting one (called \textit{cone}) defined by means of jumps. As a consequence, we get a syntax for polarized nets where, instead of a structure of boxes nested one into the other, we have one of cones which can be \textit{partially overlapping}. Moreover, we define cut-elimination for exponential J-proof nets, proving, by a variant of Gandy's method, that even in case of `superposed' cones, reduction enjoys confluence and strong normalization.On geometry of interaction for polarized linear logic.https://www.zbmath.org/1456.030982021-04-16T16:22:00+00:00"Hamano, Masahiro"https://www.zbmath.org/authors/?q=ai:hamano.masahiro"Scott, Philip"https://www.zbmath.org/authors/?q=ai:scott.philip-jSummary: We present Geometry of Interaction (GoI) models for Multiplicative Polarized Linear Logic, \textsf{MLLP}, which is the multiplicative fragment of Olivier Laurent's Polarized Linear Logic. This is done by uniformly adding \textit{multi-points} to various categorical models of GoI. Multi-points are shown to play an essential role in semantically characterizing the dynamics of proof networks in polarized proof theory. For example, they permit us to characterize the key feature of polarization, \textit{focusing}, as well as being fundamental to our construction of concrete polarized GoI models.
Our approach to polarized GoI involves following two independent studies, based on different categorical perspectives of GoI:
(i) Inspired by the work of Abramsky, Haghverdi and Scott, a \textit{polarized GoI situation} is defined in which multi-points are added to a traced monoidal category equipped with a reflexive object \(U\). Using this framework, categorical versions of Girard's execution formula are defined, as well as the GoI interpretation of \textsf{MLLP} proofs. Running the execution formula is shown to characterize the focusing property (and thus polarities) as well as the dynamics of cut elimination.
(ii) The construction of Joyal-Street-Verity is another fundamental categorical structure for modelling GoI. Here, we investigate it in a multi-pointed setting. Our presentation yields a compact version of Hamano-Scott's polarized categories, and thus denotational models of \textsf{MLLP}. These arise from a contravariant duality between monoidal categories of \textit{positive} and \textit{negative} objects, along with an appropriate bimodule structure (representing `non-focused proofs') between them.
Finally, as a special case of (ii) above, a compact model of \textsf{MLLP} is also presented based on \textsf{Rel} (the category of sets and relations) equipped with multi-points.Transport of finiteness structures and applications.https://www.zbmath.org/1456.031082021-04-16T16:22:00+00:00"Tasson, Christine"https://www.zbmath.org/authors/?q=ai:tasson.christine"Vaux, Lionel"https://www.zbmath.org/authors/?q=ai:vaux.lionelSummary: We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: These include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the lines of the coherence semantics of system T.An introduction to differential linear logic: proof-nets, models and antiderivatives.https://www.zbmath.org/1456.030972021-04-16T16:22:00+00:00"Ehrhard, Thomas"https://www.zbmath.org/authors/?q=ai:ehrhard.thomasSummary: Differential linear logic enriches linear logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for differential linear logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last, we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.Expressing additives using multiplicatives and subexponentials.https://www.zbmath.org/1456.030942021-04-16T16:22:00+00:00"Chaudhuri, Kaustuv"https://www.zbmath.org/authors/?q=ai:chaudhuri.kaustuvSummary: Subexponential logic is a variant of linear logic with a family of exponential connectives -- called \textit{subexponentials} -- that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that a classical propositional multiplicative subexponential logic (\textsc{msel}) with one unrestricted and two linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. We then show how the additive connectives can be directly simulated by giving an encoding of propositional multiplicative additive linear logic (\textsc{mall}) in an \textsc{msel} with one unrestricted and four linear subexponentials.Multi-focused cut elimination.https://www.zbmath.org/1456.030932021-04-16T16:22:00+00:00"Brock-Nannestad, Taus"https://www.zbmath.org/authors/?q=ai:brock-nannestad.taus"Guenot, Nicolas"https://www.zbmath.org/authors/?q=ai:guenot.nicolasSummary: We investigate cut elimination in multi-focused sequent calculi and the impact on the cut elimination proof of design choices in such calculi. The particular design we advocate is illustrated by a multi-focused calculus for full linear logic using an explicitly polarised syntax and incremental focus handling, for which we provide a syntactic cut elimination procedure. We discuss the effect of cut elimination on the structure of proofs, leading to a conceptually simple proof exploiting the strong structure of multi-focused proofs.A simulation of natural deduction and Gentzen sequent calculus.https://www.zbmath.org/1456.030842021-04-16T16:22:00+00:00"Kozhemiachenko, Daniil"https://www.zbmath.org/authors/?q=ai:kozhemiachenko.daniilWe consider four natural deduction systems: Fitch-style systems, Gentzen-style systems (in the form of dags), general deduction Frege systems and nested deduction Frege systems, as well as dag-like Gentzen-style sequent calculi. All these calculi soundly and completely formalize classical propositional logic.
We show that general deduction Frege systems and Gentzen-style natural calculi provide at most quadratic speedup over nested deduction Frege systems and Fitch-style natural calculi and at most cubic speedup over Gentzen-style sequent calculi.Some results related to the continuity problem.https://www.zbmath.org/1456.030632021-04-16T16:22:00+00:00"Spreen, Dieter"https://www.zbmath.org/authors/?q=ai:spreen.dieterSummary: The continuity problem, i.e., the question whether effective maps between effectively given topological spaces are effectively continuous, is reconsidered. In earlier work, it was shown that this is always the case, if the effective map also has a witness for non-inclusion. The extra condition does not have an obvious topological interpretation. As is shown in the present paper, it appears naturally where in the classical proof that sequentially continuous maps are continuous, the Axiom of Choice is used. The question is therefore whether the witness condition appears in the general continuity theorem only for this reason, i.e., whether effective operators are effectively sequentially continuous. For two large classes of spaces covering all important applications, it is shown that this is indeed the case. The general question, however, remains open.
Spaces in this investigation are in general \textit{not} required to be Hausdorff. They only need to satisfy the weaker \(T_{0}\) separation conditionTowards a descriptive theory of cb\(_{0}\)-spaces.https://www.zbmath.org/1456.030772021-04-16T16:22:00+00:00"Selivanov, Victor"https://www.zbmath.org/authors/?q=ai:selivanov.victor-lSummary: The paper tries to extend some results of the classical Descriptive Set Theory to as many countably based \(T_{0}\)-spaces (cb\(_{0}\)-spaces) as possible. Along with extending some central facts about Borel, Luzin and Hausdorff hierarchies of sets we also consider the more general case of \(k\)-partitions. In particular, we investigate the difference hierarchy of \(k\)-partitions and the fine hierarchy closely related to the Wadge hierarchy.On the weak computability of continuous real functions.https://www.zbmath.org/1456.030642021-04-16T16:22:00+00:00"Bauer, Matthew S."https://www.zbmath.org/authors/?q=ai:bauer.matthew-steven"Zheng, Xizhong"https://www.zbmath.org/authors/?q=ai:zheng.xizhongSummary: In computable analysis, sequences of rational numbers which effectively converge to a real number \(x\) are used as the (\(\rho\text{-})\) names of \(x\). A real number \(x\) is computable if it has a computable name, and a real function \(f\) is computable if there is a Turing machine \(M\) which computes \(f\) in the sense that, \(M\) accepts any \(\rho\)-name of \(x\) as input and outputs a \(\rho\)-name of \(f(x)\) for any \(x\) in the domain of \(f\). By weakening the effectiveness requirement of the convergence and classifying the converging speeds of rational sequences, several interesting classes of real numbers of weak computability have been introduced in literature, e.g., in addition to the class of computable real numbers (EC), we have the classes of semi-computable (SC), weakly computable (WC), divergence bounded computable (DBC) and computably approximable real numbers (CA). In this paper, we are interested in the weak computability of continuous real functions and try to introduce an analogous classification of weakly computable real functions. We present definitions of these functions by Turing machines as well as by sequences of rational polygons and prove these two definitions are not equivalent. Furthermore, we explore the properties of these functions, and among others, show their closure properties under arithmetic operations and composition.
For the entire collection see [Zbl 1391.03010].Effective Riemann mappings of multiply connected domains and Riemann surfaces.https://www.zbmath.org/1456.030702021-04-16T16:22:00+00:00"Rettinger, Robert"https://www.zbmath.org/authors/?q=ai:rettinger.robertSummary: We give new proofs of effective versions of the Riemann mapping theorem, its extension to multiply connected domains and the uniformization on Riemann surfaces. Astonishingly, in the presented proofs, we need barely more than computational compactness and the classical results.On the computational complexity of the Dirichlet problem for Poisson's equation.https://www.zbmath.org/1456.030692021-04-16T16:22:00+00:00"Kawamura, Akitoshi"https://www.zbmath.org/authors/?q=ai:kawamura.akitoshi"Steinberg, Florian"https://www.zbmath.org/authors/?q=ai:steinberg.florian"Ziegler, Martin"https://www.zbmath.org/authors/?q=ai:ziegler.martinSummary: The last years have seen an increasing interest in classifying (existence claims in) classical mathematical theorems according to their strength. We pursue this goal from the refined perspective of computational complexity. Specifically, we establish that rigorously solving the Dirichlet Problem for Poisson's Equation is in a precise sense `complete' for the complexity class \(\#\mathcal{P}\) and thus as hard or easy as parametric Riemann integration [\textit{H. Friedman}, Adv. Math. 53, 80--98 (1984; Zbl 0563.03023); \textit{K.-I Ko}, Complexity theory of real functions. Boston, MA etc.: Birkhäuser (1991; Zbl 0791.03019)].Subexponentials in non-commutative linear logic.https://www.zbmath.org/1456.030992021-04-16T16:22:00+00:00"Kanovich, Max"https://www.zbmath.org/authors/?q=ai:kanovich.max-i"Kuznetsov, Stepan"https://www.zbmath.org/authors/?q=ai:kuznetsov.s-l"Nigam, Vivek"https://www.zbmath.org/authors/?q=ai:nigam.vivek"Scedrov, Andre"https://www.zbmath.org/authors/?q=ai:scedrov.andreSummary: Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.On the unification of classical, intuitionistic and affine logics.https://www.zbmath.org/1456.031012021-04-16T16:22:00+00:00"Liang, Chuck"https://www.zbmath.org/authors/?q=ai:liang.chuckSummary: This article presents a \textit{unified logic} that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the \(\lambda\mu\) calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.Hybrid linear logic, revisited.https://www.zbmath.org/1456.030952021-04-16T16:22:00+00:00"Chaudhuri, Kaustuv"https://www.zbmath.org/authors/?q=ai:chaudhuri.kaustuv"Despeyroux, Joëlle"https://www.zbmath.org/authors/?q=ai:despeyroux.joelle"Olarte, Carlos"https://www.zbmath.org/authors/?q=ai:olarte.carlos"Pimentel, Elaine"https://www.zbmath.org/authors/?q=ai:pimentel.elaineSummary: HyLL (Hybrid Linear Logic) is an extension of intuitionistic linear logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgements are labelled by \textit{worlds} (having a monoidal structure) and hybrid connectives (\texttt{at} and \(\downarrow)\) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in linear logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the LL exponentials (!, ?) are decorated with labels representing \textit{locations}, and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL\(^\Cap\) (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (\(\mu\)HyMALL), which can be encoded into multiplicative additive linear logic with fixed points (\(\mu\)MALL). As an application, we propose encodings of Computational Tree Logic (CTL) into both \(\mu\)MALL and \(\mu\)HyMALL. In the former, states are represented as atoms in the linear context, hence reflecting a more \textit{operational} view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the \textit{semantics} of CTL.On Banach spaces of sequences and free linear logic exponential modality.https://www.zbmath.org/1456.031062021-04-16T16:22:00+00:00"Slavnov, Sergey"https://www.zbmath.org/authors/?q=ai:slavnov.sergeySummary: We introduce a category of vector spaces modelling full propositional linear logic, similar to probabilistic coherence spaces and to Koethe sequences spaces. Its objects are \textit{rigged sequence spaces}, Banach spaces of sequences, with norms defined from pairing with finite sequences, and morphisms are bounded linear maps, continuous in a suitable topology. The main interest of the work is that our model gives a realization of the free linear logic exponentials construction.Complexity of translations from resolution to sequent calculus.https://www.zbmath.org/1456.030872021-04-16T16:22:00+00:00"Reis, Giselle"https://www.zbmath.org/authors/?q=ai:reis.giselle"Woltzenlogel Paleo, Bruno"https://www.zbmath.org/authors/?q=ai:woltzenlogel-paleo.brunoSummary: Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.Deep inference and expansion trees for second-order multiplicative linear logic.https://www.zbmath.org/1456.031072021-04-16T16:22:00+00:00"Straßburger, Lutz"https://www.zbmath.org/authors/?q=ai:strassburger.lutzSummary: In this paper, we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.Expansion trees with cut.https://www.zbmath.org/1456.030852021-04-16T16:22:00+00:00"Aschieri, Federico"https://www.zbmath.org/authors/?q=ai:aschieri.federico"Hetzl, Stefan"https://www.zbmath.org/authors/?q=ai:hetzl.stefan"Weller, Daniel"https://www.zbmath.org/authors/?q=ai:weller.daniel-sSummary: Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher-order logics by recording the information of which instances have been chosen for which quantifiers. This compact representation is known in the literature as Miller's expansion tree proof. It is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cuts have been proposed. These extensions are based on graphical formalisms similar to proof nets and are limited to prenex formulas.
In this paper, we present a new syntactic approach that directly extends Miller's expansion trees by cuts and also covers non-prenex formulas. We describe a cut-elimination procedure for our expansion trees with cut that is based on the natural reduction steps and shows that it is weakly normalizing.Does the implication elimination rule need a minor premise?https://www.zbmath.org/1456.030832021-04-16T16:22:00+00:00"Francez, Nissim"https://www.zbmath.org/authors/?q=ai:francez.nissimSummary: The paper introduces \(NJ^g\), a variant of Gentzen's \(NJ\) natural deduction system, in which the implication elimination rule has no minor premise. The \(NJ^g\)-systems extends traditional ND-system with a new kind of action in derivations, assumption incorporation, a kind of dual to the assumption discharge action. As a result, the implication \((I/E)\)-rules are invertible and, almost by definition, harmonious and stable, a major condition imposed by proof-theoretic semantics on ND-systems to qualify as meaning-conferring. There is also a proof-term assignment to \(NJ^g\)-derivations, materialising the Curry-Howard correspondence for this system.A correspondence between maximal abelian sub-algebras and linear logic fragments.https://www.zbmath.org/1456.031052021-04-16T16:22:00+00:00"Seiller, Thomas"https://www.zbmath.org/authors/?q=ai:seiller.thomasSummary: We show a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by \textit{J. Dixmier} [Ann. Math. (2) 59, 279--286 (1954; Zbl 0055.10702)] and fragments of linear logic. We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction [\textit{J.-Y. Girard}, Theor. Comput. Sci. 412, No. 20, 1860--1883 (2011; Zbl 1230.03093)]. The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation. We also unveil the essential role played by MASAs in previous geometry of interaction constructions.On various negative translations.https://www.zbmath.org/1456.030892021-04-16T16:22:00+00:00"Ferreira, Gilda"https://www.zbmath.org/authors/?q=ai:ferreira.gilda"Oliva, Paulo"https://www.zbmath.org/authors/?q=ai:oliva.pauloSummary: Several proof translations of classical mathematics into intuitionistic mathematics have been proposed in the literature over the past century. These are normally referred to as negative translations or double-negation translations. Among those, the most commonly cited are translations due to Kolmogorov, Gödel, Gentzen, Kuroda and Krivine (in chronological order). In this paper we propose a framework for explaining how these different translations are related to each other. More precisely, we define a notion of a (modular) simplification starting from Kolmogorov translation, which leads to a partial order between different negative translations. In this derived ordering, Kuroda and Krivine are minimal elements. Two new minimal translations are introduced, with Godel and Gentzen translations sitting in between Kolmogorov and one of these new translations.
For the entire collection see [Zbl 1391.03011].A linear/producer/consumer model of classical linear logic.https://www.zbmath.org/1456.031042021-04-16T16:22:00+00:00"Paykin, Jennifer"https://www.zbmath.org/authors/?q=ai:paykin.jennifer"Zdancewic, Steve"https://www.zbmath.org/authors/?q=ai:zdancewic.steveSummary: This paper defines a new proof- and category-theoretic framework for \textit{classical linear logic} that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions reflecting the LPC structure. The paper's meta-theoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model.Kreisel's interests. On the foundations of logic and mathematics. Contributions of the conference, Salzburg, Austria, August 13--14, 2018.https://www.zbmath.org/1456.030052021-04-16T16:22:00+00:00"Weingartner, Paul (ed.)"https://www.zbmath.org/authors/?q=ai:weingartner.paul"Leeb, Hans-Peter (ed.)"https://www.zbmath.org/authors/?q=ai:leeb.hans-peterPublisher's description: The contributions to this volume are from participants of the international conference Kreisel's Interests -- On the Foundations of Logic and Mathematics, which took place from 13 to 14 August 2018 at the University of Salzburg in Salzburg, Austria. The contributions have been revised and partially extended. Among the contributors are Akihiro Kanamori, Göran Sundholm, Ulrich Kohlenbach, Charles Parsons, Daniel Isaacson, and Kenneth Derus. The contributions cover the discussions between Kreisel and Wittgenstein on philosophy of mathematics, Kreisel's Dictum, proof theory, the discussions between Kreisel and Gödel on philosophy of mathematics, some biographical facts, and a collection of extracts from Kreisel's letters.
The articles of this volume will be reviewed individually.On the inevitability of the consistency operator.https://www.zbmath.org/1456.030912021-04-16T16:22:00+00:00"Montalbán, Antonio"https://www.zbmath.org/authors/?q=ai:montalban.antonio"Walsh, James"https://www.zbmath.org/authors/?q=ai:walsh.james-a|walsh.james-bruce|walsh.james-jThe paper is concerned with recursive monotone functions on the Lindenbaum-Tarski algebra of the elementary arithmetic EA. Denote the equivalence class of a sentence \(\varphi\), modulo EA-provability, by \([\varphi]\). Write \([\psi]\leq[\varphi]\) when \(\mathrm{EA} \vdash\psi\rightarrow\varphi\). A function \(f\) on sentences is \textit{monotone} if \(f([\psi])\leq f([\varphi])\) for every \(\psi\) and \(\varphi\) with \([\psi]\leq[\varphi]\). Note that then \(f\) is also \textit{extensional} in the sense that \(f([\psi])= f([\varphi])\) when \([\psi]=[\varphi]\).
\textit{V. Yu. Shavrukov} and \textit{A. Visser} proved in [Notre Dame J. Formal Logic 55, No. 4, 569--582 (2014; Zbl 1339.03056)] that there exists a recursive extensional function on the Lindenbaum-Tarski algebra of Peano's arithmetic such that it lies strictly between the identity function and the mapping \(\varphi\mapsto\varphi\wedge \mathrm{Con} (\varphi)\). The main result of the present paper is that there is no recursive monotone function on the Lindenbaum-Tarski algebra of Con that lies strictly between the identity function and the mapping \(\varphi\mapsto\varphi\wedge \mathrm{Con}(\varphi)\).
This also negatively answers a question of Shavrukov and Visser in [loc. cit.] which asked if there exists a recursive binary function that is monotonic in both its coordinates and satisfies (i) \([\psi] < g([\psi],[\varphi])<[\varphi]\) if \([\psi]<[\varphi]\), and (ii) \(g([\psi],[\theta]) = g([\varphi],[\theta])\) and \(g([\theta],[\psi]) = g([\theta],[\varphi])\) if \([\psi]=[\varphi]\).
The authors also generalize their results ``to iterates of consistency into the effective transfinite''. They leave open three interesting questions in the paper, one of which is the following: if \(f\) is a recursive monotone \(\Pi_1^0\)(-valued) function such that for every \(\varphi\) we have \([\varphi\wedge\mathrm{Con}^\alpha(\varphi)]\leq[f(\varphi)]\) for some fixed ordinal \(\alpha\), must there exist some \(\beta\leq\alpha\) and some true sentence \(\theta\) such that \([\theta\wedge f(\theta)]=[\theta\wedge\mathrm{Con}^\beta(\theta)]\)?
Reviewer: Saeed Salehi (Tabriz)