Constructive Logic with Strong Negation is a Substructural Logic. II

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL _ew of the substructural logic FL _ew . The main result of Part I of this series [41] shows that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL _ew (namely, a certain variety of FL _ew -algebras) are term equivalent. In this paper, the term equivalence result of Part I [41] is lifted to the setting of deductive systems to establish the definitional equivalence of the logics N and NFL _ew . It follows from the definitional equivalence of these systems that constructive logic with strong negation is a substructural logic. Presented by Heinrich Wansing     

Interpolation in computing science: the semantics of modularization

The Interpolation Theorem, first formulated and proved by W. Craig fifty years ago for predicate logic, has been extended to many other logical frameworks and is being applied in several areas of computer science. We give a short overview, and focus on the theory of software systems and modules. An algebra of theories TA is presented, with a nonstandard interpretation of the existential quantifier . In TA, the interpolation property of the underlying logic corresponds with the quantifier combination property . It is shown how the Modularization Theorem, the Factorization Lemma and the Normal Form Theorem for module expressions can be proved in TA. Dedicated to the 50th anniversary of William Craig’s Interpolation Theorem.     

Simulating Turing machines on Maurer machines

In a previous paper, we used Maurer machines to model and analyse micro-architectures. In the current paper, we investigate the connections between Turing machines and Maurer machines with the purpose to gain an insight into computability issues relating to Maurer machines. We introduce ways to simulate Turing machines on a Maurer machine which, dissenting from the classical theory of computability, take into account that in reality computations always take place on finite machines. In one of those ways, multi-threads and thread forking have an interesting theoretical application.     

Nonparametric Estimation of Standard Errors in Covariance Analysis Using the Infinitesimal Jackknife

The infinitesimal jackknife provides a simple general method for estimating standard errors in covariance structure analysis. Beyond its simplicity and generality what makes the infinitesimal jackknife method attractive is that essentially no assumptions are required to produce consistent standard error estimates, not even the requirement that the population sampled has the covariance structure assumed. Commonly used covariance structure analysis software uses parametric methods for estimating parameters and standard errors. When the population sampled has the covariance structure assumed, but fails to have the distributional form assumed, the parameter estimates usually remain consistent, but the standard error estimates do not. This has motivated the introduction of a variety of nonparametric standard error estimates that are consistent when the population sampled fails to have the distributional form assumed. The only distributional assumption these require is that the covariance structure be correctly specified. As noted, even this assumption is not required for the infinitesimal jackknife. The relation between the infinitesimal jackknife and other nonparametric standard error estimators is discussed. An advantage of the infinitesimal jackknife over the jackknife and the bootstrap is that it requires only one analysis to produce standard error estimates rather than one for every jackknife or bootstrap sample.     

On the Compositional Extension Problem

A semantics may be compositional and yet partial, in the sense that not all well-formed expressions are assigned meanings by it. Examples come from both natural and formal languages. When can such a semantics be extended to a total one, preserving compositionality? This sort of extension problem was formulated by Hodges, and solved there in a particular case, in which the total extension respects a precise version of the fregean dictum that the meaning of an expression is the contribution it makes to the meanings of complex phrases of which it is a part. Hodges' result presupposes the so-called Husserl property, which says roughly that synonymous expressions must have the same category. Here I solve a different version of the compositional extension problem, corresponding to another type of linguistic situation in which we only have a partial semantics, and without assuming the Husserl property. I also briefly compare Hodges' framework for grammars in terms of partial algebras with more familiar ones, going back to Montague, which use many-sorted algebras instead.

     

Products of Modal Logics. Part 3: Products of Modal and Temporal Logics

In this paper we improve the results of [2] by proving the product f.m.p. for the product of minimal n-modal and minimal n-temporal logic. For this case we modify the finite depth method introduced in [1]. The main result is applied to identify new fragments of classical first-order logic and of the equational theory of relation algebras, that are decidable and have the finite model property.     

How True It Is = Who Says It’s True

This is a largely expository paper in which the following simple idea is pursued. Take the truth value of a formula to be the set of agents that accept the formula as true. This means we work with an arbitrary (finite) Boolean algebra as the truth value space. When this is properly formalized, complete modal tableau systems exist, and there are natural versions of bisimulations that behave well from an algebraic point of view. There remain significant problems concerning the proper formalization, in this context, of natural language statements, particularly those involving negative knowledge and common knowledge. A case study is presented which brings these problems to the fore. None of the basic material presented here is new to this paper—all has appeared in several papers over many years, by the present author and by others. Much of the development in the literature is more general than here—we have confined things to the Boolean case for simplicity and clarity. Most proofs are omitted, but several of the examples are new. The main virtue of the present paper is its coherent presentation of a systematic point of view—identify the truth value of a formula with the set of those who say the formula is true.     

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.     

Multivariate analysis with linearizable regressions

We study the class of multivariate distributions in which all bivariate regressions can be linearized by separate transformation of each of the variables. This class seems more realistic than the multivariate normal or the elliptical distributions, and at the same time its study allows us to combine the results from multivariate analysis with optimal scaling and classical multivariate analysis. In particular a two-stage procedure which first scales the variables optimally, and then fits a simultaneous equations model, is studied in detail and is shown to have some desirable properties.     

Naming and Diagonalization, from Cantor to Godel to Kleene

We trace self-reference phenomena to the possibility of namingfunctions by names that belong to the domain over which thefunctions are defined. A naming system is a structure of theform (D, type( ),{ }), where D is a non-empty set; for everya D, which is a name of a k-ary function, {a}: D^k D is thefunction named by a, and type(a) is the type of a, which tellsus if a is a name and, if it is, the arity of the named function.Under quite general conditions we get a fixed point theorem,whose special cases include the fixed point theorem underlyingGödel's proof, Kleene's recursion theorem and many othertheorems of this nature, including the solution to simultaneousfixed point equations. Partial functions are accommodated byincluding "undefined" values; we investigate different systemsarising out of different ways of dealing with them. Many-sortednaming systems are suggested as a natural approach to generalcomputatability with many data types over arbitrary structures.The first part of the paper is a historical reconstruction ofthe way Gödel probably derived his proof from Cantor'sdiagonalization, through the semantic version of Richard. Theincompleteness proof–including the fixed point construction–resultfrom a natural line of thought, thereby dispelling the appearanceof a "magic trick". The analysis goes on to show how Kleene'srecursion theorem is obtained along the same lines.