In any nonstandard model of Peano arithmetic, the standard part is not first order definable. But we show that in some model the standard part is definable as the unique solution ...
We apply Mints' technique for proving the termination of the epsilon substitution method via cut-elimination to the system of Peano Arithmetic with Transfinite Induction give...
We aim at a conceptually clear and technical smooth investigation of Ackermann's substitution method. Our analysis provides a direct classification of the provable recursive ...
We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The form of witness terms in cut-free p...
Programs and Abstract Complexity A. Beckmann University of Wales Swansea Swansea, UK Axiom systems are ubiquitous in mathematical logic, one famous and well studied example being ï...
Showing termination of the Battle of Hercules and Hydra is a challenge. We present the battle both as a rewrite system and as an arithmetic while program, provide proofs of their t...
We give a combinatorial proof of a tight relationship between the Kanamori-McAloon principle and the Paris-Harrington theorem with a number-theoretic parameter function. We show th...