Related papers: Proofs that Modify Proofs
Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof…
We propose developing the theory of consequences of morasses relevant in mathematical applications in the language alternative to the usual one, replacing commonly used structures by families of sets originating with Velleman's neat…
We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of…
Ordinal analysis is a research program wherein recursive ordinals are assigned to axiomatic theories. According to conventional wisdom, ordinal analysis measures the strength of theories. Yet what is the attendant notion of strength? In…
There are two major generalizations of the standard ordinal analysis: One is Girard's $\Pi^1_2$-proof theory in which dilators are assigned to theories instead of ordinals. The other is Pohlers' generalized ordinal analysis with Spector…
Walsh [MR4525964, Zbl 1569.03151] has shown that comparing proof-theoretic ordinals is equivalent to comparing $\Pi^1_1$-consequence comparison and $\Pi^1_1$-reflection comparison, all modulo true $\Sigma^1_1$-sentences. In this paper, we…
Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these…
Justification theory is an abstract unifying formalism that captures semantics of various non-monotonic logics. One intriguing problem that has received significant attention is the consistency problem: under which conditions are…
Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for…
The theory of operads (May, cyclic, modular, PROPs, etc) is extended to include higher dimensional phenomena, i.e. operations between operations, mimicking the algebraic structure on varieties of arbitrary dimensions, having marked…
We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a k-tuple of input nodes to represent a…
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is…
We propose a novel approach for studying rooted trees by using functions that we will call descent functions. We provide a construction method for rooted trees that allows to study their properties through the use of descent functions.…
The consistency of a second-order version of a theorem of Morley on the number of countable models was proved in arXiv:2107.07636 with the aid of large cardinals. We here dispense with them.
Existing ordinal trees and random forests typically use scores that are assigned to the ordered categories, which implies that a higher scale level is used. Versions of ordinal trees are proposed that take the scale level seriously and…
Exhibiting an explicit Boolean function with a large high-order nonlinearity is an important problem in cryptography, coding theory, and computational complexity. We prove lower bounds on the second-order, third-order, and higher-order…
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions…
We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity,…
In this article we provide an intrinsic characterization of the famous Howard-Bachmann ordinal in terms of a natural well-partial-ordering by showing that this ordinal can be realized as a maximal order type of a class of generalized trees…
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting…