nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqw9kjj2cu9q6vtvg5m9j9szkl0z9fvcxfxc93aeamrvgl9fjtjjuswyz2n3 (nprofile…z2n3) Answering your question, part II.
The "ordinal strength" of Gödel's system T is ε₀.
This is the first ordinal such that ε₀. = ω^ε₀.
Intuively, ε₀ = ω^ω^⋯ forever.
But you can restrict the higher-type "recursion" constant of system T to type level ≤ n, to get system Tₙ.
Then the ordinal strength of Tₙ is ω^ω^⋯ω n-times.
So, by the above,
(1) Ackermann is definable in T₂.
(2) T₂ can define much more than Ackerman, in fact any function that is provably total using induction up to ω^ω, not just ω², which is all what Ackermann needs.
Read William Tait's papers for the strength of system T, including it's stratified levels.
I could find a specific reference for the minumum ordinal to prove the totality of the Ackermann function. Search engines give lot of garbage. But I am sure *many* papers proved that already beginning from the time the Ackermann function was defined.
nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqknzsux7p6lzwzdedp3m8c3c92z0swzc0xyy5glvse58txj5e9ztqt54hp5 (nprofile…4hp5) nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpq5m29pdfzjm5zj3hhjs7zm329cwlrxwjr4mvl607vw0yxd8kdrjmscms7d2 (nprofile…s7d2)
Martin Escardo
npub1t3…fg3z4
2026-01-30 19:37:01 UTC
in reply to nevent1q…23uw
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4Seen on
wss://relay.ditto.pubPublished at
2026-01-30 19:37:01 UTCEvent JSON
{
"id": "c44f95af8e8451ff32ad5b858c7f3ff4f29dfb83e7b3b9feccafce7bbb1a76f9",
"pubkey": "5c675fe7561c52f2c0ea8db391d2c3a46556bec9a3c0a4b4f10f234fe03f58ca",
"created_at": 1769801821,
"kind": 1,
"tags": [
[
"p",
"716d292b1c2834c5b114d964580adf788a9660c9360b1ee7bb1b11f2a64b94b9",
"wss://relay.ditto.pub"
],
[
"p",
"b4c50e1bc1d7c4e1372d0c767c4705509f070b0f3109447d90cd0eb34a992896",
"wss://relay.ditto.pub"
],
[
"p",
"a6d450b52296e82946f7943c2dc545c3be333a43aed9fd3fcc73c8669ecd1cb7",
"wss://relay.ditto.pub"
],
[
"p",
"65d4e39aa72b601fc99e66c5d6152300f33fac494b05f837adf9bfa789fe36a3",
"wss://relay.ditto.pub"
],
[
"p",
"f7346eb283902ada9d21c109a93e83128d9f87d8fcfe70ad819b3bf2ad9bce16",
"wss://relay.ditto.pub"
],
[
"p",
"6d285f1e8895fd62ed11f194efe2ce8357b2ab01d77a7060cd8708410fb2477c",
"wss://relay.ditto.pub"
],
[
"e",
"5ea791fae4e9e3e73b83b537ea59fb445fa44838eda89402367f450acdc174b6",
"wss://relay.ditto.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/MartinEscardo/statuses/115985732171534131",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqw9kjj2cu9q6vtvg5m9j9szkl0z9fvcxfxc93aeamrvgl9fjtjjuswyz2n3 Answering your question, part II.\n\nThe \"ordinal strength\" of Gödel's system T is ε₀.\n\nThis is the first ordinal such that ε₀. = ω^ε₀.\n\nIntuively, ε₀ = ω^ω^⋯ forever. \n\nBut you can restrict the higher-type \"recursion\" constant of system T to type level ≤ n, to get system Tₙ.\n\nThen the ordinal strength of Tₙ is ω^ω^⋯ω n-times.\n\nSo, by the above,\n\n(1) Ackermann is definable in T₂.\n\n(2) T₂ can define much more than Ackerman, in fact any function that is provably total using induction up to ω^ω, not just ω², which is all what Ackermann needs.\n\nRead William Tait's papers for the strength of system T, including it's stratified levels.\n\nI could find a specific reference for the minumum ordinal to prove the totality of the Ackermann function. Search engines give lot of garbage. But I am sure *many* papers proved that already beginning from the time the Ackermann function was defined.\n\nnostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqknzsux7p6lzwzdedp3m8c3c92z0swzc0xyy5glvse58txj5e9ztqt54hp5 nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpq5m29pdfzjm5zj3hhjs7zm329cwlrxwjr4mvl607vw0yxd8kdrjmscms7d2",
"sig": "5d3651405f98577acffcbe90ba944e7a41cd0623b60510dccbc765bda2987fc5c7f8e140eaf78abc5860ca79450c9f09f00cefda2de838a7977a3434e7c8621c"
}