We introduce and study a PDL-style logic for reasoning about protocols, or plans, under imperfect information. Our paper touches on a number of issues surrounding the relationship between an agent’s abilities, available choices, and information in an interactive situation. The main question we address is under what circumstances can the agent commit to a protocol or plan, and what can she achieve by doing so?

Mathematicians judge proofs to possess, or lack, a variety of different qualities, including, for example, explanatory power, depth, purity, beauty and fit. Philosophers of mathematical practice have begun to investigate the nature of such qualities. However, mathematicians frequently draw attention to another desirable proof quality: being motivated. Intuitively, motivated proofs contain no “puzzling” steps, but they have received little further analysis. In this article, I begin a philosophical investigation into motivated proofs. I suggest that a proof is motivated if and only if mathematicians can identify (i) the tasks each step is intended to perform; and (ii) where each step could have reasonably come from. I argue that motivated proofs promote understanding, convey new mathematical resources and stimulate new discoveries. They thus have significant epistemic benefits and directly contribute to the efficient dissemination and advancement of mathematical knowledge. Given their benefits, I also discuss the more practical matter of how we can produce motivated proofs. Finally I consider the relationship between motivated proofs and proofs which are explanatory, beautiful and fitting.

In this paper we show how to interpret Robinson’s arithmetic Q and the theory R of Tarski, Mostowski, and Robinson as theories of cardinals in very weak theories of relations over a domain.

We show that if we interpret modal diamond as the derived set operator of a topological space, then the modal logic of Stone spaces is K4 and the modal logic of weakly scattered Stone spaces is K4G. As a corollary, we obtain that K4 is also the modal logic of compact Hausdorff spaces and K4G is the modal logic of weakly scattered compact Hausdorff spaces.

In this paper, we establish the first-order definability of sequents with consistent variable occurrence on bi-approximation semantics by means of the Sahlqvist–van Benthem algorithm. Then together with the canonicity results in Suzuki (2011), this allows us to establish a Sahlqvist theorem for substructural logic. Our result is not limited to substructural logic but is also easily applicable to other lattice-based logics.

Logical inferentialism claims that the meaning of the logical constants should be given, not model-theoretically, but by the rules of inference of a suitable calculus. It has been claimed that certain proof-theoretical systems, most particularly, labelled deductive systems for modal logic, are unsuitable, on the grounds that they are semantically polluted and suffer from an untoward intrusion of semantics into syntax. The charge is shown to be mistaken. It is argued on inferentialist grounds that labelled deductive systems are as syntactically pure as any formal system in which the rules define the meanings of the logical constants.

Dialetheism is the metaphysical claim that there are true contradictions. And based on this view, Graham Priest and his collaborators have been suggesting solutions to a number of paradoxes. Those paradoxes include Russell’s paradox in naive set theory. For the purpose of dealing with this paradox, Priest is known to have argued against the presence of classical negation in the underlying logic of naive set theory. The aim of the present paper is to challenge this view by showing that there is a way to handle classical negation.

The paper offers a matrix-based logic (relevant matrix quantum physics) for propositions which seems suitable as an underlying logic for empirical sciences and especially for quantum physics. This logic is motivated by two criteria which serve to clean derivations of classical logic from superfluous redundancies and uninformative complexities. It distinguishes those valid derivations (inferences) of classical logic which contain superfluous redundancies and complexities and are in this sense “irrelevant” from those which are “relevant” or “nonredundant” in the sense of allowing only the most informative consequences in the derivations. The latter derivations are strictly valid in RMQ, whereas the former are only materially valid. RMQ is a decidable matrix calculus which possesses a semantics and has the finite model property. It is shown in the paper how RMQ by its strictly valid derivations can avoid the difficulties with commensurability, distributivity, and Bell's inequalities when it is applied to quantum physics.

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program promoted by Friedman and Simpson. We look in particular at: (i) the long arc from Poincaré to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles equivalent to Weak König’s Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others.

Feferman (1977) argues that category theory cannot stand on its own as a structuralist foundation for mathematics: he claims that, because the notions of operation and collection are both epistemically and logically prior, we require a background theory of operations and collections. Recently [2011], I have argued that in rationally reconstructing Hilbert’s organizational use of the axiomatic method, we can construct an algebraic version of category-theoretic structuralism. That is, in reply to Shapiro (2005), we can be structuralists all the way down; we do not have to appeal to some background theory to guarantee the truth of our axioms. In this paper, I again turn to Hilbert; I borrow his (Hilbert, 1900a) distinction between the genetic method and the axiomatic method to argue that even if the genetic method requires the notions of operation and collection, the axiomatic method does not. Even if the genetic method is in some sense epistemically or logically prior, the axiomatic method stands alone. Thus, if the claim that category theory can act as a structuralist foundation for mathematics arises from the organizational use of the axiomatic method, then it does not depend on the prior notions of operation or collection, and so we can be structuralists all the way up.

