Rule of Inference - Example: Hilbert Systems For Two Propositional Logics

Example: Hilbert Systems For Two Propositional Logics

In a Hilbert system the premises and conclusion of the inference rules are simply formulas of some language, usually employing metavariables. For graphical compactness of the presentation and to emphasize the distinction between axioms and rules of inference we use the sequent notation (⊢) in this section instead of a vertical presentation of rules.

The formal language for classical propositional logic can be expressed using just negation (¬), implication (→) and propositional symbols. A well-known axiomatization, comprised of thee axiom schema and one inference rule (modus ponens) is:

(CA1) ⊢ A → (B → A)
(CA2) ⊢ (A → (B → C)) → ((A → B) → (A → C))
(CA3) ⊢ (¬A → ¬B) → (B → A)
(MP) A, A → B ⊢ B

It may seem redundant to have two notions of inference in this case, ⊢ and →. In classical propositional logic they indeed coincide; the deduction theorem states that A ⊢ B if and only if ⊢ A → B. For other logics, this result does not hold however. For example, the three-valued logic Ł3 of Łukasiewicz can be axiomatized as:

(CA1) ⊢ A → (B → A)
(LA2) ⊢ (A → B) → ((B → C) → (A → C))
(CA3) ⊢ (¬A → ¬B) → (B → A)
(LA4) ⊢ ((A → ¬A) → A) → A
(MP) A, A → B ⊢ B

This differs from classical logic by the change in axiom 2 and the addition of axiom 4. The classical deduction theorem does not hold for this logic, however a modified form does hold, namely A ⊢ B if and only if ⊢ A → (A → B).