Linear mixed-effects models (LMMs) are increasingly being used for data analysis in cognitive neuroscience and experimental psychology, where within-participant designs are common. The current article provides an introductory review of the use of LMMs for within-participant data analysis and describes a free, simple, graphical user interface (LMMgui). LMMgui uses the package lme4 (Bates et al., 2014a, b ) in the statistical environment R (R Core Team).

Variants of classical linear logics are presented based on the modal version of new structural rule !?mingle instead of the known rules !weakening and ?weakening. The cut-elimination theorems, the completeness theorems and a characteristic property named the mix separation principle are proved for these logics.

Causal set theory and the theory of linear structures (which has recently been developed by Tim Maudlin as an alternative to standard topology) share some of their main motivations. In view of that, I raise and answer the question how these two theories are related to each other and to standard topology. I show that causal set theory can be embedded into Maudlin’s more general framework and I characterise what Maudlin’s topological concepts boil down to when applied to discrete linear (...) structures that correspond to causal sets. Moreover, I show that all topological aspects of causal sets that can be described in Maudlin’s theory can also be described in the framework of standard topology. Finally, I discuss why these results are relevant for evaluating Maudlin’s theory. The value of this theory depends crucially on whether it is true that (a) its conceptual framework is as expressive as that of standard topology when it comes to describing well-known continuous as well as discrete models of spacetime and (b) it is even more expressive or fruitful when it comes to analysing topological aspects of discrete structures that are intended as models of spacetime. On the one hand, my theorems support (a): the theory is rich enough to incorporate causal set theory and its definitions of topological notions yield a plausible outcome in the case of causal sets. On the other hand, the results undermine (b): standard topology, too, has the conceptual resources to capture those topological aspects of causal sets that are analysable within Maudlin’s framework. This fact poses a challenge for the proponents of Maudlin’s theory to prove it fruitful. (shrink)

A new combined temporal logic called synchronized linear-time temporal logic (SLTL) is introduced as a Gentzen-type sequent calculus. SLTL can represent the n -Cartesian product of the set of natural numbers. The cut-elimination and completeness theorems for SLTL are proved. Moreover, a display sequent calculus δ SLTL is defined.

Humankind is currently confronted with a critical challenge that determines its very existence, not only on an individual, racial, or national level but as a whole species: the fight against climate change and environmental degradation. To win this battle, humanity needs innovations and non-linear thinking. Nature has long been a substantial information source for unthinkable discoveries that save human lives. The paper suggests that by understanding the nature, emergence, and mechanism of serendipity, the survival skill of humans, humanity can capitalize (...) on it to learn from nature and generate nature-based innovations that can address the climate and environmental degradation crises. In the era of Artificial Intelligence (AI) proliferation, AI will be a vital tool providing navigational and useful information to leverage the power of serendipity in climate and sustainability science. However, an eco-surplus culture that incorporates core values pertaining to nature and sees environmental sustainability as the conscience of the times needs to be built to direct and control the immense power of AI-leveraged serendipity. Insights applied in this paper are drawn from the book titled “A New Theory of Serendipity: Nature, Emergence and Mechanism”. (shrink)

Temporal logic can be used to describe processes: their behaviour ischaracterized by a set of temporal models axiomatized by a temporaltheory. Two types of models are most often used for this purpose: linearand branching time models. In this paper a third approach, based onsocalled joint closure models, is studied using models which incorporateall possible behaviour in one model. Relations between this approach andthe other two are studied. In order to define constructions needed torelate branching time models, appropriate algebraic notions are (...) defined(in a category theoretical manner) and exploited. In particular, thenotion of joint closure is used to construct one model subsuming a setof models. Using this universal algebraic construction we show that aset of linear models can be merged to a unique branching time model.Logical properties of the described algebraic constructions are studied.The proposed approach has been successfully aplied to obtain anappropriate semantics for non-monotonic reasoning processes based ondefault logic. References are discussed that show the details of theseapplications. (shrink)

The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.

