
Logical Laws

Logical laws are expressions of the
firstorder logic,
which hold for any choice of propositions, predicates, or logical formulas
replacing variables in the expressions.
Logical expressions are constructed using the following
connectives
and quantifiers:
&  and
∨  or
⊃  implication
∼  equivalence
¬  negation


∀  universal quantifier
∃  existential quantifier

Most of these laws are logical equivalences.
Two logical expressions are said to be equivalent if each of them implies the other.
Equivalences are particularly important in logic because of the
replacement theorem.
Apparently, the laws not cointaining quantifiers are expressions of the
propositional calculus as well.
Most of these laws hold in both
classical logic and
intuitionistic logic.
Still, some hold in classical logic only.
As far as formal proofs of these logical laws are concerned,
some examples of such proofs in sequent calculus can be found
here.
The laws for which these Gentzenstyle proofs are available are
marked with links to the proofs.
S.C. Kleene compiled an extensive collection of logical laws.
The collection of logical laws presented here is based on the Kleene's collection
and contains a few additions.
The laws holding in classical logic only are marked as such.
Most of these classicalonly laws are equivalences, and one of the respective implications
still holds both classically and intuitionistically.
In particular, these implications are listed here as well.
*** Note that the browser has to support numeric character references in order for
logical symbols on this page to show correctly.
Some older browsers may not have this feature.
***
The following laws hold for any formulas A, B, and C.
Implication
( A ⊃ B ) ⊃ ( ( A ⊃ ( B ⊃ C ) ) ⊃ ( A ⊃ C ) ) )

( A ⊃ C ) ⊃ ( ( B ⊃ C ) ⊃ ( A ∨ B ⊃ C ) )

( A ⊃ B ) ⊃ ( ( A ⊃ ¬B ) ⊃ ¬A )



proof

( A ⊃ B ) ⊃ ( ( B ⊃ A ) ⊃ ( A ∼ B ) )

( A ⊃ B ) ⊃ ( ( B ⊃ C ) ⊃ ( A ⊃ C ) )

( A ⊃ B ) ⊃ ( ( C ⊃ A ) ⊃ ( C ⊃ B ) )

( A ⊃ B ) ⊃ ( ( A & C ) ⊃ ( B & C ) )

( A ⊃ B ) ⊃ ( ( A ∨ C ) ⊃ ( B ∨ C ) )

( A ⊃ ( B ⊃ C ) ) ∼ ( B ⊃ ( A ⊃ C ) )

( A ⊃ ( B ⊃ C ) ) ∼ ( A & B ⊃ C )

( ¬A ⊃ B ) ⊃ ( ¬B ⊃ A )


(classicalonly)

Reflexivity
Transitivity
( ( A ⊃ B ) & ( B ⊃ C ) ) ⊃ ( A ⊃ C )



proof

Equivalence
Reflexivity
Commutativity
Transitivity
( ( A ∼ B ) & ( B ∼ C ) ) ⊃ ( A ∼ C )

( A ∼ B ) ∼ ( ( A ⊃ B ) & ( B ⊃ A ) )

( A ∼ B ) ⊃ ( ( A ∼ C ) ∼ ( B ∼ C ) )

( A ∼ B ) ⊃ ( ( A ⊃ C ) ∼ ( B ⊃ C ) )

( A ∼ B ) ⊃ ( ( C ⊃ A ) ∼ ( C ⊃ B ) )

( A ∼ B ) ⊃ ( ( A & C ) ∼ ( B & C ) )

( A ∼ B ) ⊃ ( ( A ∨ C ) ∼ ( B ∨ C ) )

