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).
Best Answer
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$.