We extend Barbanera and Berardi's symmetric lambda calculus [2] to second-order classical propositional logic and prove its strong normalization.

The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of (...) natural language form and meaning. (shrink)

Two new first-order paraconsistent logics with De Morgan-type negations and co-implication, called symmetric paraconsistent logic (SPL) and dual paraconsistent logic (DPL), are introduced as Gentzen-type sequent calculi. The logic SPL is symmetric in the sense that the rule of contraposition is admissible in cut-free SPL. By using this symmetry property, a simpler cut-free sequent calculus for SPL is obtained. The logic DPL is not symmetric, but it has the duality principle. Simple semantics for SPL and DPL (...) are introduced, and the completeness theorems with respect to these semantics are proved. The cut-elimination theorems for SPL and DPL are proved in two ways: One is a syntactical way which is based on the embedding theorems of SPL and DPL into Gentzen’s LK, and the other is a semantical way which is based on the completeness theorems. (shrink)

Symmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a muchstrongertheorem that no symmetric combinatory logic that containsat least two proper symmetric combinatoryhas the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic,the proof is differentbecause symmetric combinators may form redexes in both left and right associated terms. (...) Perhaps surprisingly, we are also able to show that certain symmetric combinatory logics that include justone particular constantare not confluent. This result (beyond other differences) clearly sets apart symmetric combinatory logic from dual combinatory logic, since all dual combinatory systems with a single combinator or a single dual combinator are Church-Rosser. Lastly, we prove that a symmetric combinatory logic that contains the fixed point and the one-place identity combinator has the Church-Rosser property. (shrink)

Symmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a much stronger theorem that no symmetric combinatory logic that contains at least two proper symmetric combinators has the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic, the proof is different because symmetric combinators may form redexes in (...) both left and right associated terms. Perhaps surprisingly, we are also able to show that certain symmetric combinatory logics that include just one particular constant are not confluent. This result (beyond other differences) clearly sets apart symmetric combinatory logic from dual combinatory logic, since all dual combinatory systems with a single combinator or a single dual combinator are Church-Rosser. Lastly, we prove that a symmetric combinatory logic that contains the fixed point and the one-place identity combinator has the Church-Rosser property. (shrink)

We present a version of system Fω, called image, in which the layer of type constructors is essentially the traditional one of Fω, whereas provability of types is classical. The proof-term calculus accounting for the classical reasoning is a variant of Barbanera and Berardi’s symmetric λ-calculus.We prove that the whole calculus is strongly normalising. For the layer of type constructors, we use Tait and Girard’s reducibility method combined with orthogonality techniques. For the layer of terms, we (...) use Barbanera and Berardi’s method based on a symmetric notion of reducibility candidate. We prove that orthogonality does not capture the fixpoint construction of symmetric candidates.We establish the consistency of image, and relate the calculus to the traditional system Fω, also when the latter is extended with axioms for classical logic. (shrink)

Gödel logic is the extension of intuitionistic logic by the linearity axiom. Symmetric Gödel logic is a logical system, the language of which is an enrichment of the language of Gödel logic with their dual logical connectives. Symmetric Gödel logic is the extension of symmetric intuitionistic logic. The proof-intuitionistic calculus, the language of which is an enrichment of the language of intuitionistic logic by modal operator was investigated by Kuznetsov and Muravitsky. Bimodal symmetric Gödel logic (...) is a logical system, the language of which is an enrichment of the language of Gödel logic with their dual logical connectives and two modal operators. Bimodal symmetric Gödel logic is embedded into an extension of Gödel–Löb logic, the language of which contains disjunction, conjunction, negation and two modal operators. The variety of bimodal symmetric Gödel algebras, that represent the algebraic counterparts of bimodal symmetric Gödel logic, is investigated. Description of free algebras and characterization of projective algebras in the variety of bimodal symmetric Gödel algebras is given. All finitely generated projective bimodal symmetric Gödel algebras are infinite, while finitely generated projective symmetric Gödel algebras are finite. (shrink)

Gentzen’s classical sequent calculus has explicit structural rules for contraction and weakening. They can be absorbed by replacing the axiom P,¬P by Γ,P,¬P for any context Γ, and replacing the original disjunction rule with Γ,A,B implies Γ,AB.This paper presents a classical sequent calculus which is also free of contraction and weakening, but more symmetrically: both contraction and weakening are absorbed into conjunction, leaving the axiom rule intact. It uses a blended conjunction rule, combining the standard context-sharing and context-splitting (...) rules: Γ,Δ,A and Γ,Σ,B implies Γ,Δ,Σ,AB. We refer to this system as minimal sequent calculus.We prove a minimality theorem for the propositional fragment : any propositional sequent calculus S is complete if and only if S contains. Thus one can view as a minimal complete core of Gentzen’s. (shrink)

