# Is equational logic in universal algebra a proof system not a logic system?

As far as I know a logic system defines its own semantics (e.g. $$\models$$), but not a proof calculus/system on its language. See p261 in Ebbinghaus et al's Mathematical Logic:

In universal algebra, it seems to me that "equational logic" is defined as a proof system, so is it not a logic system in the above sense, and is a counterexample of the use of "logic" in "logic system"? See p94 in Burris et al's A Course in Universal Algebra:

and p42 of Baader et al's Term Writing and All That

Thanks.

• Birkhoff's Completeness Theorem for equational logic proves the equivalence. However, I think the main issue is applying one book's definitions to another book by different authors, which is generally ill advised. – François G. Dorais Sep 17 at 20:35
• @RodrigoFreire Thanks. (1) From Burris' book and a new source, "equational logic" doen't seem be defined the way you suggest me to think of. (2) What other definitions of logic systems have you seen, and which ones are popular? – Tim Sep 17 at 21:25
• @FrançoisG.Dorais What other definitions of logic systems have you seen, and which ones are popular? – Tim Sep 17 at 21:25
• The definition of Tarskian operator (finitary closure operator) is closer to what you want. en.wikipedia.org/wiki/… – Rodrigo Freire Sep 17 at 23:05
• There is a general definition of logic according to which a logic is a finitary closure operator. The link I gave is for the corresponding wikipedia page. The proof system of equational logic defines an example of a finitary closure operator. – Rodrigo Freire Sep 17 at 23:14

The model-theoretic definition of logic quoted in the question is given in that book to be used in Lindström's theorem. Nevertheless, equational logic is a model-theoretic logic and the induced consequence relation is equivalent to the one defined via proof theory (for this logic is complete).

Now, other questions about other general definition of logic were raised in the comments. In order to address those questions we need some preliminary remarks and notation.

• Let $$X$$ be a set (think of $$X$$ as a set of formulas). A logic on $$X$$ is a subset of $$\wp(X)\times X$$ (think of such a subset as a consequence relation). We use $$\Gamma$$ and $$\Delta$$ to denote general subsets of $$X$$ and $$\phi$$ and $$\psi$$ to denote general elements of $$X$$.

• A valuation on $$X$$ is a subset of $$X$$ (think of such a subset as the formulas which are true according to the valuation).

• We say that a valuation $$w$$ is compatible with a logic $$l$$ iff for every $$(\Gamma,\phi)\in l$$, if $$\Gamma\subseteq w$$, then $$\phi\in w$$. If $$l$$ is a logic on $$X$$, then $$l$$ defines a set of valuations $$G(l)$$, those compatible with $$l$$.

• Conversely, if $$m$$ is a set of valuations, then $$m$$ defines a logic $$L(m)$$: the set of the pairs $$(\Gamma,\phi)$$ such that for all $$w\in m$$, if $$\Gamma\subseteq w$$, then $$\phi\in w$$. $$G$$ and $$L$$ constitute a Galois connection.

For a given logic $$l$$, the following are equivalent:

1. There is a set of valuations $$m$$ such that $$l=L(m)$$
2. $$l=L(G(l))$$
3. $$l$$ is reflexive, idempotent and monotonic.

A logic $$l$$ is reflexive if for every $$\phi\in\Gamma$$, $$(\Gamma,\phi)\in l$$. A logic $$l$$ is idempotent if whenever $$\Delta, \Gamma\subseteq X$$, $$\phi\in X$$, $$(\Gamma, \phi)\in l$$ and for every $$\psi\in\Gamma$$ , $$(\Delta,\psi)\in l$$, we have $$(\Delta,\phi)\in l$$. A logic $$l$$ is monotonic if whenever $$\Gamma\subseteq\Delta$$, if $$(\Gamma,\phi)\in l$$, then $$(\Delta,\phi)\in l$$.

Now, we can consider the question:

Is the reverse true: does $$\models$$ between sets of formulas and formulas induce $$\models$$ between structures and formulas?

Yes, in some trivial sense: We can look at the structures inducing valuations compatible with $$l$$ (assuming that structures induce valuations in that case). But the difficulty is to recover your first consequence relation from the induced relation. This is not always possible:

We can look at the structures inducing valuations compatible with $$l$$, then we can look at all the consequence relations preserved by those structures. In general, we will not recover $$l$$ this way, even if $$l$$ is a finitary, reflexive, idempotent and monotonic relation. We can start with a set $$m$$ of valuations which are not induced by structures. We can take $$l=L(m)$$, and this will be finitary if $$X$$ is finite, for example.

But if we allow those general valuations, not only those induced by structures, then yes, from a tarskian logic $$l$$ we can define a canonical set of valuations $$G(l)$$ such that $$l$$ can be recovered from that set.

• I have a little trouble with the quantifiers in "idempotent": "whenever $(\Gamma, \phi) \in l$ and for every $\psi \in \Gamma$, $\Delta, \psi \in l$, we have $(\Delta, \phi) \in l$". First, $\Delta, \psi$ should be $(\Delta, \psi)$, right? Second, should it be (with extra parentheses hopefully for clarity) "whenever (($(\Gamma, \phi) \in l$ and $\Delta \subseteq X$), and, (for every $\psi \in \Gamma$, we have $(\Delta, \psi) \in l$)), we have ($(\Delta, \phi) \in l$)"? – LSpice Sep 18 at 13:05
• Right, there is a missing parentheses, thanks. Your reformulation is great. – Rodrigo Freire Sep 18 at 13:49
• @LSpice I have edited the answer. The idea is simple (the consequences of consequences of $\Delta$ are consequences of $\Delta$ directly), but it is a bit cumbersome to write it informally. Formally, $\forall\Delta\forall\Gamma\forall\phi(((\Gamma,\phi)\in l\wedge \forall\psi\in\Gamma(\Delta,\psi)\in l)\rightarrow (\Delta,\phi)\in l)$ – Rodrigo Freire Sep 18 at 14:00
• Thanks, that's what I thought! I'm teaching an intro to proof course right now, and one of the things I struggle with is how to instill in them the proper balance between, on one hand, "(almost?) nobody learns best from stacked quantifiers, so try to say it in (mathematical) English"; and, on the other hand, "there are some things, noteably subtle grouping, that non-symbolic English just doesn't handle very well." – LSpice Sep 18 at 14:24