is the statement proved or derived. If premises are left unsatisfied in the derivation, then the derivation is a proof of a hypothetical statement: "if the premises hold, then the conclusion holds." Example: Hilbert systems for two propositional logics In a Hilbert system, the premises and conclusion of the inference rules are simply formulae of some language, usually employing metavariables. For graphical compactness of the presentation and to emphasize the distinction between axioms and rules of inference, this section uses the sequent notation () instead of a vertical presentation of rules. In this notation, is written as . The formal language for classical propositional logic can be expressed using just negation (¬), implication (→) and propositional symbols. A well-known axiomatization, comprising three axiom schemata 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. There is however a distinction worth emphasizing even in this case: the first notation describes a deduction, that is an activity of passing from sentences to sentences, whereas A → B is simply a formula made with a logical connective, implication in this case. Without an inference rule (like modus ponens in this case), there is no deduction or inference. This point is illustrated in Lewis Carroll's dialogue called "What the Tortoise Said to Achilles", as well as later attempts by Bertrand Russell and Peter Winch to resolve the paradox introduced in the dialogue. For some non-classical logics, the deduction theorem does not hold. For example, the three-valued logic 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 sequence 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