Using implication to argue for all members of a set, something is true

Question

I am trying to express some statements in a formal language that allows universal quantification over domains, but not over sets. I was wondering how to express that something is true for all elements of a given set.

Let us assume $D$ is a domain and we can write $\forall x:D, A(x)$ to mean that "Forall $x$ in the domain $D$, $A(x)$ is true".

Now, let us assume we have a non-empty set $S$ that contains elements of the domain $D$ and the $\in$ relation is a binary predicate over the domain $D_S$ of all such sets such that $\in : D_S \times D \rightarrow \{true,false\}$.

My goal is to be able to express the statement "For every member of the set $S$, $A(x)$ is true".

However, the language I am using does not allow me to write something like $\forall x \in S: A(x)$.

In this case, would it be correct to write $\forall x:D, ((x \in S) \implies A(x))$?

I realize that if $S$ was allowed to be empty, the statement would be vacuously true, but that is not a concern for the universe I am trying to reason about. My main concern is if $\forall x:D, ((x \in S) \implies A(x))$ means "For every member of the set $S$, $A(x)$ is true".

Answer 1

If $\in$ is part of the formal language, then yes, you can write it this way.
Technically, you would then have to explicitly specify the interpretation for this relation symbol as well as write "$\in(x, S)$" rather than "$x \in S$". However, in practice people will understand (perhaps even better) what you mean if you just write $x \in S$ without further comment.

That being said, unless you are doing set theory itself, there is no real need for the additional complication of having a $\in$ relation symbol: You could instead consider defining the set as a predicate, given that the interpretation of a one-place predicate is a set. That is, instead of writing $x \in S$ where $S$ denotes, say, the set of even numbers, you could also just define $S$ as a one-place predicate $S(x)$ with the interpretation $\mathcal{I}(S) = \{x: x \text{ is even}\}$. That way you can convey the same meaning using just the default inventory of FOL syntax.

Answer 2

Assume $x\in S$. If you can then prove $A(x)$, and you have discharged any and all other subsequent assumptions about $x$ in your proof, then you can generalize to obtain:

$~~~~~~\forall x: D, [x \in S \implies A(x)]$

if I understand your notation correctly. You don't really need '$D,$' however. You could write:

$~~~~~~\forall x: [x \in S \implies A(x)]$

or

$~~~~~~\forall x\in S: A(x)$