The Suslin operator in applicative theories: Its proof-theoretic analysis via ordinal theories

The Suslin operator E1 is a type-2 functional testing for the wellfoundedness of binary relations on the natural numbers. In the context of applicative theories, its proof-theoretic strength has been analyzed in J¨ager and Strahm [18]. This article provides a more direct approach to the computation of the upper bounds in question. Several theories featuring the Suslin operator are embedded into ordinal theories tailored for dealing with non-monotone inductive definitions that enable a smooth definition of the application relation.

• Type: Journal
• Year: 2011
• Where: APAL
• Authors: Gerhard Jäger, Dieter Probst
• Keywords: APAL 2011, Non-monotone Inductive Definitions, Software Engineering, Suslin Operator, Type-2 Functional Testing