Constructivism versus the unicorn

Question

Consider the following statement: "All unicorns have wings". As far as I know, Aristotle would consider this statement false, because as there are no unicorns, they cannot have any properties (like "having wings").

But modernly, said statement is considered true, precisely because there are no unicorns: for the statement to be false, there would have to exist (at least one) unicorn with no wings.

My question is this: the modern interpretation seems to be based (somewhat) in the principle of the excluded middle, that is, the statement must be true because it cannot be false (i.e. assuming its falsity leads to a "contradiction"). But from a constructive point of view, would one still consider the statement as being true? (And in case I have gone astray, does it even make sense to talk about constructivism for that sort of statement?)

Thank you in advance.

Answer 1

The issue of Aristotle's beliefs is somewhat complex, and I will merely link to an article on the Stanford Encyclopedia: The Traditional Square of Opposition.

The answer to the main question depends on the sort of constructive logic we employ. In what is often called "intuitionistic" constructive logic, we have a rule called the "principle of explosion" (also called ex falso quodlibet), which says that if can prove a contradiction then, from this, we can conclude any formula that we wish. This rule is also present in classical logic, but it is not as strong constructively as it is in classical logic, because we do not have excluded middle in constructive systems. Nevertheless, some weaker varieties of constructive logic do not include the principle of explosion.

Suppose we do accept that principle. Here is how to show "All unicorns have wings" in the usual informal constructive style, assuming we know that there are no unicorns. Knowing that there are no unicorns, constructively, means that we have a method to derive a contradiction from any proof of "there is a unicorn".

We next need to think about the constructive meaning of "All unicorns have wings". To prove "All unicorns have wings" constructively means to produce a procedure which, given an object $x$ and a proof that $x$ is a unicorn, produces a proof that $x$ has wings. This is related to the BHK interpretation of constructive logic.

One such procedure is as follows:

1. First, suppose we are given a proof that some object $x$ is a unicorn. In particular, we have a proof of "there is a unicorn".
2. But we know that there are no unicorns. In other words, we know some proof of a contradiction from "there is a unicorn".
3. Therefore, we can derive a contradiction from (1) and (2).
4. Finally, we use the principle of explosion, which says in particular that from a contradiction we can conclude "$x$ has wings".

Overall, this procedure gives a proof of "$x$ has wings" from any proof of "$x$ is a unicorn". This means that we can prove "Every unicorn has wings" constructively, if we assume the principle of explosion.

---

Another approach to this is to ignore the quantifier, and work in propositional constructive logic. Here we assume $\lnot U$ (something is not a unicorn) and want to prove $W$ (that something has wings). So we want to look at the scheme $$ (\lnot U) \to (U \to W). $$ This scheme is provable in intuitionistic propositional logic (which includes the principle of explosion), but it is not provable in minimal logic, which is a weaker form of constructive logic without the principle of explosion.

The proof of the identity $(\lnot U) \to (U \to W)$ in intuitionistic logic is actually very simple. $\lnot U$ means $U \to \bot$, where $\bot$ is a symbol for a contradictory statement, and the principle of explosion says we may assume $\bot \to W$. We then obtain $U \to W$ from $U \to \bot$ and $\bot \to W$ by applying the inference rule of hypothetical syllogism, which is constructively acceptable.

Answer 2

The first part of your analysis is correct.

Modern logic symbolize :

"All unicorns have wings" i.e. "All unicorns are winged"

as :

$\forall x \ (U(x) \to W(x))$ --- (*).

Its negation is : $\exists x \ (U(x) \land \lnot W(x))$. Due to the fact that $\lnot \exists x \ U(x)$, we conclude that it is false, and thus (*) must be true (by bivalence).

But the conncetion with constructive logic does not seem to me pertinent; according to Intuitionistic Logic the equivalence :

$¬∃xϕ(x) ↔ ∀x¬ϕ(x)$

is valid.

Thus, from the fact that (presumibely) unicorns do not exists, it is costructively correct to derive that "All unicorns have wings" is (vacuously) true.

---

Note what is not constructively valid is the inference from : $¬∀x¬ϕ(x)$ to : $∃xϕ(x)$.