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?