Beginning Mathematical Logic
Notes

1. The Guide
2. Informal Set Theory
3. First-order logic
4. Second-order logic
- 4.1. A preliminary note on many-sorted logic
  - 4.1.1. Notation 1: many-sorted logic
  - 4.1.2. Notation 2: standard single-sorted FOL (revised version tho)
- 4.2. Second-order logic
5. Model theory
6. Arithmetic, computability, and incompleteness
7. Set theory, less naively
8. Intuitionistic logic
9. Elementary proof theory
10. Modal logics
11. Other logics?
12. Going further
13. Glossary
14. Natural Deduction (Huth, Michael and Ryan, Mark, 2004)
- 14.1. Rules for natural deduction (Transformation rules)
  - 14.1.1. Rules of Inference
  - 14.1.2. Rules of replacement

1. The Guide

2. Informal Set Theory

2.1. Sets: a very quick checklist

2.2. A note about naivety

2.3. Recommendations on informal basic set theory

2.4. Virtual classes, real sets

3. First-order logic

3.1. Propositional logic

3.1.1. Syntax

propositional ‘atomic’ wffs: \(\mathsf{P, Q, R}\), …
logical operators: \(\land, \lor, \to\) and \(\neg\)
always-false absurdity constant: \(\bot\)

3.1.2. Semantic

Interpretation (case) and argument

For a given language \(\mathcal{L}\), an interpretation, valuation, or case, is an assignment of semantic values (truth [T, or 1] or falsity [F, or 0]) to each formula of \(\mathcal{L}\). (classical two-valued semantics, for many-valued semantics, see here)

(Each formula is only assigned a single truth-value, an interpretation may be viewed as a function, whose domain is \(\mathcal{L}\), and range is its sets of semantic values \(\mathcal{V}=\{\mathsf{T, F}\}\)) ref
Propositional connective semantics
Semantic truth, validity, consequence

3.1.3. Truth-functional logic (zeroth-order logic):

(d) … It’s an early theorem that every truth-function can in fact be expressed using just a handful of connectives.

The most thoroughly researched branch of propositional logic: classical truth-functional propositional logic, in which formulas are interpreted as having precisely one of two possible truth values, the truth value of true or the truth value of false.

Principle of bivalence: the semantic principle / law of bivalence states that every declarative sentence expressing a proposition (of a theory under inspection) has exactly one truth value, either true or false. (Lou Goble, 2006)
Law of excluded middle: the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true.

3.1.4. crucial pair of definitions

tautology
A wff A from a propositional language is a tautology iff it is true on any assignment of values to the relevant atoms.

Also see:
- tautology
- (Peter Smith, 2004)
tautological entailment

A set of wffs \(\Gamma\) tautologically entails A iff any assignment of values to the relevant atoms which makes all the sentences in \(\Gamma\) true makes A true too.

regiment the idea of an argument’s being logically valid in virtue of the way the connectives appear in its premisses and conclusion.

3.1.5. formal deductive system

3.1.6. two quite different ways of defining

what makes for a deductively good argument in propositional classical logic:

We said that a set of premisses \(\Gamma\) tautologically entails the conclusion A iff every possible valuation which makes \(\Gamma\) all true makes A true. (That’s a semantically defined idea.) (tautological entailment)

We can now also say that \(\Gamma\) yields the conclusion A in your chosen proof-system \(S\) iff there is an S-type derivation of the conclusion A from premisses in \(\Gamma\). (This is a matter of there being a proof-array with the right syntactic shape.)

3.2. FOL basics

3.2.1. Syntax

3.2.2. quantified wffs

Socrates is wise.

\(\mathsf{Ws}\) (Names: lower case; properties and relations: upper case. The predicate-first syntax is conventional but without deep significance.)

(i) the formation of quatified sentences: \(\forall \mathsf{xWx}\) (Everyone x is such that x is wise)

Generalizing:

