Related papers: Proofs that Modify Proofs
We provide mutual elementary recursive order isomorphisms between classical ordinal notations, based on Skolem hulling, and notations from pure elementary patterns of resemblance of order $2$, showing that the latter characterize the…
In this paper it is shown that higher order quasiconvex functions suitable in the variational treatment of problems involving second derivatives may be extended to the space of all matrices as classical quasiconvex functions. Precisely, it…
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for…
Working with generating functions, the combinatorics of a recurrence relation can be expressed in a way that allows for more efficient calculation of the quantity. This is true of the Catalan numbers for an ordered binary tree…
The following is an introduction to the study of higher walks, by which we mean a family of higher-dimensional extensions of Todorcevic's method of walks on the ordinals. After a brief review of this method, including, for example,…
We describe an approach to modelling and reasoning about data-centric business processes and present a form of general model checking. Our technique extends existing approaches, which explore systems only from concrete initial states.…
Permutation rational functions over finite fields have attracted high interest in recent years. However, only a few of them have been exhibited. This article studies a class of permutation rational functions constructed using trace maps on…
A folk theorem says higher order arithmetic has the proof theoretic strength of set theory with limited power set. This paper makes the theorem precise in terms of several axiom system based on ZF.
This thesis is intended to provide an account of the theory and applications of Operational Methods that allow the "translation" of the theory of special functions and polynomials into a "different" mathematical language. The language we…
We show that Morley's theorem on the number of countable models of a countable first-order theory becomes an undecidable statement when extended to second-order logic. More generally, we calculate the number of equivalence classes of…
Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure…
We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted…
We formulate a well-posedness and approximation theory for a class of generalised saddle point problems. In this way we develop an approach to a class of fourth order elliptic partial differential equations using the idea of splitting into…
The class of type-two basic feasible functionals ($\mathtt{BFF}_2$) is the analogue of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments.…
Monadic Second-Order Logic (MSO) extends First-Order Logic (FO) with variables ranging over sets and quantifications over those variables. We introduce and study Monadic Tree Logic (MTL), a fragment of MSO interpreted on infinite-tree…
An interactive theorem prover, Isabelle, is under development. In LCF, each inference rule is represented by one function for forwards proof and another (a tactic) for backwards proof. In Isabelle, each inference rule is represented by a…
G\"odel's second incompleteness theorem is standardly understood as showing that no sufficiently strong, consistent theory of arithmetic can prove its own consistency, a result typically interpreted against a model-theoretic background in…
The arithmetic of the natural numbers can be extended to arithmetic operations on planar binary trees. This gives rise to a non-commutative arithmetic theory. In this exposition, we describe this arithmetree, first defined by Loday, and…
Here it is shown that standard set theory can be interpreted in a theory about order. The ordering here is about non-extensional flat classes, i.e. classes that are not elements of classes. So, stipulating a nearly well order over all those…
This dissertation is a contribution to the project of second-order set theory, which has seen a revival in recent years. The approach is to understand second-order set theory by studying the structure of models of second-order set theories.…