By logic without equality I mean those kind of logics where equality is treated as a binary relation satisfying some axioms, as opposed to a logics where equality is a logical symbol satisfying some inference rules.

In my understanding there should be no difference at the syntactic level between logics with or without equality since the syntax should not be able to distinguish a logic-primitive predicate or any other predicate (but in case I am wrong please correct me).

So I am wondering what are the differences at a semantic level between these kind of logics. In particular I am wondering whether all the definitions and theorems of classical model theory can be transported verbatim to the without-equality logics.

If it is possible I would also appreciate references that treat the subject.

Addendum: After Andrej Bauer's answer I realize it would be better to add some specification. I am interested basically in logical theories where every theory comes equipped with an axiom-schema for substitution, that is a family of axioms of the form $$\forall x,y. (x=y) \land \varphi(x) \rightarrow \varphi(y)$$ where $\varphi$ is a formula of the language.

In short I am curious to know what changes we get if we change the semantics of the symbol of equality.

Addendum 2: also it seems from the answer provided so far that the model theory should remain unchanged but it does not look like it to me.

First of all while quotienting for the equivalence relation should provide a (elementary?) equivalent model it does not (necessarily) preserves the homomorphisms: consider a set with an equivalence relation that identifies all elements, the corresponding quotient structure should be the terminal model (in the sense of category theory) but the first model clearly does not have to be a terminal object in the category.

Also it seems to me that one could lose the characterisation of homomorphisms as mapping that preserve atomic formulas, since, if we drop the requirement of interpreting the equality symbol as the identity relation, then we could have mappings that preserve atomic formulas but for some operations symbols do not respect the external equality: i.e. we could have a mapping $f \colon A \to B$ and an operation symbol $o$ such that $$B \models f(o^A(a)) = o^B(f(a))$$ but $f(o^A(a))$ and $o^B(f(a))$ are not identical.

It seems rather difficult to find references that deal with this kind of phenomena, that is why I would really appreciate if someone could provide some pointers.

Thanks in advance.


Yes, logic with equality treats equality in a special way because it relates equality to substitution. That is, we have the substutition rule (to be read as a schema, of course) $$\frac{\vdash \phi[s/x] \qquad \vdash s = t}{\vdash \phi[t/x]}$$ which expresses the fact that $\phi[s/x]$ entails $\phi[t/x]$ when $s = t$, for any formula $\phi$. In other words, we may always replace a term with an equal one. This together with reflexivity is enough to get all of the rules of equality. For instance, to get symmetry, take $\phi$ to be the formula $x = s$.

If equality is not treated in a special way, then we may still express the fact that it is an equivalence relation, but the substution rule is not directly expressible. We might try to simulate the substitution rule by further axioms stating that all function symbols and relations respect equality, but at that point we might as well admit we've just axiomatized the substitution rule by hand.

The difference carries over to model theory. Suppose we have a model $M$ in which equality is interpreted by some relation $E \subseteq M \times M$. It follows that $E$ is an equivalence relation. In order for $M$ to validate the substitution rule, the interpretations of all other functions and relation symbols must be congruences with respect to $E$. Consequently, we may quotient the model by $E$ to obtain another model $M/E$ in which equality is equality. The upshot of this is that nothing much is gained by the extra generality of taking equality to be a general relation $E$.

  • 3
    $\begingroup$ Well, that's what I had in mind too when I wrote down the rule. It's a scheme. My point is that equality is axiomatized in terms of its relationship with substitution, and this is unlike axomatizations of other relations, therefore equality is special. $\endgroup$ – Andrej Bauer Dec 1 '18 at 18:38
  • 1
    $\begingroup$ That's true but still using the axiom-scheme one should obtain the same proof theory while changing the meaning of the equality should provide a different semantics. I have made some changes to the question to try to make clearer what kind of issues I am trying to address. $\endgroup$ – Giorgio Mossa Dec 1 '18 at 19:54
  • 2
    $\begingroup$ It's not clear to me what you're after (even, or perhaps because of the addendum). Sure, there's more than one way to axiomatize equality. Perhaps you're asking for a more caregory-theoretic approach to model theory. For instance, you seem to talk about the difference between models in the category of sets and functions vs. the category of equivalence relations and equivariant maps between them. These two categories are equivalent under the axiom of choice, so their categories of models will be equivalent, too. $\endgroup$ – Andrej Bauer Dec 1 '18 at 20:00
  • 3
    $\begingroup$ It's a little more subtle than that: those two categories are only equivalent after you quotient the morphisms in the latter one by pointwise equivalence. $\endgroup$ – Mike Shulman Dec 3 '18 at 7:52
  • 1
    $\begingroup$ @AndrejBauer I figured you probably meant to do that, but I thought it was worth mentioning explicitly in this context. In particular, the OP's two examples in "Addendum 2" seem to be based on working in the category of equivalence relations without quotienting it. $\endgroup$ – Mike Shulman Dec 3 '18 at 20:27

The short answer is not much.

If equality $=$ is not included in logic, but is a relation satisfying some axioms, then its interpretation in a structure $\mathcal A$ can be any relation $E$ satisfying these axioms. Typically these axioms would force $E$ to be an equivalence relations such that all other relations are $E$-invariant. Then you can quotient the universe under $E$ and obtain a structure $\mathcal A/E$ were $=$ is interpreted by actual equality.

Edit: Let me elaborate why $\mathcal A$ and $\mathcal A/E$ are essentially the same. Each structure $\mathcal A$ is now characterised by $\mathcal A/E$ together with a function that tells you how many copies of each element of $\mathcal A/E$ you have (i.e. the size of the equivalence class). Since there is no way to control this function whatsoever, it is essentially noise and is best ignored. (Of course, you can choose not to ignore it, but it is hard to see what is the gain.) So you would want to identify functions $f_1, f_2 : \mathcal A_1 \to \mathcal A_2$ if $\mathcal A_2 \models f_1(x) = f_2(x)$ for every $x \in \mathcal A_1$. The effect of this is that you look at functions $\mathcal A_1/E_1 \to \mathcal A_2/E_2$.

  • 2
    $\begingroup$ Why the downvote? This answer is correct. $\endgroup$ – Alex Kruckman Dec 1 '18 at 19:48

When dealing with model theory without equality, I think it is better not to deal with isomorphisms (functions) but with isomorphism relations. For example, in order to recover Fraïssé's theorem, one may consider partial isomorphism relations because one cannot infer the existence of a partial isomorphism from the satisfaction of the same atomic formulas when equality is absent.

What is gained in doing this? I think that something is gained, and it is not extra generality. I will try to make a point:

1) A natural question in foundational investigations is: what are the minimal resources that a classical logical system must have in order to be a possible vehicle for classical mathematical reasoning? One can, with first-order logic without equality, axiomatize set theory with only one primitive binary relation (membership). So, equality is certainly not part of the minimum. Is this (first-order logic with membership but without equality) the minimal vehicle? For one interpretation of what is meant by classical mathematical reasoning, one can prove, using some model theory without equality, that it is not.

2) For pedagogical purposes, results in logic without equality are usually simpler to prove, one can get more focused on the essential ideas, not being distracted by some technical details. For example, the construction of the canonical structure is simpler, either from Hintikka sets or from maximal Henkin sets. Also, proof theory without equality is simpler. For example, one need not talk about quasi-tautologies in Herbrand's theorem without equality. The proof-theoretic characterizations of logical theorems are clearer in this setting. It is more general and simpler.

The following paper of mine deals with some model-theoretic stuff:



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.