The paper contains an exposition of some non standard approach to gentzenization of modal logics. The first section is devoted to short discussion of desirable properties of Gentzen systems and the short review of various sequential systems for modal logics. Two non standard, cut-free sequent systems are then presented, both based on the idea of using special modal sequents, in addition to usual ones. First of them, GSC I is well suited for nonsymmetric modal logics The second one, GSC II (...) is devised specially for symmetric, i.e. Blogics. GSC I and GSC II are not different formalizations, from the theoretical point of view GSC I may be seen as a simplification of the more general approach present in GSC II. They are considered separately, mainly because Blogics demand different, and more complicated, strategy in completeness proof, whereas non symmetric logics are easily and uniformly characterised by means of Fitting's Consistency Properties. The weakest modal logic captured by this formalization is minimal regular logic C, but many stronger logics are obtainable by addition of suitable structural rules, which conforms to Do en's methodology. Both variants of GSC satisfy also other, besides cut-freedom, desirable properties. (shrink)

It is a commonplace in the philosophy of physics that any local physical theory can be represented using arbitrary coordinates, simply by using tensor calculus. On the other hand, the physics literature often claims that spinors \emph{as such} cannot be represented in coordinates in a curved space-time. These commonplaces are inconsistent. What general covariance means for theories with fermions, such as electrons, is thus unclear. In fact both commonplaces are wrong. Though it is not widely known, Ogievetsky and Polubarinov (...) constructed spinors in coordinates in 1965, enhancing the unity of physics and helping to spawn particle physicists' concept of nonlinear group representations. Roughly and locally, these spinors resemble the orthonormal basis or "tetrad" formalism in the symmetric gauge, but they are conceptually self-sufficient and more economical. The typical tetrad formalism is de-Ockhamized, with six extra field components and six compensating gauge symmetries to cancel them out. The Ogievetsky-Polubarinov formalism, by contrast, is Ockhamized, with most of the fluff removed. As developed nonperturbatively by Bilyalov, it admits any coordinates at a point, but "time" must be listed first. Here "time" is defined in terms of an eigenvalue problem involving the metric components and the matrix $diag$, the product of which must have no negative eigenvalues in order to yield a real symmetric square root that is a function of the metric. Thus even formal general covariance requires reconsideration; the atlas of admissible coordinate charts should be sensitive to the types and \emph{values} of the fields involved. Apart from coordinate order and the usual spinorial two-valuedness, Ogievetsky-Polubarinov spinors form, with the metric, a nonlinear geometric object, for which important results on Lie and covariant differentiation are recalled. Such spinors avoid a spurious absolute object in the Anderson-Friedman analysis of substantive general covariance. They also permit the gauge-invariant localization of the infinite-component gravitational energy in General Relativity. Density-weighted spinors exploit the conformal invariance of the massless Dirac equation to show that the volume element is absent. Thus instead of an arbitrary nonsingular matrix with 16 components, 6 of which are gauged away by a new local $O$ gauge group and one of which is irrelevant due to conformal covariance, one can, and presumably should, use density-weighted Ogievetsky-Polubarinov spinors coupled to the 9-component symmetric square root of the part of the metric that fixes null cones. Thus $\frac{7}{16}$ of the orthonormal basis is eliminated as surplus structure. Greater unity between spinors and tensors and the like is achieved, such as regarding conservation laws. Regarding the conventionality of simultaneity, an unusually wide range of $\epsilon$ values is admissible, but some extreme values are inadmissible. Standard simultaneity uniquely makes the spinor transformation law linear and independent of the metric, because transformations among the standard Cartesian coordinate systems fall within the conformal group, for which the spinor transformation law is linear. The surprising mildness of the restrictions on coordinate order as applied to the Schwarzschild solution is exhibited. (shrink)

We introduce Boolean-like algebras of dimension n ($$n{\mathrm {BA}}$$ n BA s) having n constants $${{{\mathsf {e}}}}_1,\ldots,{{{\mathsf {e}}}}_n$$ e 1, …, e n, and an $$(n+1)$$ ( n + 1 ) -ary operation q (a “generalised if-then-else”) that induces a decomposition of the algebra into n factors through the so-called n-central elements. Varieties of $$n{\mathrm {BA}}$$ n BA s share many remarkable properties with the variety of Boolean algebras and with primal varieties. The $$n{\mathrm {BA}}$$ n BA s provide the (...) algebraic framework for generalising the classical propositional calculus to the case of n–perfectly symmetric–truth-values. Every finite-valued tabular logic can be embedded into such a n-valued propositional logic, $$n{\mathrm {CL}}$$ n CL, and this embedding preserves validity. We define a confluent and terminating first-order rewriting system for deciding validity in $$n{\mathrm {CL}}$$ n CL, and, via the embeddings, in all the finite tabular logics. (shrink)

