F
 o
  u
   n
    d
     a
      t
       i
        o
         n
          s

o
 f

M
 a
  t
   h
    e
     m
      a
       t
        i
         c
          s

Logical laws are expressions of the first-order 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 Gentzen-style 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 classical-only 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 )

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

A ⊃ ( B ⊃ A & B )

( 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 ⊃ ( A ⊃ B )

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

(classical-only)

Reflexivity

A ⊃ A

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

proof

Equivalence

Reflexivity

A ∼ A

Commutativity

( A ∼ B ) ∼ ( B ∼ A )

Transitivity

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

( A ∼ B ) ⊃ ( A ⊃ B )

( A ∼ B ) ⊃ ( B ⊃ A )

( 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 ) )

A ⊃ ( ( A ∼ B ) ∼ B )

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

A ⊃ ( ( A ⊃ B ) ∼ B )

A ⊃ ( ( B ⊃ A ) ∼ A )

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

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

A ⊃ ( ( A & B ) ∼ B )

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

A ⊃ ( ( A ∨ B ) ∼ A )

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

Conjunction

Associativity

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

Commutativity

( A & B ) ∼ ( B & A )

Distributivity

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

Idempotency

( A & A ) ∼ A

( A & ( A ∨ B ) ) ∼ A

( A & ( A ⊃ B ) ) ⊃ B

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

A & B ⊃ A A & B ⊃ B

Disjunction

Associativity

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

Commutativity

( A ∨ B ) ∼ ( B ∨ A )

Distributivity

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

Idempotency

( A ∨ A ) ∼ A

( A ∨ ( A & B ) ) ∼ A

A ⊃ A ∨ B B ⊃ A ∨ B

Negation

A ⊃ ¬¬A

¬A ∼ ¬¬¬A

Double Negation Elimination

¬¬A ∼ A

(classical-only)

Denial of Contradiction

¬( A & ¬A )

Law of Excluded Middle

A ∨ ¬A

(classical-only)

De Morgan's Law ¬( A ∨ B ) ∼ ( ¬A & ¬B )

proof

( ¬A ∨ ¬B ) ⊃ ¬( A & B ) De Morgan's Law ¬( A & B ) ∼ ( ¬A ∨ ¬B )            (classical-only)

proof

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

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

(classical-only)

Expression of Connectives in Terms of Others

( A ∨ B ) ⊃ ¬( ¬A & ¬B )

( A ∨ B ) ∼ ¬( ¬A & ¬B )            (classical-only)

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

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

(classical-only)

( A & B ) ⊃ ¬( ¬A ∨ ¬B )

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

(classical-only)

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

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

(classical-only)

( ¬A ∨ B ) ⊃ ( A ⊃ B ) ( A ⊃ B ) ∼ ( ¬A ∨ B )            (classical-only)

proof

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

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

(classical-only)

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

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

(classical-only)

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

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

(classical-only)

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 ∨ ⊤ ) ∼ ⊤

( 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 A ∼ A

∃x A ∼ A

∀x ∀y A(x,y) ∼ ∀y ∀x A(x,y)

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

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

∃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.

∀x A(x) ∼ ∀y A(y)

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

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.

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

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

Quantifiers with Negation

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

proof

∃x ¬A(x) ⊃ ¬∀x A(x)

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

(classical-only)

∃x A(x) ⊃ ¬∀x ¬A(x)

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

(classical-only)

∀x A(x) ⊃ ¬∃x ¬A(x)

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

(classical-only)

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

(classical-only)

( ∃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) )

(classical-only)

( ∃x ( A(x) ⊃ B ) ) ⊃ ( ∀x A(x) ⊃ B ) ( ∃x ( A(x) ⊃ B ) ) ∼ ( ∀x A(x) ⊃ B )            (classical-only)

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

(classical-only)

( ∃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_B|C the formula obtained from A by replacing that occurrence B by formula C. Let x₁, ..., x_n be the free variables of B or C, which are bound in A or A_B|C. If ∀x₁ ... ∀x_n ( B ∼ C ), then A ∼ A_B|C.

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₁, ..., x_n be the free variables of B or C, which are bound in A or A_B|C. If ∀x₁ ... ∀x_n ( B ⊃ C ) and B is positive, then A ⊃ A_B|C. If ∀x₁ ... ∀x_n ( B ⊃ C ) and B is negative, then A_B|C ⊃ A.

Let us combine Law of Excluded Middle

A ∨ ¬A

and one of De Morgan's Laws

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

Here is the result of applying the first theorem:

A ∨ B ∨ ( ¬A & ¬B )

Since Law of Excluded Middle is classical-only, the resulting law is also classical-only.

Now, let us combine

A ⊃ A ∨ B

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.