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 R of structural rules, the cut elimination theorem holds for FL enriched with R if and only if R satisfies the propagation property. As an application, we show that any set R of structural rules can be "completed" into another set R*, so that the cut elimination theorem holds for FL enriched with R*, while the provability remains the same. (shrink)

In [7], a naive set theory is introduced based on a polynomial time logical system, Light Linear Logic (LLL). Although it is reasonably claimed that the set theory inherits the intrinsically polytime character from the underlying logic LLL, the discussion there is largely informal, and a formal justification of the claim is not provided sufficiently. Moreover, the syntax is quite complicated in that it is based on a non-traditional hybrid sequent calculus which is required for formulating LLL.In this paper, we (...) consider a naive set theory based on Intuitionistic Light Affine Logic (ILAL), a simplification of LLL introduced by [1], and call it Light Affine Set Theory (LAST). The simplicity of LAST allows us to rigorously verify its polytime character. In particular, we prove that a function over {0, 1}* is computable in polynomial time if and only if it is provably total in LAST. (shrink)

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not. In this paper, we (...) introduce an untyped term calculus, called Light Affine Lambda Calculus (λLA), which corresponds to ILAL. λLA is a bi-modal λ-calculus with certain constraints, endowed with very simple reduction rules. The main property of LALC is the polynomial time strong normalization: any reduction strategy normalizes a given λLA term in a polynomial number of reduction steps, and indeed in polynomial time. Since proofs of ILAL are structurally representable by terms of λLA, we conclude that the same holds for ILAL. (shrink)

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 FL c and GL - c of Ono [11], that will settle the open problems stated in Ono [12]. (shrink)

Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic and for affine logic, 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, and intuitionistic LLW. In addition, we shall show the finite model property for contractive linear logic, i.e., linear logic with contraction, and for its intuitionistic version. 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 FL$_c$ and GL$^-_c$ of Ono [11], that will settle the open problems stated in Ono [12]. (shrink)

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

Apathy and depression are frequently observed as behavioral and psychological symptoms of dementia, respectively, and are important for ensuring adequate care. This study aims to explore effective non-pharmacological interventions for apathy and depression with mild cognitive impairment and dementia. Five search engines including PubMed, Scopus, CINAHL, PsycInfo, and Web of Science were used to extract relevant studies. Inclusion criteria were studies that involved participants who were diagnosed with MCI or dementia, included quantitative assessments of each symptom, and employed randomized controlled (...) trials. Twenty studies were extracted, with interventions have been conducted in care facilities, the community, and hospitals. Participants in many studies had MCI or mild-to-moderate dementia but were not diagnosed with the subtypes of dementia. Few studies had set apathy and depression as the primary outcomes of non-pharmacological interventions. The findings suggested that emotional and stimulation-oriented approaches to apathy and depression would be useful for people with MCI or mild-to-moderate dementia. It would be helpful for therapists to assess the clinical features of the target symptoms for selecting suitable interventions. Additionally, increasing the number of randomized controlled trials focusing on apathy or depression as primary outcomes would offer a more definite conclusion for future systematic reviews. (shrink)

We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. (...) Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17]. (shrink)

We show that the variety of residuated lattices is generated by its finite simple members, improving upon a finite model property result of Okada and Terui. The reasoning is a blend of proof-theoretic and algebraic arguments.