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 &lt; b \land b &lt; c \rightarrow a &lt; 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 ($&lt;, \neq, &gt;$) to refute or at least discover a contradiction.
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$.