Logical connectives
AND ${\displaystyle A\land B}$, ${\displaystyle A\cdot B}$, ${\displaystyle AB}$, ${\displaystyle A\&B}$, ${\displaystyle A\&\&B}$ equivalent ${\displaystyle A\equiv B}$, ${\displaystyle A\Leftrightarrow B}$, ${\displaystyle A\leftrightharpoons B}$ implies ${\displaystyle A\Rightarrow B}$, ${\displaystyle A\supset B}$, ${\displaystyle A\rightarrow B}$ NAND ${\displaystyle A{\overline {\land ))B}$, ${\displaystyle A\uparrow B}$, ${\displaystyle A\mid B}$, ${\displaystyle {\overline {A\cdot B))}$ nonequivalent ${\displaystyle A\not \equiv B}$, ${\displaystyle A\not \Leftrightarrow B}$, ${\displaystyle A\nleftrightarrow B}$ NOR ${\displaystyle A{\overline {\lor ))B}$, ${\displaystyle A\downarrow B}$, ${\displaystyle {\overline {A+B))}$ NOT ${\displaystyle \neg A}$, ${\displaystyle -A}$, ${\displaystyle {\overline {A))}$, ${\displaystyle \sim A}$ OR ${\displaystyle A\lor B}$, ${\displaystyle A+B}$, ${\displaystyle A\mid B}$, ${\displaystyle A\parallel B}$ XNOR ${\displaystyle A\ {\text{XNOR))\ B}$ XOR ${\displaystyle A{\underline {\lor ))B}$, ${\displaystyle A\oplus B}$ converse ${\displaystyle A\Leftarrow B}$, ${\displaystyle A\subset B}$, ${\displaystyle A\leftarrow B}$
Related concepts
Propositional calculus Predicate logic Boolean algebra Truth table Truth function Boolean function Functional completeness Scope (logic)
Applications
Digital logic Programming languages Mathematical logic Philosophy of logic
Category
v t e

In logic and mathematics, the logical biconditional, also known as material biconditional or equivalence or biimplication or bientailment, is the logical connective used to conjoin two statements ${\displaystyle P}$ and ${\displaystyle Q}$ to form the statement "${\displaystyle P}$ if and only if ${\displaystyle Q}$" (often abbreviated as "${\displaystyle P}$ iff ${\displaystyle Q}$"^[1]), where ${\displaystyle P}$ is known as the antecedent, and ${\displaystyle Q}$ the consequent.^[2][3]

Nowadays, notations to represent equivalence include ${\displaystyle \leftrightarrow ,\Leftrightarrow ,\equiv }$.

${\displaystyle P\leftrightarrow Q}$ is logically equivalent to both ${\displaystyle (P\rightarrow Q)\land (Q\rightarrow P)}$ and ${\displaystyle (P\land Q)\lor (\neg P\land \neg Q)}$, and the XNOR (exclusive nor) Boolean operator, which means "both or neither".

Semantically, the only case where a logical biconditional is different from a material conditional is the case where the hypothesis (antecedent) is false but the conclusion (consequent) is true. In this case, the result is true for the conditional, but false for the biconditional.^[2]

In the conceptual interpretation, P = Q means "All P's are Q's and all Q's are P's". In other words, the sets P and Q coincide: they are identical. However, this does not mean that P and Q need to have the same meaning (e.g., P could be "equiangular trilateral" and Q could be "equilateral triangle"). When phrased as a sentence, the antecedent is the subject and the consequent is the predicate of a universal affirmative proposition (e.g., in the phrase "all men are mortal", "men" is the subject and "mortal" is the predicate).

In the propositional interpretation, ${\displaystyle P\leftrightarrow Q}$ means that P implies Q and Q implies P; in other words, the propositions are logically equivalent, in the sense that both are either jointly true or jointly false. Again, this does not mean that they need to have the same meaning, as P could be "the triangle ABC has two equal sides" and Q could be "the triangle ABC has two equal angles". In general, the antecedent is the premise, or the cause, and the consequent is the consequence. When an implication is translated by a hypothetical (or conditional) judgment, the antecedent is called the hypothesis (or the condition) and the consequent is called the thesis.