The large-structure tools of cohomology including toposes and derived categories stay close to arithmetic in practice, yet published foundations for them go beyond ZFC in logical strength. We reduce the gap by founding all the theorems of Grothendieck’s SGA, plus derived categories, at the level of Finite-Order Arithmetic, far below ZFC. This is the weakest possible foundation for the large-structure tools because one elementary topos of sets with infinity is already this strong.

The paper is concerned with the way in which “ontology” and “realism” are to be interpreted and applied so as to give us a deeper philosophical understanding of mathematical theories and practice. Rather than argue for or against some particular realistic position, I shall be concerned with possible coherent positions, their strengths and weaknesses. I shall also discuss related but different aspects of these problems. The terms in the title are the common thread that connects the various sections.

The collapse models of arithmetic are inconsistent, nontrivial models obtained from ℕ and set out in the Logic of Paradox (LP). They are given a general treatment by Priest (Priest, 2000). Finite collapse models are decidable, and thus axiomatizable, because finite. LP, however, is ill-suited to normal axiomatic reasoning, as it invalidates Modus Ponens, and almost all other usual conditional inferences. I set out a logic, A3, first given by Avron (Avron, 1991), and give a first order axiom system for the finite collapse models. I present some standard arithmetical axioms in addition to a cyclic axiom and prove that these axioms are sound and complete for the cyclic models, reporting a similar result for the heap models. The state of the situation for the each of the kinds of infinite collapse model is, however, left an open question.

Sound and complete semantics for classical propositional logic can be obtained by interpreting sentences as sets. Replacing sets with commuting dense binary relations produces an interpretation that turns out to be sound but not complete for R. Adding transitivity yields sound and complete semantics for RM, because all normal Sugihara matrices are representable as algebras of binary relations.

The purpose of this paper is to investigate categoricity arguments conducted in second order logic and the philosophical conclusions that can be drawn from them. We provide a way of seeing this result, so to speak, through a first order lens divested of its second order garb. Our purpose is to draw into sharper relief exactly what is involved in this kind of categoricity proof and to highlight the fact that we should be reserved before drawing powerful philosophical conclusions from it.

The big question at the end of Feferman (2013) is: Is it possible to find a foundation for unlimited category theory? I show that the answer is no by showing that unlimited category theory is inconsistent.

We show how in the hierarchies ${F_\alpha }$ of Fieldian truth sets, and Herzberger’s ${H_\alpha }$ revision sequence starting from any hypothesis for ${F_0}$ (or ${H_0}$) that essentially each ${H_\alpha }$ (or ${F_\alpha }$) carries within it a history of the whole prior revision process.

As applications (1) we provide a precise representation for, and a calculation of the length of, possible path independent determinateness hierarchies of Field’s (2003) construction with a binary conditional operator. (2) We demonstrate the existence of generalized liar sentences, that can be considered as diagonalizing past the determinateness hierarchies definable in Field’s recent models. The ‘defectiveness’ of such diagonal sentences necessarily cannot be classified by any of the determinateness predicates of the model. They are ‘ineffable liars’. We may consider them a response to the claim of Field (2003) that ‘the conditional can be used to show that the theory is not subject to “revenge problems”.’

I argue that recent defenses of the view that in 1936 Tarski required all interpretations of a language to share one same domain of quantification are based on misinterpretations of Tarski’s texts. In particular, I rebut some criticisms of my earlier attack on the fixed-domain exegesis and I offer a more detailed report of the textual evidence on the issue than in my earlier work. I also offer new considerations on subsisting issues of interpretation concerning Tarski’s views on the logical correctness of certain omega-arguments, on the Tarskian proof that Etchemendy took to be modal and fallacious, and on Tarski’s appeals to the “common concept of consequence”.

In proof-theoretic semantics of intuitionistic logic it is well known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases, these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all—they can be flattened in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.

The paper proposes a semantic value for the logical constants (connectives and quantifiers) within the framework of proof-theoretic semantics, basic meaning on the introduction rules of a meaning conferring natural deduction proof system. The semantic value is defined based on Frege’s Context Principle, by taking “contributions” to sentential meanings as determined by the function-argument structure as induced by a type-logical grammar. In doing so, the paper proposes a novel proof-theoretic interpretation of the semantic types, traditionally interpreted in Henkin models. The compositionality of the resulting attribution of semantic values is discussed. Elsewhere, the same method was used for defining proof-theoretic meaning of subsentential phrases in a fragment of natural language. Doing the same for (the simpler and clearer case of) logic sheds more light on the proposal.