The purpose of this paper is to invite structural proof theorists to a challenging problem in substructural and fuzzy logics: the consistency of Cantor-Łukasiewicz naive set theory. To this end, we consider two logics: FLew (Full Lambek calculus with exchange and weakening) and its extension Ł (Lukasiewicz logic). The former is equivalent to !-free intuitionistic linear logic with weakening, while the latter is the most prominent system of mathematical fuzzy logic. For each of them, we consider two extensions: one with a fixed point operator (which is neither least nor greatest) and the other with a naive set theory with unrestricted comprehension, so that we end up with four systems: FLew_{fp}, FLew_{set}, Ł_{fp} and Ł_{set}. The first two admit an easy proof of consistency by cut elimination, while the third admits a proof by the Brouwer fixed point theorem. The last system Ł_{set} (known as Cantor-Łukasiewicz set theory) is our main target. Although there are some partial results, the consistency of the full system is still open. In this paper, we consider a restricted fragment of Ł_{set} and prove its consistency.

Buchholz' Omega-rule is a way to give a syntactic, possibly ordinal-free proof of cut elimination for various subsystems of second order arithmetic. Our goal is to understand it from an algebraic point of view. Among many proofs of cut elimination for higher order logics, Maehara and Okada's algebraic proofs are of particular interest, since the essence of their arguments can be algebraically described as the (Dedekind-)MacNeille completion together with Girard's reducibility candidates. Interestingly, it turns out that the $Ω$-rule, formulated as a rule of logical inference, finds its algebraic foundation in the MacNeille completion. In this paper, we consider the parameter-free fragments LIP0, LIP1, LIP2, ... of the second order intuitionistic logic, that correspond to the arithmetical theories ID0, ID1, ID2, ... of iterated inductive definitions up to omega. In this setting, we observe a formal connection between the Omega-rule and the MacNeille completion, that leads to a way of interpreting second order quantifiers in a first order way in Heyting-valued semantics, called the Omega-interpretation. Based on this, we give an algebraic proof of cut elimination for LIPn for every n

One of the basic principles in typed lambda calculi is that typable lambda terms are normalizable. Since the converse direction does not hold for simply typed lambda calculus, people have been studying its extensions. This gave birth to the intersection type systems, that exactly characterize various classes of lambda terms, such as strongly/weakly normalizable terms and solvable ones (see e.g. [van Bakel/TCS/1995] for a survey). More recently, a new trend has emerged: intersection types are not only useful for extending simple types but also for refining them [Salvati/JoLLI/2010]. One thus obtains finer information on simply typed terms by assigning intersection types. This in particular leads to the concept of normalization by typing, that turns out to be quite efficient in some situations [Terui/RTA/2012]. Moreover, intersection types are invariant under beta-equivalence, so that they constitute a denotational semantics in a natural way [Ehrhard/CSL/2012]. Finally, intersection types also work in an infinitary setting,where terms may represent infinite trees and types play the role of automata. This leads to a model checking framework for higher order recursion schemes via intersection types [Kobayashi/POPL/2009, Kobayashi+Luke Ong/LICS/2009]. The purpose of this talk is to outline the recent development of intersection types described above. In particular, we explain how an efficient evaluation algorithm is obtained by combining normalization by typing, beta-reduction and Krivine's abstract machine, to result in the following complexity characterization. Consider simply typed lambda terms of boolean type o -> o -> o and of order r. Then the problem of deciding whether a given term evaluates to "true" is complete for n-EXPTIME if r = 2n +2, and complete for n- EXPSPACE if r = 2n + 3 [Terui/RTA/2012].

Consider the following problem: given a simply typed lambda term of Boolean type and of order r, does it normalize to "true"? A related problem is: given a term M of word type and of order r together with a finite automaton D, does D accept the word represented by the normal form of M? We prove that these problems are n-EXPTIME complete for r=2n+2, and n-EXPSPACE complete for r=2n+3. While the hardness part is relatively easy, the membership part is not so obvious; in particular, simply applying beta reduction does not work. Some preceding works employ semantic evaluation in the category of sets and functions, but it is not efficient enough for our purpose. We present an algorithm for the above type of problem that is a fine blend of beta reduction, Krivine abstract machine and semantic evaluation in a category based on preorders and order ideals, also known as the Scott model of linear logic. The semantic evaluation can also be presented as intersection type checking.

