Proof Theory
 What are Proofs?
 Consistency
 Completeness
 Soundness
 Structural Proof
 Cut Elimination
 Interpolation
 Reverse Mathematics
 Proof Calculi
 Ordinal Analysis
 Things
 Interpetability
Should I seperate this out into a computability, logic, model theory, and proof theory notes?
https://en.wikipedia.org/wiki/Proof_theory
What are Proofs?
Consistency
https://en.wikipedia.org/wiki/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 https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
Completeness
Soundness
Structural Proof
Cut Elimination
Interpolation
Reverse Mathematics
https://en.wikipedia.org/wiki/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
https://en.wikipedia.org/wiki/Proof_calculus
###
Axioms
Axiom Schemes
https://en.wikipedia.org/wiki/Axiom_schema 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
https://en.wikipedia.org/wiki/Logical_harmony logical harmony. See notes of frank pfenning
Hilbert systems
https://en.wikipedia.org/wiki/Hilbert_system 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
https://en.wikipedia.org/wiki/Sequent_calculus
Left and Right rules. You are breaking down formula going up the inference rule
Natural Deduction
Ordinal Analysis
Transfinite induction https://en.wikipedia.org/wiki/Transfinite_induction Ordinals Order theoretic strength The Art of Measuring the Strength of Theories The Curious Dependence of Set Theory on Order Theory
https://en.wikipedia.org/wiki/Ordinal_analysis
Well Ordering
Things
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("zero")
Nat.declare("succ", ("pred", Nat))
Nat = Nat.create()
#Nat = Datatype("Nat", ["zero", "succ"])
print(Nat.succ(Nat.zero))
def induct(P):
# assert P.type == Nat > Bool ?
n = FreshConst(Nat)
return ForAll(n, Implies(P(Nat.zero), Forall(n, Implies(P(n), P(Nat.succ(n))))), Forall(n, P(n)))
inj = Function("inj", Nat, IntSort())
n = FreshConst(Nat)
axioms = [
inj(Nat.zero) == 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.data = {}
self.defns = {}
def induction(self, name, P): # make n a parameter?
n = FreshInt() # make n a nat?
self.data[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 self.data
s = Solver()
for lemma in lemmas:
s.add(self.data[lemma][1])
s.add(Not(th))
res = s.check()
if res == unsat:
self.data[name] = ("theorem", th, lemmas)
elif res == sat:
print(s.model())
raise Exception("Not a theorem")
else:
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)
self.data = ("definition", )
#self.data[name] = ("definition", th)
def axiom(name, th):
self.data[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 https://en.wikipedia.org/wiki/G%C3%B6del_numbering “arithmetization”
Sequences of numbers https://en.wikipedia.org/wiki/G%C3%B6del_numbering_for_sequences
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)))
print(quote(expr))
Quotation as a theoyr? HOL QE https://arxiv.org/abs/1802.00405 “Interesting. They keep things consistent by not allowing eval to occur inside of quotation. This is a kinda like adding Tsentences, 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 quasiquotes (standing for Godel coding)
”  Graham
lisp3
https://plato.stanford.edu/entries/truthaxiomatic/#TSent https://plato.stanford.edu/entries/quotation/
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
https://www.lesswrong.com/posts/ALCnqX6Xx8bpFMZq3/thecartoonguidetoloebstheorem cartoon guide to lob’s theorem
Undefinability of Truth
https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem
We can godel code statements. We cannot define the subset of coded statements that are true inside our system.
https://inferencereview.com/article/loebstheoremandcurrysparadox Löb’s Theorem and Curry’s Paradox
“Suppose you’ve got a theory (just like, a firstorder 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 nonconstructive 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
https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument
Godel Completeness
Godel Incompleteness
https://arxiv.org/pdf/2104.13792.pdf 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
https://en.wikipedia.org/wiki/LOOP_(programming_language) https://plato.stanford.edu/entries/recursivefunctions/
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 SecondOrder Arithmetic
Second Order Logic
Robinson Arithmetic (Q)
Weaker than Peano Airthemtic, Induction schema removed. Still a complex thing
Primitive Recursive Arithmetic
https://en.wikipedia.org/wiki/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
https://en.wikipedia.org/wiki/Tarski%E2%80%93Kuratowski_algorithm 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
https://en.wikipedia.org/wiki/Interpretability Reduction of one logic to another.
Uhhhh
https://github.com/neelkrishnaswami/proofchecker simple proof checker
Computability theory
https://en.wikipedia.org/wiki/Computability_theory
Binders
Many of this can be compiled to equivalent formula involving
Mu operator
Minimization operator. The least such that. https://en.wikipedia.org/wiki/%CE%9C_operator
epsilon operator
Hilbert Choice.
forall
exists
exists unique
Bounded quantification
lambda
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? https://www.cl.cam.ac.uk/~ad260/talks/oviedo.pdf Fixed point logic
comprehesion
You could consider ${x  phi(x) }$ it’s own kind of binder 
modal operators
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