Neuroethological investigations of mammalian and avian auditory systems have documented species-specific specializations for processing complex acoustic signals that could, if viewed in abstract terms, have an intriguing and striking relevance for human speech sound categorization and representation. Each species forms biologically relevant categories based on combinatorial analysis of information-bearing parameters within the complex input signal. This target article uses known neural models from the mustached bat and barn owl to develop, by analogy, a conceptualization of human processing of consonant plus (...) vowel sequences that offers a partial solution to the noninvariance dilemma the locus equations orderly output constraint”) is hypothesized based on the notion of an evolutionarily conserved auditory-processing strategy. High correlation and linearity between critical parameters in the speech signal that help to cue place of articulation categories might have evolved to satisfy a preadaptation by mammalian auditory systems for representing tightly correlated, linearly related components of acoustic signals. (shrink)

A linear notation for Charles S. Peirce's alpha and beta diagrammatic systems of existential graphs is presented. These two systems are equivalent to propositional and first-order logic. Some differences between the linear and graphical notation are analyzed, revealing some of the strengths and weaknesses of Peirce's system.

The present paper introduces and studies the variety [MATHEMATICAL SCRIPT CAPITAL W]ℋn of n-linear weakly Heyting algebras. It corresponds to the algebraic semantic of the strict implication fragment of the normal modal logic K with a generalization of the axiom that defines the linear intuitionistic logic or Dummett logic. Special attention is given to the variety [MATHEMATICAL SCRIPT CAPITAL W]ℋ2 that generalizes the linear Heyting algebras studied in [10] and [12], and the linear Basic algebras introduced in [2].

Let ⪯R be the preorder of embeddability between countable linear orders colored with elements of Rado's partial order . We show that ⪯R has fairly high complexity with respect to Borel reducibility , although its exact classification remains open.

In the paper we obtain a new characterization of the BCK-algebras which are subdirect product of BCK-chains. We give an axiomatic algebraizable extension of the BCK-calculus, by means of a recursively enumerable set of axioms, such that its equivalent algebraic semantics is definitionally equivalent to the quasivariety of BCK-algebras generated by the BCK-chains. We propose the concept of "linearization of a system" and we give some examples.

We introduce the notion of τ-like partial order, where τ is one of the linear order types ω, ω*, ω + ω*, and ζ. For example, being ω-like means that every element has finitely many predecessors, while being ζ-like means that every interval is finite. We consider statements of the form “any τ-like partial order has a τ-like linear extension” and “any τ-like partial order is embeddable into τ” . Working in the framework of reverse mathematics, we show that these (...) statements are equivalent either to equation image or to equation image over the usual base system equation image. (shrink)

In an unpublished note Reddy introduced an extended intuitionistic linear calculus, called LLMS (for Linear Logic Model of State), to model state manipulation via the notions of sequential composition and ‘regenerative values’. His calculus introduces the connective ‘before’ ▹ and an associated modality †, for the storage of objects sequentially reusable. Earlier and independently de Paiva introduced a (collection of) dialectica categorical models for (classical and intuitionistic) Linear Logic, the categories Dial2Set. These categories contain, apart from the structure needed to (...) model linear logic, an extra tensor product functor and an extra comonad structure corresponding to a modality related to the extra tensor product. It is surprising that these works arising from completely different motivations can be related in a meaningful way. In this article, following joint work with Corrêa and Haeusler, we first adapt Reddy's system LLMS providing a commutative version of the connective ‘before’ and its associated modality and then construct a dialectica category on Sets , which we show is a sound model for the modified version of Reddy's the system LLMSc. Moreover, following the work of Tucker, we provide another variant of the Dialectica categories with a non-commutative tensor and its associated modality, which models soundlyLLMS itself. We conclude with some speculation on future applications. (shrink)

The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced (...) normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(NBox+-wC) and show how to reduce the problem for admissibility to the decidability of TL(NBox+-wC) itself using definable universal modalities. (shrink)

