Suppose I've got the following model
M = <D, S, i>
where D is a non-empty set {John, Jane, Jonathan, Julia}, S = {L, a, b, c, d} where L is a binary relation symbol, read as 'loves', a-d are nullary function constant symbols, and finally, i, the interpretation function.
Interpreting each member ∈ S, we get:
i(L) = {<i(a), i(b)>, <i(b), i(a)>, <i(d), i(c)>, <i(c), i(d)>} (a subset of D²)
i(a) = John
i(b) = Jane
i(c) = Jonathan
i(d) = Julia
I want to say, purely formally, that
(1) For all ordered pairs contained in L all are non-reflexive.
So the issue I am having is with transcribing this piece of English into a set-theoretic syntax that makes sense.
My initial, and only, guess, is this:
(2) ∀x∀y∀z(x ∈ L → (x = <y, z> ∧ y ≠ z))
But my worry is whether or not it is legal to range over (what the first universal quantifier above was intended to do) ordered pairs, even though, strictly speaking, they are reducible to sets... Furthermore I am wondering if the construction, (2), as a whole is a faithful transcription of what I had expressed in English, (1).
Finally, If I am right, and if we abbreviate (2) as φ, then surely, M ⊨ φ holds?
Standard notation for having a pair $(x,y)$ belong to a relation $l$ is just writing $L(x,y)$ or $(x,y)\in L$, so you should not to use the extra $x\in L $ and $x=(y,z)$ part. Thus I would instead translate to $$\forall x\forall y \big(L(x,y)\rightarrow x\neq y\big)$$ The notation $x\in L \rightarrow x=(y,z) ...$ is even wrong if we are getting picky, aince the tuple $(y,z)$ is acutally not a part of the universe, while the $\forall x$ quantifier only quantifies over the elements in the universe.
Though nitpicky formalities aside, the translation is correct, and yes $M\models \varphi$.