# Any Non-trivial Logic System Defined with only Equality

### Preface

We can define a system of logic by conjunctions of rules that system must follow. For example, if we wanted to define transitivity of numbers: $$F_1: \forall a,b,c. a < b \land b < c \rightarrow a < c$$ We could similarly define associativity: $$F_2: \forall d,e,f. (d + e) + f = d + (e + f)$$ Then we could define a system that follows these rules by the conjunction of all these rules: $$F : F_1 \land F_2$$ Then if we wanted to check if a statement is satisfiable, say $$S: c + 2 = b \land b = 1 \land c = 0$$, we could take the conjunction of $$S \land F$$ and then calculating their congruences classes to see if any contradictions arise.

### Question

I am curious: Can any valid non-trivial systems of logic be describe only using equalities ($$=$$) and conjunctions ($$\land$$)?

What I mean by non-trivial is that for the logical system in question, $$F$$, there exists some statements $$S$$, only using conjunction and equality for both $$F$$ and $$S$$, such that: $$SAT(S \land F) \neq SAT(S)$$ Where $$SAT$$ evaluates to $$\top$$ or $$\bot$$ if the logic is satisfiable or not.

This is to say, the conjunction of $$F$$ with $$S$$ changes the satisfiability of $$S$$. If $$S$$ were already satisfiable, $$F$$ may define a system where $$S$$ is in fact a contradiction.

### Example 1

As an example say: $$S: x = 1 \land x = 0$$ This is satisfiable by $$x = 1 = 0$$, because we haven't defined what the relation of 1 and 0 are. If we introduce a system of logic: $$F: 1 \neq 0$$ Then take their conjunction: $$1 \neq 0 \land x = 1 \land x = 0$$ This is no longer satisfiable. You can see this is mainly because we introduced an inequality from $$F$$. I am wondering if you could define such an $$F$$ only using equality and conjunction that changes the satisfiability of an $$S$$.

### Example 2

I don't think this is possible. Let's say, for instance we define a system of logic $$I$$ that defines a set of integers and the addition operation ($$+$$), conjunctions of associativity, transitivity, reflexivity, axioms, etc. Let's assume we do this only using equality and conjunctions.

Then we describe a statement: $$S: a = b \land a = b + 1$$

$$S$$ is perfectly satisfiable on it's own because they would all be in the same congruence class, and because $$+$$ is not defined we have $$a = b = b + 1$$. Then introduce $$I$$: $$I \land S$$ Clearly this should not be satisfiable. However, if we have only used equality then there is nothing to let us know that any particular congruence class will have a conflict and thus it is still satisfiable (I think). Thus resulting in a contradiction that we have not actually define the logic system of integers. From this, I would conjecture that this is not possible, as you would need some inequality ($$<, \neq, >$$) to refute or at least discover a contradiction.

• 1. Your preface doesn't look right to me. The axioms in $F$ are all universally quantified, and you haven't shown that. As a result I don't think just taking the conjunction and applying congruence closure is enough to test satisfiability. 2. Are you going to allow $F$ to contain statements with universal/existential quantification? (your first example had quantifiers that you didn't write down explicitly, which is why I ask) 3. Is it just $F$ that is restricted to only equalities and conjunctions, or also $S$ too?
– D.W.
Sep 22 '17 at 4:25
• @D.W., I see your point, I have added in the quantifiers for that first example. Yes existential and universal quantifiers are allowed. To the last point, $S$ should also be restricted to equalities due to the symmetric nature of $\land$, e.g. We could shift all the inequalities from $F$ to $S$ if we needed.
– ryan
Sep 22 '17 at 17:00
• @D.W., I also realize now that if we restrict $F$ and $S$ both to equality, then there is really no need for both of them. Rather the question could just be: Is there such an $F$ where a contradiction arises only using equality?
– ryan
Sep 22 '17 at 17:02

If all you have is equalities and uninterpreted function symbols, then you have an algebraic theory a la universal algebra. A singleton set (or a collection of them in the multi-sorted case) is always a model of an algebraic theory. That is, every algebraic theory is, at least, trivially satisfiable. So if both $S$ and $F$ are required to simply be conjunctions of equations, then $SAT(S)=SAT(F)=SAT(S\land F)=\top$.
• If all sorts are singleton sets, then all operations are the unique function into the singleton set, and all equations look like $*=*$ where $*$ stands for the single element. The hardest part of proving this formally would be defining algebraic theories and their models; the actual proof would be simple. As an overkill approach: the category of algebras of any Lawvere theory has a terminal object (in fact all limits) which is computed pointwise, so every Lawvere theory has a model whose carrier is a singleton set. Sep 22 '17 at 22:44
Every set of axioms involving only equations and conjunctions is satisfiable by the structure consisting of a single element $\star$, with all constants interpreted as $\star$ and all operations as trivial. This is so because in this structure all equations hold.