# How to deal with second argument of implication being defined if only if the first argument is true?

Let $$S$$ be a set. Let $$f$$ be a function with $$\operatorname{dom}(f)=S$$. Let $$P$$ be a one-place property. Is the following statement well formed?

$$∀x \, x∈S → P(f(x))$$

$$\text{For any x∈S}, P(f(x)) \text{ holds}$$

Many theorems are of similar structure to these statements. But I see a problem here: logical implication is defined even when both arguments are false, but in this particular case if the first argument is false, the second argument is undefined.

Formally, are these 2 statements different or the same? I.e., does the latter statement, if we were to write it down formally, use logical implication or something else? How do mathematicians (I guess we're talking about logicians and maybe set theorists) solve this problem?

Update: The problem dissipates if I rewrite the statement more formally: $$\forall x \, x \in S \rightarrow \exists! y \exists q \, \left( q=(x, y) \land q \in f \land P(y) \right)$$

• If any of you want to edit tags, feel free to do so. I am not sure if "first-order-logic" tag has place here - I don't know exactly what first order logic is. But I think "predicate-calculus" is not suitable here because it doesn't deal with sets in ZF set theory. – CrabMan May 2 at 19:10
• The first statement is precisely how we usually write the second one more formally (this is called a bounded quantifier.) Your issue is really about what $f(x)$ means. If $f$ isn’t total, how can we in good conscience write $f(x)$ where $x$ is a variable that ranges over the entire domain? If $f$ is a formal function symbol the usual approach is to simply not allow partial functions and use default values when necessary. More often though, $f$ is a set and $P(f(x))$ is an abbreviation for a more elaborate formula in the language of set theory that can be meticulously arranged to make sense. – spaceisdarkgreen May 2 at 19:28
• @spaceisdarkgreen f is a total function on $S$. I see a problem when $x \notin S$. Can you clarify how can construct that elaborate formula? This question arose precisely while I was studying ZF set theory. – CrabMan May 2 at 19:32
• Hww. Actually, I don't know what bounded quantifier is. Perhaps that's my problem. In my post by $\forall$ I meant just "for any x" quantifier. – CrabMan May 2 at 19:35
• A bounded quantifier is $\forall x\in S$ as opposed to an unbounded quantifier $\forall x$ which ranges over the entire universe. In set theory it’s generally just an abbreviation for your first expression. By “total” I meant having the entire universe as the domain. So a function whose domain is $S$ doesn’t count. I may have time to elaborate later, but in set theory, functions are treated as sets of ordered pairs, and any kind of function notation is just abbreviation. In those terms, you can try to piece together a formula that means $f(x)=y$ or some other predicate involving $f(x).$ – spaceisdarkgreen May 2 at 20:04