Sciweavers

Share
APAL
2011

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

8 years 3 months ago
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.
Gerhard Jäger, Dieter Probst
Added 12 May 2011
Updated 12 May 2011
Type Journal
Year 2011
Where APAL
Authors Gerhard Jäger, Dieter Probst
Comments (0)
books