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.

Systems can’t prove themselves consistent (?) You need more “power”

Gentzen proved peano arith consistent



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 logical harmony. See notes of frank pfenning

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

Transfinite induction Ordinals Order theoretic strength The Art of Measuring the Strength of Theories The Curious Dependence of Set Theory on Order Theory

Well Ordering


Peano Arithmetic

Axiom schema vs second order axiom.

Or are you in a second order system and tracking Are peano axioms conditions for an embedding in a larger system, or are hey

Peano embedded in term of ZF theory.

inductive pterm where
  | Add : pterm -> pterm -> pterm
inductive pform where
  | Eq : pterm -> pterm -> pform
inductive pproof where
 | Induct : (pterm -> pform) -> 

from z3 import *
# Z3py adt of natural numbers
Nat = Datatype("Nat")
Nat.declare("succ", ("pred", Nat))
Nat = Nat.create()
#Nat = Datatype("Nat", ["zero", "succ"])

def induct(P):
  # assert P.type == Nat -> Bool ?
  n = FreshConst(Nat)
  return ForAll(n, Implies(P(, Forall(n, Implies(P(n), P(Nat.succ(n))))), Forall(n, P(n)))

inj = Function("inj", Nat, IntSort())
n = FreshConst(Nat)
axioms = [
  inj( == 0,
  ForAll(n, inj(Nat.succ(n)) == inj(n) + 1) # recursive definition of inj

theorem1 = ForAll(n, inj(n) >= 0)
theorem2 = ForAll(i, Implies(i >= 0, Exist(n, inj(n) == i)))
P = lambda x: 

from z3 import *

def Peano():
  def __init__(self): = {}
    self.defns = {}
  def induction(self, name, P): # make n a parameter?
    n = FreshInt() # make n a nat?[name] = Implies(And(P(0), Forall([n],Implies(P(n), P(n+1)))), ForAll(n, P(n)))
  def theorem(self, name, th, *lemmas):
    assert name not in
    s = Solver()
    for lemma in lemmas:
    res = s.check()
    if res == unsat:[name] = ("theorem", th, lemmas)
    elif res == sat:
      raise Exception("Not a theorem")
      raise Exception("Unknown")
  def definition(self, name, args, res, th):
    assert name not in self.defns
    self.theorem(name + "_total", ForAll(args, Exist(res, th)))
    self.theorem(name + "_unique", ForAll(args, Forall([res, res2], Implies(And(th, th2), res == res2))))
    self.defns[name] = (args, res, th) = ("definition", )[name] = ("definition", th)
  def axiom(name, th):[name] = ("axiom", th)

Godel numbering

Quotation - see note on macros?

We can encode syntax as a number. The details don’t matter that much except you need to be concrete to make sure things are working “arithmetization”

Sequences of numbers

inference rules

from z3 import *
import functools
import z3.z3consts as z3consts
Formula = Datatype("Formula")
Formula.declare("FAnd", ("arg0", Formula), ("arg1", Formula))
Formula.declare("FOr", ("arg0", Formula), ("arg1", Formula))
Formula.declare("FNot", ("arg0", Formula))
Formula.declare("FBoolLit", ("arg0", BoolSort()))
Formula.declare("FAtom", ("arg0", StringSort()))
Formula = Formula.create()

# match on z3 ast and return a Formula
# This is a metalevel (python) function that observese syntax
def quote(expr):
  match expr.decl().kind():
    case z3consts.Z3_OP_AND:
      return functools.reduce(Formula.FAnd, map(quote, expr.children()))
    case z3consts.Z3_OP_OR:
      return Formula.FOr(quote(expr.arg(0)), quote(expr.arg(1)))
    case z3consts.Z3_OP_NOT:
      return Formula.FNot(quote(expr.arg(0)))
    case z3consts.Z3_OP_TRUE:
      return Formula.FBool(True)
    case z3consts.Z3_OP_FALSE:
      return Formula.FBool(False)
    case z3consts.Z3_OP_UNINTERPRETED:
      return Formula.FAtom(String(expr.decl().name()))
    case _:
      raise Exception("Unknown", expr)
a,b,c = Bools("a b c")
expr = And(a,b,Or(c,Not(c)))

Quotation as a theoyr? HOL QE “Interesting. They keep things consistent by not allowing eval to occur inside of quotation. This is a kinda like adding T-sentences, that say “the sentence ‘P’ is true iff P”, for each sentence P that doesn’t contain the predicate “is true”, but at the level of an evaluation rule rather than as a bunch of new axioms. I wonder what other theories of truth you could lift into evaluation rules? For modal logic with quotes, there’s provability logic, which is a modal logic where the box is supposed to mean “P is provable (in some formal system)”. The big adequacy results for that involve translating the box into a first order sentence of arithmetic (or something similar) that you’d write with quasi-quotes (standing for Godel coding)

” - Graham


if we have formula objects, we really can make a relation R over them representing a single step of inference. Then standard translation of modal logic and provability logic cartoon guide to lob’s theorem

Undefinability of Truth

We can godel code statements. We cannot define the subset of coded statements that are true inside our system. Löb’s Theorem and Curry’s Paradox

“Suppose you’ve got a theory (just like, a first-order one for simplicity, FOL + some designated relations and function symbols maybe, and some axioms. Peano Arithmetic for example), that can represent its own syntax, in some sense, so that you’ve got a kind of “quotation function” ⌜:black_small_square:⌝ in the metalanguage such that for every sentence φ of the of the theory, there’s some term ⌜φ⌝ in the language of the theory (usually built up in some kind of systematic way, like with Godel numbering). Then Tarskian truth is roughly some predicate T such that T(⌜φ⌝) :left_right_arrow: φ. The English language equivalent is the fact that the sentence “snow is white” is true if and only if snow is white. For any reasonably strong theory and reasonably simple quotation function, the theory ends up being able to reason enough about quotation that, for every definable predicate ψ of the language of the theory, there’s some sentence φ of the language of the theory such that the theory proves φ :left_right_arrow: ψ(⌜φ⌝). (The fact that these biconditionals are always provable is the “diagonal lemma” - Gödel figured it out, Carnap wrote down the general pattern). You can’t define a Tarskian truth predicate in any model of the theory T (this is stronger than just the Tarski biconditionals not being provable). Suppose you could define a predicate T in some model M of your theory such that, for every sentence φ of the language of T, M satisfies T(⌜φ⌝) :left_right_arrow: φ. Then ¬T(x) would also be a definable predicate, and you’d have a sentence L (for liar) such that ¬T(⌜L⌝) :left_right_arrow: L was provable in T, and satisfied by M. In that situation, ¬T(⌜L⌝) ↔ L (by diagonal lemma) ↔ T(⌜L⌝) (by T a truth predicate) But ¬T(⌜L⌝) :left_right_arrow: T(⌜L⌝) is unsatisfiable so it can’t be true in M. Hence you can’t define a predicate T like that.

This gives you a slick non-constructive proof of Godel’s first incompleteness theorem. If every truth of arithmetic were provable by PA, then “provable by PA” would be a definable truth predicate in the standard model of PA. But truth isn’t definable in the standard model of PA. Therefore, not every truth of arithmetic is provable by PA. “ - graham

Diagonal Argument

Godel Completeness

Godel Incompleteness A Mechanised Proof of G¨odel’s Incompleteness Theorems using Nominal Isabelle - Paulson

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

A comprhenesion axiom schema and inducton axioms schema

Subsystems of second order arithmetic - simpson The Prehistory of the Subsystems of Second-Order Arithmetic

Second Order Logic

Robinson Arithmetic (Q)

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

Primitive Recursive Arithmetic

Arithmetic Hierarchy

Formula (logically) equivalent to one using some particular combo of quantifiers.

Logically equivalent is with respect to a particular model.

Proof algoirthm to get upper bound. Finding upper bound is easy. Basically, convert the formula to prenex form (put quantifiers in front). This can be done algorithmically. 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


Interpetability Reduction of one logic to another.

Uhhhh 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