It is a commonplace in the philosophy of physics that any local physical theory can be represented using arbitrary coordinates, simply by using tensor calculus. On the other hand, the physics literature often claims that spinors \emph{as such} cannot be represented in coordinates in a curved space-time. These commonplaces are inconsistent. What general covariance means for theories with fermions, such as electrons, is thus unclear. In fact both commonplaces are wrong. Though it is not widely known, Ogievetsky and Polubarinov (...) constructed spinors in coordinates in 1965, enhancing the unity of physics and helping to spawn particle physicists' concept of nonlinear group representations. Roughly and locally, these spinors resemble the orthonormal basis or "tetrad" formalism in the symmetric gauge, but they are conceptually self-sufficient and more economical. The typical tetrad formalism is de-Ockhamized, with six extra field components and six compensating gauge symmetries to cancel them out. The Ogievetsky-Polubarinov formalism, by contrast, is Ockhamized, with most of the fluff removed. As developed nonperturbatively by Bilyalov, it admits any coordinates at a point, but "time" must be listed first. Here "time" is defined in terms of an eigenvalue problem involving the metric components and the matrix $diag$, the product of which must have no negative eigenvalues in order to yield a real symmetric square root that is a function of the metric. Thus even formal general covariance requires reconsideration; the atlas of admissible coordinate charts should be sensitive to the types and \emph{values} of the fields involved. Apart from coordinate order and the usual spinorial two-valuedness, Ogievetsky-Polubarinov spinors form, with the metric, a nonlinear geometric object, for which important results on Lie and covariant differentiation are recalled. Such spinors avoid a spurious absolute object in the Anderson-Friedman analysis of substantive general covariance. They also permit the gauge-invariant localization of the infinite-component gravitational energy in General Relativity. Density-weighted spinors exploit the conformal invariance of the massless Dirac equation to show that the volume element is absent. Thus instead of an arbitrary nonsingular matrix with 16 components, 6 of which are gauged away by a new local $O$ gauge group and one of which is irrelevant due to conformal covariance, one can, and presumably should, use density-weighted Ogievetsky-Polubarinov spinors coupled to the 9-component symmetric square root of the part of the metric that fixes null cones. Thus $\frac{7}{16}$ of the orthonormal basis is eliminated as surplus structure. Greater unity between spinors and tensors and the like is achieved, such as regarding conservation laws. Regarding the conventionality of simultaneity, an unusually wide range of $\epsilon$ values is admissible, but some extreme values are inadmissible. Standard simultaneity uniquely makes the spinor transformation law linear and independent of the metric, because transformations among the standard Cartesian coordinate systems fall within the conformal group, for which the spinor transformation law is linear. The surprising mildness of the restrictions on coordinate order as applied to the Schwarzschild solution is exhibited. (shrink)

It is a commonplace in the philosophy of physics that any local physical theory can be represented using arbitrary coordinates, simply by using tensor calculus. On the other hand, the physics literature often claims that spinors \emph{as such} cannot be represented in coordinates in a curved space-time. These commonplaces are inconsistent. What general covariance means for theories with fermions, such as electrons, is thus unclear. In fact both commonplaces are wrong. Though it is not widely known, Ogievetsky and Polubarinov (...) constructed spinors in coordinates in 1965, enhancing the unity of physics and helping to spawn particle physicists' concept of nonlinear group representations. Roughly and locally, these spinors resemble the orthonormal basis or "tetrad" formalism in the symmetric gauge, but they are conceptually self-sufficient and more economical. The typical tetrad formalism is de-Ockhamized, with six extra field components and six compensating gauge symmetries to cancel them out. The Ogievetsky-Polubarinov formalism, by contrast, is Ockhamized, with most of the fluff removed. As developed nonperturbatively by Bilyalov, it admits any coordinates at a point, but "time" must be listed first. Here "time" is defined in terms of an eigenvalue problem involving the metric components and the matrix $diag$, the product of which must have no negative eigenvalues in order to yield a real symmetric square root that is a function of the metric. Thus even formal general covariance requires reconsideration; the atlas of admissible coordinate charts should be sensitive to the types and \emph{values} of the fields involved. Apart from coordinate order and the usual spinorial two-valuedness, Ogievetsky-Polubarinov spinors form, with the metric, a nonlinear geometric object, for which important results on Lie and covariant differentiation are recalled. Such spinors avoid a spurious absolute object in the Anderson-Friedman analysis of substantive general covariance. They also permit the gauge-invariant localization of the infinite-component gravitational energy in General Relativity. Density-weighted spinors exploit the conformal invariance of the massless Dirac equation to show that the volume element is absent. Thus instead of an arbitrary nonsingular matrix with 16 components, 6 of which are gauged away by a new local $O$ gauge group and one of which is irrelevant due to conformal covariance, one can, and presumably should, use density-weighted Ogievetsky-Polubarinov spinors coupled to the 9-component symmetric square root of the part of the metric that fixes null cones. Thus $\frac{7}{16}$ of the orthonormal basis is eliminated as surplus structure. Greater unity between spinors and tensors and the like is achieved, such as regarding conservation laws. Regarding the conventionality of simultaneity, an unusually wide range of $\epsilon$ values is admissible, but some extreme values are inadmissible. Standard simultaneity uniquely makes the spinor transformation law linear and independent of the metric, because transformations among the standard Cartesian coordinate systems fall within the conformal group, for which the spinor transformation law is linear. The surprising mildness of the restrictions on coordinate order as applied to the Schwarzschild solution is exhibited. (shrink)

We prove that the equational theory of a semigroups becomes undecidable if we add a semilattice structure with a ‘touch of symmetric difference’. As a corollary we obtain that the variety of all Boolean algebras with an associative binary operator has a ‘hereditarily’ undecidable equational theory. Our results have implications in logic, e.g. they imply undecidability of modal logics extending the Lambek Calculus and undecidability of Arrow Logics with an associative arrow modality.

