Editing Intuitionistic logic (section)

====Existential vs. universal quantification====
Firstly, when <math>x</math> is not free in the proposition <math>\varphi</math>, then
:<math>\big(\exists x\, (\phi(x)\to \varphi)\big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)</math>
When the [[domain of discourse]] is empty, then by the [[principle of explosion]], an existential statement implies anything. When the domain contains at least one term, then assuming excluded middle for <math>\forall x \, \phi(x)</math>, the inverse of the above implication becomes provably too, meaning the two sides become equivalent. This inverse direction is equivalent to the [[drinker's paradox]] (DP). Moreover, an existential and dual variant of it is given by the [[independence of premise]] principle (IP). Classically, the statement above is moreover equivalent to a more disjunctive form discussed further below. Constructively, existence claims are however generally harder to come by.

If the domain of discourse is not empty and <math>\phi</math> is moreover independent of <math>x</math>, such principles are equivalent to formulas in the propositional calculus. Here, the formula then just expresses the identity <math>(\phi\to\varphi)\to(\phi\to\varphi)</math>. This is the [[currying|curried]] form of [[modus ponens]] <math>((\phi\to\varphi)\land\phi)\to\varphi</math>, which in the special the case with <math>\varphi</math> as a false proposition results in the [[law of non-contradiction]] principle <math>\neg(\phi\land\neg\phi)</math>.

Considering a false proposition <math>\varphi</math> for the original implication results in the important
* <math>(\exists x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))</math>
In words: "If there exists an entity <math>x</math> that does ''not'' have the property <math>\phi</math>, then the following is ''refuted'': Each entity has the property <math>\phi</math>."

The quantifier formula with negations also immediately follows from the non-contradiction principle derived above, each instance of which itself already follows from the more particular <math>\neg(\neg\neg\phi\land\neg\phi)</math>. To derive a contradiction given <math>\neg\phi</math>, it suffices to establish its negation <math>\neg\neg\phi</math> (as opposed to the stronger <math>\phi</math>) and this makes proving double-negations valuable also. By the same token, the original quantifier formula in fact still holds with <math>\forall x \ \phi(x)</math> weakened to <math>\forall x \big((\phi(x)\to\varphi)\to\varphi\big)</math>. And so, in fact, a stronger theorem holds:
:<math>(\exists x \ \neg \phi(x)) \to \neg (\forall x \, \neg\neg\phi(x))</math>
In words: "If there exists an entity <math>x</math> that does ''not'' have the property <math>\phi</math>, then the following is ''refuted'': For each entity, one is ''not'' able to prove that it does ''not'' have the property <math>\phi</math>".

Secondly,
:<math>\big(\forall x \, (\phi(x)\to \varphi)\big)\,\,\leftrightarrow\,\,\big((\exists x \ \phi(x))\to\varphi\big)</math>
where similar considerations apply. Here the existential part is always a hypothesis and this is an equivalence. Considering the special case again,
* <math>(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exists x \ \phi(x))</math>
The proven conversion <math>(\chi\to\neg \phi)\leftrightarrow(\phi\to\neg \chi)</math> can be used to obtain two further implications:
:<math>(\forall x \ \phi(x)) \to \neg (\exists x \ \neg \phi(x))</math>
:<math>(\exists x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))</math>
Of course, variants of such formulas can also be derived that have the double-negations in the antecedent.
A special case of the first formula here is <math>(\forall x \, \neg\phi(x)) \to \neg (\exists x \, \neg \neg \phi(x))</math> and this is indeed stronger than the <math>\to</math>-direction of the equivalence bullet point listed above. For simplicity of the discussion here and below, the formulas are generally presented in weakened forms without all possible insertions of double-negations in the antecedents.

More general variants hold. Incorporating the predicate <math>\psi</math> and currying, the following generalization also entails the relation between implication and conjunction in the predicate calculus, discussed below.
:<math>\big(\forall x \ \phi(x)\to (\psi(x)\to\varphi)\big)\,\,\leftrightarrow\,\,\Big(\big(\exists x \ \phi(x)\land \psi(x)\big)\to\varphi\Big)</math>
If the predicate <math>\psi</math> is decidedly false for all <math>x</math>, then this equivalence is trivial. If <math>\psi</math> is decidedly true for all <math>x</math>, the schema simply reduces to the previously stated equivalence. In the language of [[Constructive_set_theory#Classes|classes]], <math>A=\{x\mid\phi(x)\}</math> and <math>B=\{x\mid\psi(x)\}</math>, the special case of this equivalence with false <math>\varphi</math> equates two characterizations of [[Disjoint sets|disjointness]] <math>A\cap B=\emptyset</math>:
:<math>\forall(x\in A).x\notin B\,\,\leftrightarrow\,\,\neg\exists(x\in A).x\in B</math>