In this book, the authors introduce the notion of Super linear algebra and super vector spaces using the definition of super matrices defined by Horst (1963). Many theorems on super linear algebra and its properties are proved. Some theorems are left as exercises for the reader. These new class of super linear algebras which can be thought of as a set of linear algebras, following a stipulated condition, will find applications in several fields using computers. The authors feel that such (...) a paradigm shift is essential in this computerized world. (shrink)

For years now, phase-amplitude cross frequency coupling (CFC) has been observed across multiple brain regions under different physiological and pathological conditions. It has been suggested that CFC serves as a mechanism that facilitates communication and information transfer between local and spatially separated neuronal populations. In non-invasive brain computer interfaces (BCI), CFC has not been thoroughly explored. In this work, we propose a CFC estimation method based on Linear Parameter Varying Autoregressive (LPV-AR) models and we assess its performance using both synthetic (...) data and electroencephalographic (EEG) data recorded during attempted arm/hand movements of spinal cord injured (SCI) participants. Our results corroborate the potentiality of CFC as a feature for movement attempt decoding and provide evidence of the superiority of our proposed CFC estimation approach compared to other commonly used techniques. (shrink)

Linear Syntax makes a case for a critical reassessment of the wide-spread view that syntax can be reduced to tree structures. It argues that a crucial part of the description of German clausal syntax should instead be based on concepts that are defined in terms of linear order. By connecting the descriptive tools of modern phrase-structure grammar with traditional descriptive scholarship, Andreas Kathol offers a new perspective on many long-standing problems in syntactic theory.

O-minimal structures have long been thought to occupy the base of a hierarchy of ordered structures, in analogy with the role that strongly minimal structures play with respect to stable theories. This is the first in an anticipated series of papers whose aim is the development of model theory for ordered structures of rank greater than one. A class of ordered structures to which a notion of finite rank can be assigned, the decomposable structures, is introduced here. These include all (...) ordered structures definable in o-minimal structures. The principal result in this paper, Theorem 5.1, asserts roughly that a decomposable structure [Formula: see text] can be partitioned into finitely many definable subsets such that on each set the restriction of < is a "twisted lexicographic" order. As a consequence, for all n and linear orders ≺ definable on a subset X ⊆ Mn in an o-minimal structure [Formula: see text], there is a definable partition of X such that the restriction of ≺ to each set in the partition is "lexicographic". (shrink)

Sussman et al. state that auditory systems exploit linear correlations in the sound signal in order to identify perceptual categories. Can the auditory system recognize linearity? In bats and owls, separability of emergent features is an additional constraint that goes beyond linearity and for which linearity is not a necessary prerequisite.

We introduce a linear analogue of Läuchli's semantics for intuitionistic logic. In fact, our result is a strengthening of Läuchli's work to the level of proofs, rather than provability. This is obtained by considering continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivariant with respect to all such actions. Such dinatural transformations are called uniform. To any sequent in Multiplicative Linear Logic (...) , we associate a vector space of“diadditive” uniform transformations. We then show that this space is generated by denotations of cut-free proofs of the sequent in the theory MLL + MIX. Thus we obtain a full completeness theorem in the sense of Abramsky and Jagadeesan, although our result differs from theirs in the use of dinatural transformations.As corollaries, we show that these dinatural transformations compose, and obtain a conservativity result: diadditive dinatural transformations which are uniform with respect to actions of the additive group of integers are also uniform with respect to the actions of arbitrary cocommutative Hopf algebras. Finally, we discuss several possible extensions of this work to noncommutative logic.It is well known that the intuitionistic version of Läuchli's semantics is a special case of the theory of logical relations, due to Plotkin and Statman. Thus, our work can also be viewed as a first step towards developing a theory of logical relations for linear logic and concurrency. (shrink)

