Skip to content
Topos Uranos
English

Formal deductive systems

Summary

This lesson turns the language of the previous unit into an instrument for proving. It defines what a formal deductive system is (a language, some axiom schemas and some rules of inference) and presents the first of the two with which the course works, Łukasiewicz's system: three axiom schemas and modus ponens as its only rule. It defines precisely deduction from a set of premises, theorem and the relation Γ⊢φ\Gamma \vdash \varphi, deduces ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) in five lines and proves the structural properties of deduction: reflexivity, monotonicity, modus ponens between deductions, cut and finiteness. It then proves, by strong induction on the number of lines, the deduction theorem and its converse, which make it possible to reason with deductions about deductions, and defines provable equivalence. Finally, without appealing to truth values, it establishes the limit of that system in a language whose only connective is joint denial: a marking with values 00 and 11, computed by recursion on formulas, which Łukasiewicz's axioms and modus ponens preserve, proves that certain formulas that ought to be deduced are not deduced, and that one cannot even pass from (v1↓v2)(v_{1} \downarrow v_{2}) to (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}). Hence the need for a second rule, replacement of double negation, with which the next lesson completes the system.

Learning objectives

  1. Recognize the instances of the schemas A1, A2 and A3 and decide whether a sequence of formulas is a deduction from a set of premises.
  2. Construct deductions in Łukasiewicz's system, with axioms, premises and modus ponens, and deductions about deductions with reflexivity, monotonicity, cut, the deduction theorem and its converse.
  3. Prove the structural properties of deduction and the deduction theorem by strong induction on the number of lines.
  4. Establish provable equivalences and use the fact that provable equivalence is reflexive, symmetric and transitive.
  5. Prove that a formula is not derivable by means of a marking that the axioms and modus ponens preserve, and use it to explain the limit of Łukasiewicz's system in the language with a single connective and why a second rule is needed.

What a formal deductive system is

The previous unit built a language: it decided which strings of circles and disks are formulas, and nothing more. Now, a language by itself neither asserts nor proves anything; to prove, one needs, in addition, a starting point and a way of advancing. A formal deductive system therefore consists of three components: a formal language, which fixes the formulas; a set of axioms, formulas admitted without proof; and a set of rules of inference, which say which formula may be written on the basis of others already written. What is decisive is that all three are purely syntactic: to check that a formula is an axiom, or that a rule was applied correctly, it suffices to look at the strings, without asking what they mean. If this is so, a proof in a formal system can be checked mechanically, symbol by symbol, and all its value lies in that possibility.

It should be noted from the outset that an axiom is not here a “self-evident truth”, as in the old use of the word, but a formula chosen as a starting point. Whether the choice is a good one (whether the axioms are true in a sense that semantics will make precise, and whether they suffice to deduce everything that ought to be deduced) is a question about the system, which is answered by theorems about it and not by intuition: the unit on metatheory answers it, and the last section of this lesson shows that the question is not an idle one.

Axiom schemas and instances

The systems of propositional logic do not state their axioms one by one, because there are infinitely many of them, but by means of schemas: expressions of the metalanguage written with metavariables, such as (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). A schema is not a formula; it is a mould. An instance of the schema is the formula that results from substituting a formula for each metavariable in a uniform way: the same formula is substituted for all the occurrences of the same metavariable, although different metavariables may receive the same formula or different formulas.

ExampleInstances of a schema

With φ:=v1\varphi := v_{1} and ψ:=¬v2\psi := \neg v_{2}, the schema (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) gives the instance (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})); with φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) and ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}), it gives ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), because nothing prevents two metavariables from receiving the same formula. On the other hand, (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) is not an instance of that schema: the first and the last occurrence of φ\varphi would receive different formulas, and the substitution would not be uniform. Each instance, once the abbreviations are unfolded, is a string of circles and disks; the schema, by contrast, lives only in the metalanguage.