We provide infinitary proof theories for three common semantic theories of truth: strong Kleene, van Fraassen supervaluation and Cantini supervaluation. The value of these systems is that they provide an easy method of proving simple facts about semantic theories. Moreover we shall show that they also give us a simpler understanding of the computational complexity of these definitions and provide a direct proof that the closure ordinal for Kripke’s definition is $\omega _1^{CK}$. This work can be understood as an effort to provide a proof-theoretic counterpart to Welch’s game-theoretic (Welch, 2009).

We explore the question of whether sustained rational disagreement is possible from a broadly Bayesian perspective. The setting is one where agents update on the same information, with special consideration being given to the case of uncertain information. The classical merging of opinions theorem of Blackwell and Dubins shows when updated beliefs come and stay closer for Bayesian conditioning. We extend this result to a type of Jeffrey conditioning where agents update on evidence that is uncertain but solid (hard Jeffrey shifts). However, merging of beliefs does not generally hold for Jeffrey conditioning on evidence that is fluid (soft Jeffrey shifts, Field shifts). Several theorems on the asymptotic behavior of subjective probabilities are proven. Taken together they show that while a consensus nearly always emerges in important special cases, sustained rational disagreement can be expected in many other situations.

The term ‘harmony’ refers to a condition that the rules governing a logical constant ought to satisfy in order to endow it with a proper meaning. Different characterizations of harmony have been proposed in the literature, some based on the inversion principle, others on normalization, others on conservativity. In this paper we discuss the prospects for showing how conservativity and normalization can be combined so to yield a criterion of harmony equivalent to the one based on the inversion principle: We conjecture that the rules for connectives obeying the inversion principle are conservative over normal deducibility. The plausibility of the conjecture depends in an essential way on how normality is characterized. In particular, a normal deduction should be understood as one which is irreducible, rather than as one which does not contain any maximal formula.

What is the logical strength of theories of truth? That is: If you take a theory ${\cal T}$ and add a theory of truth to it, how strong is the resulting theory, as compared to ${\cal T}$? Once the question has been properly formulated, the answer turns out to be about as elegant as one could want: At least when ${\cal T}$ is finitely axiomatized theory, theories of truth act more or less as a kind of abstract consistency statement. To prove this result, however, we have to formulate truth-theories somewhat differently from how they have been and instead follow Tarski in ‘disentangling’ syntactic theories from object theories.

Robert Aumann presents his Agreement Theorem as the key conditional: “if two people have the same priors and their posteriors for an event A are common knowledge, then these posteriors are equal” (Aumann, 1976, p. 1236). This paper focuses on four assumptions which are used in Aumann’s proof but are not explicit in the key conditional: (1) that agents commonly know, of some prior μ, that it is the common prior; (2) that agents commonly know that each of them updates on the prior by conditionalization; (3) that agents commonly know that if an agent knows a proposition, she knows that she knows that proposition (the “KK” principle); (4) that agents commonly know that they each update only on true propositions. It is shown that natural weakenings of any one of these strong assumptions can lead to countermodels to Aumann’s key conditional. Examples are given in which agents who have a common prior and commonly know what probability they each assign to a proposition nevertheless assign that proposition unequal probabilities. To alter Aumann’s famous slogan: people can “agree to disagree”, even if they share a common prior. The epistemological significance of these examples is presented in terms of their role in a defense of the Uniqueness Thesis: If an agent whose total evidence is E is fully rational in taking doxastic attitude D to P, then necessarily, any subject with total evidence E who takes a different attitude to P is less than fully rational.

In an earlier paper in this journal I provided detailed motivation for the constructive and relevant system of Core Logic; explained its main features; and established that, even though Cut is not a rule of the system, nevertheless Cut is admissible for it, and indeed with potential epistemic gain. If Π is a proof of the sequent Δ : A, and Σ is a proof of the sequent Г, A : θ, then there is a computable reduct [Π, Σ] of some subsequent of the ‘overall target sequent’ Δ, Г : θ. In the constructive case the potential epistemic gain consists in the possibility that the subsequent in question be a proper subsequent of Δ, Г : θ, and indeed even logically stronger than Δ, Г : θ.

In this paper it is established that Cut is likewise admissible for Classical Core Logic, which is obtained from Core Logic by adding a suitably relevantized form of the rule of Classical Dilemma. In the classical case there is an additional feature of potential epistemic gain: the proof [Π, Σ] might have a lower degree of non-constructivity than do Π and Σ.

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.

We discuss the interplay between the axiomatic and the semantic approach to truth. Often, semantic constructions have guided the development of axiomatic theories and certain axiomatic theories have been claimed to capture a semantic construction. We ask under which conditions an axiomatic theory captures a semantic construction. After discussing some potential criteria, we focus on the criterion of ℕ-categoricity and discuss its usefulness and limits.

A method of supervaluation for Kripke’s theory of truth is presented. It differs from Kripke’s own method in that it employs trees; results in a compositional semantics; assigns the intuitively correct truth values to the sentences of a particularly tricky example of Gupta’s; and – it is argued – is acceptable as an explication of the correspondence theory of truth.

We present an extension of the basic revision theory of circular definitions with a unary operator, □. We present a Fitch-style proof system that is sound and complete with respect to the extended semantics. The logic of the box gives rise to a simple modal logic, and we relate provability in the extended proof system to this modal logic via a completeness theorem, using interpretations over circular definitions, analogous to Solovay’s completeness theorem for GL using arithmetical interpretations. We adapt our proof to a special class of circular definitions as well as to the first-order case.

