Relational semantics for full linear logic

Relational semantics, given by Kripke frames, play an essential role in the study of modal and intuitionistic logic. In [4] it is shown that the theory of relational semantics is also available in the more general setting of substructural logic, at least in an algebraic guise. Building on these ideas, in [5] a type of frames is described which generalise Kripke frames and provide semantics for substructural logics in a purely relational form.In this paper we study full linear logic from an algebraic point of view. The main additional hurdle is the exponential. We analyse this operation algebraically and use canonical extensions to obtain relational semantics. Thus, we extend the work in [4], [5] and use their approach to obtain relational semantics for full linear logic. Hereby we illustrate the strength of using canonical extension to retrieve relational semantics: it allows a modular and uniform treatment of additional operations and axioms.Traditionally, so-called phase semantics are used as models for (provability in) linear logic [8]. These have the drawback that, contrary to our approach, they do not allow a modular treatment of additional axioms. However, the two approaches are related, as we will explain.     

Order Algebras as Models of Linear Logic

The starting point of the present study is the interpretation of intuitionistic linear logic in Petri nets proposed by U. Engberg and G. Winskel. We show that several categories of order algebras provide equivalent interpretations of this logic, and identify the category of the so called strongly coherent quantales arising in these interpretations. The equivalence of the interpretations is intimately related to the categorical facts that the aforementioned categories are connected with each other via adjunctions, and the compositions of the connecting functors with co-domain the category of strongly coherent quantales are dense. In particular, each quantale canonically induces a Petri net, and this association gives rise to an adjunction between the category of quantales and a category whose objects are all Petri nets.     

A linear conservative extension of Zermelo-Fraenkel set theory

In this paper, we develop the system LZF of set theory with the unrestricted comprehension in full linear logic and show that LZF is a conservative extension of ZF^– i.e., the Zermelo-Fraenkel set theory without the axiom of regularity. We formulate LZF as a sequent calculus with abstraction terms and prove the partial cut-elimination theorem for it. The cut-elimination result ensures the subterm property for those formulas which contain only terms corresponding to sets in ZF^–. This implies that LZF is a conservative extension of ZF^– and therefore the former is consistent relative to the latter. Hiroakira Ono     

Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA

The previously introduced algorithm SQEMA computes first-order frame equivalents for modal formulae and also proves their canonicity. Here we extend SQEMA with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of first-order logic with monadic least fixed-points FOμ. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid μ-calculus. In particular, we prove that the recursive extension of SQEMA succeeds on the class of ‘recursive formulae’. We also show that a certain version of this algorithm guarantees the canonicity of the formulae on which it succeeds.     

SLAP: Specification logic of actions with probability

A logic for specifying probabilistic transition systems is presented. Our perspective is that of agents performing actions. A procedure for deciding whether sentences in this logic are valid is provided. One of the main contributions of the paper is the formulation of the decision procedure: a tableau system which appeals to solving systems of linear equations. The tableau rules eliminate propositional connectives, then, for all open branches of the tableau tree, systems of linear equations are generated and checked for feasibility. Proofs of soundness, completeness and termination of the decision procedure are provided.     

A sequent calculus for a logic of contingencies

We introduce a sequent calculus that is sound and complete with respect to propositional contingencies, i.e., formulas which are neither provable nor refutable. Like many other sequent and natural deduction proof systems, this calculus possesses cut elimination and the subformula property and has a simple proof search mechanism.     

Proof-Theoretic Functional Completeness for the Hybrid Logics of Everywhere and Elsewhere

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.     

A Modal Logic for Discretely Descending Chains of Sets

We present a modal logic for the class of subset spaces based on discretely descending chains of sets. Apart from the usual modalities for knowledge and effort the standard temporal connectives are included in the underlying language. Our main objective is to prove completeness of a corresponding axiomatization. Furthermore, we show that the system satisfies a certain finite model property and is decidable thus.     

An Elementary Proof of Chang's Completeness Theorem for the Infinite-valued Calculus of Lukasiewicz

The interpretation of propositions in Lukasiewicz's infinite-valued calculus as answers in Ulam's game with lies--the Boolean case corresponding to the traditional Twenty Questions game--gives added interest to the completeness theorem. The literature contains several different proofs, but they invariably require technical prerequisites from such areas as model-theory, algebraic geometry, or the theory of ordered groups. The aim of this paper is to provide a self-contained proof, only requiring the rudiments of algebra and convexity in finite-dimensional vector spaces.     

The logic of the medical research article

As do all forms of science, medical theories have a factual as well as a logical basis. New information is presented in medical research articles. These papers have three separate arguments: the argument of the hypothesis, the argument of the experimental protocol, and the argument of the hypothesis's judgment. These arguments may be examples of the hypothetico-deductive or confirmational model of scientific inference. The logical form of these arguments are informal and inductive rather than formal and deductive. Understanding the nature of the logic of the medical research article may help avoid erroneous conclusions.     

The logic of generalization: Five principles common to experiments and ethnographies

Both experiments and ethnographies are highly localized, so they are often criticized for lack of generalizability. The present article describes a logic of generalization that may help solve such problems. The logic consists of five principles outlined by Cook (1990): (a) proximal similarity, (b) heterogeneity of irrelevancies, (c) discriminant validity, (d) empirical interpolation and extrapolation, and (e) explanation. Because validity is a property of knowledge claims, not methods, these five principles apply to claims about generalization generated by any method, including both ethnographies and experiments. The principles are illustrated using Rizzo and Corsaro's interesting ethnographies as examples.     

Bayesian inference for finite mixtures of generalized linear models with random effects

We present an hierarchical Bayes approach to modeling parameter heterogeneity in generalized linear models. The model assumes that there are relevant subpopulations and that within each subpopulation the individual-level regression coefficients have a multivariate normal distribution. However, class membership is not known a priori, so the heterogeneity in the regression coefficients becomes a finite mixture of normal distributions. This approach combines the flexibility of semiparametric, latent class models that assume common parameters for each sub-population and the parsimony of random effects models that assume normal distributions for the regression parameters. The number of subpopulations is selected to maximize the posterior probability of the model being true. Simulations are presented which document the performance of the methodology for synthetic data with known heterogeneity and number of sub-populations. An application is presented concerning preferences for various aspects of personal computers.