We study subsets of countable recursively saturated models of PA which can be defined using pathologies in satisfaction classes. More precisely, we characterize those subsets X such that there is a satisfaction class S where S behaves correctly on an idempotent disjunction of length c if and only if c∈X. We generalize this result to characterize several types of pathologies including double negations, blocks of extraneous quantifiers, and binary disjunctions and conjunctions. We find a surprising relationship between the cuts which can be defined in this way and arithmetic saturation: namely, a countable nonstandard model is arithmetically saturated if and only if every cut can be the “idempotent disjunctively correct cut” in some satisfaction class. We describe the relationship between types of pathologies and the closure properties of the cuts defined by these pathologies.

Abstract Gödel’s Incompleteness Theorems suggest that no single formal system can capture the entirety of one’s mathematical beliefs, while pointing at a hierarchy of systems of increasing logical strength that make progressively more explicit those implicit assumptions. This notion of implicit commitment motivates directly or indirectly several research programmes in logic and the foundations of mathematics; yet there hasn’t been a direct logical analysis of the notion of implicit commitment itself. In a recent paper, we carried out an initial assessment of this project by studying necessary conditions for implicit commitments; from seemingly weak assumptions on implicit commitments of an arithmetical system $S$, it can be derived that a uniform reflection principle for $S$—stating that all numerical instances of theorems of $S$ are true—must be contained in $S$’s implicit commitments. This study gave rise to unexplored research avenues and open questions. This paper addresses the main ones. We generalize this basic framework for implicit commitments along two dimensions: in terms of iterations of the basic implicit commitment operator, and via a study of implicit commitments of theories in arbitrary first-order languages, not only couched in an arithmetical language.

Abstract We employ the lens provided by formal truth theory to study axiomatizations of Peano Arithmetic ${\textsf {(PA)}}$ . More specifically, let Elementary Arithmetic ${\textsf {(EA)}}$ be the fragment $\mathsf {I}\Delta _0 + \mathsf {Exp}$ of ${\textsf {PA}}$ , and let ${\textsf {CT}}^-[{\textsf {EA}}]$ be the extension of ${\textsf {EA}}$ by the commonly studied axioms of compositional truth ${\textsf {CT}}^-$ . We investigate both local and global properties of the family of first order theories of the form ${\textsf {CT}}^-[{\textsf {EA}}] +\alpha $ , where $\alpha $ is a particular way of expressing “ ${\textsf {PA}}$ is true” (using the truth predicate). Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to ${\textsf {PA}}$ and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of ${\textsf {PA}}$ .

Abstract The current paper studies the formal properties of the Global Reflection Principle, to wit the assertion “All theorems of $\mathrm {Th}$ are true,” where $\mathrm {Th}$ is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski’s proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only ( $\mathrm {CT}_0$ ). Furthermore, we extend the above result showing that $\Sigma _1$ -uniform reflection over a theory of uniform Tarski biconditionals ( $\mathrm {UTB}^-$ ) is provable in $\mathrm {CT}_0$ , thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of $\mathrm {CT}_0$ . In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of $\mathrm {CT}_0$ .

Abstract Let ${\cal T}$ be any of the three canonical truth theories CT− (compositional truth without extra induction), FS− (Friedman–Sheard truth without extra induction), or KF− (Kripke–Feferman truth without extra induction), where the base theory of ${\cal T}$ is PA (Peano arithmetic). We establish the following theorem, which implies that ${\cal T}$ has no more than polynomial speed-up over PA. Theorem. ${\cal T}$ is feasibly reducible to PA, in the sense that there is a polynomial time computable function f such that for every ${\cal T}$ -proof π of an arithmetical sentence ϕ, f (π) is a PA-proof of ϕ.

We study an extension of modal $\mu$-calculus to sets with atoms and we study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show expressive limitations of atom-enriched $\mu$-calculi, and explain how their expressive power depends on the structure of atoms used, and on the choice between basic or vectorial syntax.

We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.