A Q -Heyting algebra is an algebra of type such that is a Heyting algebra and the unary operation ∇ satisfies the conditions ∇0=0, a ∧∇ a = a , ∇=∇ a ∧∇ b and ∇=∇ a ∨∇ b , for any a , b ∈ H . This paper is devoted to the study of the subvariety QH L of linear Q -Heyting algebras. Using Priestley duality we investigate the subdirectly irreducible linear Q -Heyting algebras and, as consequences, we (...) derive some properties of the lattice of subvarieties of QH L and find equational bases for some of these subvarieties. (shrink)

We apply linear algebra to the study of the inconsistent figure known as the Crazy Crate. Disambiguation by means of occlusions leads to a class of sixteen such figures: consistent, complete, both and neither. Necessary and sufficient conditions for inconsistency are obtained.

When a linear order has an order preserving surjection onto each of its suborders, we say that it is strongly surjective. We prove that the set of countable strongly surjective linear orders is a [Formula: see text]-complete set. Using hypotheses beyond ZFC, we prove the existence of uncountable strongly surjective orders.

We prove linear and polynomial growth properties of sets and functions that are existentially definable in the ordered group of integers with divisibility. We determine the laws of addition with order and divisibility.

Linear Logic is a branch of proof theory which provides refined tools for the study of the computational aspects of proofs. These tools include a duality-based categorical semantics, an intrinsic graphical representation of proofs, the introduction of well-behaved non-commutative logical connectives, and the concepts of polarity and focalisation. These various aspects are illustrated here through introductory tutorials as well as more specialised contributions, with a particular emphasis on applications to computer science: denotational semantics, lambda-calculus, logic programming and concurrency theory. The (...) volume is rounded-off by two invited contributions on new topics rooted in recent developments of linear logic. The book derives from a summer school that was the climax of the EU Training and Mobility of Researchers project 'Linear Logic in Computer Science'. It is an excellent introduction to some of the most active research topics in the area. (shrink)

This study presents the results of an empirical analysis of the relationship between managerial thinking style and ethical decision-making. Data from 200 managers across multiple organizations and industries demonstrated that managers predominantly adopt a utilitarian perspective when forming ethical intent across a series of business ethics vignettes. Consistent with expectations, managers utilizing a balanced linear/nonlinear thinking style demonstrated a greater overall willingness to provide ethical decisions across ethics vignettes compared to managers with a predominantly linear thinking style. However, results comparing (...) the ethical decision-making of balanced thinking managers and nonlinear thinking managers were generally inconsistent across the ethics vignettes. Unexpectedly, managers utilizing a balanced linear/nonlinear thinking style were least likely to adopt an act utilitarian rationale for ethical decision-making across the vignettes, suggesting that balanced thinkers may be more likely to produce ethical decisions by considering a wider range of alternatives and ruling out those that are justified solely on the basis of their outcomes. Implications are discussed for future research and practice related to management education and development, and ethical decision-making theory. (shrink)

This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic . A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be (...) introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism with respect to the logical system in question. MSC: 03B40, 03F05. (shrink)

LetB be the set of bounded observables on a quantum logic. A mapJ: B →R is called an expectation functional ifJ is normalized, positive, continuous, and compatibly linear. Two questions are considered. IsJ linear, and isJ an expectation relative to some state? It is shown that the answers are affirmative for hidden variable logics and most Hilbert space logics. An example is given which shows thatJ can be nonlinear on an arbitrary quantum logic.

In this article, we propose a new method to learn the underlying acyclic mixed graph of a linear non-Gaussian structural equation model with given observational data. We build on an algorithm proposed by Wang and Drton, and we show that one can augment the hidden variable structure of the recovered model by learning multidirected edges rather than only directed and bidirected ones. Multidirected edges appear when more than two of the observed variables have a hidden common cause. We detect the (...) presence of such hidden causes by looking at higher order cumulants and exploiting the multi-trek rule. Our method recovers the correct structure when the underlying graph is a bow-free acyclic mixed graph with potential multidirected edges. (shrink)

