The constituents of language
At the base of the syntax of the calculus of propositions are the propositional variables or atomic propositions, denoted by p, q, etc., which generally constitute a countable infinite set.
The second basic constituents of the language of the calculus of propositions are the operators or connectives. These are symbols that make it possible to construct more elaborate proposals. The most common of these logical connectors are:
We also often consider the constant denoted ⊥, pronounced “up tack” or “falsum”, which aims to represent the false.
Next to these symbols, parentheses are used to remove ambiguities in the formulas (choice adopted below), or a notation like the Polish notation, invented by the Polish logician Jan Łukasiewicz. It is important that the definition of formulas be simple and unambiguous, in particular to allow inductive definitions on the structure of formulas, but practically it is possible to save parentheses, either by adopting certain conventions to remove ambiguities, or because that the context makes these ambiguities irrelevant.
The calculus of propositions is also based on formation rules indicating how to construct complex propositions from elementary propositions, or atoms, which are propositional variables, and possible constants such as ⊥. These rules determine which combinations of signs, which words, are well formed and designate propositions. The definition depends on a choice of connectors, and a choice of atoms.
We are given a set P of propositional variables. The set of formulas of the calculus of propositions (over P ), or simply propositions, is defined by induction, i.e. it is the smallest set such that:
- a propositional variable p of P is a formula;
- ⊥ is a formula;
- if P and Q are formulas, then (P ∧ Q), (P ∨ Q), (P → Q), (P ↔ Q) and ¬P are propositions.
Examples: If P, Q and R are propositions,
(P → Q) → (¬Q → ¬P) is a proposition.
(P → ⊥) → ⊥ is a proposition.
P ∧ ¬P is a proposition.
(P ∧ Q) ∨ R is a proposition.
P ∧ Q ∨ is not a proposition.
Some syntactic conventions
In order to lighten the presentation of the expressions without jeopardizing the absence of ambiguity, we authorize by syntactic conventions certain departures from the above definition.
- Extreme parentheses in formulas are generally omitted.
- Parentheses are often removed when combining expressions from left to right when dealing with the same connector: A ∧ B ∧ C for ((A ∧ B) ∧ C).
- Involvement is a special case. By convention, it is right-associative: A → B → C → D reads A → (B → (C → D)).
For readability, we also use several forms of parentheses (size, replacement with square brackets, etc.)
Moreover, we demonstrate that only the opening parentheses are necessary for the non-ambiguity of the reading of the formulas which for this reason are replaced by a point “.” in some notations.
The calculus of propositions makes it possible to present the three most well-known deductive systems. For this, we limit ourselves to propositions containing, besides propositional variables, only implications, disjunctions and occurrences of false, in other words of ⊥. We assume that ¬P is an abbreviation of P → ⊥. If P is a theorem, in other words a proposition which has a proof, we denote this by ├P.
Deductive systems use deduction rules (also called inference rules) which are written:
φ1 . . . φn
The φi are called the premises and ψ is called the conclusion.
The Hilbert deduction
There is only one rule called the modus ponens, it is written:
├ (P → Q) ├ P
It can be understood as follows: if P → Q is a theorem and P is a theorem then Q is a theorem. To this we can add:
- three axioms for implication and falsehood:
- ├ P → ( Q → P ) ,
- ├ ( P → ( Q → R ) ) → ( ( P → Q ) → ( P → R ) ) ,
- ├ (¬P → ¬Q) → (Q → P);
- three axioms for disjunction:
- ( P → R ) → ( ( Q → R ) → ( ( P ∨ Q ) → R ) ) ,
- P → (P ∨ Q),
- Q → (P ∨ Q).
- three axioms for the conjunction:
- ( R → P ) → ( ( R → Q ) → ( R → ( P ∧ Q ) ) ) ,
- (P ∧ Q) → P.
- (P ∧ Q) → Q.
The natural deduction
While Hilbert deduction manipulates and demonstrates theorems, natural deduction demonstrates propositions under assumptions and when there are no (more) assumptions, they are theorems. To say that a proposition P is a consequence of a set Γ of hypotheses, we write Γ ├ P . Whereas in Hilbert deduction there is only one rule and several axioms, in natural deduction there is only one axiom and several rules. For each connector, the rules are classified into rules of introduction and rules of elimination.
- The axiom is Γ, P ├ P.
- The rule of introduction of implication:
Γ , P ├ Q
Γ ├ P → Q
- The rule of elimination of implication:
Γ ├ P → Q Γ ├ P
Γ ├ Q
- The two rules of introduction of disjunction, right and left:
Γ ├ P Γ ├ Q
Γ├ P ∨ Q Γ├ P ∨ Q
- The disjunction elimination rule:
Γ├ P ∨ Q Γ , P├ R Γ , Q├ R
- The false elimination rule:
In addition, there is a rule of reductio ad absurdum, necessary in classical logic:
Γ , ¬P├⊥
Note that the rule of elimination of implication is very close to the modus ponens, moreover it is also called modus ponens. It will be noted that there is no rule of introduction of the false and that the rule of elimination of the false comes down to saying that if from a set of hypotheses I deduce the false (or the absurd) then from this even together I can deduce anything. Note that reduction to absurd is the rule that corresponds to reasoning by absurd: to prove P, we add ¬P to the hypotheses and if we obtain the absurd, then we have P.
Calculus of sequents
One of the ideas that led to the calculus of sequents is to have only introductory rules in addition to a so-called cut rule and structural rules. For this, we use formulas which are called sequents and which are of the form Γ ├ Δ where Γ and Δ are multisets of propositions. The sequent P1 , . . . , Pm ├ Q1 , . . . , Qn is interpreted as the assertion of the conjunction of the Pi. The Pi are called the antecedents and the Qj are called the consequents. If the list of antecedents is empty we write ├ Δ if the list of consequents is empty we write Γ├ . A theorem is still a sequent without antecedents and with a single consequent.
- The axiom is A├ A .
- Introduction of implication on the right:
Γ , A├ Δ , B
Γ├ Δ , A → B
- Introduction of implication on the left:
Γ, A├ Δ Γ′├ Δ′, B
Γ, Γ′, B → A├ Δ, Δ′
- Introduction of disjunction on the right:
Γ├ Δ, A, B
Γ├ Δ, A ∨ B
- Introduction of disjunction on the left:
Γ, A├ Δ Γ′, B├ Δ′
Γ, Γ′, A∨B├ Δ, Δ′
- Introduction of false on the right:
Γ├ Δ , ⊥
- Introduction of false on the left, it has the form of an axiom: ⊥├
Γ├ Δ, A Γ′, A├ Δ′
Γ, Γ′├Δ, Δ′
Γ├ Δ Γ├ Δ
Γ , A├ Δ Γ├ Δ , A
Γ, A, A├ Δ Γ├ Δ, A, A
Γ, A├ Δ Γ├ Δ, A
A cut translates the attitude of the mathematician who demonstrates a lemma (proposition A ) which he uses elsewhere in the proof of a theorem. This lemma can express something that has nothing to do with the main theorem, hence the wish to eliminate these lemmas which are like detours in the progression towards the main result. A weakening corresponds to the addition of a superfluous clause either as an antecedent or as a consequence.
Examples of theorems
We indicate below a list of theorems that can be demonstrated using the preceding rules, together with the usual name attributed to them by tradition.
|( A → A )||identify|
|A ∨ ¬ A||excluded third party|
|A → ¬ ¬ A||double negation|
|¬ ¬ A → A||classic double negation|
|( ( A → B ) → A ) → A||Peirce’s law|
|¬ ( A ∧ ¬ A )||non contradiction|
|¬ ( A ∧ B ) ↔ ( ¬ A ∨ ¬ B )||De Morgan’s laws|
|¬ ( A ∨ B ) ↔ ( ¬ A ∧ ¬ B )|
|( A → B ) → ( ¬ B → ¬ A )||contraposition|
|( ( A → B ) ∧ A ) → B||modus ponens (propositional)|
|( ( A → B ) ∧ ¬ B ) → ¬ A||modus tollens (propositional)|
|( ( A → B ) ∧ ( B → C ) ) → ( A → C )||modus barbara (propositional)|
|( A → B ) → ( ( B → C ) → ( A → C ) )||modus barbara (implicative)|
|( A ∧ ( B ∨ C ) ) ↔ ( ( A ∧ B ) ∨ ( A ∧ C ) )||distributivity|
|( A ∨ ( B ∧ C ) ) ↔ ( ( A ∨ B ) ∧ ( A ∨ C ) )|
All three systems use the same ├ symbol, but this notation is consistent. The format Γ├ P used for natural deduction is in fact a sequent in which there is only one conclusion, one then speaks of a natural sequent. The format ├ P used for theorems in Hilbert systems corresponds to a natural sequent where there is no hypothesis.
It can be shown that these three systems are equivalent in the sense that they have exactly the same theorems.
The “classical” aspect of the calculus of propositions is obtained, in the system à la Hilbert, by the axiom of contraposition ├ ( ¬ P → ¬ Q ) → ( Q → P ) , it appears in natural deduction through the reduction to the absurd. The calculus of sequents is classical, but if we restrict ourselves to sequents with a single consequent, it becomes intuitionistic.
(Includes texts from Wikipedia translated and adapted by Nicolae Sfetcu)