Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation (...) and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. The (...) operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed. (shrink)

An embedding of the implicational propositional intuitionistic logic into the nonmodal fragment of intuitionistic linear logic is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofs.

We consider formal theories synonymous with various free categories . Their Lindenbaum algebras may be described as the lattices of subobjects of a terminator. These theories have intuitionistic logic. We show that the Lindenbaum algebras of second order and higher order arithmetic , and set theory are not isomorphic to the Lindenbaum algebras of first order theories such as arithmetic . We also show that there are only five kernels of representations of the free Heyting algebra on one generator in (...) these Lindenbaum algebras. (shrink)

We consider properties of sets in an intuitionistic setting corresponding to large cardinals in classical set theory. Adding such ‘large set axioms’ to intuitionistic ZF set theory does not violate well-know metamathematical properties of intuitionistic systems. Moreover, we consider statements in constructive analysis equivalent to the consistency of such ‘large set axioms’.

By a model of set theory we mean a Boolean-valued model of Zermelo-Fraenkel set theory allowing atoms (ZFA), which contains a copy of the ordinary universe of (two-valued,pure) sets as a transitive subclass; examples include Scott-Solovay Boolean-valued models and their symmetric submodels, as well as Fraenkel-Mostowski permutation models. Any such model M can be regarded as a topos. A logical subtopos E of M is said to represent M if it is complete and its cumulative hierarchy, as defined by Fourman (...) and Hayashi, coincides with the usual cumulative hierarchy of M. We show that, although M need not be a complete topos, it has a smallest complete representing subtopos, and we describe this subtopos in terms of definability in M. We characterize, again in terms of definability, those models M whose smallest representing topos is a Grothendieck topos. Finally, we discuss the extent to which a model can be reconstructed when its smallest representing topos is given. (shrink)

We consider intuitionistic number theory with recursive infinitary rules . Any primitive recursive binary relation for which transfinite induction schema is provable is in fact well founded. Its ordinal is less than ε 0 if the transfinite induction schema is intuitionistically provable in elementary number theory. These results are provable intuitionistically. In fact, it suffices to consider transfinite induction with respect to one particular number-theoretic property.

In the original publication, the affiliation of the author Max Kanovich was processed incorrectly. It has been updated in this correction.

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative connectives, additive conjunction and disjunction, brackets and bracket modalities, and the! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut. We also prove algorithmic undecidability for both (...) calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. (shrink)

§ 1. Introduction. Perhaps the most surprising recent development in complexity theory is the discovery that the class NP can be characterized using a form of randomized proof checker that only examines a constant number of bits of the “proof” that a string is in a language [6, 5, 31, 3, 4]. More specifically, writing ∣x∣ for the length of a string x, a language L in the class NP of languages recognizable in Nondeterministic polynomial time is traditionally given by (...) a polynomial p and a polynomial-time predicate P such that a string x is in L iff there is some string y satisfying P, where ∣y∣ ≤ p. Intuitively, we can think of a string y as a possible proof that x ϵ L, with the predicate P some kind of proof checker that distinguishes good proofs from bad ones. A string x is therefore in a language L ϵ NP if there is a short proof that x ϵ L, and not in L otherwise. The surprising discovery is that the deterministic proof checker that reads the entire input and proof can be replaced by a probabilistic verifier that on input x and possible proof y, where y is presented in a certain way, flips at most O coins and reads at most a constant number of bits of x and y. Obviously, a probabilistic verifier that does not read the whole proof will sometimes make mistakes. However, the surprising and essentially non-intuitive mathematical fact is that for each language L in NP, it is possible to find a polynomial q and verifier V flipping a logarithmic number of coins and reading a constant number of bits such that, for any x ϵ L, there exists y with ∣y∣ ≤ q and with V accepting with probability 1 and, for x ∉ L, there is no y with ∣y∣ ≤ q and with V accepting with probability ≥ 1/4. This idea canalsobeextended to PSPACE [10, 9], using a game that alternates between two players instead of a proof presented by a “single player.”. (shrink)

Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the of the 29th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2023, held in Halifax, NS, Canada, during July 11–14, 2023. The 24 full papers (21 contributed, 3 invited) included in this book were carefully reviewed and selected from 46 submissions. The book also contains the abstracts for the 7 invited talks and 4 tutorials presented at WoLLIC 2023. The (...) WoLLIC conference series aims at fostering interdisciplinary research in pure and applied logic. (shrink)