Skip to content
Topos Uranos
English

Logic and deductions

Summary

This lesson teaches how to write logic with LaTeX so that it serves equally those who study mathematics, computer science or philosophy. It distinguishes the connective of the object language from the arrow of the metalanguage and presents the connectives with their variants, the notations of other traditions (the horseshoe, the tilde, the dot and Polish notation) and the advantage of one command of one's own per connective; it fixes the spacing of quantifiers; it typesets sets in set-builder notation and explains why the keyboard bar and \mid are not spaced alike; it gathers the symbols of metalogic, sequents and modal logic, with the package that defines each one; it typesets truth tables with array; it builds natural deduction trees with bussproofs, whose stack logic explains its errors, and Fitch boxes with logicproof; it sets out arguments in standard form with numbered premises and a conclusion; and it ends with what is best avoided, with the real logs of each error.

Learning objectives

  1. Choose between the connective of the object language and the arrow of the metalanguage, and among \models, \vdash, \equiv and \Leftrightarrow, according to what the formula asserts.
  2. Predict the spacing of quantifiers, sets in set-builder notation and negations with a tilde, and correct the slips that produce no warning at all.
  3. Define one command per connective and explain which change of tradition it allows and which it does not.
  4. Build natural deduction trees with bussproofs by following the state of its stack, and diagnose their errors from the log.
  5. Typeset a truth table and an argument in standard form, and choose between a tree and a Fitch box for a given proof.

Two levels of language

A text on logic always speaks on two levels. There is an object language, that of the formulas under study, with its connectives and its quantifiers; and there is a metalanguage, the author's, which asserts things about those formulas: that one is deducible from others, that two are equivalent, that one is true in every model. The notation must keep both levels apart, because an arrow in the wrong place is not a typographical slip but a different assertion. This lesson assumes the symbols and operators of the lesson on symbols and notation and the environments of the lesson on theorems and proofs; here we study what is specific to logic. Whoever wants the theory that these notations express will find it in the course Mathematical Logic I: Propositional Logic.