The substitution method revisited

MaRDI QIDQ3001106zbMATH OpenFDO

Authors W. W. Tait

Publication date 31 May 2011

zbMATH Keywords

\(\varepsilon\)-termSkolem functionsubstitution method

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Recursive ordinals and ordinal notations (03F15) First-order arithmetic and fragments (03F30)

Recommendations

• scientific article; zbMATH DE number 1870415
• Epsilon substitution method for elementary analysis
• Epsilon substitution for first- and second-order predicate logic
• A termination proof for epsilon substitution using partial derivations
• Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX

Cited in

(9)

• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus
• Point-free substitution
• Ackermann's substitution method (remixed)
• scientific article; zbMATH DE number 3849199 (Why is no real title available?)
• The Substitution Vanishes
• scientific article; zbMATH DE number 1078590 (Why is no real title available?)
• A categorical interpretation of the intuitionistic, typed, first order logic with Hilbert's -terms
• A simplified proof of the epsilon theorems

This page was built for publication: The substitution method revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3001106)