Traditional Gödel completeness holds between finite proofs and infinite models over formulas of finite depth, where proofs and models are heterogeneous. Our purpose is to provide an interactive form of completeness between infinite proofs and infinite models over formulas of infinite depth (that include recursive types), where proofs and models are homogenous. We work on a nonlinear extension of ludics, a monistic variant of game semantics which has the same expressive power as the propositional fragment of polarized linear logic. In order to extend the completeness theorem of the original ludics to the infinitary setting, we modify the notion of orthogonality by defining it via safety rather than termination of the interaction. Then the new completeness ensures that the universe of behaviours (interpretations of formulas) is Cauchy-complete, so that every recursive equation has a unique solution. Our work arises from studies on recursive types in denotational and operational semantics, but is conceptually simpler, due to the purely logical setting of ludics, the completeness theorem, and use of coinductive techniques.

We introduce a systematic procedure to transform large classes of (Hilbert) axioms into equivalent inference rules in sequent and hypersequent calculi. This allows for the automated generation of analytic calculi for a wide range of prepositional nonclassical logics including intermediate, fuzzy and substructural logics. Our work encompasses many existing results, allows for the definition of new calculi and contains a uniform semantic proof of cut-elimination for hypersequent calculi.

Abstract Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus ( FL ), i.e., intuitionistic logic without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL . In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set ℛ of structural rules, the cut elimination theorem holds for FL enriched with ℛ if and only if ℛ satisfies the propagation property. As an application, we show that any set ℛ of structural rules can be “completed” into another set ℛ*, so that the cut elimination theorem holds for FL enriched with ℛ*. while the provability remains the same.

In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta reduction and all Ptime functions can be represented. In the present work we address the problem of typing lambda-terms in second-order DLAL. For that we give a procedure which, starting with a term typed in system F, determines whether it is typable in DLAL and outputs a concrete typing if there exists any. We show that our procedure can be run in time polynomial in the size of the original Church typed system F term.

We study the relationship between classical phase semantics for classical linear logic (LL) and intuitionistic phase semantics for intuitionistic linear logic (ILL). We prove that (i) every intuitionistic phase space is a subspace of a classical phase space, and (ii) every intuitionistic phase space is phase isomorphic to an ‘almost classical’ phase space. Here, by an ‘almost classical’ phase space we mean an intuitionistic phase space having a double-negation-like closure operator. Based on these semantic considerations, we give a syntactic embedding of propositional ILL into LL.

We propose a new type system for lambda-calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DIAL). DIAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DIAL ensures good properties on lambda-terms: subject reduction is satisfied and a well-typed term admits a polynomial bound on the reduction by any strategy. Finally we establish that as LAL, DIAL allows to represent all polytime functions.

We study the relationship between proof nets for mutiplicative linear logic (with unbounded fan-in logical connectives) and Boolean circuits. We give simulations of each other in the style of the proofs-as-programs correspondence; proof nets correspond to Boolean circuits and cut-elimination corresponds to evaluation. The depth of a proof net is defined to be the maximum logical depth of cut formulas in it, and it is shown that every unbounded fan-in Boolean circuit of depth n, possibly with stC0NN/sub 2/ gates, is polynomially simulated by a proof net of depth O(n) and vice versa. Here, stC0NN/sub 2/ stands for st-connectivity gates for undirected graphs of degree 2. Let APN/sup i/ be the class of languages for which there is a polynomial size, log/sup i/-depth family of proof nets. We then have APN/sup i/ = AC/sup i/(stCONN/sub 2/).

Light linear logic (LLL) and its variant, intuitionistic light affine logic (ILAL), are logics of polytime computation. All polynomial-time functions are representable by proofs of these logics (via the proofs-as-programs correspondence), and, conversely, that there is a specific reduction (cut-elimination) strategy which normalizes a given proof in polynomial time (the latter may well be called the polytime "weak" normalization theorem). In this paper, we introduce an untyped term calculus, called the light affine lambda calculus (/spl lambda//sub LA/), generalizing the essential ideas of light logics into an untyped framework. It is a simple modification of the /spl lambda/-calculus, and has ILAL as a type assignment system. Then, in this generalized setting, we prove the polytime "strong" normalization theorem: any reduction strategy normalizes a given /spl lambda//sub LA/ term (of fixed depth) in a polynomial number of reduction steps, and indeed in polynomial time.

Abstract Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction. and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL−-systems except FLc and of Ono [11], that will settle the open problems stated in Ono [12].