The non-constructive μ operator, fixed point theories with ordinals, and the bar rule

https://doi.org/10.1016/S0168-0072(00)00016-6Get rights and content
Under an Elsevier user license
open archive

Abstract

This paper deals with the proof theory of first-order applicative theories with non-constructive μ operator and a form of the bar rule, yielding systems of ordinal strength Γ0 and ϕ20, respectively. Relevant use is made of fixed-point theories with ordinals plus bar rule.

MSC

03F03
03F05
03F10
03F35

Keywords

Applicative theories
Theories with ordinals
Non-constructive μ-operator
Bar rule

Cited by (0)