LetEbe a computably enumerable equivalence relation on the setωof natural numbers. We say that the quotient set$\omega /E$realizesa linearly ordered set${\cal L}$if there exists a c.e. relation ⊴ respectingEsuch that the induced structure is isomorphic to${\cal L}$. Thus, one can consider the class of all linearly ordered sets that are realized by$\omega /E$; formally,${\cal K}\left = \left\{ {{\cal L}\,|\,{\rm{the}}\,{\rm{order}}\, - \,{\rm{type}}\,{\cal L}\,{\rm{is}}\,{\rm{realized}}\,{\rm{by}}\,E} \right\}$. In this paper we study the relationship between computability-theoretic properties ofEand algebraic properties of linearly ordered sets realized (...) byE. One can also define the following pre-order$ \le _{lo} $on the class of all c.e. equivalence relations:$E_1 \le _{lo} E_2 $if every linear order realized byE1is also realized byE2. Following the tradition of computability theory, thelo-degrees are the classes of equivalence relations induced by the pre-order$ \le _{lo} $. We study the partially ordered set oflo-degrees. For instance, we construct various chains and anti-chains and show the existence of a maximal element among thelo-degrees. (shrink)

Linear structural equation models with latent (unmeasured) variables are used widely in sociology, psychometrics, and political science. When such models have a unidimensional..

A review of the literature indicates that linear models are frequently used in situations in which decisions are made on the basis of multiple codable inputs. These models are sometimes used normatively to aid the decision maker, as a contrast with the decision maker in the clinical vs statistical controversy, to represent the decision maker "paramorphically" and to "bootstrap" the decision maker by replacing him with his representation. Examination of the contexts in which linear models have been successfully employed indicates (...) that the contexts have the following structural characteristics in common: each input variable has a conditionally monotone relationship with the output; there is error of measurement; and deviations from optimal weighting do not make much practical difference. These characteristics ensure the success of linear models, which are so appropriate in such contexts that random linear models may perform quite well. 4 examples involving the prediction of such codable output variables as GPA and psychiatric diagnosis are analyzed in detail. In all 4 examples, random linear models yield predictions that are superior to those of human judges. (shrink)

In this sequel, linear algebra methods are used to study the Routley Functor, both in single Neckers and in Necker chains. The latter display a certain irreducible higher-order inconsistency. A definition of degree of inconsistency is given, which classifies such inconsistency correctly with other examples of local and global inconsistency.

We develop an extension of the familiar linear mixed logit model to allow for the direct estimation of parametric non-linear functions defined over structural parameters. Classic applications include the estimation of coefficients of utility functions to characterize risk attitudes and discounting functions to characterize impatience. There are several unexpected benefits of this extension, apart from the ability to directly estimate structural parameters of theoretical interest.

In this paper, we give a classification of ℵ0-categorical coloured linear orders, generalizing Rosenstein's characterization of ℵ0-categorical linear orderings. We show that they can all be built from coloured singletons by concatenation and ℚn-combinations . We give a method using coding trees to describe all structures in our list.

We show that considerable sets of positive linear operators namely their extensions as closures, adjoints or Friedrichs positive self-adjoint extensions form operator (generalized) effect algebras. Moreover, in these cases the partial effect algebraic operation of two operators coincides with usual sum of operators in complex Hilbert spaces whenever it is defined. These sets include also unbounded operators which play important role of observables (e.g., momentum and position) in the mathematical formulation of quantum mechanics.

A non-repeated item design refers to an experimental design in which items used in one level of experimental conditions are not repeatedly used at other levels. Recent literature has suggested the use of generalized linear mixed-effects models for experimental data analysis, but the existing specification of GLMMs does not account for all possible dependencies among the outcomes in NRI designs. Therefore, the current study proposed a GLMM with a level-specific item random effect for NRI designs. The hypothesis testing performance of (...) the newly proposed model was evaluated via a simulation study to detect the experimental condition effect. The model with a level-specific item random effect performed better than the existing model in terms of power when the variance of the item effect was heterogeneous. Based on these results, we suggest that experimental researchers using NRI designs consider setting a level-specific item random effect in the model. (shrink)

