Tautologies form the rules of Boolean algebra, an algebraic theory describing
operations on the Boolean type, interpreted as the pair of elements 0 and 1 but also
admiting more sophisticated interpretations beyond the scope of this chapter.
Statements or formulas having like tautologies the property of being always true by virtue
of the logical framework are called logically valid ; they are necessary theorems of
any theory regardless of axioms
where they need not appear.
More logically valid formulas will be given in 1.9 (axioms of equality).
¬1 ¬0 ¬(¬A) 
⇔ 0 ⇔ 1 ⇔ A 
x ≠ y x ∉ E (A ⇎ B) 
⇔ ¬(x = y) ⇔ ¬(x ∈ E) ⇔ (A ⇔ ¬B) 
(x is not equal to y) (x is not an element of E) (inequivalence) 
Idempotent (A ∧ A) ⇔ A (A ∨ A) ⇔ A 
Commutative (B∧A) ⇔ (A∧B)
(B∨A) ⇔ (A∨B) 
Associative ((A∧B)∧C) ⇔ (A∧(B∧C))
((A∨B)∨C) ⇔ (A∨(B∨C)) 
Distributive over the other (A ∧ (B∨C)) ⇔ ((A∧B)
∨ (A∧C))
(A ∨ (B∧C)) ⇔ ((A∨B) ∧ (A∨C)) 
(A ∨ B)
⇎ (¬A ∧ ¬B)
(A ∧ B) ⇎ (¬A ∨ ¬B)
Chains of conjunctions such as (A ∧ B ∧ C), abbreviate any formula with more parenthesis such as ((A ∧ B) ∧ C), all equivalent by associativity ; similarly for chains of disjunctions such as (A ∨ B ∨ C).
Asserting (declaring as true) a conjunction of formulas amounts to successively asserting all these formulas.(A ⇒ B) ⇎ (A ⇒ B) ⇔ 
(A ∧ ¬B) (¬B ⇒ ¬A) 
The formula A ∧ (A ⇒ B) is equivalent to A ∧ B but will be written A ∴ B, which reads «A therefore B», to indicate that it is deduced from the truths of A and A ⇒ B.
Negations turn the associativity and distributivity of ∧ and ∨, into various tautologies involving implications:
In a different kind of abbreviation, any chain of formulas linked by ⇔ and/or ⇒ will mean the chain of conjunctions of these implications or equivalences between adjacent formulas:
(A ⇒ B
⇒ C) ⇔ ((A ⇒ B) ∧ (B ⇒ C)) ⇒
(A ⇒ C)
(A ⇔ B ⇔ C) ⇔ ((A ⇔ B) ∧ (B
⇔ C)) ⇒ (A ⇔ C)
0 ⇒ A ⇒ A ⇒ 1
(¬A) ⇔ (A ⇒ 0) ⇔ (A ⇔ 0)
(A ∧ 1) ⇔ A ⇔ (A ∨ 0) ⇔ (1 ⇒ A) ⇔ (A
⇔ 1)
(A ∧ B) ⇒ A ⇒ (A ∨ B)
A proof of a statement A in a theory T, is
a finite model of proof theory, involving A and some axioms of T; it
can also be seen as a proof of (conjunction of these axioms ⇒ A) without axiom,
so that the existence of such a system ensures the logical validity of this implication.
But, beyond tautologies, logically valid statements with some size may be only provable
by proofs with indescribably larger size.
We say that A is provable in T and write T ⊢
A if there exists a proof of A in T.
Again in T, a refutation of A is a proof of ¬A. If one exists
(T ⊢ ¬A), the statement A is called refutable (in T).
A statement is called decidable (in T) if it is either provable or refutable.
A theory T is called contradictory or inconsistent if T ⊢ 0, otherwise it is called consistent. If a statement is both provable and refutable in T then all are, because it means that T is inconsistent, independently of the chosen statement:
(A ∧ ¬A) ⇔ 0
((T ⊢ A) ∧ (T ⊢ B))
⇔ (T ⊢ A∧B)
((T ⊢ A) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).
Set theory and Foundations of Mathematics  
1. First
foundations of mathematics 
1.6. Logical connectives
⇨ 1.7. Classes
in set theory 1.8. Binders
in set theory
1.9. Quantifiers 1.10. Formalization of set theory 1.11. Set generation principle 

Philosophical aspects  ⇨ Time in model theory  Interpretation of classes
Concepts of truth in mathematics 
2. Set theory (continued)  3. Algebra  4. Arithmetic  5. Secondorder foundations 