Combinatory logic is known to be related to substructural logics. Algebraic considerations of the latter, in particular, algebraic considerations of two distinct implications, led to the introduction of dual combinators in Dunn & Meyer 1997. Dual combinators are "mirror images" of the usual combinators and as such do not constitute an interesting subject of investigation by themselves. However, when combined with the usual combinators, the whole system exhibits new features. A dual combinatory system with weak equality typically lacks the Church-Rosser (...) property, and in general it is inconsistent. In many subsystems terms "unexpectedly" turn out to be weakly equivalent. The paper is a preliminary attempt to investigate some of these issues, as well as, briefly compare function application in symmetric -calculus and dual combinatory logic. (shrink)

We introduce a graphical framework for Bayesian inference that is sufficiently general to accommodate not just the standard case but also recent proposals for a theory of quantum Bayesian inference wherein one considers density operators rather than probability distributions as representative of degrees of belief. The diagrammatic framework is stated in the graphical language of symmetric monoidal categories and of compact structures and Frobenius structures therein, in which Bayesian inversion boils down to transposition with respect to an appropriate compact (...) structure. We characterize classical Bayesian inference in terms of a graphical property and demonstrate that our approach eliminates some purely conventional elements that appear in common representations thereof, such as whether degrees of belief are represented by probabilities or entropie quantities. We also introduce a quantum-like calculus wherein the Frobenius structure is noncommutative and show that it can accommodate Leifer's calculus of 'conditional density operators'. The notion of conditional independence is also generalized to our graphical setting and we make some preliminary connections to the theory of Bayesian networks. Finally, we demonstrate how to construct a graphical Bayesian calculus within any dagger compact category. (shrink)

A symmetric monoidal category naturally arises as the mathematical structure that organizes physical systems, processes, and composition thereof, both sequentially and in parallel. This structure admits a purely graphical calculus. This paper is concerned with the encoding of a fixed causal structure within a symmetric monoidal category: causal dependencies will correspond to topological connectedness in the graphical language. We show that correlations, either classical or quantum, force terminality of the tensor unit. We also show that well-definedness of (...) the concept of a global state forces the monoidal product to be only partially defined, which in turn results in a relativistic covariance theorem. Except for these assumptions, at no stage do we assume anything more than purely compositional symmetric-monoidal categorical structure. We cast these two structural results in terms of a mathematical entity, which we call a causal category . We provide methods of constructing causal categories, and we study the consequences of these methods for the general framework of categorical quantum mechanics. (shrink)

A new calculus, based upon the multivector derivative, is developed for Lagrangian mechanics and field theory, providing streamlined and rigorous derivations of the Euler-Lagrange equations. A more general form of Noether's theorem is found which is appropriate to both discrete and continuous symmetries. This is used to find the conjugate currents of the Dirac theory, where it improves on techniques previously used for analyses of local observables. General formulas for the canonical stress-energy and angular-momentum tensors are derived, with spinors (...) and vectors treated in a unified way. It is demonstrated that the antisymmetric terms in the stress-energy tensor are crucial to the correct treatment of angular momentum. The multivector derivative is extended to provide a functional calculus for linear functions which is more compact and more powerful than previous formalisms. This is demonstrated in a reformulation of the functional derivative with respect to the metric, which is then used to recover the full canonical stress-energy tensor. Unlike conventional formalisms, which result in a symmetric stress-energy tensor, our reformulation retains the potentially important antisymmetric contribution. (shrink)

We compare the logic HYPE recently suggested by H. Leitgeb as a basic propositional logic to deal with hyperintensional contexts and Heyting-Ockham logic introduced in the course of studying logical aspects of the well-founded semantics for logic programs with negation. The semantics of Heyting-Ockham logic makes use of the so-called Routley star negation. It is shown how the Routley star negation can be obtained from Dimiter Vakarelov’s theory of negation and that propositional HYPE coincides with the logic characterized by the (...) class of all involutive Routley star information frames. This result provides a much simplified semantics for HYPE and also a simplified axiomatization, which shows that HYPE is identical with the modal symmetric propositional calculus introduced by G. Moisil in 1942. Moreover, it is shown that HYPE can be faithfully embedded into a normal bi-modal logic based on classical logic. Against this background, we discuss the notion of hyperintensionality. (shrink)

Charles Peirce’s alpha system \ is reformulated into a deep inference system where the rules are given in terms of deep graphical structures and each rule has its symmetrical rule in the system. The proof analysis of \ is given in terms of two embedding theorems: the system \ and Brünnler’s deep inference system for classical propositional logic can be embedded into each other; and the system \ and Gentzen sequent calculus \ can be embedded into each other.

We study the coherence, that is the equality of canonical natural transformations in non-free symmetric monoidal closed categories . To this aim, we use proof theory for intuitionistic multiplicative linear logic with unit. The study of coherence in non-free smccs is reduced to the study of equivalences on terms in the free category, which include the equivalences induced by the smcc structure. The free category is reformulated as the sequent calculus for imll with unit so that only equivalences (...) on derivations in this system are to be considered. We establish that any equivalence induced by the equality of canonical natural transformations over a model can be axiomatized by some set of “critical” pairs of derivations. From this, we derive certain sufficient conditions for full coherence, and establish that the system of identities defining smccs is not Post-complete: extending this system with an identity that does not hold in the free smcc does not in general cause the free smcc to collapse into a preorder. In order to give a larger context to these results, we study the equality of canonical morphisms in non-free symmetric monoidal categories, and establish that w.r.t. a broad subclass of smccs, the equivalences induced by the equality of canonical natural transformations over a model coincide with the equivalences induced by the equality of canonical morphisms for all interpretations in that model. (shrink)

