Intuitionistic logic
Equivalences

The above lists also contain equivalences.The equivalence involving a conjunction and a disjunction stems from (P ∨ Q) → R {\displaystyle (P\lor Q)\to R} actually being stronger than P → R {\displaystyle P\to R}. Both sides of the equivalence can be understood as conjunctions of independent implications. Above, absurdity ⊥ {\displaystyle \bot } is used for R {\displaystyle R}. In functional interpretations, it corresponds to if-clause constructions.So e.g. "Not (P {\displaystyle P} or Q {\displaystyle Q})" is equivalent to "Not P {\displaystyle P}, and also not Q {\displaystyle Q} ".

An equivalence itself is generally defined as, and then equivalent to, a conjunction (∧ {\displaystyle \land }) of implications (→ {\displaystyle \to }), as follows:

With it, such connectives become in turn definable from it:

In turn, { ∨, ↔, ⊥ } {\displaystyle \{\lor,\leftrightarrow,\bot \}} and { ∧, ↔, ¬ } {\displaystyle \{\land,\leftrightarrow,\neg \}} are complete bases of intuitionistic connectives, for example.
startend:quotation, change_case:english_capital