Editing Intuitionistic logic (section)

===Non-interdefinability of operators===
Already minimal logic easily proves the following theorems, relating [[logical conjunction|conjunction]] resp. [[logical disjunction|disjunction]] to the [[material conditional|implication]] using [[logical negation|negation]]. Firstly,
* <math>(\phi \lor \psi) \to \neg (\neg \phi \land \neg \psi)</math>
In words: "<math>\phi</math> and <math>\psi</math> each imply that it is not the case that both <math>\phi</math> and <math>\psi</math> fail to hold together."

And here the logically negative conclusion <math>\neg (\neg \phi \land \neg \psi)</math> is in fact equivalent to <math>\neg \phi \to \neg \neg \psi</math>. The alternative implied theorem, <math>(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)</math>, represents a weakened variant of the disjunctive syllogism.
Secondly,
* <math>(\phi \land \psi) \to \neg (\neg \phi \lor \neg \psi)</math>
In words: "<math>\phi</math> and <math>\psi</math> both together imply that neither <math>\phi</math> nor <math>\psi</math> fail to hold."

And here the logically negative conclusion <math>\neg (\neg \phi \lor \neg \psi)</math> is in fact equivalent to <math>\neg(\phi \to \neg \psi)</math>. A variant of the converse of the implied theorem here does also hold, namely
* <math>(\phi \to \psi) \to \neg (\phi \land \neg\psi)</math>
In words: "<math>\phi</math> implying <math>\psi</math> implies that it is not the case that <math>\phi</math> holds while <math>\psi</math> fails to hold."

And indeed, stronger variants of all of these still do hold - for example the antecedents may be double-negated, as noted, or all <math>\psi</math> may be replaced by <math>\neg\neg\psi</math> on the antecedent sides, as will be discussed.

However, neither of these five implications above can be reversed without immediately implying excluded middle (consider <math>\neg \psi</math> for <math>\phi</math>) resp. double-negation elimination (consider true <math>\phi</math>). Hence, the left hand sides do not constitute a possible definition of the right hand sides.

In contrast, in classical propositional logic it is possible to take one of those three connectives plus negation as primitive and define the other two in terms of it, in this way. Such is done, for example, in [[Jan Łukasiewicz|Łukasiewicz]]'s [[propositional logic#Łukasiewicz's_P2|three axioms of propositional logic]]. 
It is even possible to define all in terms of a [[sole sufficient operator]] such as the [[Peirce arrow]] (NOR) or [[Sheffer stroke]] (NAND). Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation.
These are fundamentally consequences of the [[law of bivalence]], which makes all such connectives merely [[Boolean function]]s.
The law of bivalence is not required to hold in intuitionistic logic. As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary. So most of the classical identities between connectives and quantifiers are only theorems of intuitionistic logic in one direction. Some of the theorems go in both directions, i.e. are equivalences, as subsequently discussed.

====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>

