In this paper, I motivate a cut free sequent calculus for classical logic with first order quantification, allowing for singular terms free of existential import. Along the way, I motivate a criterion for rules designed to answer Prior’s question about what distinguishes rules for logical concepts, like conjunction from apparently similar rules for putative concepts like Prior’s tonk, and I show that the rules for the quantifiers—and the existence predicate—satisfy that condition.

Sorites is an ancient piece of paradoxical reasoning pertaining to sets with the following properties: (Supervenience) elements of the set are mapped into some set of “attributes”; (Tolerance) if an element has a given attribute then so are the elements in some vicinity of this element; and (Connectedness) such vicinities can be arranged into pairwise overlapping finite chains connecting two elements with different attributes. Obviously, if Superveneince is assumed, then (1) Tolerance implies lack of Connectedness, and (2) Connectedness implies lack of Tolerance. Using a very general but precise definition of “vicinity”, Dzhafarov & Dzhafarov (2010) offered two formalizations of these mutual contrapositions. Mathematically, the formalizations are equally valid, but in this paper, we offer a different basis by which to compare them. Namely, we show that the formalizations have different proof-theoretic strengths when measured in the framework of reverse mathematics: the formalization of (1) is provable in $RC{A_0}$, while the formalization of (2) is equivalent to $AC{A_0}$ over $RC{A_0}$. Thus, in a certain precise sense, the approach of (1) is more constructive than that of (2).

We introduce unification in first-order logic. In propositional logic, unification was introduced by S. Ghilardi, see Ghilardi (1997, 1999, 2000). He successfully applied it in solving systematically the problem of admissibility of inference rules in intuitionistic and transitive modal propositional logics. Here we focus on superintuitionistic predicate logics and apply unification to some old and new problems: definability of disjunction and existential quantifier, disjunction and existential quantifier under implication, admissible rules, a basis for the passive rules, (almost) structural completeness, etc. For this aim we apply modified specific notions, introduced in propositional logic by Ghilardi, such as projective formulas, projective unifiers, etc.

Unification in predicate logic seems to be harder than in the propositional case. Any definition of the key concept of substitution for predicate variables must take care of individual variables. We allow adding new free individual variables by substitutions (contrary to Pogorzelski & Prucnal (1975)). Moreover, since predicate logic is not as close to algebra as propositional logic, direct application of useful algebraic notions of finitely presented algebras, projective algebras, etc., is not possible.

Recently, several epistemologists have defended an attractive principle of epistemic rationality, which we shall call Ur-Prior Conditionalization. In this essay, I ask whether we can justify this principle by appealing to the epistemic goal of accuracy. I argue that any such accuracy-based argument will be in tension with Evidence Externalism, i.e., the view that agent’s evidence may entail nontrivial propositions about the external world. This is because any such argument will crucially require the assumption that, independently of all empirical evidence, it is rational for an agent to be certain that her evidence will always include truths, and that she will always have perfect introspective access to her own evidence. This assumption is incompatible with Evidence Externalism. I go on to suggest that even if we don’t accept Evidence Externalism, the prospects for any accuracy-based justification for Ur-Prior Conditionalization are bleak.

Recent discussions on Fregean and neo-Fregean foundations for arithmetic and real analysis pay much attention to what is called either ‘Application Constraint’ ($AC$) or ‘Frege Constraint’ ($FC$), the requirement that a mathematical theory be so outlined that it immediately allows explaining for its applicability. We distinguish between two constraints, which we, respectively, denote by the latter of these two names, by showing how $AC$ generalizes Frege’s views while $FC$ comes closer to his original conceptions. Different authors diverge on the interpretation of $FC$ and on whether it applies to definitions of both natural and real numbers. Our aim is to trace the origins of $FC$ and to explore how different understandings of it can be faithful to Frege’s views about such definitions and to his foundational program. After rehearsing the essential elements of the relevant debate (§1), we appropriately distinguish $AC$ from $FC$ (§2). We discuss six rationales which may motivate the adoption of different instances of $AC$ and $FC$ (§3). We turn to the possible interpretations of $FC$ (§4), and advance a Semantic $FC$ (§4.1), arguing that while it suits Frege’s definition of natural numbers (4.1.1), it cannot reasonably be imposed on definitions of real numbers (§4.1.2), for reasons only partly similar to those offered by Crispin Wright (§4.1.3). We then rehearse a recent exchange between Bob Hale and Vadim Batitzky to shed light on Frege’s conception of real numbers and magnitudes (§4.2). We argue that an Architectonic version of $FC$ is indeed faithful to Frege’s definition of real numbers, and compatible with his views on natural ones. Finally, we consider how attributing different instances of $FC$ to Frege and appreciating the role of the Architectonic $FC$ can provide a more perspicuous understanding of his foundational program, by questioning common pictures of his logicism (§5).

This paper is a follow-up to [4], in which a mistake in [6] (which spread also to [9]) was corrected. We give a strenghtening of the main result on the semantical nonconservativity of the theory of PT− with internal induction for total formulae ${(\rm{P}}{{\rm{T}}^ - } + {\rm{INT}}\left( {{\rm{tot}}} \right)$, denoted by PT− in [9]). We show that if to PT− the axiom of internal induction for all arithmetical formulae is added (giving ${\rm{P}}{{\rm{T}}^ - } + {\rm{INT}}$), then this theory is semantically stronger than ${\rm{P}}{{\rm{T}}^ - } + {\rm{INT}}\left( {{\rm{tot}}} \right)$. In particular the latter is not relatively truth definable (in the sense of [11]) in the former. Last but not least, we provide an axiomatic theory of truth which meets the requirements put forward by Fischer and Horsten in [9]. The truth theory we define is based on Weak Kleene Logic instead of the Strong one.

The operations of expansion and refinement on nondeterministic matrices (Nmatrices) are composed to form a new operation called rexpansion. Properties of this operation are investigated, together with their effects on the induced consequence relations. Using rexpansions, a semantic method for obtaining conservative extensions of (N)matrix-defined logics is introduced and applied to fragments of the classical two-valued matrix, as well as to other many-valued matrices and Nmatrices. The main application of this method is the construction and investigation of truth-preserving ¬-paraconsistent conservative extensions of Gödel fuzzy logic, in which ¬ has several desired properties. This is followed by some results regarding the relations between the constructed logics.

We present a new axiomatization of classical mereology in which the three components of the theory—ordering, composition, and decomposition principles—are neatly separated. The equivalence of our axiom system with other, more familiar systems is established by purely deductive methods, along with additional results on the relative strengths of the composition and decomposition axioms of each system.