Iff:
In
logic: Term for if and only if, equivalence, biimplication.
The term 'iff' or 'if and only if' is a
logical term. In English, it is usually
rendered with four words, and one reason to prefer 'iff' over 'if and only if'
is that it is one word. It is used to convey that the two statements it
connects, as in 'p iff q' are such that the each follows from the other, in
the sense that if one has derived p and also has derived that p iff q, that
then one may infer q, and also that if one has derived q and also has derived
that p iff q, that then one may infer p.
In formal logic, 'if and only if' is often written as 'iff' or as '3'
or as '<=>' and rules that are
adopted for 'iff' are often these:
From (p iff q) it follows that (p > q).
From (p iff q) it follows that (q > p).
From (p > q) and (q > p) it follows that (p iff q).
That is: If p iff q is true, then so are p implies q and q implies p, and
conversely if both p implies q and q implies p are true then p iff q is true.
The table for p iff q is:

(p iff q) 
p q 
T 
p ~q 
F 
~p q 
F 
~p ~q 
T 
This shows that 'iff' can be wholly avoided, though usually it isn't
because it is quite handy to have a brief expression for the statement
of logical equivalence.
Note that (p iff q) as defined by the table amounts to ((p&q) V
(~p&~q)), which is to say that (p iff q) precisely if either both p and
q or both notp and notq, which again amounts to: Both are true or both
are not true, or again: both have the same truthvalue.
This definition also makes it possible to use ~(p iff q) as an
expression for exclusive disjunction, since it amounts to: Either p is
true and q is not true or p is not true and q is true.
Some theorems in Propositional Logic concerning iff:
T1. (p iff p)
T2. (p iff q) iff (q iff p)
T3. ((p iff q) & (q iff r)) > (p iff r)
T4. (p iff q) iff (~p iff ~q)
T5. (~(p iff q)) iff (p iff ~q)
T6. (p iff ~q) iff (~p iff q)
Also, it may be worth remarking that ~(p iff q) has the defining column of exclusive or that is of ((p&~q) V (~p&q)).