This paper is a study of the opening section of Gentzen’s first publication of 1932, Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen, a text which shows the relevance of Hertz’s work of the 1920’s for the young Gentzen. In fact, Gentzen borrowed from Hertz the analysis of the notion of consequence, which was given in terms of the rules of thinning (Verdünnung) and cut (Schnitt) on sequents (there called “sentences”(Sätze)). Moreover, following Hertz again, he also judged it necessary to justify the forms of inference of the system by providing a semantics for them, so that it became possible to make precise the informal notion of consequence, and to show that the inference rules adopted are correct and sufficient.

We present a semantics for a language that includes sentences that can talk about their own probabilities. This semantics applies a fixed point construction to possible world style structures. One feature of the construction is that some sentences only have their probability given as a range of values. We develop a corresponding axiomatic theory and show by a canonical model construction that it is complete in the presence of the ω-rule. By considering this semantics we argue that principles such as introspection, which lead to paradoxical contradictions if naively formulated, should be expressed by using a truth predicate to do the job of quotation and disquotation and observe that in the case of introspection the principle is then consistent.

A proposition is noncontingent, if it is necessarily true or it is necessarily false. In an epistemic context, ‘a proposition is noncontingent’ means that you know whether the proposition is true. In this paper, we study contingency logic with the noncontingency operator Δ but without the necessity operator □. This logic is not a normal modal logic, because Δ(φ → ψ) → (Δφ → Δψ) is not valid. Contingency logic cannot define many usual frame properties, and its expressive power is weaker than that of basic modal logic over classes of models without reflexivity. These features make axiomatizing contingency logics nontrivial, especially for the axiomatization over symmetric frames. In this paper, we axiomatize contingency logics over various frame classes using a novel method other than the methods provided in the literature, based on the ‘almost-definability’ schema AD proposed in our previous work. We also present extensions of contingency logic with dynamic operators. Finally, we compare our work to the related work in the fields of contingency logic and ignorance logic, where the two research communities have similar results but are apparently unaware of each other’s work. One goal of our paper is to bridge this gap.

This paper explores how a semantics for Prior’s infamous connective tonk should be, a connective defined by inference rules that trivialize the logic of a deductive system if that logic is supposed to be transitive. To avoid triviality, one must reject transitivity and in a relatively recent paper, Roy Cook develops a semantics for tonk with non-transitive entailment. However, I show in this paper that a cut-free sequent calculus for tonk - the arguably most natural and simplest deductive system for a non-transitive logic - can neither be complete with respect to Cook’s semantics nor with respect to a semantics with non-transitive entailment based on a semantics for vagueness and transparent truth developed by Cobreros et al. It is argued that the failure to adequately represent tonk is connected with the fact that tonk is not uniquely defined in a cut-free sequent calculus system unless the logic is in addition non-reflexive. To remedy this, the paper develops a semantics with non-transitive and non-reflexive entailment based on the idea that complex formulae are true or false relative to them being assessed as premise or as conclusion.

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.

If ${\cal C}$ is a category whose objects are themselves categories, and ${\cal C}$ has a rich enough structure, it is known that we can recover the internal structure of the categories in ${\cal C}$ entirely in terms of the arrows in ${\cal C}$. In this sense, the internal structure of the categories in a rich enough category of categories is visible in the structure of the category of categories itself.

In this paper, we demonstrate that this result follows as a matter of logic – given one starts from the right definitions. This is demonstrated by first producing an abstraction principle whose abstracts are functors, and then actually recovering the internal structure of the individual categories that intuitively stand at the sources and targets of these functors by examining the way these functors interact. The technique used in this construction will be useful elsewhere, and involves providing an abstract corresponding not to every object of some given family, but to all the relevant mappings of some family of objects.

This construction should settle, in particular, questions about whether categories of categories qualify as autonomous mathematical objects – categories of categories are perfectly acceptable autonomous objects and thus, in particular, suitable for foundational purposes.

Some theorists have developed formal approaches to truth that depend on counterexamples to the structural rules of contraction. Here, we study such approaches, with an eye to helping them respond to a certain kind of objection. We define a contractive relative of each noncontractive relation, for use in responding to the objection in question, and we explore one example: the contractive relative of multiplicative-additive affine logic with transparent truth, or maalt.

The paper proposes an extension of the definition of a canonical proof, central to proof-theoretic semantics, to a definition of a canonical derivation from open assumptions. The impact of the extension on the definition of (reified) proof-theoretic meaning of logical constants is discussed. The extended definition also sheds light on a puzzle regarding the definition of local-completeness of a natural-deduction proof-system, underlying its harmony.

Spectrum Exchangeability, Sx, is an irrelevance principle of Pure Inductive Logic, and arguably the most natural (but not the only) extension of Atom Exchangeability to polyadic languages. It has been shown1 that all probability functions which satisfy Sx are comprised of a mixture of two essential types of probability functions; heterogeneous and homogeneous functions. We determine the theory of Spectrum Exchangeability, which for a fixed language L is the set of sentences of L which must be assigned probability 1 by every probability function satisfying Sx, by examining separately the theories of heterogeneity and homogeneity. We find that the theory of Sx is equal to the theory of finite structures, i.e., those sentences true in all finite structures for L, and it emerges that Sx is inconsistent with the principle of Super-Regularity (Universal Certainty). As a further consequence we are able to characterize those probability functions which satisfy Sx and the Finite Values Property.