1.6. Logical connectives

We already saw the nullary connectives : the Boolean constants 0 (false) and 1 (true).
The binary connective of equality between Booleans is written ⇔ and called equivalence: AB is read «A is equivalent to B».

Let us present other useful connectives, with their properties true for all possible values of the Boolean variables (A, B, C, that can be replaced by formulas).

Negation

The only useful unary connective is the negation ¬, that exchanges Booleans (¬A is read «not A»):
¬1
¬0
¬(¬A)
⇔ 0
⇔ 1
A
It is often denoted by barring the root of its argument, forming with it another symbol with the same format:
xy
xE
(AB)
(AB)
⇔ ¬(x=y)
⇔ ¬(xE)
⇔ ¬(AB)
⇔ (A ⇔ ¬B))
(x is not equal to y)
(x is not an element of E)
(Inequivalence)

Conjunctions, disjunctions

The conjunction ∧ means «and», being true only when both arguments are true;
The disjunction ∨ means «or», being true except when both arguments are false.
Each of them is :
Idempotent
(AA) ⇔ A
(AA) ⇔ A
Commutative
(BA) ⇔ (AB)
(BA) ⇔ (AB)
Associative
((AB) ∧ C) ⇔ (A ∧ (BC))
((AB) ∨ C) ⇔ (A ∨ (BC))
Distributive over the other
(A ∧ (BC)) ⇔ ((AB) ∨ (AC))
(A ∨ (BC)) ⇔ ((AB) ∧ (AC))

The symmetry between them comes from the fact they are exchanged by negation:

(AB) ⇎ (¬A ∧ ¬B)
(AB) ⇎ (¬A ∨ ¬B)

Strings of conjunctions such as (ABC), abbreviate any formula with more parenthesis such as ((AB) ∧ C), which are equivalent to each other thanks to associativity ; and similarly for strings of disjunctions such as (ABC).
Asserting a conjunction of formulas amounts to successively asserting all these formulas.
The inequivalence ⇎ is also called «exclusive or» because (AB) can also be written ((AB) ∧ ¬(AB)).

Implication

The binary connective of implication ⇒ is defined as (AB) ⇔ ((¬A) ∨ B). It can be read «A implies B», «A is a sufficient condition for B», or «B is a necessary condition for A». Being true except when A is true and B is false, it expresses the truth of B when A is true, but no more gives information on B when A is false (as it is then true).
Moreover,
(AB) ⇎
(AB) ⇔
(A ∧ ¬B)
B ⇒ ¬A)
The formula ¬B ⇒ ¬A is called the contrapositive of AB.
The equivalence can also be redefined as
(AB) ⇔ ((AB) ∧ (BA)).
Thus, a proof of AB can be made of a proof of the first implication (AB), then a proof of the second one (BA), called the converse of (AB).

The formula (A ∧ (AB)) will be abbreviated as AB, which reads «A therefore B». It is equivalent to (AB), but indicating that it is deduced from the truths of A and (AB).

Negations transform the associativity and distributivity formulas of conjunctions and disjunctions, into various formulas with implications:
(A ⇒ (BC)) ⇔ ((AB) ⇒ C)
(A ⇒ (BC)) ⇔ ((AB) ∨ C)
(A ⇒ (BC)) ⇔ ((AB) ∧ (AC))
((AB) ⇒ C) ⇔ ((AC) ∧ (BC))
((AB) ⇒ C) ⇔ ((AC) ∧ (BC))
(A ∧ (BC)) ⇔ ((AB) ⇒ (AC))
Finally,
((AB) ∧ (AC)) ⇒ (BC)
((AB) ∧ (AC)) ⇒ (BC)

Chains of implications and equivalences

In a different kind of abbreviation, any string of formulas linked by ⇔ and/or ⇒ will mean the conjunction of all these implications or equivalences between adjacent formulas:

(ABC) ⇔ ((AB) ∧ (BC)) ⇒ (AC)
(ABC) ⇔ ((AB) ∧ (BC)) ⇒ (AC)
0 ⇒ AA ⇒ 1
A) ⇔ (A ⇒ 0) ⇔ (A ⇔ 0)
(A ∧ 1) ⇔ A ⇔ (A ∨ 0) ⇔ (1 ⇒ A) ⇔ (A ⇔ 1)
(AB) ⇒ A ⇒ (AB)

Axioms of equality

For any objects (or abbreviations of terms) x, y, any functor T and any unary predicate A,
x = y
x = y
x = x
T(x) = T(y)
(A(x) ⇔ A(y))
The last formula can also be written (A(x) ∧ x = y) ⇒ A(y), since the converse A(y) ⇒ A(x) can be deduced either by its contrapositive (replacing A by ¬A) or by the symmetry of equality (x = yy = x) obtained by taking as A(z) the formula (z = x).
It also gives for all x, y, z, (x = yy = z) ⇒ x = z. The formula (x = yy = z) will be abbreviated as x = y = z.

Provability

A proof of a formula A in a first-order theory T, is a finite model of proof theory, connecting A to some axioms of T.
We say that A is provable in T and write TA if there exists a proof of A in T.
Again in T, a refutation of a formula A is a proof of ¬A. If one exists (T⊢ ¬A), the formula A is called refutable (in T).
A formula is called undecidable (in T) if it is neither provable nor refutable.

If a formula is both provable and refutable then all are, which means that the theory is inconsistent:

(A ∧ ¬A) ⇔ 0
((TA)∧(T⊢ ¬A))⇔(T⊢ 0).

The theory T is called contradictory or inconsistent if T⊢ 0, otherwise it is called consistent. In an inconsistent theory, every formula is provable. Such a theory has no model.

Without trying to formalize what a proof is, we shall just write proofs naturally, usually as a succession of formulas, each visibly true thanks to previous ones and the above properties of connectives and equality. Natural language articulations may also appear, especially when dealing with quantifiers (1.9) and introducing symbols defined by expressions.
In particular, an equality between terms x = y allows to replace any occurrence of x by y in any expression without affecting the result; when a symbol is defined by a term, both are equal, thus can be substituted to each other in any expression. Axioms and other rules expressed with variable symbols (under universal quantifiers, see 1.9) can then be used replacing these variables by terms.
Provable formulas with a known proof (either by humans or by computers) can be differently named in usual language according to their importance: a theorem is more important than a proposition; either of them may be deduced from an otherwise less important lemma, and a corollary may be easily deduced from it.

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions, objects, meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
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
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
2. Set theory (continued) 3. Model theory

Other languages:
FR : 1.6. Connecteurs