A common way of demonstrating a biconditional of the form ${\displaystyle P\leftrightarrow Q}$ is to demonstrate that ${\displaystyle P\rightarrow Q}$ and ${\displaystyle Q\rightarrow P}$ separately (due to its equivalence to the conjunction of the two converse conditionals^[2]). Yet another way of demonstrating the same biconditional is by demonstrating that ${\displaystyle P\rightarrow Q}$ and ${\displaystyle \neg P\rightarrow \neg Q}$.

When both members of the biconditional are propositions, it can be separated into two conditionals, of which one is called a theorem and the other its reciprocal.^{[citation needed]} Thus whenever a theorem and its reciprocal are true, we have a biconditional. A simple theorem gives rise to an implication, whose antecedent is the hypothesis and whose consequent is the thesis of the theorem.

It is often said that the hypothesis is the sufficient condition of the thesis, and that the thesis is the necessary condition of the hypothesis. That is, it is sufficient that the hypothesis be true for the thesis to be true, while it is necessary that the thesis be true if the hypothesis were true. When a theorem and its reciprocal are true, its hypothesis is said to be the necessary and sufficient condition of the thesis. That is, the hypothesis is both the cause and the consequence of the thesis at the same time.

Notations to represent equivalence used in history include:

• ${\displaystyle =}$ in George Boole in 1847.^[4] Although Boole used ${\displaystyle =}$ mainly on classes, he also considered the case that ${\displaystyle x,y}$ are propositions in ${\displaystyle x=y}$, and at the time ${\displaystyle =}$ is equivalence.
• ${\displaystyle \equiv }$ in Frege in 1879;^[5]
• ${\displaystyle \sim }$ in Bernays in 1918;^[6]
• ${\displaystyle \rightleftarrows }$ in Hilbert in 1927 (while he used ${\displaystyle \sim }$ as the main symbol in the article);^[7]
• ${\displaystyle \leftrightarrow }$ in Hilbert and Ackermann in 1928^[8] (they also introduced ${\displaystyle \rightleftarrows ,\sim }$ while they use ${\displaystyle \sim }$ as the main symbol in the whole book; ${\displaystyle \leftrightarrow }$ is adopted by many followers such as Becker in 1933^[9]);
• ${\displaystyle E}$ (prefix) in Łukasiewicz in 1929^[10] and ${\displaystyle Q}$ (prefix) in Łukasiewicz in 1951;^[11]
• ${\displaystyle \supset \subset }$ in Heyting in 1930;^[12]
• ${\displaystyle \Leftrightarrow }$ in Bourbaki in 1954;^[13]
• ${\displaystyle \subset \supset }$ in Chazal in 1996;^[14]

and so on. Somebody else also use ${\displaystyle \operatorname {EQ} }$ or ${\displaystyle \operatorname {EQV} }$ occasionally.^{[citation needed][vague][clarification needed]}

Logical equality (also known as biconditional) is an operation on two logical values, typically the values of two propositions, that produces a value of true if and only if both operands are false or both operands are true.^[2]

The following is a truth table for ${\displaystyle A\leftrightarrow B}$:

${\displaystyle A}$	${\displaystyle B}$	${\displaystyle A\leftrightarrow B}$
F	F	T
F	T	F
T	F	F
T	T	T

When more than two statements are involved, combining them with ${\displaystyle \leftrightarrow }$ might be ambiguous. For example, the statement

${\displaystyle x_{1}\leftrightarrow x_{2}\leftrightarrow x_{3}\leftrightarrow \cdots \leftrightarrow x_{n))$

may be interpreted as

${\displaystyle (((x_{1}\leftrightarrow x_{2})\leftrightarrow x_{3})\leftrightarrow \cdots )\leftrightarrow x_{n))$,

or may be interpreted as saying that all x_i are jointly true or jointly false:

${\displaystyle (x_{1}\land \cdots \land x_{n})\lor (\neg x_{1}\land \cdots \land \neg x_{n})}$

As it turns out, these two statements are only the same when zero or two arguments are involved. In fact, the following truth tables only show the same bit pattern in the line with no argument and in the lines with two arguments:

