1
$\begingroup$

The usual proof of the upward Löwenheim-Skolem theorem rests on the use of the equality symbol as a primitive symbol, interpreted in every relevant structure as true equality. My question is on how the upward Löwenheim-Skolem theorem has to be modified if equality is not a primitive symbol anymore and, say, just introduced as a binary relation with the relevant axioms expressing that it is a congruence with respect to the other non-logical symbols.

EDIT: Based on the answer of t09l, the above paragraph is best augmented by the following: Is there a meaningful reformulation in contexts without equality or does the literature just not consider upward-type theorems without something like a strong equality?


My question in particular comes from the point of view of many-valued predicate logics where the inclusion of a (crisp) equality primitive creates further expressive strength.


Also I wonder how an exclusion of equality affects the Hanf numbers of extensions of classical first-order logic, i.e. of (e.g.) infinitary first-order logic (without equality).

$\endgroup$
3
  • 1
    $\begingroup$ I don't understand the question "Is there a meaningful reformulation in contexts without equality or does the literature just not consider upward-type theorems without something like a strong equality?" No "limitative theorem applying to first-order logic with equality (e.g. upwards or downwards LS, compactness, ...) needs to be reformulated for first-order logic without equality, since the latter is a fragment of the former. Some can be optimized, but upward LS is already as strong as makes sense. So I'm not seeing what improvement you're hoping for here. $\endgroup$ Commented Feb 21, 2021 at 16:32
  • $\begingroup$ @NoahSchweber I am just trying to wrap my head around how the fragment without equality and the logic with equality are connected. In particular, my initial motivation comes from if and how a Hanf number changes from a logic with to a logic without equality. $\endgroup$
    – blub
    Commented Feb 21, 2021 at 20:05
  • $\begingroup$ See my (modified, the original version was wrong) answer below. The situation is very clear-cut for "tame" logics, and goes weird in general. $\endgroup$ Commented Feb 21, 2021 at 20:46

2 Answers 2

3
$\begingroup$

Concerning your first question, the upward Löwenheim-Skolem theorem in FOL without equality is much simpler (and less interesting). Let $M$ be an infinite model, and pick an element $m\in M$. Then you can always adjoin an arbitrary collection $\{m_i|i\in I\}$ of copies of $m$ to the model $M$ by stipulating that the $m_i$'s satisfy the same relations as $m$, and are mapped to the same elements as $m$ by any function. The resulting model $M\cup\{m_i|i\in I\}$ satisfies the same sentences (without $=$) as $M$.

$\endgroup$
4
  • $\begingroup$ That is what I thought, so my question is rather what is done in contexts without equality to make this meaningful again? Is there even such a thing or does the literature just not consider upward-type theorems without something like a strong equality? $\endgroup$
    – blub
    Commented Feb 21, 2021 at 16:18
  • $\begingroup$ Also, would this not also work in the context of finite models? In that case, would the Hanf number reduce to 1? $\endgroup$
    – blub
    Commented Feb 21, 2021 at 16:32
  • 2
    $\begingroup$ @blub No, you can whip up a sentence in first-order logic without equality which is satisfiable but has no finite models. Take e.g. a single binary relation $R$, and consider the sentence: "$R$ is transitive and for every $x$ there is some $y$ such that $xRy$ but $\neg yRx$." (That said, any sentence in which every relation symbol occurs positively is indeed satisfied in the one-element structure in the appropriate language.) $\endgroup$ Commented Feb 21, 2021 at 16:39
  • $\begingroup$ @blub Note that my parenthetical is true for sentences with equality too! $\endgroup$ Commented Feb 21, 2021 at 20:16
2
$\begingroup$

EDIT: There's a major error here which I will fix later today. (I can't delete this post since it has been accepted; if it is unaccepted, I will delete it until I have time to repair it.)

Per the comments, your main interest is in the behavior of Hanf numbers when we drop equality from a logic. (Below we suppose $\mathcal{L}$ is a "reasonable" logic since we need some meaningful syntax to even talk about equality-free fragments after all.)


For reasonably simple logics - including first-order logic and its infinitary veresions - the situation is quite nice: the Hanf number of the equality-free fragment, the downwardl Lowenheim-Skolem number of the equality-free fragment, and the downward Lowenheim-Skolem number of the original logic all coincide. The argument is as follows:

  • First, by appropriate "blowing up" we have that for every satisfiable equality-free $\mathcal{L}$-sentence $\sigma$, the class of cardinalities of models of $\sigma$ is closed upwards. So the Hanf number of the equality-free fragment of $\mathcal{L}$ is just the downward Lowenheim-Skolem number of $\mathcal{L}$'s equality-free fragment (= the smallest cardinal $\kappa$ such that every satisfiable sentence has a model of size $\le\kappa$).

  • Next, for every $\mathcal{L}$-sentence $\varphi$, let $\varphi'$ be the sentence gotten from $\varphi$ by replacing $=$ with $E$ everywhere (for $E$ a fresh binary relation symbol) and adding a clause saying that $E$ is a congruence on the structure (which we can do without equality since reflexivity is expressible as "$\forall x(xEx)$"). For every $\mathcal{M}\models\varphi'$, the quotient $\mathcal{M}/E$ is a model of $\varphi$; this shows that the downward Lowenheim-Skolem number of the equality-free fragment of $\mathcal{L}$ is exactly that of $\mathcal{L}$ itself.

Putting this all together we have, as long as $\mathcal{L}$ is "reasonably simple" (of course I haven't said what that means yet):

The Hanf number of the equality-free fragment of a logic $\mathcal{L}$ is just the downward Lowenheim-Skolem number of $\mathcal{L}$.

In particular, passing from $\mathsf{FOL}$ to the equality-free fragment of $\mathsf{FOL}$ doesn't change the Hanf number.


However, not all logics are so "smooth" when we remove equality. For example, note that the equality-free fragment of second-order logic is as expressive as the whole, since we have $x=y$ iff every equivalence relation $E$ satisfies $xEy$. So here the Hanf number doesn't change at all, even though (contra first-order logic) the "Hanfy" behavior of second-order logic is quite intricate.

So the general picture appears complicated. Certainly as long as our logic "allows blowing-up" in the appropriate sense, as first-order logic does but second-order logic does not, we get the collapse described in the previous section. But in the absence of this the situation is unclear to me.

I suspect, however, that naturally-occurring logics fall into one of the two cases "blow-uppable" or "makes equality redundant," which would explain the absence of much study in the literature.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .