Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order natural deduction proofs of a mathematical theorem are pure. Formal proofs that refer to the ontological content of a theorem will be called ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, because they preserve the structural content of a theorem. We will use interpretations between theories to develop a proof-theoretic criterion that guarantees secondary ontological purity for formal proofs.

A theory T is tight if different deductively closed extensions of T (in the same language) cannot be bi-interpretable. Many well-studied foundational theories are tight, including $\mathsf {PA}$ [39], $\mathsf {ZF}$, $\mathsf {Z}_2$, and $\mathsf {KM}$ [6]. In this article we extend Enayat’s investigations to subsystems of these latter two theories. We prove that restricting the Comprehension schema of $\mathsf {Z}_2$ and $\mathsf {KM}$ gives non-tight theories. Specifically, we show that $\mathsf {GB}$ and $\mathsf {ACA}_0$ each admit different bi-interpretable extensions, and the same holds for their extensions by adding $\Sigma ^1_k$-Comprehension, for $k \ge 1$. These results provide evidence that tightness characterizes $\mathsf {Z}_2$ and $\mathsf {KM}$ in a minimal way.

This article takes a critical look at the development of international humanitarian law (IHL), from its early codification in the Hague and Geneva Conventions to the present day. It examines why and how IHL develops – through treaty, custom, interpretation and soft-law instruments, as well as the influence of jurisprudence and other branches of law. In doing so, it highlights some of the distinctive elements of IHL that set it apart from other bodies of law and explains how these elements influence IHL development. Turning to the present, it addresses some of the key arguments commonly heard against attempting any further development of IHL, by answering the following three key questions: Does IHL need to develop further? If so, how can this be achieved? And what are the prospects for such development in the near future? In answering these questions, the article argues that IHL will continue to develop in many ways, and that while the current environment does not appear propitious for new legally binding norms of IHL, they continue to be both necessary and possible.

The provability logic of a theory T captures the structural behavior of formalized provability in T as provable in T itself. Like provability, one can formalize the notion of relative interpretability giving rise to interpretability logics. Where provability logics are the same for all moderately sound theories of some minimal strength, interpretability logics do show variations.

The logic IL (All) is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this article we raise the previously known lower bound of IL (All) by exhibiting two series of principles which are shown to be provable in any such theory. Moreover, we compute the collection of frame conditions for both series.

Resentment and other hard feelings may outlive their targets, and people often express a desire to overcome these feelings through forgiveness. While some see forgiving the dead as an important moral accomplishment, others deny that genuine forgiveness of the dead is coherent, let alone desirable or valuable. According to one line of thought, forgiveness is something we do for certain reasons, such as the offender’s expressed contrition. Given that the dead cannot express remorse, forgiveness of the dead is impossible. Others see the apparent coherence and moral importance of forgiving the dead as a reason to give up on the idea that forgiveness is conditional upon the offender’s remorse. According to these philosophers, forgiveness of the dead poses no special problems; forgiveness of the dead, like forgiveness of the living, is not contingent upon the offender’s contrition. I steer a path between these two positions in such a way as to bring out an important aspect of forgiveness that is not adequately addressed in the literature: I argue that forgiving the dead may be perfectly coherent and morally valuable even though the dead cannot ask for forgiveness or engage in reparative activities. A full appreciation of the relational character of forgiveness allows us to make sense of forgiving the dead.

We introduce the notion of infinitary interpretation of structures. In general, an interpretation between structures induces a continuous homomorphism between their automorphism groups, and furthermore, it induces a functor between the categories of copies of each structure. We show that for the case of infinitary interpretation the reversals are also true: every Baire-measurable homomorphism between the automorphism groups of two countable structures is induced by an infinitary interpretation, and every Baire-measurable functor between the set of copies of two countable structures is induced by an infinitary interpretation. Furthermore, we show that the complexities are maintained in the sense that if the functor is ${\bf{\Delta }}_\alpha ^0$, then the interpretation that induces it is ${\rm{\Delta }}_\alpha ^{in}$ up to ${\bf{\Delta }}_\alpha ^0$ equivalence.

This paper addresses the structures (M, ω) and (ω, SSy(M)), where M is a nonstandard model of PA and ω is the standard cut. It is known that (ω, SSy(M)) is interpretable in (M, ω). Our main technical result is that there is an reverse interpretation of (M, ω) in (ω, SSy(M)) which is ‘local’ in the sense of Visser [11]. We also relate the model theory of (M, ω) to the study of transplendent models of PA [2].

This yields a number of model theoretic results concerning the ω-models (M, ω) and their standard systems SSy(M, ω), including the following.

• $\left( {M,\omega } \right) \prec \left( {K,\omega } \right)$ if and only if $M \prec K$ and $\left( {\omega ,{\rm{SSy}}\left( M \right)} \right) \prec \left( {\omega ,{\rm{SSy}}\left( K \right)} \right)$.

• $\left( {\omega ,{\rm{SSy}}\left( M \right)} \right) \prec \left( {\omega ,{\cal P}\left( \omega \right)} \right)$ if and only if $\left( {M,\omega } \right) \prec \left( {{M^{\rm{*}}},\omega } \right)$ for some ω-saturated M*.

• $M{ \prec _{\rm{e}}}K$ implies SSy(M, ω) = SSy(K, ω), but cofinal extensions do not necessarily preserve standard system in this sense.

• SSy(M, ω)=SSy(M) if and only if (ω, SSy(M)) satisfies the full comprehension scheme.

• If SSy(M, ω) is uniformly defined by a single formula (analogous to a β function), then (ω, SSy(M, ω)) satisfies the full comprehension scheme; and there are models M for which SSy(M, ω) is not uniformly defined in this sense.