Buchholz ψ analyzer

About this program

This program analyzes Buchholz ψ function defined in Buchholz (1986). When the user gives an ordinal term a ∈ T, as defined in the reference, the program determines if a ∈ OT. If a ∉ OT, b ∈ OT (o(a) = o(b)) is suggested. For example:

Input: D1(D0(0),D1(D4(0)),D3(D0(0)))
a = D1(D0(0),D1(D4(0)),D3(D0(0)))
where a ∈ T, a ∉ OT. Showing b ∈ OT where o(a) = o(b):
b = D1(D3(D0(0)),D2(0))
o(a) = o(b) = ψ1(ψ3(ψ0(0))+ψ2(0))
 = ψ1(ψ3(1)+ψ2(0))

Input string

Examples

• D0(D1(Dw(0)),0(0))
• D0(D0(D2(0)),D0(0))
• D2(D0(D4(0)),D3(0),D6(D3(D6(0))))
• D0(D3(0),D1(D2(0)),D0(0))
• 0(1(2),w(3))
• 0(1(2(0)),0(0))
• 0(w,1(2(0
• w#3
• 1#w
• ψ0(ψω(0)#1)

Rules

• Input a ∈ T as shown in the reference
• D, ψ, ' ' are neglected
• # is regarded as ,
• natural numbers are analyzed
• w and ω are regarded as ω
• ) is added at the end if needed

Reference

Buchholz, W. (1986): A New System of Proof-Theoretic Ordinal Function. Annals of Pure and Applied Logic, 32:195-207.

Buchholz ψ analyzer 1.0 by Fish