Conjunction
Associativity
( ( A & B ) & C ) ∼ ( A & ( B & C )

Commutativity
Distributivity
( A & ( B ∨ C ) ∼ ( ( A & B ) ∨ ( A & C ) )

Idempotency
( ( A ⊃ B ) & ( A ⊃ ¬B ) ) ⊃ ¬A

Disjunction
Associativity
( ( A ∨ B ) ∨ C ) ∼ ( A ∨ ( B ∨ C )

Commutativity
Distributivity
( A ∨ ( B & C ) ∼ ( ( A ∨ B ) & ( A ∨ C ) )

Idempotency
Negation
Double Negation Elimination
Denial of Contradiction
Law of Excluded Middle
De Morgan's Law
¬( A & B ) ∼ ( ¬A ∨ ¬B )


(classicalonly)



proof

¬( A ⊃ B ) ∼ ( A & ¬B )


(classicalonly)

Expression of Connectives in Terms of Others
( A ∨ B ) ∼ ¬( ¬A & ¬B )
(classicalonly)

( A ∨ B ) ∼ ( ¬A ⊃ B )


(classicalonly)

( A & B ) ∼ ¬( ¬A ∨ ¬B )


(classicalonly)

( A & B ) ∼ ¬( A ⊃ ¬B )


(classicalonly)

( A ⊃ B ) ∼ ( ¬A ∨ B )


(classicalonly)



proof

( A ⊃ B ) ∼ ¬( A & ¬B )


(classicalonly)

( A ⊃ B ) ∼ ( ¬B ⊃ ¬A )


(classicalonly)

( A ∼ B ) ∼ ( ¬B ∼ ¬A )


(classicalonly)

If logical constants ⊤ (true) and ⊥ (false) are in use,
then the following laws are also relevant:
( A ⊃ ⊥ ) ∼ ¬A


( ⊤ ⊃ A ) ∼ A

( A & ⊤ ) ∼ A


( A & ⊥ ) ∼ ⊥

( A ∨ ⊤ ) ∼ ⊤


( A ∨ ⊥ ) ∼ A

Here, x and y are any distinct variables, A(x), B(x), A(x,y)
are any formulas, A anf B are any formulas not containing x as a free variable,
i.e. not bound by a quantifier.
Quantifier Alterations
∀x ∀y A(x,y) ∼ ∀y ∀x A(x,y)

∃x ∃y A(x,y) ∼ ∃y ∃x A(x,y)

∃x ∀y A(x,y) ⊃ ∀y ∃x A(x,y)

A(y) is the result of substituting y for the free occurrences of x in A(x)
provided that y does not occur free in A(x) and that
all occurrences of y resulting from this substitution are free.
A(x,x) is the result of substituting x for the free occurrences of y in A(x,y)
provided that all occurrences of x resulting from this substitution are free.
Quantifiers with Negation
¬∀x A(x) ∼ ∃x ¬A(x)


(classicalonly)

∃x A(x) ∼ ¬∀x ¬A(x)


(classicalonly)

∀x A(x) ∼ ¬∃x ¬A(x)


(classicalonly)

Quantifiers with Conjunction/Disjunction
( ∀x ( A(x) & B(x) ) ) ∼ ( ∀x A(x) & ∀x B(x) )

( ∃x ( A(x) ∨ B(x) ) ) ∼ ( ∃x A(x) ∨ ∃x B(x) )



proof

( ∀x ( A(x) & B ) ) ∼ ( ∀x A(x) & B )
( ∀x ( B & A(x) ) ) ∼ ( B & ∀x A(x) )

( ∃x ( A(x) ∨ B ) ) ∼ ( ∃x A(x) ∨ B )
( ∃x ( B ∨ A(x) ) ) ∼ ( B ∨ ∃x A(x) )

( ∃x ( A(x) & B ) ) ∼ ( ∃x A(x) & B )
( ∃x ( B & A(x) ) ) ∼ ( B & ∃x A(x) )

( ∀x A(x) ∨ B ) ⊃ ( ∀x ( A(x) ∨ B ) )
( B ∨ ∀x A(x) ) ⊃ ( ∀x ( B ∨ A(x) ) )

( ∀x ( A(x) ∨ B ) ) ∼ ( ∀x A(x) ∨ B )
( ∀x ( B ∨ A(x) ) ) ∼ ( B ∨ ∀x A(x) )


(classicalonly)

( ∃x ( A(x) & B(x) ) ) ⊃ ( ∃x A(x) & ∃x B(x) )

( ∀x A(x) ∨ ∀x B(x) ) ⊃ ( ∀x ( A(x) ∨ B(x) ) )

Quantifiers with Implication
( ∀x ( A ⊃ B(x) ) ) ∼ ( A ⊃ ∀x B(x) )

( ∃x ( A ⊃ B(x) ) ) ⊃ ( A ⊃ ∃x B(x) )

( ∃x ( A ⊃ B(x) ) ) ∼ ( A ⊃ ∃x B(x) )


(classicalonly)

( ∃x ( A(x) ⊃ B ) ) ⊃ ( ∀x A(x) ⊃ B )

( ∃x ( A(x) ⊃ B ) ) ∼ ( ∀x A(x) ⊃ B )


(classicalonly)



proof

( ∀x ( A(x) ⊃ B ) ) ∼ ( ∃x A(x) ⊃ B )

( ∃x ( A(x) ⊃ B(x) ) ) ⊃ ( ∀x A(x) ⊃ ∃x B(x) )

( ∃x ( A(x) ⊃ B(x) ) ) ∼ ( ∀x A(x) ⊃ ∃x B(x) )


(classicalonly)

( ∃x A(x) ⊃ ∀x B(x) ) ⊃ ( ∀x ( A(x) ⊃ B(x) ) )



proof

These are basic logical laws. Many more of them can be constructed
from the above by using the two following theorems as tools
for generating more complex laws.
Replacement Theorem
Let A be a logical formula and B be a particular sunformula occurence in A.
Denote A_{BC} the formula obtained from A by replacing that occurrence B
by formula C. Let x_{1}, ..., x_{n} be the free variables of B or C,
which are bound in A or A_{BC}.
If ∀x_{1} ... ∀x_{n} ( B ∼ C ), then A ∼ A_{BC}.
Positive and negative subformula occurrences in formula A are defined recursively
by the following rules:
 A itself is positive
 If subformula B ∨ C or B & C is positive (negative), then so are A and B
 If subformula ¬B is positive (negative), then B is negative (positive)
 If subformula B ⊃ C is positive (negative), then B is negative (positive) and C is positive (negative)
 If subformula ∀x B(x) or ∃x B(x) is positive (negative), then so is B(x)
Theorem
Let A be a logical formula, B be a particular sunformula occurence in A,
B is not in the scope of any ∼. Let x_{1}, ..., x_{n} be the free variables of B or C,
which are bound in A or A_{BC}.
If ∀x_{1} ... ∀x_{n} ( B ⊃ C ) and B is positive, then A ⊃ A_{BC}.
If ∀x_{1} ... ∀x_{n} ( B ⊃ C ) and B is negative, then A_{BC} ⊃ A.
Let us combine Law of Excluded Middle
and one of De Morgan's Laws
Here is the result of applying the first theorem:
Since Law of Excluded Middle is classicalonly, the resulting law is
also classicalonly.
Now, let us combine
and
( ∃x ( A(x) & B(x) ) ) ⊃ ( ∃x A(x) & ∃x B(x) )

By using the second theorem and implication transitivity, we can get
( ∃x ( A(x) & B(x) ) ) ⊃ ( ( ∃x A(x) ∨ ∃x ¬B(x) ) & ∃x B(x) )

References
S. C. Kleene. Mathematical Logic. Dover, 2002.
S. C. Kleene. Introduction to Metamathematics. North Holland, 1952.