if \(\textit{A}(\mathsf{n})\) is a formula containing some occurrence(s) of the name ‘\(\mathsf{n}\)’. Quantified wffs: \(\forall \mathsf{x}\textit{A}(\mathsf{x})\) and \(\exists y\textit{A}(\mathsf{y})\)

3.2.3. Semantics

And here we treat properties etc. extensionally. In other words, we can think of a property as a set of objects from the domain, a binary relation as a set of pairs from the domain, and so on. (See Sets: a very quick checklist)

interpretation of an FOL language: (Also see Interpretation (case) and argument)
- (Names): Names are interpreted as denoting objects in the domain.
- one-place / intransitive [predicate]: ( Socrates ) is [wise] (\(\mathsf{Ws}\)), A one-place predicate gets assigned a property, i.e. a set of objects from the domain.
- two-place / transitive [predicate]: ( Romeo ) [loves] ( Juliet ) (\(\mathsf{Lrj}\)), a two-place predicate gets assigned a binary relation.
True
- \(\mathsf{Ws}\) will be true if, the object denoted by ‘\(\mathsf{s}\)’ is in the extension of \(\mathsf{W}\). (“Socrates” is in the extension of “Wise”)
- \(\mathsf{Lrj}\) will be true if the ordered pair of the objects denoted by ‘\(\mathsf{r}\)’ and ‘\(\mathsf{j}\)’ is in the extension of \(\mathsf{L}\). (The pair “Romeo” and “Juliet” is in the extension of “Love”)
“a new Big Idea”

p.18

3.2.4. a model

an interpretation which makes a set of the sentences true together.

define a semantic relation of entailment:

A set of FOL sentences \(\Gamma\) semantically entails A (\(\Gamma \models A\)) iff any interpretation which makes all the sentences in \(\Gamma\) true also makes the sentence A true – i.e., when any model for \(\Gamma\) is a model for A.

If \(\Gamma\) has no model, \(\Gamma\) semantically entails A for any A at all, including any contradiction.

3.2.5. the use of proof systems to warrant entailments

See note in Logic and computability, building a proof system is to mechanically check whether a purported proof really obeys the rules of the system.

3.2.6. sound and completeness

With propositional logic, our chosen proof system for FOL is SOUND and doesn’t give false positives; COMPLETE and doesn’t leaving us unable to derive some semantically valid entailments.

S is our FOL proof system, \(\Gamma\) is a set of sentences, A is a particular sentence, we need to show:

Soundness

If there is an S-proof of A from premisses in \(\Gamma\), then \(\Gamma\) does indeed semantically entail A. \(\Gamma \models A\) says that \(A\) is semantically entailed by \(\Gamma\).
Completeness

If \(\Gamma\) semantically entails A, then there is an S-proof of A from premisses in \(\Gamma\). \(\Gamma \vdash A\) says that there is a proof of \(A\) from \(\Gamma\);
Establish soundness and completeness

Is to prove \(\Gamma \vdash A\) iff \(\Gamma \models A\).
Two versions of completeness theorem

weaker: \(\Gamma\) is restricted to having only finitely many members (perhaps zero).

strong: allow \(\Gamma\) to be infinite.
Compactness theorem

The strong completeness theorem for FOL allows \(\Gamma\) to have an infinite number of members. This combination of facts immediately implies the compactness theorem for sentences of FOL languages:

Compactness theorem: If every finite subset of \(\Gamma\) has a model, so does \(\Gamma\).

3.3. A little more about types of proof-system

3.3.1. axiomatic logical system

Most of these books present other proof systems besides natural deduction such as axiomatic systems and tableau systems. Although natural deduction has the advantages of elegance and simplicity over axiomatic methods, there are few expositions of it in logic books aimed at a computer science audience. (Huth, Michael and Ryan, Mark, 2004)

Mini example
General idea of an axiomatized theory

A standard axiomatic system for FOL will include as axioms all wffs of the following shapes:

Ax1. \((A\to(B\to A))\)

Ax2. \(((A\to(B\to C))\to((A\to B)\to(A\to C)))\)