Numerous results about capturing complexity classes of queries by means of logical languages work for ordered structures only, and deal with non-generic, or order-dependent, queries. Recent attempts to improve the situation by characterizing wide classes of finite models where linear order is definable by certain simple means have not been very promising, as certain commonly believed conjectures were recently refuted (Dawar's Conjecture). We take on another approach that has to do with normalization of a given order (rather than with defining (...) a linear order from scratch). To this end, we show that normalizability of linear order is a strictly weaker condition than definability (say, in the least fixpoint logic), and still allows for extending Immerman-Vardi-style results to generic queries. It seems to be the weakest such condition. We then conjecture that linear order is normalizable in the least fixpoint logic for any finitely axiomatizable class of rigid structures. Truth of this conjecture, which is a strengthened version of Stolboushkin's conjecture, would have the same practical implications as Dawar's Conjecture. Finally, we suggest a series of reductions of the two conjectures to specialized classes of graphs, which we believe should simplify further work. (shrink)

This paper is about equality of proofs in which a binary predicate formalizing properties of equality occurs, besides conjunction and the constant true proposition. The properties of equality in question are those of a preordering relation, those of an equivalence relation, and other properties appropriate for an equality relation in linear logic. The guiding idea is that equality of proofs is induced by coherence, understood as the existence of a faithful functor from a syntactical category into a category whose arrows (...) correspond to diagrams. Edges in these diagrams join occurrences of variables that must remain the same in every generalization of the proof. It is found that assumptions about equality of proofs for equality are parallel to standard assumptions about equality of arrows in categories. They reproduce standard categorial assumptions on a different level. It is also found that assumptions for a preordering relation involve an adjoint situation. (shrink)

The notions of linear and metric independence are investigated in relation to the property: if U is a set of n+1 independent vectors, and X is a set of n independent vectors, then adjoining some vector in U to X results in a set of n+1 independent vectors. It is shown that this property holds in any normed linear space. A related property – that finite-dimensional subspaces are proximinal – is established for strictly convex normed spaces over the real or (...) complex numbers. It follows that metric independence and linear independence are equivalent in such spaces. Proofs are carried out in the context of intuitionistic logic without the axiom of countable choice. (shrink)

We consider certain linear orders with a function on them, and discuss for which types of functions the resulting structure is or is not computably categorical. Particularly, we consider computable copies of the rationals with a fixed-point free automorphism, and also ω with a non-decreasing function.

A successivity in a linear order is a pair of elements with no other elements between them. A recursive linear order with recursive successivities U is recursively categorical if every recursive linear order with recursive successivities isomorphic to U is in fact recursively isomorphic to U . We characterize those recursive linear orders with recursive successivities that are recursively categorical as precisely those with order type k 1 + g 1 + k 2 + g 2 +…+ g n -1 (...) + k n where each k n is a finite order type, non-empty for i ϵ{2,…, n -1} and each g i is an order type from among {ω,ω * ,ω+ω * }∪{ k ·η: k. (shrink)

In recent work, semantic games of independence-friendly logic were studied in strategic form in terms of Nash equilibria. The class of strategic games of independence-friendly logic is contained in the class of win-loss, zero-sum two-player games. In this note we draw on the theory of linear programming to develop tools to analyze the value of such games. We give two applications of these tools to independence-friendly logic under the so-called equilibrium semantics.

The interpretation of complex eigenvalues of linear transformations defined on a real geometric algebra presents problems in that their geometric significance is dependent upon the kind of linear transformation involved, as well as the algebraic lack of universal commutivity of bivectors. The present work shows how the machinery of geometric algebra can be adapted to the study of complex linear operators defined on a unitary space. Whereas the well-defined geometric significance of real geometric algebra is not lost, the primary concern (...) here is the study of the algebraic properties of complex eigenvalues and eigenvectors of these operators. (shrink)

Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and (...) provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules. Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents. (shrink)

A new logic, quantized intuitionistic linear logic, is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.