Effect algebras form a formal algebraic description of the structure of the so-called effects in a Hilbert space which serves as an event-state space for effects in quantum mechanics. This is why effect algebras are considered as logics of quantum mechanics, more precisely as an algebraic semantics of these logics. Because every productive logic is is equipped with a connective implication, we introduce here such a concept and demonstrate its properties. In particular, we show that this implication is connected with conjunction via a certain "unsharp" residuation which is formulated on the basis of a strict unsharp residuated poset. Though this structure is rather complicated, it can be converted back into an effect algebra and hence it is sound. Further, we study the Modus Ponens rule for this implication by means of so-called deductive systems and finally we study the contraposition law.
Since orthomodular posets serve as an algebraic axiomatization of the logic of quantum mechanics, it is a natural question how the connective of implication can be defined in this logic. It should be introduced in such a way that it is related with conjunction, i.e. with the partial operation meet, by means of some kind of adjointness. We present here such an implication for which a so-called unsharp residuated poset can be constructed. Then this implication is connected with the operation meet by the so-called unsharp adjointness. We prove that also conversely, under some additional assumptio…
It is well-known that intuitionistic logics can be formalized by means of Brouwerian semilattices, i.e. relatively pseudocomplemented semilattices. Then the logical connective implication is considered to be the relative pseudocomplement and conjunction is the semilattice operation meet. If the Brouwerian semilattice has a bottom element 0 then the relative pseudocomplement with respect to 0 is called the pseudocomplement and it is considered as the connective negation in this logic. Our idea is to consider an arbitrary meet-semilattice with 0 satisfying only the Ascending Chain Condition, whi…
We expand FLew with a unary connective whose algebraic counterpart is the operation that gives the greatest complemented element below a given argument. We prove that the expanded logic is conservative and has the Finite Model Property. We also prove that the corresponding expansion of the class of residuated lattices is an equational class.
Effect algebras were introduced in order to describe the structure of effects, i.e. events in quantum mechanics. They are partial algebras describing the logic behind the corresponding events. It is natural to ask how to introduce the logical connective implication in effect algebras. For lattice-ordered effect algebras this task was already solved by several authors, including the present ones. We concentrate on effect algebras that need not be lattice-ordered since these can better describe the events occurring in the quantum physical system. Although an effect algebra is only partial, we tr…
In this paper we investigate the algebraic structure of the truth tables of all bracketed formulae with n distinct variables connected by the binary connective of implication.
When an algebraic logic based on a poset instead of a lattice is investigated then there is a natural problem how to introduce the connective implication to be everywhere defined and satisfying (left) adjointness with the connective conjunction. We have already studied this problem for the logic of quantum mechanics which is based on an orthomodular poset or the logic of quantum effects based on a so-called effect algebra which is only partial and need not be lattice-ordered. For this, we introduced the so-called operator residuation where the values of implication and conjunction need not be …
Both propositional dependence logic and inquisitive logic are expressively complete. As a consequence, every formula with intuitionistic disjunction or intuitionistic implication can be translated equivalently into a formula in the language of propositional dependence logic without these two connectives. We show that although such a (non-compositional) translation exists, neither intuitionistic disjunction nor intuitionistic implication is uniformly definable in propositional dependence logic.
In this paper we investigate the general combinatorical structure of the truth tables of all bracketed formulae with n distinct variables connected by the binary connective of implication, an m-implication.
When a physicist performs a quantic measurement, new information about the system at hand is gathered. This paper studies the logical properties of how this new information is combined with previous information. It presents Quantum Logic as a propositional logic under two connectives: negation and the "and then" operation that combines old and new information. The "and then" connective is neither commutative nor associative. Many properties of this logic are exhibited, and some small elegant subset is shown to imply all the properties considered. No independence or completeness result is claim…
Orthomodular posets form an algebraic formalization of the logic of quantum mechanics. The question is how to introduce the connective implication in such a logic. We show that this is possible when the orthomodular poset in question is of finite height. The main point is that the corresponding algebra, called implication orthomodular poset, i.e. a poset equipped with a binary operator of implication, corresponds to the original orthomodular poset and this operator is everywhere defined. We present here the complete list of axioms for implication orthomodular posets. This enables us to derive …
In a recent work Foulis and Pulmannov\' a \cite{Foulis2012} studied the logical connectives in lattice effect algebras. In this paper we extend their study and investigate further the logical calculus for which the lattice effect algebras can serve as semantic models. We shall first focus on some properties of lattice effect algebras and will then give a complete axiomatisation of this logic.
An algebraic setting for the validity of Pavelka style completeness for some natural expansions of Łukasiewicz logic by new connectives and rational constants is given. This algebraic approach is based on the fact that the standard MV-algebra on the real segment $[0, 1]$ is an injective MV-algebra. In particular the logics associated with MV-algebras with product and with divisible MV-algebras are considered.
An algebraically expandable (AE) class is a class of algebraic structures axiomatizable by sentences of the form $\forall \exists! \land p = q$. For a logic $L$ algebraized by a quasivariety $\mathcal{Q}$ we show that the AE-subclasses of $\mathcal{Q}$ correspond to certain natural expansions of $L$, which we call {\em algebraic expansions}. These turn out to be a special case of the expansions by implicit connectives studied by X. Caicedo. We proceed to characterize all the AE-subclasses of Abelian $\ell$-groups and perfect MV-algebras, thus fully describing the algebraic expansions of their …
We discuss an algebraic approach to propositional logic with side effects. To this end, we use Hoare's conditional [1985], which is a ternary connective comparable to if-then-else. Starting from McCarthy's notion of sequential evaluation [1963] we discuss a number of valuation congruences and we introduce Hoare-McCarthy algebras as the structures that characterize these congruences.
We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Vaananen, and their compositional semantics due to Hodges. We show how Hodges' semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics is the logic of Bunched Implications due to Pym and O'Hearn, which combines intuitionistic and multiplicative connectives. Thi…
This paper deals with join-semilattices whose sections, i.e. principal filters, are pseudocomplemented lattices. The pseudocomplement of a\vee b in the section [b,1] is denoted by a\rightarrow b and can be considered as the connective implication in a certain kind of intuitionistic logic. Contrary to the case of Brouwerian semilattices, sections need not be distributive lattices. This essentially allows possible applications in non-classical logics. We present a connection of the semilattices mentioned in the beginning with so-called non-classical implication semilattices which can be converte…
We extend classical Propositional Logic (PL) by adding a new primitive binary connective $φ|ψ$, intended to represent the "superposition" of sentences $φ$ and $ψ$, an operation motivated by the corresponding notion of quantum mechanics, but not intended to capture all aspects of the latter as they appear in physics. To interpret the new connective, we extend the classical Boolean semantics by employing models of the form $\langle M,f\rangle$, where $M$ is an ordinary two-valued assignment for the sentences of PL and $f$ is a choice function for all pairs of classical sentences. In the new sema…
Representable implication algebras are known to be axiomatised by a finite number of equations (making the representation and finite representation problems decidable here). We show that this also holds in the context of unary (and binary) relations and present a Stone-style representation theorem. We then show that the (finite) representation decision problem is undecidable for implication semigroups, in stark contrast with implication algebras.
The tangled closure of a collection of subsets of a topological space is the largest subset in which each member of the collection is dense. This operation models a logical `tangle modality' connective, of significance in finite model theory. Here we study an abstract equational algebraic formulation of the operation which generalises the McKinsey-Tarski theory of closure algebras. We show that any dissectable tangled closure algebra, such as the algebra of subsets of any metric space without isolated points, contains copies of every finite tangled closure algebra. We then exhibit an example o…
Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication
School of Computing The Australian National University（澳大利亚国立大学计算机学院）；Chair For Theoretical Computer Science FAU Erlangen-Nuremberg（埃尔朗根-纽伦堡大学理论计算机科学教席）
