0
$\begingroup$

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".

$\endgroup$

2 Answers 2

0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thank you for your answer. The machine-checkable language I am using does not have the $\in$ operator, so I have to explicitly define the $\in$ operator. And it will be a prefix operator like you stated. The language does not support set theory implicity, so I will also be encoding the set theory axioms I need to reason further. My main concern was if the expression $\forall x:D, ((x \in S) \implies A(x))$ means what I want to express. I am quite sure that it does, but I wanted to double-check. $\endgroup$ Commented Nov 19, 2020 at 17:40
  • $\begingroup$ Oh, I misunderstood then. Yes, that's exactly what it means. $\endgroup$ Commented Nov 19, 2020 at 17:59
0
$\begingroup$

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)$

$\endgroup$
5
  • $\begingroup$ Thank you for your answer. My main concern was if it means what I want to express, i.e., "Forall $x \in S$, $A(x)$ is true/holds". The notation $\forall x \in S: A(x)$ is exactly what I want to say, but the formal language I am using does not allow that. $\endgroup$ Commented Nov 19, 2020 at 16:35
  • $\begingroup$ Looking at your other comments, perhaps you should let $S$ be a unary predict instead of a set, i.e. you could write $\forall x: D, (S(x) \implies A(x))$ (using your notation). $\endgroup$ Commented Nov 19, 2020 at 19:41
  • $\begingroup$ Well, eventually, I will also have to reason over the domain $D_S$ of non-empty sets whose elements are of the domain $D$. So using a predicate is probably not going to help. $\endgroup$ Commented Nov 19, 2020 at 20:29
  • $\begingroup$ You can indicate that $S$ is a non-empty of subdomain of $D$ by stating $\forall x: (S(x) \implies D(x)) \land \exists x: S(x)$. BTW what software are you using as a proof checker? Is it for a course? $\endgroup$ Commented Nov 19, 2020 at 21:00
  • $\begingroup$ I am using Athena (proofcentral.org/athena). It is for some research ideas I am playing around with. $\endgroup$ Commented Nov 19, 2020 at 21:24

You must log in to answer this question.

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