All instances of those two schemas will count as axioms. among the rules of inference for our system will be the modus ponens rule.
Informal deductive reasoning
ways of keeping track of the scope of assumptions
1. Fitch-style multi-colume layout (Frederic Brenton Fitch, 1952)
2. Gentzen-style tree layout (Gentzen style proof)
commonly used types of proof system
1. Old-school axiomatic systems.
2. (i) Natural deduction done Gentzen-style. (ii) Natural deduction done Fitch-style.
3. ‘Semantic tableaux’ or ‘truth trees’.
4. Sequent calculi.
5. Resolution calculi.
semantic tableaux

Begin instead by assuming the premisses are all true while the wanted conclusion is false.

3.4. Basic recommendations for reading on FOL

3.5. Some parallel and slightly more advanced reading

3.6. A little history (and some philosophy too)

3.7. Postscript: Other treatments?

4. Second-order logic

4.1. A preliminary note on many-sorted logic

Consider a scalar multiplication: \[a(\mathbf{v_1}+\mathbf{v_2})=a\mathbf{v_1}+a\mathbf{v_2}.\]

4.1.1. Notation 1: many-sorted logic

\[\forall a\forall \mathbf{v_1}\forall \mathbf{v_2}(\mathbf{v_1}+\mathbf{v_2})=a\mathbf{v_1}+a\mathbf{v_2}.\]

Allowing multiple independent domains of objects, with different sorts of variables restricted to running over the different domains.

4.1.2. Notation 2: standard single-sorted FOL (revised version tho)

Explicitly declare which domain a quantified variable is running over: \((\forall a:S)\) and \((\forall\mathbf{v}:V)\) (this means assign \(a\) to scalars, \(\mathbf{v}\) to vectors), then:

\[\forall \mathsf{x}\forall \mathsf{y}\forall \mathsf{z}((\mathsf{Sx}\land \mathsf{Vy}\land \mathsf{Vz})\to \mathsf{x(y+z)=xy+xz})\]

All variables \((\mathsf{x}, \mathsf{y}, \mathsf{z})\) are drawn from a single domain, without distinguishing between different domains based on sorts. Only predicates are used to simulate different “types” or “kinds” within this single-sorted system.

4.2. Second-order logic

