2

Suppose we have the following: $\forall x \in X, P$.
Considering $x$ does not occur on the right hand side, we can also reformulate to: $X \rightarrow P$.

Let us now assume that $X$ means "it's raining" and $P$ "it's cold". We can read the second part as follows: "If it's raining, it's cold."

What is a reasonable formulation in English of the very same thing using the universally quantified version? "Forall whatever that's raining, it's cold." doesn't quite flow off the tongue.

AntlerM
  • 23
  • Be careful: in $\forall x \in X, P$, $X$ is a set, whereas in $X \rightarrow P$, $X$ is a proposition. – mrp Jun 26 '17 at 10:54
  • You may find my comments at https://math.stackexchange.com/questions/2220857/importance-of-implication-vs-its-tautology/2220954#2220954 enlightening. – hmakholm left over Monica Jun 26 '17 at 10:55

1 Answers1

1

You're right that an implication in natural language often it best interpreted as something universally quantified. Something like:

  • At all times when it is raining, it is also cold.
  • In every possible world where it is raining, it is also cold.

Your particular formalization of this intuition is problematic, though. If $X$ stands for "it's raining" (such that you can write $X\to P$), then $X$ is not a set, and therefore writing $x\in X$ is not meaningful.

If we want to make the implicit quantification explicit, then we need to parameterize both $X$ and $P$ to for example $X(t)$ and $P(t)$, meaning "at time $t$ it is raining (respectively, it is cold)". Then we can write $$(\forall t)(X(t)\to P(t)) $$

In some situations -- in particular in propositional logic as developed by introductory textbooks -- one can get away with keeping the quantification implicit, with the understanding that everything we say is assumed to hold at an arbitrary point in time.

This should not be sneered at -- technically, in proof theory, there's almost always an implicit quantification over all models of our theory. But it shouldn't lead us to think that keeping it implicit will always work for modeling natural-language statements. Depending in how complex the idea we want to express is, we may need to go to predictate logic or some kind of modal logic.

  • Your answer (along with the one you had mentioned in the comment to my question) makes perfect sense. I am mostly interested in the curry-howard part wrt. dependently typed programming, and I was wondering as to whether it makes sense at all to reformulate non-dependent functions of form $A \rightarrow B$ as dependently typed $\forall$ _ $: A, B$. What I completely missed was the fact that you (and @mrp) mentioned - I cannot really mistake propositions for sets, in spite of the C-H "propositions as types" pun. – AntlerM Jun 26 '17 at 11:08
  • @AntlerM: Hmm, yes, there ought to be a way for that to make sense, but I don't think ordinary predicate logic is what you'd get out of it. – hmakholm left over Monica Jun 26 '17 at 11:14
  • @AntlerM: It certainly makes sense to reformulate $A\to B$ as a dependent type -- the notation usually employed is to take not $\forall$ but the dependent product $\Pi, x:A. B(x)$ (or $\prod\limits_{x:A} B(x)$ in more mathematical typography), which corresponds to $A\to B$ in the case that $B$ does not contain $x$ free. It may be worthwhile to ask as a separate question whether there's any well-known logical C-H counterpart of this dependent product. – hmakholm left over Monica Jun 26 '17 at 11:21
  • I think one could argue that a dependent product (pi) is simply universal quantification (a dependent function space). Within this particular formulation, people also have an explicit notation for existential quantification (as sigma, dependent pair), and considering we could easily restate a dependent pair as a dependent function $\forall P,\ x \in A, P\ x \rightarrow \exists P$, where P is $A \rightarrow proposition$, this particular interpretation seems to fit just fine. It's just implication that in seome sense doesn't fit when thought of as a part of propositional logic - I think. – AntlerM Jun 26 '17 at 11:42