I am looking for inspiration for how to design a programming language construct or DSL to represent the $\forall$ quantifier, as in:
$$\forall n\!\in\!\mathbb{N}\; \bigl( Q(n) \rightarrow P(n) \bigr)$$
My initial attempt at such a DSL would be something like this:
claim "For all natural numbers n, if Q(n) then P(n)" {
assume n
accept if Q(n) then P(n)
}
Here, the assume n I would take to mean "$\forall n$", as it would be like a function parameter, and functions can accept "any" parameter of a certain type.
A tangential question which would be interesting to comment on are: What sorts of systems like my example do there exist? Are there any standards outside of the standard $\forall$ symbol and "forall" phrase?
Mainly, I don't like "for all" as a programming construct because it is neither a noun nor a verb (it is not an object, or action, which are two things that are very easy to visualize and work with). "For" isn't even a thing of any type. "For" is a preposition, which is hard to represent in programming (TBH I don't have any idea how to properly represent it yet). And "all" is some sort of "determiner", also not a verb or noun.
The real question I would like to as is, what would be a verb or noun that can take on the meaning of $\forall$? (Or a verb or noun phrase)? That's why I tried doing assume as the replacement verb.
I want to say that this would be a replacement, but this is an actual "loop / iteration sequence", which specifies computation, and I'm not sure $\forall$ represents actual computation.
walk(n, accept(verify(Q(n), P(n))))