Quite often the compatibility of the EPR correlations with the relativity theory has been questioned; it has been stated that “the first in time of two correlated measurements instantaneously collapses the other subsystem”; it has been suggested that a causal asymmetry is built into the Feynman propagator. However, the EPR transition amplitude, as derived from the S matrix, is Lorentz andCPT invariant; the correlation formula is symmetric in the two measurements irrespective of their time ordering, so that the link (...) of the correlations is the Feynman zigzag, and that causality isCPT invariant at the microlevel; finally, although the Feynman propagator has theP andCT symmetries, no causal asymmetry follows from that. As for Stapp's views concerning “process” and “becoming,” and his Whiteheadean concept of an advancing front, I object that they belong to “factlike macrophysics,” and are refuted at the microlevel by the EPR phenomenology, which displays direct Fokker-like space-time connections. The reason for this is a radical one. The very blending of a space-time picture and of a probability calculus is a paradox. The only adequate paradigm is one denying objectivity to space-time—but this, of course, is also required by the complementary of the x and the k pictures, which only “look” compatible at the macrolevel. Therefore, the classical “objectivity” must yield in favor of “intersubjectivity.” Only the macroscopic preparing and measuring devices have “factlike” objectivity; the “transition” of the “quantal system” takes place beyond both thex and thek 4-spaces. Then, the intrinsic symmetries between retarded and advanced waves, and statistical prediction and retrodiction, entails that the future has no less (but no more) existence than the past. It is the future that is significant in “creative process,” the “elementary” forms of which should be termed “precognition” or “psychokinesis”—respectively symmetric to the factlike taboos that “we can neither know into the future nor act into the past.” It is gratifying that Robert Jahn, at the Engineering School of Princeton University, is conducting (after others) conclusive experiments demonstrating “low level psychokinesis”—a phenomenon implied by the very symmetry of the negentropy-information transition. So, what pierces the veil of “maya” is the (rare) occurrence of “paranormal phenomena.” The essential severance between “act” and “potentia” is not a spacelike advancing front, but the “out of” and the “into” factlike space-time. Finally, I do not feel that an adequate understanding of the EPR phenomenology requires going beyond the present status of relativistic quantum mechanics. Rather, I believe that the potentialities of this formalism have not yet been fully exploited. (shrink)

This book stands at the intersection of two topics: the decidability and computational complexity of hybrid logics, and the deductive systems designed for them. Hybrid logics are here divided into two groups: standard hybrid logics involving nominals as expressions of a separate sort, and non-standard hybrid logics, which do not involve nominals but whose expressive power matches the expressive power of binder-free standard hybrid logics.The original results of this book are split into two parts. This division reflects the division of (...) the book itself. The first type of results concern model-theoretic and complexity properties of hybrid logics. Since hybrid logics which we call standard are quite well investigated, the efforts focused on hybrid logics referred to as non-standard in this book. Non-standard hybrid logics are understood as modal logics with global counting operators ) whose expressive power matches the expressive power of binder-free standard hybrid logics. The relevant results comprise: 1. Establishing a sound and complete axiomatization for the modal logic K with global counting operators ), which can be easily extended onto other frame classes, 2. Establishing tight complexity bounds, namely NExpTime-completeness for the modal logic with global counting operators defined over the classes of arbitrary, reflexive, symmetric, serial and transitive frames ), MT), MD), MB), MK4) with numerical subscripts coded in binary. Establishing the exponential-size model property for this logic defined over the classes of Euclidean and equivalential frames ), MS5).Results of the second type consist of designing concrete deductive systems for standard and non-standard hybrid logics. More precisely, they include: 1. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for a rich class of binder-free standard hybrid logics. An interesting feature of indicated calculi is the nonbranching character of the rule, 2. Devising a prefixed and an internalized tableau calculi which are sound, complete and terminating for non-standard hybrid logics. The internalization technique applied to a tableau calculus for the modal logic with global counting operators is novel in the literature, 3. Devising the first hybrid algorithm involving an inequality solver for modal logics with global counting operators. Transferring the arithmetical part of reasoning to an inequality solver turned out to be sufficient in ensuring termination.The book is directed to philosophers and logicians working with modal and hybrid logics, as well as to computer scientists interested in deductive systems and decision procedures for logics. Extensive fragments of the first part of the book can also serve as an introduction to hybrid logics for wider audience interested in logic.The content of the book is situated in the areas of formal logic and theoretical computer science with some elements of the theory of computational complexity. (shrink)

We extend to the exponential connectives of linear logic the study initiated in Bucciarelli and Ehrhard 247). We define an indexed version of propositional linear logic and provide a sequent calculus for this system. To a formula A of indexed linear logic, we associate an underlying formula of linear logic, and a family A of elements of , the interpretation of in the category of sets and relations. Then A is provable in indexed linear logic iff the family A (...) is contained in the interpretation of some proof of . We extend to this setting the product phase semantics of indexed multiplicative additive linear logic introduced in Bucciarelli and Ehrhard , defining the symmetric product phase spaces. We prove a soundness result for this truth-value semantics and show how a denotational model of linear logic can be associated to any symmetric product phase space. Considering a particular symmetric product phase space, we obtain a new coherence space model of linear logic, which is non-uniform in the sense that the interpretation of a proof of !A−B contains informations about the behavior of this proof when applied to “chimeric” arguments of type A . In this coherence semantics, an element of a web can be strictly coherent with itself, or two distinct elements can be “neutral”. (shrink)