The left Venn diagram below, and the lines (AB    ) in these matrices represent the same operation.

Red areas stand for true (as in for and).

The biconditional of two statements is the negation of the exclusive or: ${\displaystyle ~A\leftrightarrow B~~\Leftrightarrow ~~\neg (A\oplus B)}$ ${\displaystyle \Leftrightarrow \neg }$

The biconditional and the exclusive or of three statements give the same result: ${\displaystyle ~A\leftrightarrow B\leftrightarrow C~~\Leftrightarrow }$ ${\displaystyle ~A\oplus B\oplus C}$ ${\displaystyle \leftrightarrow }$ ${\displaystyle ~~\Leftrightarrow ~~}$ ${\displaystyle \oplus }$ ${\displaystyle ~~\Leftrightarrow ~~}$

But ${\displaystyle ~A\leftrightarrow B\leftrightarrow C}$ may also be used as an abbreviation for ${\displaystyle (A\leftrightarrow B)\land (B\leftrightarrow C)}$ ${\displaystyle \land }$ ${\displaystyle ~~\Leftrightarrow ~~}$

Commutativity: Yes

${\displaystyle A\leftrightarrow B}$	${\displaystyle \Leftrightarrow }$	${\displaystyle B\leftrightarrow A}$
	${\displaystyle \Leftrightarrow }$

Associativity: Yes

${\displaystyle ~A}$	${\displaystyle ~~~\leftrightarrow ~~~}$	${\displaystyle (B\leftrightarrow C)}$	${\displaystyle \Leftrightarrow }$			${\displaystyle (A\leftrightarrow B)}$	${\displaystyle ~~~\leftrightarrow ~~~}$	${\displaystyle ~C}$
	${\displaystyle ~~~\leftrightarrow ~~~}$		${\displaystyle \Leftrightarrow }$		${\displaystyle \Leftrightarrow }$		${\displaystyle ~~~\leftrightarrow ~~~}$

Distributivity: Biconditional doesn't distribute over any binary function (not even itself), but logical disjunction distributes over biconditional.

Idempotency: No

${\displaystyle ~A~}$	${\displaystyle ~\leftrightarrow ~}$	${\displaystyle ~A~}$	${\displaystyle \Leftrightarrow }$	${\displaystyle ~1~}$	${\displaystyle \nLeftrightarrow }$	${\displaystyle ~A~}$
	${\displaystyle ~\leftrightarrow ~}$		${\displaystyle \Leftrightarrow }$		${\displaystyle \nLeftrightarrow }$

Monotonicity: No

${\displaystyle A\rightarrow B}$	${\displaystyle \nRightarrow }$			${\displaystyle (A\leftrightarrow C)}$	${\displaystyle \rightarrow }$	${\displaystyle (B\leftrightarrow C)}$
	${\displaystyle \nRightarrow }$		${\displaystyle \Leftrightarrow }$		${\displaystyle \rightarrow }$

Truth-preserving: Yes
When all inputs are true, the output is true.

${\displaystyle A\land B}$	${\displaystyle \Rightarrow }$	${\displaystyle A\leftrightarrow B}$
	${\displaystyle \Rightarrow }$

Falsehood-preserving: No
When all inputs are false, the output is not false.

${\displaystyle A\leftrightarrow B}$	${\displaystyle \nRightarrow }$	${\displaystyle A\lor B}$
	${\displaystyle \nRightarrow }$

Walsh spectrum: (2,0,0,2)

Nonlinearity: 0 (the function is linear)

Like all connectives in first-order logic, the biconditional has rules of inference that govern its use in formal proofs.

Biconditional introduction allows one to infer that if B follows from A and A follows from B, then A if and only if B.

For example, from the statements "if I'm breathing, then I'm alive" and "if I'm alive, then I'm breathing", it can be inferred that "I'm breathing if and only if I'm alive" or equivalently, "I'm alive if and only if I'm breathing." Or more schematically:

 B → A   
 A → B   
 ∴ A ↔ B

 B → A   
 A → B   
 ∴ B ↔ A

Biconditional elimination allows one to infer a conditional from a biconditional: if A ↔ B is true, then one may infer either A → B, or B → A.

