2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – D.W. Sep 22 '17 at 4:25
  • $\begingroup$ @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. $\endgroup$ – ryan Sep 22 '17 at 17:00
  • $\begingroup$ @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? $\endgroup$ – ryan Sep 22 '17 at 17:02
7
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ Could you elaborate on why every algebraic theory is trivially satisfiable? It's not so clear to me. Yes, intuitively I would conjecture that, but do you have a proof or at least further explanation? $\endgroup$ – ryan Sep 22 '17 at 17:05
  • 1
    $\begingroup$ 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. $\endgroup$ – Derek Elkins Sep 22 '17 at 22:44
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.