#### ZFC + inference rules

ZFC + inference rules

[100 yrs old]

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

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

#### Order relation <-> function

Order relation <-> function

#### ?? Is the Ackermann function

?? Is the Ackermann function

#### Paris-Harrington : not provable in PA

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

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?

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?

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?

Computational complexity for tag system?

PSPACE ??

### What do TS’s that are universal look like?

What do TS’s that are universal look like?