Hypersequents are finite sets of ordinary sequents. We show that multiple-conclusion sequents and single-conclusion hypersequents represent two different natural methods of switching from a single-conclusion calculus to a multiple-conclusion one. The use of multiple-conclusion sequents corresponds to using a multiplicative disjunction, while the use of single-conclusion hypersequents corresponds to using an additive one. Moreover: each of the two methods is usually based on a different natural semantic idea and accordingly leads to a different class of algebraic structures. In the (...) cases we consider here the use of multiple-conclusion sequents corresponds to focusing the attention on structures in which there is a full symmetry between the sets of designated and antidesignated elements. The use of single-conclusion hypersequents, on the other hand, corresponds to the use of structures in which all elements except one are designated. Not surprisingly, the use of multiple-conclusion hypersequents corresponds to the use of structures which are both symmetrical and with a single nondesignated element. (shrink)

There is currently much interest in bringing together the tradition of categorial grammar, and especially the Lambek calculus, with the recent paradigm of linear logic to which it has strong ties. One active research area is designing non-commutative versions of linear logic (Abrusci, 1995; Retoré, 1993) which can be sensitive to word order while retaining the hypothetical reasoning capabilities of standard (commutative) linear logic (Dalrymple et al., 1995). Some connections between the Lambek calculus and computations in groups have (...) long been known (van Benthem, 1986) but no serious attempt has been made to base a theory of linguistic processing solely on group structure. This paper presents such a model, and demonstrates the connection between linguistic processing and the classical algebraic notions of non-commutative free group, conjugacy, and group presentations. A grammar in this model, or G-grammar is a collection of lexical expressions which are products of logical forms, phonological forms, and inverses of those. Phrasal descriptions are obtained by forming products of lexical expressions and by cancelling contiguous elements which are inverses of each other. A G-grammar provides a symmetrical specification of the relation between a logical form and a phonological string that is neutral between parsing and generation modes. We show how the G-grammar can be oriented for each of the modes by reformulating the lexical expressions as rewriting rules adapted to parsing or generation, which then have strong decidability properties (inherent reversibility). We give examples showing the value of conjugacy for handling long-distance movement and quantifier scoping both in parsing and generation. The paper argues that by moving from the free monoid over a vocabulary V (standard in formal language theory) to the free group over V, deep affinities between linguistic phenomena and classical algebra come to the surface, and that the consequences of tapping the mathematical connections thus established can be considerable. (shrink)

In the Böhm theorem workshop on Crete, Zoran Petric called Statman’s “Typical Ambiguity theorem” the typed Böhm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Böhm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit the weak typed Böhm theorem holds. The system (...) IMLL exactly corresponds to the linear lambda calculus with multiplicative pairing. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner. (shrink)

We study the sequent system mentioned in the author's work as CyInFL with ‘intuitionistic’ sequents. We explore the connection between this system and symmetric constructive logic of Zaslavsky and develop an algebraic semantics for both of them. In contrast to the previous work, we prove the strong completeness theorem for CyInFL with ‘intuitionistic’ sequents and all of its basic variants, including variants with contraction. We also show how the defined classes of structures are related to cyclic involutive FL‐algebras and (...) Nelson FLew‐algebras. In particular, we prove the definitional equivalence of symmetric constructive FLewc‐algebras (algebraic models of symmetric constructive logic) and Nelson FLew‐algebras (algebras introduced by Spinks and Veroff, as the termwise equivalent definition of Nelson algebras). Because of the strong completeness theorem that covers all basic variants of CyInFL with ‘intuitionistic’ sequents, we rename this sequent system to symmetric constructive full Lambek calculus (). We verify the decidability of this system and its basic variants, as we did in the case of their distributive cousins. As a consequence we obtain that the corresponding theories of (distributive and nondistributive) symmetric constructive FL‐algebras are decidable. (shrink)

