Például a bizonyítás "definíciójában" (ahogyan ők mondják) nem hivatkozhatunk magára a bizonyításra, mert az már nem primitív rekurzív.


Mármint a finit bizonyításelmélet megalapozásánál. Ők tehát azt mondják, hogy ha van egy bizonyítás-típusom, akkor más bizonyításokkal, vagy önmagával nem igazolhatom, csak a primitív rekurzív aritmetikával.

Kreisel, a neves logikus egyébként másfajta finitizmust képviselt, szerinte a PA-bizonyítható rekurzív függvények finitek, és ez jóval erősebb rendszer.

Kreiselhez kötődik a Kreisel-sejtés. Ez a következő.

Legyen PA|-F(n), minden n-re, és a levezetéshossz mindig legfeljebb k!
Akkor PA|-'minden x F(x)'.