While it is well known that classical propositional logic is modelled by booleaan algebras, I have never heard of the logic modelled by generalized boolean algebras (GBA) defined by M.Stone (author of Stone's reprezentation theorem). Does anybody know anything about this logic or any attempts to find it? It would be nice to know at least what could be a good analog of implication in GBA. Since Stone axiomatized the GBAs in terms of equations, this is an equational logic, which I am not treating as proper logic  it is more algebra.But how this logic can be formulated in more regular manner by axioms in the form of implications rather than identities?

$\begingroup$ I have never seen some particular name attached to this logic; the logic of generalized Boolean algebras is (at least to me) a good enough definition. It is clear (and well known) that this logic can be axiomatized using a presentation for Johansson's minimal logic (see for instance ncatlab.org/nlab/show/minimal+logic ) plus the involutive law (i.e., the axiom $p \Leftrightarrow \neg \neg p$). $\endgroup$ – boumol Jan 30 '13 at 12:38

1$\begingroup$ @boumol: this cannot be correct because the logic of GBA cannot have a negation. There is no complement in a GBA. $\endgroup$ – Andrej Bauer Jan 30 '13 at 14:51

1$\begingroup$ @Bauer: Sorry, I answered too quick and I wrote a wrong answer. The axiom one has to add to Johansson's minimal logic is the following one $(p \lor q) \Leftrightarrow ((p\Rightarrow q)\Rightarrow q)$. This axiom is the natural generalization of the involutive law (it is obtained when one replaces $q$ with $\bot$). One place where one can find more details is in the book "Residuated lattices" books.google.es/books?id=Gy46SP7px7gC&pg=PA158 $\endgroup$ – boumol Jan 30 '13 at 15:32

1$\begingroup$ @Andrej: Yes, there is an implication, namely $yx$. You just have to realize that truth is $\bot$. And as I already mentioned, the book boumol uses as a reference defines GBAs upside down, so your $\bot$ is their $1$ (which is also $\top$ in this case, but residuated lattices are not in general assumed to have a top), and $yx$ is their $x\to y=x\setminus y=y/x$. (The monoid operation in residuated lattices is not in general commutative, hence it has two residua, which are denoted $\setminus$ and $/$ in the book. They coincide in the commutative case, and then it is written with $\to$. ... $\endgroup$ – Emil Jeřábek Jan 31 '13 at 12:26

1$\begingroup$ ... GBA are commutative, but since Prop. 3.23 gives equivalent axiomatizations of GBA over the noncommutative base theory, it needs to emply $\setminus$ and $/$.) $\endgroup$ – Emil Jeřábek Jan 31 '13 at 12:29
Propositional logic captures the partial order of a Boolean algebra, i.e., logical entailment $p_1, \ldots, p_n \vdash q$ corresponds to $p_1 \land \cdots \land p_n \leq q$. To obtain a logic for a generalised Boolean algebra we should express its laws in terms of partial order. If the laws are written as adjunctions, the rules of inference will be clearly visible.
A GBA has finite binary meets $\land$ and joins $\lor$, a least element $\bot$, and relative complements $\setminus$. There will be no surprises in the rules for $\land$, $\lor$ and $\bot$.
Conjunction is the easiest. Meet is characterised as $$r \leq p \land q \quad\text{iff}\quad \text{$r \leq p$ and $r \leq q$}.$$ Reading this from left to right gives us the elimination rules (where I write $\Gamma$ to indicate an arbitrary number of hypotheses $p_1, \ldots, p_n$) $$\frac{\Gamma \vdash p \land q}{\Gamma \vdash p} \quad\text{and}\quad \frac{\Gamma \vdash p \land q}{\Gamma \vdash q} $$ while the other direction gives the introduction rule $$\frac{\Gamma \vdash p \quad \Gamma \vdash q}{\Gamma \vdash p \land q}.$$ Notice how $\Gamma$ took the role of $r$.
A naive conversion of the characterisation of $\bot$, namely $$\bot \leq p,$$ would give us the rule $\bot \vdash p$. We actually want $\Gamma, \bot \vdash p$, but this is ok because $\bot$ is just as well characterised by $$r \land \bot \leq p.$$ This is a small point which becomes very important when we think about disjunctions. Again, a naive conversion of $$p \lor q \leq r \quad\text{iff}\quad \text{$p \leq r$ and $q \leq r$}$$ would give us something without $\Gamma$. What we really need is the characterisation $$s \land (p \lor q) \leq r \quad\text{iff}\quad \text{$s \land p \leq r$ and $s \land q \leq r$}.$$ But does this really characterize joins? Yes, thanks to the distributivity law! And so by writing $\Gamma$ instead of $s$ we get the laws $$\frac{\Gamma, p \lor q \vdash r}{\Gamma, p \vdash r} \quad\text{and}\quad \frac{\Gamma, p \lor q \vdash r}{\Gamma, q \vdash r}$$ and $$\frac{\Gamma, p \vdash r \quad \Gamma, q \vdash r}{\Gamma, p \lor q \vdash r}.$$ You may find these rules for $\lor$ a bit odd, but they are equivalent to whatever variant you are used to.
The laws for disjunction baked in just enough distributivity to make the distributivity law provable from the rules stated so far. So we need not worry about distributivity.
The interesting connective is the relative complement. If we secretly think of $p \setminus q$ as "$p$ and not $q$", then it would seem that the relative complement is to be characterised in terms of its lower bounds because it is like a conjunction. Indeed, we have $$r \leq p \setminus q \quad\text{iff}\quad \text{$r \leq p$ and $r \land q \leq \bot$}$$ which suggests the rules $$\frac{\Gamma \vdash p \quad \Gamma, q \vdash \bot}{\Gamma \vdash p \setminus q}$$ and $$\frac{\Gamma \vdash p \setminus q}{\Gamma \vdash p} \quad\text{and}\quad \frac{\Gamma \vdash p \setminus q}{\Gamma, q \vdash \bot}$$ These seem perfectly reasonable to me.
The point here is not what precise rules I derived, but how I derived them in a principled way:
 logical entailment corresponds to the partial order
 logical operations correspond to the operations
 logical rules corespond to adjunctions that characterize the operations
By the way, there is of course no truth $\top$ in this calculus. If we add it, we get the usual classical propositional calculus, just like a GBA with a top element is a Boolean algebra.

$\begingroup$ Does your calculus include any structural rules? In any case, I don’t understand the rationale why you chose the rules you did, and left out others, it all seems rather arbitrary. As far as I can see, if structural rules are included, your calculus describes the $\{\land,\lor,\bot,x\land\neg y\}$fragment of intuitionistic logic. In particular, it does not derive e.g. $p\setminus(p\setminus q)\vdash q$, which is valid in the semantics given in the first sentence. $\endgroup$ – Emil Jeřábek Jan 30 '13 at 15:36

$\begingroup$ Anyway, a sequent $\Gamma\vdash\phi$ is valid in your semantics iff $\Gamma\models\phi$ in the semantics #1 in my answer, so a complete calculus should be the respective fragment of classical logic. $\endgroup$ – Emil Jeřábek Jan 30 '13 at 15:56

1$\begingroup$ I assume that in a sequence $\Gamma \vdash p$ we have a set of propositions $\Gamma$. That's an alternative to fiddling with structural rules which I find more pleasant. My rules are direct transcripts of adjunctions, but it is quite possible I got the characterization of $p \setminus q$ wrong, and so the rules would be wrong as well. $\endgroup$ – Andrej Bauer Jan 30 '13 at 20:48

$\begingroup$ Making antecedents of sequents sets takes care of contraction and exchange, but it will not give you $p\vdash p$, cut, or weakening. The equational theory of GBAs includes more than just adjunctions, that’s the point. $\endgroup$ – Emil Jeřábek Jan 31 '13 at 12:08
The question is not quite well posed. In algebraic logic, logics are not defined by algebras, but by logical matrices: these are pairs $\langle A,D\rangle$, where $D$ is a subset of $A$, termed the set of designated values. The logic of a class $K$ of matrices is then the consequence relation $\models_K$ such that for any formula $\phi$ and a set of formulas $\Gamma$, $\Gamma\models_K\phi$ holds iff for every $\langle A,D\rangle\in K$ and every homomorphism $v$ from the algebra of formulas to $A$: if $v(\Gamma)\subseteq D$, then $v(\phi)\in D$. In the most important situations, $D$ is equationally definable in $A$: $D=\{x\in A:A\models E(x)\}$ for a set of equations $E$, which reduces matrices back to pure algebraic language. However, there may be many different choices of $E$, hence it is not sufficient to specify just a class of algebras.
For example, the matrices for classical logic are $\langle A,\{1\}\rangle$, where $A$ is a Boolean algebra. Here, $\{1\}$ is definable by $E(x)=\{x\approx1\}$.
See R. Jansana’s SEP article Propositional consequence relations and algebraic logic for a comprehensive introduction to algebraic propositional logic.
Since you didn’t specify which sets of designated values to take in generalized Boolean algebras (and the most obvious choice doesn’t work as GBA do not need to have a top), the question does not necessarily admit a unique answer. Let me give some specific examples. For the following, I assume GBA formulated in the signature $\{\land,\lor,0,\}$, where $xy$ is the relative complement of $y$ in $[0,x]$:
Let $K$ be the class of matrices $\langle A,D\rangle$, where $A$ is a GBA, and $D$ is a nonempty filter in $A$. Then the logic of $K$ is the $\{\land,\lor,0,\}$fragment of classical logic.
Let $K$ be the class of matrices $\langle A,\{0\}\rangle$, where $A$ is a GBA. Then the logic of $K$ is a notational variant of the positive fragment (i.e., $\{\lor,\land,1,\to\}$) of classical logic, where the connectives have been renamed to their duals as indicated by the order in which I have written them.
Let $K$ be the class of matrices $\langle A,\varnothing\rangle$, where $A$ is a GBA. Then the logic of $K$ is the maximal logic with no theorems, i.e., $\Gamma\models_K\phi$ iff $\Gamma\ne\varnothing$.
Let $K$ be the class of matrices $\langle A,A\rangle$, where $A$ is a GBA. Then the logic of $K$ is the inconsistent logic, i.e., $\Gamma\models_K\phi$ for every $\Gamma,\phi$.
Choice #2 is better behaved than the other three as the matrices in question are (equationally definable and) reduced, and in particular, the logic obtained is (finitely, strongly, and regularly) algebraizable, with GBA being its equivalent semantics. (See Jansana’s article for the basic definitions.) While in principle the condition of algebraizability still does not lead to a unique logic from a given class of algebras, it means that the upsidedown positive fragment of classical logic corresponds to GBA in as good a sense as the full classical logic corresponds to BA.
[EDIT 2: Let me qualify the previous sentence. It’s true that in general, more than one logic can be algebraizable wrt the same variety of algebras. However, in the case of GBA, there are not that many possible choices for $E(x)$, and it is in fact easy to check that positive classical logic is the unique logic algebraized by GBA (and the translations given below are also unique up to equivalence). Thus, the question does have a welldefined unique answer after all.]
EDIT: I will spell out explicitly what algebraizability of the positive fragment means, and how it provides a logic modelled by GBA. Consider the propositional logic $\vdash$ defined by the following Hilbert calculus: $$\begin{gather} (\phi\psi)\phi\\\\ ((\chi\phi)(\psi\phi))((\chi\psi)\phi)\\\\ \phi(\phi(\psi\phi))\\\\ 0\\\\ \phi(\phi\lor\psi)\\\\ \psi(\phi\lor\psi)\\\\ ((\phi\lor\psi)\phi)\psi\\\\ (\phi\land\psi)\phi\\\\ (\phi\land\psi)\psi\\\\ ((\chi(\phi\land\psi))(\chi\psi))(\chi\phi)\\\\ \phi,\psi\phi\vdash\psi \end{gather}$$ Let $\let\sd\vartriangle\phi\sd\psi:=(\phi\psi)\lor(\psi\phi)$, and let $\models$ denote validity in GBA. Then we have:
$\phi_1\approx\psi_1,\dots,\phi_n\approx\psi_n\models\phi\approx\psi$ iff $\phi_1\sd\psi_1,\dots,\phi_n\sd\psi_n\vdash\phi\sd\psi$
$\phi_1,\dots,\phi_n\vdash\psi$ iff $\phi_1\approx0,\dots,\phi_n\approx0\models\psi\approx0$
$\phi\approx\psi\models(\phi\sd\psi)\approx0$, $(\phi\sd\psi)\approx0\models\phi\approx\psi$
$\phi\vdash\phi\sd0$, $\phi\sd0\vdash\phi$
Thus, the mappings $\phi\approx\psi\mapsto\phi\sd\psi$ and $\phi\mapsto\phi\approx0$ provide a biinterpretation of the quasiequational theory of GBA with the logic given by $\vdash$. (This is what distinguishes this case from other choices of matrices based on GBA, such as #1,3,4 above. These choices give logics modeled in GBA’s, but they do not have matching translations of algebra into logic, hence passing from GBA to such logics is losing structure and information.)

1$\begingroup$ Actually, I did not find the question illposed. My view was that we are trying to describe a particular class of posets, namely GBAs. If at the outset we postulate that $\Gamma \vdash p$ is to be interpreted as "$p$ is an upper bound for the set $\Gamma$", then I think it is clear what the game should be: all inference rules must be valid for GBAs, and every GBA is a model for our inference rules. $\endgroup$ – Andrej Bauer Jan 30 '13 at 20:52

$\begingroup$ @Andrej: That’s exactly the problem: the postulate is unwarranted. $\endgroup$ – Emil Jeřábek Jan 31 '13 at 12:00