13 citations · 50 across the 19 of their papers we have counts for
5 papers · 1 filter
Arithmetic, Infinite Trees, and Second-order Subsystems: Notes and Observations
David M. Cerna
Work in progress concerning alternative formalizations of arithmetic.
Taking a Detour to Zero: An Alternative Formalization of Functions Beyond PR
David M. Cerna
There are two well known systems formalizing total recursion beyond primitive recursion (\textbf{PR}), system \textbf{T} by Gödel and system \textbf{F} by Girard and Reynolds. syst…
A Generalized Resolution Proof Schema and the Pigeonhole Principle
David M. Cerna
The schematic CERES method is a method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can be thought of as a way…
Total Recursion over Lexicographical Orderings: Elementary Recursive Operators Beyond PR
David Cerna
In this work we generalize primitive recursion in order to construct a hierarchy of terminating total recursive operators which we refer to as {\em leveled primitive recursion of o…
Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]
David Cerna, Alexander Leitsch
In previous work, an attempt was made to apply the schematic CERES method [8] to a formal proof with an arbitrary number of Π 2 cuts (a recursive proof encapsulating the infinitary…