For example, if it is true that I'm breathing if and only if I'm alive, then it's true that if I'm breathing, then I'm alive; likewise, it's true that if I'm alive, then I'm breathing. Or more schematically:

 A ↔ B  
 ∴ A → B

 A ↔ B  
 ∴ B → A

One unambiguous way of stating a biconditional in plain English is to adopt the form "b if a and a if b"—if the standard form "a if and only if b" is not used. Slightly more formally, one could also say that "b implies a and a implies b", or "a is necessary and sufficient for b". The plain English "if'" may sometimes be used as a biconditional (especially in the context of a mathematical definition^[15]). In which case, one must take into consideration the surrounding context when interpreting these words.

For example, the statement "I'll buy you a new wallet if you need one" may be interpreted as a biconditional, since the speaker doesn't intend a valid outcome to be buying the wallet whether or not the wallet is needed (as in a conditional). However, "it is cloudy if it is raining" is generally not meant as a biconditional, since it can still be cloudy even if it is not raining.

• If and only if
• Logical equivalence
• Logical equality
• XNOR gate
• Biconditional elimination
• Biconditional introduction

• Media related to Logical biconditional at Wikimedia Commons

v t e Common logical connectives
Tautology/True ${\displaystyle \top }$
Alternative denial (NAND gate) ${\displaystyle \uparrow }$ Converse implication ${\displaystyle \leftarrow }$ Implication (IMPLY gate) ${\displaystyle \rightarrow }$ Disjunction (OR gate) ${\displaystyle \lor }$
Negation (NOT gate) ${\displaystyle \neg }$ Exclusive or (XOR gate) ${\displaystyle \not \leftrightarrow }$ Biconditional (XNOR gate) ${\displaystyle \leftrightarrow }$ Statement (Digital buffer)
Joint denial (NOR gate) ${\displaystyle \downarrow }$ Nonimplication (NIMPLY gate) ${\displaystyle \nrightarrow }$ Converse nonimplication ${\displaystyle \nleftarrow }$ Conjunction (AND gate) ${\displaystyle \land }$
Contradiction/False ${\displaystyle \bot }$
Philosophy portal

v t e Mathematical logic
General	Axiom list Cardinality First-order logic Formal proof Formal semantics Foundations of mathematics Information theory Lemma Logical consequence Model Theorem Theory Type theory
Theorems (list)  and paradoxes	Gödel's completeness and incompleteness theorems Tarski's undefinability Banach–Tarski paradox Cantor's theorem, paradox and diagonal argument Compactness Halting problem Lindström's Löwenheim–Skolem Russell's paradox
Logics	Traditional Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram Propositional Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞ Predicate First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus
Set theory	Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities Types of sets Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann Maps and cardinality Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary Set theories Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive
Formal systems (list), language and syntax	Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list Example axiomatic systems (list) of arithmetic: Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry: Euclidean: Elements Hilbert's Tarski's non-Euclidean Principia Mathematica
Proof theory	Formal proof Natural deduction Logical consequence Rule of inference Sequent calculus Theorem Systems axiomatic deductive Hilbert list Complete theory Independence (from ZFC) Proof of impossibility Ordinal analysis Reverse mathematics Self-verifying theories
Model theory	Interpretation function of models Model equivalence finite saturated spectrum submodel Non-standard model of arithmetic Diagram elementary Categorical theory Model complete theory Satisfiability Semantics of logic Strength Theories of truth semantic Tarski's Kripke's T-schema Transfer principle Truth predicate Truth value Type Ultraproduct Validity
Computability theory	Church encoding Church–Turing thesis Computably enumerable Computable function Computable set Decision problem decidable undecidable P NP P versus NP problem Kolmogorov complexity Lambda calculus Primitive recursive function Recursion Recursive set Turing machine Type theory
Related	Abstract logic Algebraic logic Automated theorem proving Category theory Concrete/Abstract category Category of sets History of logic History of mathematical logic timeline Logicism Mathematical object Philosophy of mathematics Supertask
Mathematics portal

This article incorporates material from Biconditional on PlanetMath, which is licensed under the Creative Commons Attribution/Share-Alike License.