# 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. – Derek Elkins left SE 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.