How would you define a truth set $A$: for all $x \in B$ that satisfies $Q(x)$ where $B$ is another truth set that satisfies $P(x)$? I'm trying to formalize the natural intuition of if-then as distinct from modus ponens.
My attempts:
- Let $B = \{\,y\;|\;P(y)\,\}$ and $A = \{x\in B\;|\;Q(x)\,\}$
- Let $A = \{\,x\in \{\;y\;|\;P(y)\,\}\;|\;Q(x)\,\}$
Are (1) and (2) correct with respect to the definition I gave above? Are (1) and (2) equivalent? Is there an even better way to reduce (2)? Did I successfully entail the notion that in order for Q to even be considered that P must first be true? Could you remark on the differences between this form of a conditional and that of modus ponens and quantified conditionals, in general? Any help is greatly appreciated.
You are using set-theoretic notation, which is usually interpreted according to standard set theory. In that case, no you did not "entail the notion that in order for Q to even be considered that P must first be true".
Both the sets you defined are exactly the same sets, by the extensionality axiom. Thus there is no difference between them and $\{ x : P(x) \land Q(x) \}$.
In standard set theory (which is used in almost all of mathematics), you can only define properties using first-order formulae, and the intended domain of the set theory is the 'universe' of all sets, so if you managed to define a property $Q$ in the first place, $Q(x)$ would be well-defined for any set $x$, and there is no need to first require $P(x)$ to hold before testing $Q(x)$.
But there are alternative formal systems that are different from the standard set theory. Most of them are type theories of some sort, and most type theories syntactically require properties to be about previously typed objects. So you could construct a type that accepts only the objects that are firstly of type $B$ and then secondly satisfying $Q$. Depending on the specific system, it might be able to express the notion that $Q(x)$ is only required to be syntactically valid in the case when $x$ is of type $B$. You would want to read up about dependent type theories.
Now why should we even consider type theories, since almost all mathematics can be translated into the standard set theory (ZFC or extensions of it)? It is simply because a lot of mathematics is actually done informally and mathematicians have an innate type-theoretic intuition. If you are not familiar with set theory, you would never consider "$\mathbb{N} \in 3$" as a meaningful question. Similarly, you would never write the function notation "$f(x)$" unless $f$ is in the current context already proven to be a function and $x$ is already proven to be in its domain. These intuitive notions are completely captured by type-theoretic syntax rules, and not by standard set theory.
Some type theories are interpretable in ZFC, meaning that there is a way to translate statements in such a theory $T$ into statements in ZFC such that any statement that can be proven in $T$ can also be proven in ZFC. This property would imply that if we believe the consistency of ZFC (it cannot be proven if it is true), then we are justified in believing the consistency of $T$, and so if $T$ 'makes more intuitive sense' then we can go ahead in using $T$ for all our everyday mathematical work. This is exactly what most mathematicians (who are not set theorists or logicians) do in practice. I read a published article describing in significant detail the usual type theory that most mathematicians unconsciously work in, but I can't recall where it is at the moment.