Should I seperate this out into a computability, logic, model theory, and proof theory notes?

What are Proofs?

Consistency It is surprisingly subtle and difficult to make a reasoning system in which you don’t end up being able to prove everything A system is consistent if you can’t prove “false” in it.



Structural Proof

Cut Elimination


Reverse Mathematics Proof mining. You can take proofs, which are things (annotated trees basically?), and extract interesting content from them.

Determine which axioms are required to prove theorems. Often subsystems of second order arithmetic (peano arithmetic with set objects)

Proof Calculi ###


Axiom Schemes Axiom schemes are axioms that have pattern variables in them that stand for arbitrary formula. They represent an infinite class of axioms.

They can be represented as Formula -> Bool, a checker that the formula you give is an instance of the schema. Or to make life even easier for your checker Bindings -> Formula -> Bool. In principle they may also be represented as Stream Formula a possibly infinite stream of formula, but this is inconvenient to wait until you get the formula you want. All of these things are actually not the same. The first is saying it is decidable whether a formula is an instance of the axiom schema, the second is saying it is semidecidable. Maybe the second is not actually an axiom schema.

Common axiom schema:

  • Induction in Peano Arithemtic
  • Set comprehension

Axiom schema are sort of a macro system thing that lets you avoid second order logic

Rules of Inference

Hilbert systems Many axioms, few rules of inference. These are often presented as something like a sequence of steps, each being dignified by referring to the results of previous steps

Sequent Calculus

Left and Right rules. You are breaking down formula going up the inference rule

Natural Deduction

Ordinal Analysis


Peano Arithmetic

Heyting Arithmetic

PRA (Primitive Reucrsive Arithemtic)

Equivalent to Godel’s system T? People tend to imply lambda binders available when discussing T

Gentzen’s consistency proof reduced peano arithmetic to PRA

Axiom schema of induction but only over unquantified formula. All the axiom can be expressed in unquantified logic?

In a sense, because quantifier free, theorems are all universally quantified.

Second Order Arithmetic

“Analysis” Two sorts, natrual numbers a la peano and sets of natural numbers

Second Order Logic

Robinson Arithmetic (Q)

Weaker than Peano Airthemtic, Induction schema removed. Still a complex thing

Primitive Recursive Arithmetic

Set Theory

ZFC Richard Borcherd lectures on zfc


Von Neumann–Bernays–Gödel set theory

Finite axiomatization? As in no schema? That’s crazy. metamath is all schemata?

Arithmetic Hierarchy

Formula equivalent to one using some particular combo of quantifiers. Proof algoirthm to get upper bound. Finding upper bound is easy Finding lower bound may be hard.

These are considered “sets” because importantly, these are not closed formula. An unclosed formula can be considered a set via the axiom schema of comprehension ###

Undefinability of Truth

Godel Completeness

Godel Incompleteness

Interpetability Reduction of one logic to another.


Transfinite induction Ordinals simple proof checker

Computability theory


Many of this can be compiled to equivalent formula involving

Mu operator

Minimization operator. The least such that.

epsilon operator

Hilbert Choice.



exists unique

Bounded quantification


recursion/fixpoint binder

In type theory, we want to talk about recursive types. We use a fixpoint binder. How does this relate to logic? Least fixed point? Greatest? Fixed point logic


You could consider ${x | phi(x) }$ it’s own kind of binder

Of a different character?

Sum, product, min, argmin, integral If I understand the history, Boole arithmetized logic and the exists and forall operators were actually inspired by actual sum and product

Model thoery

gentle introduction to model theory Model theory is more informal? I have thought model theory is finding what logic looks like in informal set theory A more general notion and precise notion may be finding homomorphisms between . A way of mapping statements to each other such that theorems in one theory are theorems in the other.

finite model theory notes dan suciu

Finite Model Theory Finite model theory is actually interesting. Finite models are those for which Z3 can return results even in the prescence of quantifiers.