Syllabus of Mathematical Logic I

Purpose

Every course in mathematics requires proving, and every course in philosophy requires arguing; now, none of them makes reasoning itself its object, and all of them take for granted what it means for a conclusion to follow from some premises. This course takes that question as its subject. Its purpose is to construct, for the simplest language of logic, the first complete mathematical theory whose object is reasoning, with its four pieces in view: a language, whose formulas are recognized and read without ambiguity; a calculus, which produces deductions without attending to the meaning of the signs; a meaning, which assigns to each formula its truth value under each valuation of its variables; and the proof that the calculus and the meaning coincide.

If this is so, the course is not a collection of rules for manipulating symbols, but a theory with a central result, the completeness theorem, which everything before it prepares. For a set of formulas $\Gamma$ and a formula $\varphi$, derivability $\Gamma \vdash \varphi$ says that there is a finite sequence of formulas, constructed with axioms and rules, that ends in $\varphi$; semantic consequence $\Gamma \models \varphi$ says that every valuation that makes the formulas of $\Gamma$ true makes $\varphi$ true. The two relations arise from opposite ideas, the one syntactic and existential, the other semantic and universal; the course proves, however, that $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$. It follows that every question about what follows from some premises can be answered from whichever side turns out to be easier: by exhibiting a deduction, by running through a table or, as the last content lesson teaches, by refuting by resolution.

Intended students and prior knowledge

The course is intended for those beginning studies in mathematics, computer science or philosophy, and for anyone who, at any stage of their education, wants to know exactly what a proof is and why it can be trusted: students starting university mathematics who stumble over proofs, computer science students who need the logic of circuits, of programs and of satisfiability problems, and philosophy students who want to move from the logic of arguments to its theory.

It is a level 1 course, with no prerequisites and self-contained. It does not assume having studied logic, knowing set theory or ever having proved a theorem. What it uses of sets (membership, inclusion, union, sets of formulas), of functions (a valuation is a function from the variables to $\{0, 1\}$), of strings of signs and of induction it teaches where it needs it: sets and strings, in the lesson of unit 1 on the language, and induction, in the following lesson, before using it. It assumes only two things: careful reading, because in a formal language one sign added or omitted changes the string, and the elementary arithmetic of the natural numbers, which in this course, as on the rest of the site, begin at $1$.

Where it leads

From the above follows the place of the course on the site. It has no prerequisites and is a goal of three programs of study, Mathematics, Computer Science and Philosophy, because in all three reasoning is at once instrument and object. It has three complementary courses, which can be followed before, in parallel or afterward, in any order. Aristotelian Logic studies the logic of terms and the syllogism, whose validity depends on words such as “all” and “some”, which this course leaves out, and shows from which tradition the calculus was reached. Algebra and Geometry I raises a deductive edifice from the Peano axioms, and puts into practice, on numbers, the axiomatic method and the induction that this course studies as its object; its plan recommends having studied this course first, or studying it in parallel. Programming in C++ I, finally, puts into practice what is theory here: deciding whether a string is well formed, running through a truth table, calculating a normal form or searching for a refutation are procedures that can be written as programs.

Now, the course leaves open a question of expression: its language cannot say “all” or “some”, and the formalization of English arguments loses, from unit 1 onward, the quantifiers. Therefore, its planned continuation is Mathematical Logic II, devoted to predicate logic, which will travel the same road with quantifiers and with variables that range over objects: it will preserve soundness, completeness and compactness, with methods that this course anticipates, but in it consequence will cease to be decidable.

Global learning objectives

The following objectives describe what those who complete the course should be able to do. Each is formulated as an observable performance, so that it can be checked with a concrete task; each content lesson, in turn, states its own objectives, which serve one or more of the global ones, and the closing lesson shows in which units and lessons each one is worked on. The seven objectives are numbered so that they can be cited.

