ZFC + inference rules

[100 yrs old]

Halting can be thought of as a lowest term in some sequence (?)

Order relation <-> function

?? Is the Ackermann function

Paris-Harrington : not provable in PA

https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem
https://www.cs.umd.edu/~gasarch/TOPICS/largeramsey/bovINTRO.pdf
Proof structure :
total function [ every pair of elements has a definite ordering ]
well founded ordering
http://www.joostjjoosten.nl/papers/ModelsForGLPLambda.pdf

What is the simplest WL function that PA can’t prove will always terminate?

If you can’t prove halting in system X, does it mean you’re universal over system X?

Intermediate degrees: solution of Post’s problem
Computational irreducibility wrt elementary number theory....
Halting specifically is a question of computational unboundability

Computational complexity for tag system?

PSPACE ??

What do TS’s that are universal look like?