Some terms for the language of second-order logic: (https://plato.stanford.edu/entries/frege-theorem/#S1)

object names: \(a, b, \dots\)
objects variables: \(x, y, \dots\)
n-place relation names: \(P^{n}, Q^{n}, \ldots \ \ \ (n\geq1)\)
n-place relation variables: \(F^{n}, G^{n}, \ldots \ \ \ (n\geq1)\)

Explanations:

Object names and variables denote a domain of objects;
n-place relation names and variables denote a domain of n-place relations;
Objects and relations are to be regarded as mutually exclusive domains.

4.2.1. (a) Principle of induction

(Ind 1) Take any numerical property \(X\); if (i) zero has property \(X\) and (ii) any number which has \(X\) passes it on to its successor, then (iii) all numbers must share property \(X\).

(Ind 2) Suppose \(\mathsf{P}\) is a formal one-place predicate and the prime indicates the successor function, then, this is how we expresse some particular instances of the induction principle in a FOL language:

\[\mathsf{(P0\land\forall x(Px\to Px^{'}}))\to\forall \mathsf{xPx}.\]

(Ind 3) The general principle of induction that applies to any numerical property in a formal language:

\[\mathsf{\forall X((X0\land\forall x(Xx\to Xx^{'}))\to\forall x Xx)}\]

Which formally renders (Ind1), they’re equivalent. The big \(\mathsf{X}\) quantification - second-order quantification, who quantifies over properties or sets, rather than merely over individual objects - is not available in standard FOL languages.

(Ind 4) For any arithmetical L-predicate \(A()\), simple or complex, the corresponding wff of the form \((A(0)\land \forall \mathsf{x}(A(\mathsf{x})\to A(\mathsf{x^{'}}))\to\forall\mathsf{x}A(\mathsf{x})\) is an axiom.

However, (Ind4) only tells us that, induction holds for those properties that can be expressed by some L-predicate \(A()\).

4.2.2. (b) Binary Relation

Definition
(i)

\[ \mathsf{R^3ab}=_{\mathbf{def}} \mathsf{\exists x_1 \exists x_2 \exists x_3(Rax_{1}\land Rax_{1}x_{2}\land Rax_{3}b)}. \]
(ii) construct an expression \(\mathsf{R}^{*}\) for the ancestral of the relation expressed by \(\mathsf{R}\). Consider the infinite set of wffs:
\[ \mathsf{\{\neg Rab, \neg R^{1}ab, \neg R^{2}ab, \neg R^{3}ab, \dots, \neg R^{n}ab, \dots, R^{*}ab\}} \]
- (X) every finite collection of these wffs has a model
- (Y) the whole infinite set of sentences doesn’t have a model (recall our Definition: “just when there is a finite chain of R-related steps from a to b.”)
(iii)

For first-order wffs we can’t have both (X) and (Y), according to the compactness theorem, i.e. if every finite subset of some set of sentences has model, then so does the whole set.

This means, \(\mathsf{R}^{*}\) cannot be construct from \(\mathsf{R}\) and FOL.
(iv) construct by second order logic

Notes entry: Frege’s Definition on Ancestral of a Relation R

4.2.3. (c) extend the syntax and semantics

Recall that in FOL, quantifying over objects is allowed, but not over properties, so the atomic sentence like \(A(n)\) (here \(n\) is an object) could be written as a quantified FOL sentence, \(\exists xA(x)\) or \(\forall xA(x)\) (here \(x\) is a variable).

In second-order logic, we take a formula \(A(\mathsf{P})\) containing some occurrences of the unary predicate \(\mathsf{P}\), then swap out the predicate for variable and then form a second-order quantified sentence of the form \(\forall\mathsf{X}A(\mathsf{X})\).

In particular, in first-order logic the quantifiers \(\forall\) and \(\exists\) always range over elements of the domain \(M\) of discourse. By contrast, second-order logic allows one to quantify over subsets of \(M\) and functions \(F\) mapping, say, \(M \times M\) into \(M\). (Third-order logic goes on to sets of functions, etc.) Weak second-order logic allows quantification over finite subsets of \(M\) and over natural numbers.

Barwise, Handbook of Mathematical Logic, p. 7.

The relation of semantic consequence for formulas,

Some formulas \(\Gamma\) semantically entail \(A\) just in case every interpretation that makes all of \(\Gamma\) true makes \(A\) true.

4.2.4. (d) Comparision

4.2.5. (e) second-order logic’s problem on semantic entailment

4.2.6. (f)

5. Model theory

6. Arithmetic, computability, and incompleteness

6.1. Logic and computability

6.2. Computable functions

6.3. Formal arithmetic

7. Set theory, less naively

8. Intuitionistic logic

9. Elementary proof theory

10. Modal logics

11. Other logics?

12. Going further

13. Glossary

13.1. formula / Well-formed formula (wff) / sentence

a grammatically correct finite sequence of symbols from a given alphabet that is part of a formal language. “woof”, or sometimes “wiff”, “weff”, or “whiff”

Lower-case letters are used to stand for formulas and upper-case letters are used for sets of formulas. (Huth, Michael and Ryan, Mark, 2004)

If the set of all wffs of a formal language \(L\) is exactly the same as the set of all wffs of a formal language \(L'\), then \(L\) is the same formal language as \(L'\). If not, not. (Geoffrey Hunter, 1971, p. 4)

13.2. \(\neg, \land, \lor, \to, \leftrightarrow\)

Negation (not), Conjuction (and), Disjunction (or), Implication (if), biconditional (iff)

13.3. atomic formulas / atomic sentences / simple sentences

Sentences contain no logical connectives nor quantifiers.

13.4. molecular formulas / molecular sentences / compound sentences

Sentences contain one or more logical connectives.

13.5. quantifiled formulas

Sentences contain one or more quantifiers.

13.6. iff

if and only if

13.7. tautology

A formula that is true regardless of the interpretation of its component terms, with only the logical constants having a fixed meaning.

Tautology is usually, though not always, used to refer to valid formulas of propositional logic.

A formula is satisfiable if it is true under at least one interpretation, and thus a tautology is a formula whose negation is unsatisfiable, which means it cannot be false.

\(S\) is a tautology: use double turnstile notation, \(\models S\)

13.8. entailment (Logical consequence)

13.9. universal quantification \(\forall\)

It expresses that a predicate can be satisfied by every member of a domain of discourse.

13.10. universal quantifier \(\forall x, \forall (x)\) or \((x)\)

13.11. existential quantification \(\exists\)

13.12. existential quantifier \(\exists x, \exists (x)\) or \((\exists x)\)

13.13. proof systems

13.14. natural deduction

Natural deduction was invented by (Gerhard Gentzen, 1969), and further developed by (Dag. Prawitz, 1965).

Also See SEP: Natural Deduction Systems in Logic. (Pelletier, Francis Jeffry and Hazen, Allen, 2024)

13.14.1. Notation

Gentzen’s tree notation (Gentzen style proof)
1. \(P\to Q\)
2. \(P\)
3. \(\therefore~Q\)
In Gentzen’s notation:

\[\frac{P \to Q,P}{Q}\]

Premises are shown above the inference line (syntactic consequence or deductive consequence, \(\vdash\)), separated by a comma. The conclusion is written below the inference line.

\(P\to Q,P\vdash Q\) (the turnstile notation for syntactic consequence, is of lower precedence than the comma)
Suppes–Lemmon notation (only for propositional logic)

See: Example 1.4, and 1.5 of (Huth, Michael and Ryan, Mark, 2004)

13.14.2. Propositional language syntax

13.15. Sequent

Suppose we have a set of formulas \(\phi_1, \phi_2, \phi_3, \dots, \phi_n\), which we will call premisses, and another formula, \(\psi\), which we will call a conclusion. By applying proof rules to the premises, we hope to get some more formulas, and by applying more proof rules to those, to eventually obtain the conclusion. This intention we denote by

\[\phi_1, \phi_2, \dots, \phi_n \vdash \psi .\]

This is called a sequent. (Huth, Michael and Ryan, Mark, 2004)

13.16. modus ponens

From Latin, “method of putting by placing”. The first to explicitly describe the argument form modus ponens was Theophrastus, along with modus tollens. (Bobzien, Susanne, 2020)

In propositional logic, also called as implication elimination.

\[\frac{\phi\quad\phi\to\psi}{\psi}\to e.\]

13.17. modus tollens

From Latin, “method of removing by taking away”. It is an application of the general truth that if a statement is true, then so is its contrapositive.

13.18. normal form (Daniel P. Friedman, David Thrane Christiansen, 2018, p. 13)

Normal Forms: Given a type, every expression described by that type has a normal form, which is the most direct way of writing it. If two expressions are the same, then they have identical normal forms, and if they have identical normal forms, then they are the same.

13.19. canonical expression (Daniel P. Friedman, David Thrane Christiansen, 2018, p. 22)

Different from normal form, a canonical form or a value specifies a unique representation for every object, while a normal form simply specifies its form, without the requirement of uniqueness.

Values: An expression with a constructor at the top is called a value (canonical expression).

For example, these expressions are not normal, they are values:

(add 1
  (+ (add1 zero)
     (add1
        (add1 zero))))

(add 1
  (+ (add1 zero) (add1 one)))

Values and Normal Forms: Not every value is in normal form. This is because the arguments to a constructor need not be normal. Each expression has only one normal form, but it is sometimes possible to write it as a value in more than one way.

13.20. constructor

Some expressions, \(\mathsf{Nat}\) or \((\mathsf{Pair\;Nat\;Atom})\), are types. Explaining a new type is to say how they constructed, i.e., what its constructors are.

The constructor of \(\mathsf{Nat}\) are \(\mathsf{zero}\) and \(\mathsf{add1}\), the constructor of \(\mathsf{Pair}\) is \(\mathsf{cons}\).

13.21. Gentzen style proof

Gentzen’s method for natural deduction – his \(\mathcal{N}\) calculi – were given in a tree format with occurrences of formulas appearing as nodes of the tree. (Pelletier, Francis Jeffry and Hazen, Allen, 2024)

First introduced in his doctoral thesis of 1933.

13.22. Jaśkowski style proof

See more: 2.1 Gentzen and Jaśkowski

13.23. transitive closure

The transitive closure \(R^+\) of a homogeneous binary relation \(R\) on a set \(X\) is the smallest (w.r.t \(\subseteq\)) relation \(R^{+}\) on \(X\) that contains \(R\) and is transitive: \(R\subseteq R^+\)

\(R^+ = R\) iff \(R\) itself is transitive.

14. Natural Deduction (Huth, Michael and Ryan, Mark, 2004)

Example 1.1 If the train arrives late and there are no taxis at the station, then John is late for his meeting. John is not late for his meeting. The train did arrive late. Therefore, there were taxis at the station.

Example 1.2 If it is raining and Jane does not have her umbrella with her, then she will get wet. Jane is not wet. It is raining. Therefore, Jane has her umbrella with her.

If \(p\) and not \(q\) , then \(r\) . Not \(r\). \(p\). Therefore, \(q\).

The sequent* for Examples 1.1 and 1.2: \(p \land \neg q \to r, \neg r, p \vdash q\)

Example 1.4 Prove that \(p \land q, r \vdash q \land r\) is valid.

(This is a Jaśkowski style proof)

Example 1.6 Prove that \((p \land q) \land r, s \land t \vdash q \land s\).

14.1. Rules for natural deduction (Transformation rules)

14.1.1. Rules of Inference

Conjunction introduction (and-introduction)

\[\frac {\phi \quad \psi}{\phi \land \psi} \; \land i.\]
Conjunction elimination (and-elimination)

\[\frac{\phi\land\psi}{\phi} \land e_1 \qquad \frac{\phi\land\psi}{\psi} \land e_2.\]
eliminating implication (implies-elimination, arrow-elimination, modus ponens or conditional elimination)

\[\frac{\phi\quad \phi\to\psi}{\psi}\to e.\]
MT (modus tollens)

\[\frac{\phi\to\psi\quad \neg\psi}{\neg\phi}\quad\text{MT}.\]
implies introduction (conditional introduction, arrow-introduction, or Conditional proof (CP))

We can think of \(p\to q\) as a type of a procedure. Showing \(p\to q\) using the rule \(\to i\) is now called type checking, an topic in the construction of compilers for typed programming languages. (Huth, Michael and Ryan, Mark, 2004)

Formulate the rule \(\to i\) as:

Note that the line immediately following a closed box has to match the pattern of the conclusion of the rule that uses the box.

Example 1.9. Prove that \(\neg q\to\neg p \vdash p \to \neg\neg q\)
1. \(p \to p\)
  
  \(\vdash p \to p\): the argumentation for \(p \to p\) does not depend on any premises at all.
  
  Logical formulas \(\phi\) with valid sequent \(\vdash \phi\) are theorems. (Huth, Michael and Ryan, Mark, 2004, Definition 1.10)
reductio ad absurdum / argumentum ad absurdum / apagogical arguments (proof by contradiction (PBC), Indirect Proof (IP), negation introduction (−I), negation elimination (−E))

Latin for “reduction to absurdity” and “argument to absurdity”. The form of argument that attempts to establish a claim by showing that the opposite scenario would lead to absurdity or contradiction.

If from \(\neg\phi\) we obtain a contradictionm, then we are entiled to deduce \(\phi\):

14.1.2. Rules of replacement

Double negation (elimination and introduction)

\[\frac{\neg\neg\phi}{\phi}\quad \neg\neg e\qquad \frac{\phi}{\neg\neg\phi}\quad \neg\neg i.\]

Beginning Mathematical Logic Notes

Table of Contents