1. Objective 1. Distinguish the object language from the metalanguage, and decide with the formation rules whether a string is a formula.
2. Objective 2. Formalize statements and arguments of natural language, pointing out what formalization preserves and what it loses.
3. Objective 3. Construct deductions in the course system (Łukasiewicz's axioms, modus ponens and the replacement of double negation), combining axioms, primitive rules and derived rules.
4. Objective 4. Prove metatheorems by induction on the natural numbers, on the complexity of formulas and on the length of deductions.
5. Objective 5. Decide semantic validity, satisfiability, consequence and equivalence, with truth tables and with equivalences.
6. Objective 6. Transform formulas into normal forms and express truth functions and circuits with them.
7. Objective 7. Explain and apply soundness, completeness and compactness, and decide unsatisfiability by resolution.

Objectives 3 and 7 each have their own unit, deduction and metatheory; objectives 5 and 6 share the unit on semantics, the former in its first half, the latter in the second. Objective 2 has a lesson of its own, the one on formalization, and is exercised afterward every time a problem is posed in words. Objectives 1 and 4, by contrast, are transversal: the distinction between what is said within the language and what is said about it runs through the four units, and induction is the form of all the important proofs of the course, from the unique readability of formulas to the soundness of the system and Kalmár's lemma. It follows that their achievement cannot be attributed to a single lesson, and that they should be cultivated throughout the whole course.

The course system and its decisions

A course in propositional logic can be built in many ways, and the usual texts differ in the language, in the primitive connectives and in the deductive system. This course makes three decisions that are worth knowing from the start, because they explain what may, at first sight, seem strange.

A language of circles and disks

The language of the course has an alphabet of only two signs, the circle $\sigO$ and the disk $\sigI$. The $n$th variable is the string of $n$ circles followed by a disk, $v_{n} = \sigO^{n}\sigI$, so that $v_{1} = \sigO\sigI$ and $v_{2} = \sigO\sigO\sigI$; and there is a single formation rule: if $\varphi$ and $\psi$ are formulas, so is $\sigI\varphi\psi$, which is abbreviated $(\varphi \downarrow \psi)$ and read “neither $\varphi$ nor $\psi$”. Joint denial $\downarrow$ is therefore the only primitive connective, and all the others are abbreviations defined once and for all: $\neg\varphi$ is $(\varphi \downarrow \varphi)$, the disjunction $(\varphi \vee \psi)$ is $\neg(\varphi \downarrow \psi)$, and from them conjunction, implication, the biconditional and exclusive disjunction are defined. Any other way of writing them is a theorem, which is proved, and not a definition.

The choice has a price, readability, which the course pays in the metalanguage: no one writes strings of circles and disks every day, but rather their abbreviated names, which can be unfolded at any moment into the string they designate. Now, it pays off many times over. Two signs suffice for infinitely many variables, so that every formula is a finite string over a two-element alphabet. The connective is written in front of its arguments, and for that reason no parentheses are needed: unique readability is proved with a weight argument, which assigns $+1$ to each variable and $-1$ to each connective disk. And since every compound formula is a joint denial, each proof by induction on complexity has a single compound case, which shortens all those of the following units. That a single connective suffices to express any other is not assumed: the unit on semantics proves it.

A second primitive rule

The deductive system starts from that of Jan Łukasiewicz: three axiom schemas, written with negation and implication, and modus ponens as the only rule. Those schemas were formulated for languages whose primitive connectives are negation and implication; in the language of circles and disks, a formula such as $(v_{1} \downarrow v_{2})$ is neither the one nor the other, and for the axioms it is opaque. The first lesson of the unit on deduction proves, with a marking that all the axioms have, that modus ponens preserves and that the formula lacks, that Łukasiewicz's system does not derive $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$.

If this is so, the system must be completed, and the natural remedy seems to be to prove double negation, $\varphi \dashv\vdash \neg\neg\varphi$, which the second lesson deduces from the three schemas. The marking shows that this is not enough: the theorems of double negation preserve it and yet, even with them, $v_{1}$ cannot be changed into $\neg\neg v_{1}$ inside a joint denial. Therefore, after proving double negation, the second lesson adds a second primitive rule, the replacement of double negation: from a formula $\chi$ one infers the formula that results from replacing in it one occurrence of a subformula $\theta$ by $\neg\neg\theta$, or one occurrence of $\neg\neg\theta$ by $\theta$. The course system thus consists of Łukasiewicz's three schemas, modus ponens and this rule.

Other systems for joint denial obtain the same with axiom schemas made to measure. The course prefers a rule for two reasons: it is even simpler than modus ponens, because it takes a single line and changes a single occurrence, and there is nothing artificial about it, because it expresses what double negation already says, that $\theta$ and $\neg\neg\theta$ are interchangeable, extended to every place in a formula. It is, moreover, sound, because it preserves the truth value of each line, and it preserves the deduction theorem, with one more case in its proof. That with it everything that should be derivable is derivable is the completeness theorem of the last unit.

Compactness before strong completeness

Completeness comes in three degrees: the weak one says that every tautology is a theorem; the finite one, that every consequence of a finite set of premises is derivable from it; the strong one, that the same holds for an arbitrary set, infinite ones included. The method of the course, Kalmár's lemma, works with the finitely many variables of a formula and with finite premises, and for that reason reaches the first two degrees and not the third. To reach it, it suffices that, if $\Gamma \models \varphi$, some finite part $\Gamma_{0}$ of $\Gamma$ already satisfies $\Gamma_{0} \models \varphi$; now, that is precisely what the compactness theorem asserts.

Many texts first prove strong completeness by another method and deduce compactness from it. In this course, by contrast, strong completeness is what is being sought, and obtaining compactness from it would be circular. Hence the order is reversed: the lesson on compactness proves it within semantics, without mentioning any deduction, by fixing the values of $v_{1}, v_{2}, \ldots$ one by one, and only afterward, in three lines, obtains strong completeness, that is, $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ for every set $\Gamma$.

Contents

The course is organized in six units: this overview, four content units and a closing. Each content unit opens with an introduction lesson, which presents its lessons, its place in the course, what it takes for granted and the problem it solves, and begins with an entry assessment; it closes with a synthesis lesson, which reconstructs the deductive chain of the unit, links it to the rest of the course, repeats in an exit assessment the skills of the entry assessment and sets six challenges harder than the problems of the lessons.

Unit 0. Course overview

It consists of this lesson, which sets out the purpose, the global objectives, the decisions, the contents, the workload and the design of the course.

Unit 1. Language

Its objective is to build the language that the course studies, to prove that each formula is read in only one way and to link it with the arguments of English.

1. Language: introduction.
2. What is mathematical logic: validity as opposed to truth, the counterexample, the paradoxes and the distinction between object language and metalanguage.
3. The language of propositional logic: sets and strings, the language of circles and disks, its formation rule and its abbreviations.
4. Induction on the natural numbers and on formulas: simple, strong and structural induction, the weight lemma, unique readability and definitions by recursion.
5. Formalization of natural language: the dictionary, the translation of statements and arguments, and what the material conditional loses.
6. Language: synthesis and challenges.

Unit 2. Deduction

Its objective is to give the language a calculus, the course system, and to derive in it, once each, the forms of reasoning that mathematics uses without naming them.

1. Deduction: introduction.
2. Formal deductive systems: Łukasiewicz's system, deduction with premises, the deduction theorem and the marking that shows its limit.
3. Four deduction techniques: hypothetical syllogism, interchange of premises, double negation, contraposition and the replacement of double negation.
4. The symmetries of the connectives: the fundamental lemma of joint denial, the replacement of equivalents, the equivalent forms of disjunction and conjunction, and their five symmetries.
5. The techniques of classical logic: the rules of each connective, excluded middle, proof by cases and reductio ad absurdum, with premises.
6. De Morgan’s laws and the distributive laws: their proofs in both directions and the replacement of equivalents inside other formulas.
7. Deduction: synthesis and challenges.

Unit 3. Semantics

Its objective is to give the formulas a meaning, to decide validity and consequence with it, and to reduce every formula to normal forms.

1. Semantics: introduction.
2. Semantics of propositional logic: valuations and their extension by recursion, the coincidence lemma, truth tables, validity and satisfiability.
3. Semantic consequence and equivalence: consequence from sets, the semantic deduction theorem, replacement and uniform substitution.
4. Generalized De Morgan and distributive laws: conjunctions and disjunctions of $n$ terms and their laws, by induction.
5. Functional completeness: every truth function has a formula, joint denial suffices on its own, and adequate sets of connectives.
6. Normal forms: literals, clauses, disjunctive and conjunctive forms, their duality and their existence.
7. The normal form algorithm and its applications: a correct and terminating algorithm, and the design and simplification of switching circuits.
8. Semantics: synthesis and challenges.

Unit 4. Metatheory

Its objective is to prove that deduction and consequence coincide, first for finite premises and then for arbitrary premises, and to offer a third way of deciding them.

1. Metatheory: introduction.
2. Soundness and completeness: soundness by induction on the lines, consistency, Kalmár's lemma and weak and finite completeness.
3. The compactness theorem: its semantic proof, its equivalent forms, the strong completeness that follows from it and its combinatorial applications.
4. The resolution method: clausal form, the resolution rule, its soundness and its refutation completeness, and its cost.
5. Metatheory: synthesis and challenges.

Unit 5. Course closing

It consists of the lesson Final review of Mathematical Logic I, which recalls the seven global objectives, shows in a figure in which units and lessons each one is worked on, gathers by objective the first attempt at the exit assessments and points to where study continues.

Workload and credits

The workload of a course is not measured by contact hours, which do not exist in an asynchronous course, but by the total work of the person studying it: reading, following the proofs and the deductions, solving problems and reviewing. The estimate follows the same method in every course on the site: it counts the reading time of the text of each lesson at one hundred words per minute, counting each formula as one word, twenty minutes per solved problem, thirty-five per proposed problem, forty-five per challenge and twelve per entry or exit assessment, and adds a margin of one tenth for review.

Results

The lessons of the course contain in all $90$ solved problems, $90$ proposed problems and $24$ challenges, as well as eight unit assessments. The estimated workload per unit, rounded to the hour, is as follows:

• Unit 0, course overview: less than $1$ hour.
• Unit 1, language: $30$ hours.
• Unit 2, deduction: $36$ hours.
• Unit 3, semantics: $43$ hours.
• Unit 4, metatheory: $25$ hours.
• Unit 5, course closing: less than $1$ hour.

The total is about $137$ hours of work. This figure should be read for what it is: an estimate for those who study every proof and solve every problem and challenge. Those who have already studied logic, or who limit themselves to the proposed problems without tackling the challenges, will need considerably less; those who have never proved a theorem may need more, above all in the units on deduction and semantics, which are also the longest.

Now, the figure is nominal: it is the one that sets the credits of the course, and it assumes reading at a constant pace and three quarters of an hour per challenge. Until it is measured with real students, it should be accompanied by a realistic range. If reading proceeded at half the assumed pace, as happens when each deduction is copied out with pencil and paper and each string of circles and disks is decomposed by hand, and each challenge required seventy-five minutes instead of forty-five, the same method would give about $174$ hours. Therefore, the workload to be expected lies between about $137$ and about $174$ hours. The upper end is a prudent bound, not a measurement; the range will be corrected once the time spent by those who study the course is known, and until then the credits are calculated with the nominal figure.

Suggested pace

To name the paces, this plan uses the same criterion as the site's other plans: full-time study is that of an academic year of $60$ credits, about $1650$ hours spread over some forty weeks, that is, about $40$ hours a week, and half-time is half of that, about $20$ hours a week. From this follows a recommended pace of one sixteen-week semester, with about $8$ or $9$ hours of study a week, somewhat more than a fifth of full-time study; with the realistic range, from $9$ to $11$ hours a week. That semester can be shared with Algebra and Geometry I, whose proofs are read better when deduction is already a familiar object.

An intensive pace, of about $20$ hours a week, that is, half-time, completes the course in seven weeks. A more relaxed pace, of about $4$ or $5$ hours a week, stretches it over two semesters, which divide it almost in halves: units 0 to 2, language and deduction, take about $67$ hours, and units 3 to 5, semantics, metatheory and the closing, about $69$.

Equivalence in transferable credits

Transferable credit systems measure a course by the total work it requires of the person taking it, not by the hours of classroom teaching, so that studies completed at one institution can be recognized at another. The European Credit Transfer and Accumulation System, adopted by European universities following the Bologna Declaration, assigns $60$ credits to a full-time academic year and sets each credit at between $25$ and $30$ hours of work. The Chilean Transferable Credit System, adopted by Chilean universities with an analogous design, likewise assigns $60$ credits to the academic year and sets each credit at between $24$ and $31$ hours of work.

Now, dividing the estimated $137$ hours by the ends of each interval, the course is equivalent to about $5$ European credits (from 4.6 to 5.5), and to between $4$ and $6$ Chilean transferable credits (from 4.4 to 5.7). Taking as reference the central value of both intervals, 27.5 hours per credit, both systems give the same number, 4.98, which is rounded to 5. For European credits, the number $C$ of credits is bounded as follows:

Therefore, it is recommended that the course be assigned $5$ European credits and $5$ Chilean transferable credits, that is, one twelfth of a full-time academic year, somewhat less than an ordinary one-semester subject of six credits.

Course design

Mode of study

The course is asynchronous, online and self-paced: it has no dates, live sessions or deadlines, and each student progresses at the speed that their preparation and their time allow. It is offered in the site's fourteen languages, with the same logic in all of them: the formulas, the deductions and the steps of the proofs are identical in each version, and only the text is translated. The lessons state which other lessons should be studied first, so that the recommended order is explicit.

The structure of a lesson

All content lessons follow the same structure. They begin with a summary and a list of their own learning objectives, formulated as observable performances. Then comes the theory, with the definitions, the results stated precisely and their proofs, and the examples. Proofs are presented as step-by-step players: each step writes a line, highlights what changes and, when it relies on an earlier result, goes back to it. Deductions in the system are written with their numbered lines and the justification of each on the right (an axiom, a premise, modus ponens with the lines it uses, or a derived rule), and as one advances the cited lines are highlighted. The lesson closes with five solved problems, with their step-by-step solution, and five proposed problems, each with a folded hint and, after it, the final answer; the proposed problems that ask for a proof add, folded after the answer, a worked solution, which should be opened only after writing one's own.

Each lesson can also be listened to aloud with the site's reader, which pronounces in words the signs of the formulas, including the circle, the disk and the signs of deduction and of consequence.

Assessment

The course does not grade: its assessment is formative and rests on self-assessment. The proposed problems make it possible to check the achievement of the objectives of each lesson, and the challenges, that of the objectives of each unit. To this are added the unit assessments: the entry assessment, at the beginning of the introduction, measures the starting point with eleven to fifteen questions, because to those of the unit it adds some about what the unit takes for granted; the exit assessment, in the synthesis and before the challenges, measures what has been achieved with twelve questions and is compared with the entry assessment. Both are corrected in the browser itself, with an explanation for each answer and a reference to the lesson worth reviewing; their results are stored only in the browser of the person who answers them, and the final review gathers the first attempt at each exit assessment into a profile by global objective.

How to study this course

The course is designed to be studied in order. Each unit presupposes the previous ones: deduction is written in the language of the first, semantics gives a value to its formulas, and metatheory compares the second with the third; skipping a lesson means, sooner or later, going back to it.

In each lesson, it is advisable to read the summary and the objectives first; then to study the theory with pencil and paper, copying out the strings of circles and disks, separating their variables and their disks, and anticipating each line of a deduction before the player writes it; to attempt the solved problems before looking at their solution, and to solve the proposed ones without help, opening the hint only when one's own attempt is exhausted. A problem whose answer was consulted before attempting it has not been solved, but read.

Finally, it is advisable always to distinguish what level each assertion belongs to: whether it says something within the language, like a formula, or something about it, like $\Gamma \vdash \varphi$ or $\Gamma \models \varphi$. That distinction, which is the first of the objectives of the course, is also the one that makes it possible to understand its central result, which can only be stated in the metalanguage.