1.6. Logical connectives

We defined earlier the concept of logical connective. Let us now list the main useful ones, beyond both nullary ones (Boolean constants) 1 and 0. (To this will be added the conditional connective in 2.1). Their properties will be expressed by tautologies, which are formulas only involving connectives and Boolean variables (here written A, B, C), and true for all possible combinations of values of these variables. So, they also give necessarily true formulas when replacing these variables by any defining formulas using any language and interpreted in any systems. Such definitions of Boolean variables by formulas of a theory may restrict their ranges of possible values depending on each other.

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

The binary connective of equality between Booleans is written ⇔ and called equivalence: AB is read «A is equivalent to B».

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)
⇔ ¬(x = y)
⇔ ¬(xE)
⇔ (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))

This similarity (symmetry) of their properties comes from the fact they are exchanged by negation:

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

The inequivalence is also called exclusive or because (AB) ⇔ ((AB) ∧ ¬(AB)).

Chains of conjunctions such as (ABC), abbreviate any formula with more parenthesis such as ((AB) ∧ C), all equivalent by associativity ; similarly for chains of disjunctions such as (ABC).

Asserting (declaring as true) a conjunction of formulas amounts to successively asserting all these formulas.

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 in a given theory, a proof of AB can be formed 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) is equivalent to AB but will be written AB, which reads «A therefore B», to indicate that it is deduced from the truths of A and AB.

Negations turn the associativity and distributivity of ∧ and ∨, into various tautologies involving 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 chain of formulas linked by ⇔ and/or ⇒ will mean the chain of conjunctions of 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)

Provability

In this work like almost anywhere else, proofs will be written naturally without trying to formalize the concept of proof (write the full details of a proof theory, which specialists did). Sometimes using natural language articulations, they will mainly be written as a succession of statements each visibly true thanks to previous ones, premises, axioms, known theorems and rules of proof, especially those of quantifiers (1.9).
To qualify known theorems (statements with known proofs), synonyms for "theorem" are traditionally used 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 easily implies an also less important corollary.

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 TA 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
((TA) ∧ (TB)) ⇔ (TAB)
((TA) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).

In an inconsistent theory, every statement is provable. Such a theory has no model.

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. Algebra - 4. Arithmetic 5. Second-order foundations
Other languages:
FR : 1.6. Connecteurs