It is a commonplace in the foundations of physics, attributed to Kretschmann, that any local physical theory can be represented using arbitrary coordinates, simply by using tensor calculus. On the other hand, the physics and mathematics literature often claims that spinors \emph{as such} cannot be represented in coordinates in a curved space-time. These commonplaces are inconsistent. What general covariance means for theories with fermions is thus unclear. In fact both commonplaces are wrong. Though it is not widely known, Ogievetsky (...) and Polubarinov constructed spinors in coordinates in 1965, enhancing the unity of physics and helping to spawn particle physicists' concept of nonlinear group representations. Roughly and locally, OP spinors resemble the orthonormal basis or tetrad formalism in the symmetric gauge, but they are conceptually self-sufficient and more economical. The typical tetrad formalism is thus de-Ockhamized, with six extra field components and six compensating gauge symmetries to cancel them out. As developed nonperturbatively by Bilyalov, OP spinors admit any coordinates at a point, but `time' must be listed first; `time' is defined in terms of an eigenvalue problem involving the metric components and the matrix $diag$, the product of which must have no negative eigenvalues. Thus even formal general covariance requires reconsideration; the atlas of admissible coordinate charts should be sensitive to the types and \emph{values} of the fields involved. Apart from coordinate order and the usual spinorial two-valuedness, Ogievetsky-Polubarinov spinors form, with the metric, a nonlinear geometric object. Important results on Lie and covariant differentiation are recalled and applied. The rather mild consequences of the coordinate order restriction are explored in two examples: the question of the conventionality of simultaneity in Special Relativity, and the Schwarzschild solution in General Relativity. (shrink)

Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations . However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that it (...) is possible to model linear logic with implicit functions rather than general relations, an adequate language for such a semantics being differential calculus. This results in a non-degenerate model enjoying quite strong completeness properties. (shrink)

This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.

Metaphysical orthodoxy maintains that the relation of ontological dependence is irreflexive, asymmetric, and transitive. The goal of this paper is to challenge that orthodoxy by arguing that ontological dependence should be understood as non- symmetric, rather than asymmetric. If we give up the asymmetry of dependence, interesting things follow for what we can say about metaphysical explanation— particularly for the prospects of explanatory holism.

Why must incompatibility be symmetric? An odd question, but recent work in the semantics of non-classical logic, which appeals to the notion of incompatibility as a primitive and defines negation in terms of it, has brought this question to the fore. Francesco Berto proposes such a semantics for negation argues that, since incompatibility must be symmetric, double negation introduction must be a law of negation. However, he offers no argument for the claim that incompatibility really must be (...) class='Hi'>symmetric. Here, I provide such an argument, showing that, insofar as we think of incompatibility in normative pragmatic terms, it can play its basic pragmatic function only if it is symmetric. The upshot is that we can vindicate Berto’s claim about the symmetry of incompatibility but only if we, pace Berto, think about incompatibility, in the first instance, as a pragmatic relation between acts rather than a semantic relation between contents. (shrink)

Presupposing that most predicates do not correspond directly to genuine relations, I argue that all genuine relations are symmetric. My main argument depends on the premise that there are no brute necessities, interpreted so as to require logical and metaphysical necessity to coincide for sentences composed entirely of logical vocabulary and primitive predicates. Given this premise, any set of purportedly primitive predicates by which one might hope to express the facts about non-symmetric relations order their relata will generate (...) an objectionable multiplication of possibilities. In the final section I give a different argument, based on the weaker premise that brute necessities should not be multiplied without necessity. (shrink)

A time-symmetric formulation of nonrelativistic quantum mechanics is developed by applying two consecutive boundary conditions onto solutions of a time- symmetrized wave equation. From known probabilities in ordinary quantum mechanics, a time-symmetric parameter P0 is then derived that properly weights the likelihood of any complete sequence of measurement outcomes on a quantum system. The results appear to match standard quantum mechanics, but do so without requiring a time-asymmetric collapse of the wavefunction upon measurement, thereby realigning quantum mechanics with (...) an important fundamental symmetry. (shrink)

I examine and discuss in this paper Orilia’s theory of external, non-symmetrical relations, that is based on ontological roles (O-Roles). I explore several attempts to interpret O-Roles from an ontological viewpoint and I reject them because of two problems concerning the status of asymmetrical relations (to be distinguished from non-symmetrical relations simpliciter) and of exemplification as an external, non-symmetrical relation. Finally, following Heil’s and Lowe’s characterization of modes as particular properties that ontologically depend on their “bearers”, I introduce relational modes (...) in order to define a new solution to the problems of the ontological status of both external, non-symmetrical relations and O-Roles. I also deal with five objections raised by Fraser MacBride against relational modes and O-Roles and I elaborate an analysis of the relations of being to the left of and being to the right of. (shrink)

This article explores the elective affinities between Actor-Network Theory (ANT) and the sociology of critical capacities. It argues that these two research programmes can be understood as symmetrical twins. We show the extent to which the exchange between Bruno Latour and Luc Boltanski has influenced their respective theoretical developments. Three strong encounters between the twin research programmes may be distinguished. The first encounter concerns explanations for social change. The second encounter focuses on the status of objects and their relationship to (...) places. The third encounter is about the concept of critique. Drawing on their long-term mutual readings, we gain insight into how pleas for symmetrical analysis raised in response to Bourdieu’s theory of fields have evolved within both ANT and the sociology of critical capacity. We conclude by relating the development of the respective research programmes to the issue of disciplinary boundaries. (shrink)

It is a metaphysical orthodoxy that interesting non-symmetric relations cannot be reduced to symmetric ones. This orthodoxy is wrong. I show this by exploring the expressive power of symmetric theories, i.e. theories which use only symmetric predicates. Such theories are powerful enough to raise the possibility of Pythagrapheanism, i.e. the possibility that the world is just a vast, unlabelled, undirected graph.

The completeness of the axiomatization of contingency logic over symmetric frames has been thought of as a nontrivial job, the unimodal case of which cannot be generalized to the finitely multimodal case, which in turn cannot be generalized to the infinitely multimodal case. This paper deals with the completeness of symmetric contingency logic with unlimitedly many modalities, no matter whether the set of modalities is finite or infinite.

The purpose of this paper is to explore two questions:(1) Is symmetrical communication in public relations practice inherently ethical?(2) Does symmetrical communication contribute to public relations effectiveness and organizational effectiveness? Three surveys are undertaken to test seven research hypotheses for the purpose of cross-validating research findings. The results suggest that symmetrical communication is inherently ethical. Moreover, symmetrical communication indeed contributes to several performance measures, which include positive market performance, overall organizational effectiveness, conflict resolution, crisis management, favorable organizational reputation, and positive (...) media exposure, with the last two measures only partially supported. (shrink)

Symmetric generalized Galois logics (i.e., symmetric gGl s) are distributive gGl s that include weak distributivity laws between some operations such as fusion and fission. Motivations for considering distribution between such operations include the provability of cut for binary consequence relations, abstract algebraic considerations and modeling linguistic phenomena in categorial grammars. We represent symmetric gGl s by models on topological relational structures. On the other hand, topological relational structures are realized by structures of symmetric gGl s. (...) We generalize the weak distributivity laws between fusion and fission to interactions of certain monotone operations within distributive super gGl s. We are able to prove appropriate generalizations of the previously obtained theorems—including a functorial duality result connecting classes of gGl s and classes of structures for them. (shrink)

Disability and enhancement are often treated as opposing concepts. To become disabled in some respect is to move away from those who are enhanced in that same respect; to become enhanced is to move away from the corresponding state of disability. This chapter examines how best to understand the concepts of disability and enhancement in this symmetrical way. After considering various candidates, two types of accounts are identified as the most promising: welfarist accounts and typical-functioning accounts. The authors ultimately defend (...) a complex typical-functioning account as the best way to achieve a symmetrical understanding of disability and enhancement. (shrink)

Counterfactuals in quantum theory are briefly reviewed and it is argued that they are very different from counterfactuals considered in the general philosophical literature. The issue of time symmetry of quantum counterfactuals is considered and a novel time-symmetric definition of quantum counterfactuals is proposed. This definition is applied for analyzing several controversies related to quantum counterfactuals.

This paper presents a new Symmetrical Interpretation (SI) of relativistic quantum mechanics which postulates: quantum mechanics is a theory about complete experiments, not particles; a complete experiment is maximally described by a complex transition amplitude density; and this transition amplitude density never collapses. This SI is compared to the Copenhagen Interpretation (CI) for the analysis of Einstein’s bubble experiment. This SI makes several experimentally testable predictions that differ from the CI, solves one part of the measurement problem, resolves some inconsistencies (...) of the CI, and gives intuitive explanations of some previously mysterious quantum effects. (shrink)

The universe is enormous, perhaps unimaginably so. In comparison, we are very small. Does this suggest that humanity has little if any cosmic significance? And if we don’t matter, should that matter to us? Blaise Pascal, Frank Ramsey, Bertrand Russell, Susan Wolf, Harry Frankfurt, Stephen Hawking, and others have offered insightful answers to those questions. For example, Pascal and Ramsey emphasize that whereas the stars cannot think, human beings can. Through an exploration of some features of awe and its positive (...) effects on us, I offer a novel way of answering the second question: even if we don’t matter, we, unlike the stars, naturally benefit from observing our own smallness. I explore implications for accounts of the absurdity of human life. Life might be absurd. But I give reasons to think that life isn’t absurd in the ways some such as Nagel and Camus suggest. Finally, I connect non-symmetric awe with Buddhist insights to strengthen a recent and more positive account of how to find meaning in life. (shrink)

There are two ways to characterize symmetric relations. One is intensional: necessarily, _Rxy_ iff _Ryx_. In some discussions of relations, however, what is important is whether or not a relation gives rise to the same completion of a given type (fact, state of affairs, or proposition) for each of its possible applications to some fixed relata. Kit Fine calls relations that do ‘strictly symmetric’. Is there is a difference between the notions of necessary and strict symmetry that would (...) prevent them from being used interchangeably in such discussions? I show that there is. While the notions coincide assuming an intensional account of relations and their completions, according to which relations/completions are identical if they are necessarily coinstantiated/equivalent, they come apart assuming a hyperintensional account, which individuates relations and completions more finely on the basis of relations’ real definitions. I establish this by identifying two definable relations, each of which is necessarily symmetric but nonetheless results in distinct facts when it applies to the same objects in opposite orders. In each case, I argue that these facts are distinct because they have different grounds. (shrink)

The universe is enormous, perhaps unimaginably so. In comparison, we are very small. Does this suggest that humanity has little if any cosmic significance? And if we don’t matter, should that matter to us? Blaise Pascal, Frank Ramsey, Bertrand Russell, Susan Wolf, Harry Frankfurt, Stephen Hawking, and others have offered insightful answers to those questions. For example, Pascal and Ramsey emphasize that whereas the stars (in all their enormity) cannot think, human beings can. Through an exploration of some features of (...) awe and its positive effects on us, I offer a novel way of answering the second question: even if we don’t matter, we, unlike the stars, naturally benefit from observing our own smallness. I explore implications for accounts of the absurdity of human life. Life might be absurd. But I give reasons to think that life isn’t absurd in the ways some such as Nagel and Camus suggest. Finally, I connect non-symmetric awe with Buddhist insights to strengthen a recent and more positive account of how to find meaning in life. (shrink)