====Disjunction vs. conjunction====
There are finite variations of the quantifier formulas, with just two propositions:
* <math>(\neg \phi \lor \neg \psi) \to \neg (\phi \land \psi)</math>
* <math>(\neg \phi \land \neg \psi) \leftrightarrow \neg (\phi \lor \psi)</math>
The first principle cannot be reversed: Considering <math>\neg \psi</math> for <math>\phi</math> would imply the weak excluded middle, i.e. the statement <math>\neg \psi \lor \neg \neg \psi</math>. But intuitionistic logic alone does not even prove <math>\neg \psi \lor \neg \neg \psi\lor (\neg \neg \psi\to \psi)</math>. So in particular, there is no distributivity principle for negations deriving the claim <math>\neg \phi \lor \neg \psi</math> from <math>\neg(\phi \land \psi)</math>. For an informal example of the constructive reading, consider the following: From conclusive evidence it not to be the case that ''both'' Alice and Bob showed up to their date, one cannot derive conclusive evidence, ''tied to either'' of the two persons, that this person did not show up. Negated propositions are comparably weak, in that the classically valid [[De_Morgan%27s_laws#In_intuitionistic_logic|De Morgan's law]], granting a disjunction from a single negative hypothetical, does not automatically hold constructively. The intuitionistic propositional calculus and some of its extensions exhibit the [[disjunction property]] instead, implying one of the disjuncts of any disjunction individually would have to be derivable as well.

The converse variants of those two, and the equivalent variants with double-negated antecedents, had already been mentioned above. Implications towards the negation of a conjunction can often be proven directly from the non-contradiction principle. In this way one may also obtain the mixed form of the implications, e.g. <math>(\neg \phi \lor \psi) \to \neg (\phi \land \neg \psi)</math>. Concatenating the theorems, we also find
* <math>(\neg \neg \phi \lor \neg \neg \psi) \to \neg \neg (\phi \lor \psi)</math>
The reverse cannot be provable, as it would prove weak excluded middle.

In predicate logic, the constant domain principle is not valid: <math>\forall x \big(\varphi \lor \psi(x)\big)</math> does not imply the stronger <math>\varphi\lor \forall x\,\psi(x)</math>. The [[Distributive_property#Propositional_logic|distributive properties]] does however hold for any finite number of propositions. For a variant of the De Morgan law concerning two existentially closed [[Decidability (logic)|decidable]] predicates, see [[Limited principle of omniscience|LLPO]].

====Conjunction vs. implication====
From the general equivalence also follows [[Import–export (logic)|import-export]], expressing incompatibility of two predicates using two different connectives:
* <math>(\phi \to \neg \psi) \leftrightarrow \neg (\phi \land \psi)</math>
Due to the symmetry of the conjunction connective, this again implies the already established <math>(\phi \to \neg \psi) \leftrightarrow (\psi \to \neg \phi) </math>.
The equivalence formula for the negated conjunction may be understood as a special case of currying and uncurrying. Many more considerations regarding double-negations again apply. And both non-reversible theorems relating conjunction and implication mentioned in the introduction to non-interdefinability above follow from this equivalence. One is a simply proven variant of a converse, while <math>(\phi \to \psi) \to \neg (\phi \land \neg\psi)</math> holds simply because <math>\phi \to \psi</math> is stronger than <math>\phi \to \neg\neg\psi</math>.

Now when using the principle in the next section, the following variant of the latter, with more negations on the left, also holds:
* <math>\neg (\phi \to \psi) \leftrightarrow (\neg \neg \phi \land \neg \psi) </math>
A consequence is that
* <math>\neg \neg (\phi \land \psi) \leftrightarrow (\neg \neg \phi \land \neg \neg \psi) </math>

====Disjunction vs. implication====
Already minimal logic proves excluded middle equivalent to [[consequentia mirabilis]], an instance of [[Peirce's law]]. 
Now akin to modus ponens, clearly <math>(\phi \lor \psi)\to((\phi\to\psi)\to \psi)</math> already in minimal logic, which is a theorem that does not even involve negations. In classical logic, this implication is in fact an equivalence. With taking <math>\phi</math> to be of the form <math>\psi\to\varphi</math>, excluded middle together with explosion is seen to entail Peirce's law.

In intuitionistic logic, one obtains variants of the stated theorem involving <math>\bot</math>, as follows. Firstly, note that two different formulas for <math>\neg (\phi \land \psi)</math> mentioned above can be used to imply <math>(\neg \phi \vee \neg \psi) \to (\phi \to \neg \psi)</math>. It also followed from direct case-analysis, as do variants where the negations are moved around, such as the theorems <math>(\neg \phi \lor \psi) \to (\phi \to \neg \neg \psi)</math> or <math>(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)</math>, the latter being mentioned in the introduction to non-interdefinability. These are forms of the disjunctive [[syllogism]] involving negated propositions <math>\neg\psi</math>. Strengthened forms still holds in intuitionistic logic, say
* <math>(\neg \phi \lor \psi) \to (\phi \to \psi)</math>
The implication cannot generally be reversed, as that would immediately imply excluded middle. So, intuitionistically, "Either <math>P</math> or <math>Q</math>" is generally also a stronger propositional formula than "If not <math>P</math>, then <math>Q</math>", whereas in classical logic these are interchangeable.

Non-contradiction and explosion together actually also prove the stronger variant <math>(\neg \phi \lor \psi) \to (\neg\neg\phi \to \psi)</math>. And this shows how excluded middle for <math>\psi</math> implies double-negation elimination for it. For a fixed <math>\psi</math>, this implication also cannot generally be reversed. However, as <math>\neg\neg(\psi\lor\neg \psi)</math> is always constructively valid, it follows that assuming double-negation elimination for all such disjunctions implies classical logic also.

Of course the formulas established here may be combined to obtain yet more variations. For example, the disjunctive syllogism as presented generalizes to
:<math>\Big(\big(\exists x \ \neg\phi(x)\big)\lor\varphi\Big)\,\,\to\,\,\Big(\big(\forall x \ \phi(x)\big)\to\varphi\Big)</math>
If some term exists at all, the antecedent here even implies <math>\exists x \big(\phi(x)\to\varphi\big)</math>, which in turn itself also implies the conclusion here (this is again the very first formula mentioned in this section).

The bulk of the discussion in these sections applies just as well to just minimal logic. But as for the disjunctive syllogism with general <math>\psi</math> and in its form as a single proposition, minimal logic can at most prove <math>(\neg\phi \lor \psi) \to (\neg\neg \phi \to \psi')</math> where <math>\psi'</math> denotes <math>\neg\neg\psi\land(\psi\lor\neg\psi)</math>. The conclusion here can only be simplified to <math>\psi</math> using explosion.

====Equivalences====
The above lists also contain equivalences.
The equivalence involving a conjunction and a disjunction stems from <math>(P\lor Q)\to R</math> actually being stronger than <math>P\to R</math>. Both sides of the equivalence can be understood as conjunctions of independent implications. Above, absurdity <math>\bot</math> is used for <math>R</math>. In functional interpretations, it corresponds to [[Conditional (computer programming)|if-clause]] constructions.
So e.g. "Not (<math>P</math> or <math>Q</math>)" is equivalent to "Not <math>P</math>, and also not <math>Q</math>".

An equivalence itself is generally defined as, and then equivalent to, a conjunction (<math>\land</math>) of implications (<math>\to</math>), as follows:
* <math>(\phi\leftrightarrow \psi) \leftrightarrow \big((\phi \to \psi)\land(\psi\to\phi)\big)</math>
With it, such connectives become in turn definable from it:
* <math>(\phi\to\psi) \leftrightarrow ((\phi\lor\psi) \leftrightarrow \psi)</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\land\psi) \leftrightarrow \phi)</math>
* <math>(\phi\land\psi) \leftrightarrow ((\phi\to\psi)\leftrightarrow\phi)</math>
* <math>(\phi\land\psi) \leftrightarrow (((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)</math>

In turn, <math>\{\lor, \leftrightarrow, \bot\}</math> and <math>\{\lor, \leftrightarrow, \neg\}</math> are complete bases of intuitionistic connectives, for example.

====Functionally complete connectives====
As shown by [[Alexander Kuznetsov (mathematician)|Alexander V. Kuznetsov]], either of the following connectives – the first one ternary, the second one quinary – is by itself [[functionally complete]]: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the [[Sheffer stroke]] from classical propositional logic:{{sfn|Chagrov|Zakharyaschev|1997|pages=58-59}}
* <math>\big((P\lor Q)\land\neg R\big)\lor\big(\neg P\land(Q\leftrightarrow R)\big)</math>
* <math>P\to\big(Q\land\neg R\land(S\lor T)\big)</math>