On the Relationship Between Takeuti's Ordinal Diagrams O(n) and Schütte's System of Ordinal Notations Σ(n)

摘要: Publisher Summary This chapter investigates the relationship between Takeuti's ordinal diagrams O ( n ) and Schute's system of notations Σ ). Takeuti defined for each positive integer n, a that consists formal expressions called “ordinal diagrams” together with +1 well-orderings these expressions. It was showed consistency certain subsystem simple type theory by assigning to proof figures arguing transfinite induction on diagrams, cuts can be eliminated from proofs. The even more extensive subsystems using infinite order has been proved. A *( an identity is described, clauses in definition are not compatible presence identity, modified.