Introduction

This course will use a material written by J.Carlström. It can be downloaded by

https://bimsa.net/doc/notes/logic2008.pdf

Syllabus

Day 1 Introduction

• History and purpose of logic.

• Boolean algebras.

Inductively defined sets (Ch. 3 of Carlström)

• Motivation: What is formal syntax? What are formulas?

• The natural numbers; recursion and induction principles

• General inductively defined sets; their recursion and induction principles

• Example: binary trees

Suggested Exercises: Carlström exercises 3.2.28, 3.2.29.

Day 2 Propositional logic (Ch. 4)

• Syntax: the inductively defined set of propositional formulas

• Interpretation of formulas as truth-value

• Semantics: valuations, interpretations, tautologies

• Logical equivalence and entailment.

Suggested exercises: Any from Ch. 4, especially 4.1.6, 4.2.32, 4.2.34, 4.2.37, 4.2.41

Day 3 Natural deduction (Ch. 5)

• Rules of natural deduction

• Notation: φ1, φ2, … φn ⊢ ψ

• Formal definition of derivations, derivability;

Suggested exercises: any from Ch. 5, especially 5.2.4, 5.2.7, 5.3.6–10, 5.4.4, 5.6.1, 5.6.3, and 5.6.6 (this one is a bit more challenging than the rest).

Day 4 Soundness Theorem (Ch. 6)

• Statement of Soundness Theorem (6.1.5): connection between derivability and validity in interpretations

• Proof of soundness

Suggested exercises: any from Ch.6, especially 6.1.22, 6.1.25, 6.1.28, 6.1.34, 6.1.38, 6.3.4

Day 5 Applications of Soundness (Ch. 6)

• Theories and consistency

• Proofs vs countermodels

Suggested exercises: any from Ch.6, especially 6.1.22, 6.1.25, 6.1.28, 6.1.34, 6.1.38, 6.3.4

NOTE: For now, we’re skipping Ch.7, Normalization. We may come back to it later in the course, if time allows

Day 6 Completeness (Ch. 8)

• Statement of completeness

• Statement of model existence lemma

• Roadmap to proof of completeness

• Maximal consistency

Suggested exercises: 8.1.3, 8.1.14, 8.1.17, 8.2.1, 8.2.6, 8.2.7

Day 7 Predicate Logic (Ch.9)

• Concept, examples: languages/theories of groups, posets, arithmetic

• Arity types (aka signatures, etc.)

• Terms, Formulas

• Substitution

• Free/bound occurrences of variables

Suggested exercises: 9.1.15, 9.1.17, 9.1.19, 9.2.7.

Day 8 Semantics (Ch. 10)

• Structures for signatures; valuations of variables.

• NOTE: we define/notate interpretations slightly differently from Carlström — we consider the valuation of variables v as separate from the structure 𝒜, not a part of 𝒜 as in Carlström.

• Interpretation of terms and formulas, 

Suggested exercises: Any from Ch. 10

Day 9 Semantics (Ch. 10), cont’d

• Lemma: interpretation of a term/formula depends only on its free variables

• Notations, terminology: A,v ⊨ φ, etc.

Simplifications (Ch. 11)

• Definition of “bound for”, “free for” (OBS: confusing terminology — this is completely different from “bound in”, “free in”!)

• Lemmas on interpretation of substitutions

Day 10 Natural deduction for predicate logic (Ch. 12)

• New rules for predicate logic

• Rules for equality

• Rules for quantifiers

• Heuristics for derivations in predicate logic

• Useful building-block derivations

Soundness for predicate logic (Ch. 13)

• Statement + proof outline

Suggested exercises: Any from Ch. 12; especially 12.1.6, 12.1.12, but also all from §12.2 are good. For finding derivations: practice, practice, practice!

Day 11 Soundness (Ch. 13)

• Proof of soundness for predicate logic

• Adaptation of outline to predicate setting

• Cases for the new rules

Suggested exercises: Any from Ch. 13.

Day 12 Completeness (Ch. 14)

• Outline of proof: model existence lemma, constructing model from suitable theory

• Maximal consistency and the existence property

• Any maximally consistent theory with the existence property has a model

• Any consistent theory has (up to variable-renaming) a maximally consistent extension with the existence property

Suggested exercises: proof of 14.1.3, 14.1.4, 14.1.5, 14.1.15, 14.2.16.