Searcharxiv⌕ Search

arXiv subjects

David M. Cerna

Publications and source records attributed to David M. Cerna.

23 records · Page 2Linked to original sources
arXiv2018

Taking a Detour to Zero: An Alternative Formalization of Functions Beyond PR

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. system \textbf{T} defines recursion on typed objects and can construct every function of Heyting arithmetic (\textbf{HA}). System \textbf{F} introduces type variables which can define the recursion of system \textbf{T}. The result is a system as expressive as second-order Heyting arithmetic (\textbf{HA}$_{2}$). Though, both are able to express unimaginably fast growing functions, in some applications a more flexible formalism is needed. One such application is CERES cut-elimination for schematic \textbf{LK}-proofs ($CERES_{s}$) where the shape of the recursion is important. In this paper we introduce a formalism for fast growing functions without a type theory foundation. The recursion is indexed by ordered sets of natural numbers. We highlight the relationship between our recursion and the Wainer hierarchy to provide an comparison to existing systems. We can show that our formalism expresses the functions expressible using system \textbf{T}. We leave comparison to system \textbf{F} and beyond to future work.

cs.LO↗
arXiv2017

Integrating a Global Induction Mechanism into a Sequent Calculus

Most interesting proofs in mathematics contain an inductive argument which requires an extension of the LK-calculus to formalize. The most commonly used calculi for induction contain a separate rule or axiom which reduces the valid proof theoretic properties of the calculus. To the best of our knowledge, there are no such calculi which allow cut-elimination to a normal form with the subformula property, i.e. every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a variant of LK-proofs able to simulate induction by linking proofs together. There exists a schematic normal form which has comparable proof theoretic behaviour to normal forms with the subformula property. However, a calculus for the construction of proof schemata does not exist. In this paper, we introduce a calculus for proof schemata and prove soundness and completeness with respect to a fragment of the inductive arguments formalizable in Peano arithmetic.

math.LO↗
arXiv2017

Clausal Analysis of First-order Proof Schemata

Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called proof links to the standard first-order LK-calculus. Proof links allow proofs to reference proofs thus giving proof schemata a recursive structure. Unfortunately, applying reductive cut- elimination is non-trivial in the presence of proof links. Borrowing the concept of lazy instantiation from functional programming, we evaluate proof links locally allowing reductive cut-elimination to proceed past them. Though, this method cannot be used to obtain cut-free proof schemata, we nonetheless obtain important results concerning the schematic CERES method, that is a method of cut-elimination for proof schemata based on resolution. In "Towards a clausal analysis of cut-elimination", it was shown that reductive cut-elimination transforms a given LK-proof in such a way that a subsumption relation holds between the pre- and post-transformation characteristic clause sets, i.e. the clause set representing the cut-structure of an LK-proof. Let CL(A') be the characteristic clause set of a normal form A' of an LK-proof A that is reached by performing reductive cut-elimination on A without atomic cut elimination. Then CL(A') is subsumed by all characteristic clause sets extractable from any application of reductive cut-elimination to A. Such a normal form is referred to as an ACNF top and plays an essential role in methods of cut-elimination by resolution. These results can be extended to proof schemata through our "lazy instantiation" of proof links, and provides an essential step toward a complete cut-elimination method for proof schemata.

math.LO↗
arXiv2016

A Generalized Resolution Proof Schema and the Pigeonhole Principle

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 to circumvent the addition of an induction rule to the LK-calculus. In this work, we formalize a schematic version of the Infinitary Pigeonhole Principle (IPP), in the LKS-calculus, and analyse the extracted clause set schema. However, the refutation we find cannot be expressed as a resolution proof schema because there is no clear ordering of the terms indexing the recursion, every ordering is used in the refutation. Interesting enough, the clause set and its refutation is very close to a canonical form found in cut elimination of LK-proofs. Not being able to handle refutations of this form is problematic in that proof schema, when instantiated, are LK-proofs. Based on the structure of our refutation and structural results, we develop a generalized resolution proof schema based on recursion over a special type of list, and provide a refutation, using our generalization, of the clause set extracted from our formal proof of IPP. We also extract a Herbrand System from the refutation.

cs.LO↗