Related papers: How to escape Tennenbaum's theorem
We make use of generalized iterations of Jensen forcing to define a cardinal-preserving generic model of ZF for any $n\ge 1$ and each of the following four Choice hypotheses: (1)…
Peano Arithmetic is known to be provably equivalent to reflection over Elementary Arithmetic. We prove a characterization of Predicative Analysis in the guise of ATR0 in terms of stronger reflection principles.
General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent generations quickly. What structure enables this, and how might…
In a recent paper, Kaye and Wong proved the following result, which they considered to belong to the folklore of mathematical logic. THEOREM: The first-order theories of Peano arithmetic and ZF with the axiom of infinity negated are…
This paper presents a formal theory of Krivine's classical realisability interpretation for first-order Peano arithmetic ($\mathsf{PA}$). To formulate the theory as an extension of $\mathsf{PA}$, we first modify Krivine's original…
The present paper shows meta-programming turn programming, which is rich enough to express arbitrary arithmetic computations. We demonstrate a type system that implements Peano arithmetics, slightly generalized to negative numbers. Certain…
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's…
In this note, we present a puzzle. We prove that Zermelo-Fraenkel set theory is inconsistent by proving, using Zermelo-Fraenkel set theory, the false statement that any algorithm that determines whether any $n \times n$ matrix over $\mathbb…
We consider the foundational relation between arithmetic and set theory. Our goal is to criticize the construction of standard arithmetic models as providing grounds for arithmetic truth (even in a relative sense). Our method is to…
A special final coalgebra theorem, in the style of Aczel's, is proved within standard Zermelo-Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions.…
A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other…
This work uses mostly model-theoretic methods to establish new proof-theoretic theorems about several axiomatic theories of truth over KP (Kripke-Platek set theory) and stronger theories, especially ZF (Zermelo-Fraenkel set theory).
This paper outlines new paradigms for real analysis and computability theory in the recently proposed non-Aristotelian finitary logic (NAFL). Constructive real analysis in NAFL (NRA) is accomplished by a translation of diagrammatic concepts…
This paper presents a new representation of natural numbers and discusses its consequences for computability and computational complexity. The paper argues that the introduction of the first Peano axiom in the traditional definition of…
In this paper, we build Fidel-structures valued models following the methodology developed for Heyting-valued models; recall that Fidel structures are not algebras in the universal algebra sense. Taking models that verify Leibniz law, we…
This article reformulates the theory of computable physical models, previously introduced by the author, as a branch of applied model theory in first-order logic. It provides a semantic approach to the philosophy of science that…
A process algebra is proposed, whose semantics maps a term to a nondeterministic finite automaton (NFA, for short). We prove a representability theorem: for each NFA $N$, there exists a process algebraic term $p$ such that its semantics is…
This paper introduces an alternative approach to proving the existence of choice functions for specific families of sets within Zermelo-Fraenkel set theory (ZF) without assuming any form on the Axiom of Choice (AC). Traditional methods of…
We propose a method that allows us to develop tableaux modulo theories using the principles of superdeduction, among which the theory is used to enrich the deduction system with new deduction rules. This method is presented in the framework…
We show that the classical interpretations of Tarski's inductive definitions actually allow us to define the satisfaction and truth of the quantified formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers…