Questions with a quantificational subject have readings that seemingly involve quantification into questions (called ‘QiQ’ for short). In particular, in single-wh questions with a universal quantifier, QiQ-readings call for pair-list answers, similar to pair-list readings of multiple-wh questions. This paper unifies the derivation of QiQ-readings and distinguishes QiQ-readings from pair-list readings of multiple-wh questions. I propose that pair-list multiple-wh questions and QiQ-questions both involve a wh-dependency, namely, that the wh-/quantificational subject stands in a functional dependency with the trace of the (...) wh-object. In particular, in a pair-list multiple-wh question, the wh-subject binds into the trace of the wh-object across an identity operator; in a QiQ-question, the quantificational subject binds into the trace of the wh-object across a predication operator. These operations give rise to distinct definedness requirements, which vary with the quantificational force of the wh-/quantificational subject. The proposed analysis explains a contrast in domain exhaustivity between the pair-list readings of multiple-wh questions and questions with a universal quantifier, while also doing justice to the intuitive similarities between these two types of questions. I further propose that the observed QiQ-effect in a QiQ-question is derived by extracting one of the minimal proposition sets that satisfy the aforementioned quantificational predication condition. The values of these sets determine whether the QiQ-reading is available and whether a QiQ-question admits pair-list answers and/or has a choice flavor. (shrink)

The book is about logical analysis of natural language. Since we humans communicate by means of natural language, we need a tool that helps us to understand in a precise manner how the logical and formal mechanisms of natural language work. Moreover, in the age of computers, we need to communicate both with and through computers as well. Transparent Intensional Logic is a tool that is helpful in making our communication and reasoning smooth and precise. It deals with all kinds (...) of linguistic context in a fully compositional and anti-contextual way. (shrink)

The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is (...) proved in a constructive way for sequent calculi adequate for all logics under consideration. (shrink)

Free logics is a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that the domain of interpretation is not empty, every name denotes exactly one object in the domain and the quantifiers have existential import. Free logics usually reject the claim that names need to denote in, and of the systems considered in this paper, the positive free logic concedes that (...) some atomic formulas containing non-denoting names are true, while negative free logic rejects even the latter claim. Inclusive logics, which reject, are likewise considered. These logics have complex and varied axiomatizations and semantics, and the goal of this paper is to present an orderly examination of the various systems and their mutual relations. This is done by first offering a formalization, using sequent calculi which possess all the desired structural properties of a good proof system, including admissibility of contraction and cut, while streamlining free logics in a way no other approach has. We then present a simple and unified system of abstract semantics, which allows for a straightforward demonstration of the meta-theoretical properties, and offers insights into the relationship between different logics. The final part of this paper is dedicated to extending the system with modalities by using a labeled sequent calculus, and here we are again able to map out the different approaches and their mutual relations using the same framework. (shrink)

This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the two subsystems of (...) second order arithmetic, Π10-CA and Π11-CA, respectively. (shrink)

The paper provides a proof theoretic characterization of the Russellian theory of definite descriptions (RDD) as characterized by Kalish, Montague and Mar (KMM). To this effect three sequent calculi are introduced: LKID0, LKID1 and LKID2. LKID0 is an auxiliary system which is easily shown to be equivalent to KMM. The main research is devoted to LKID1 and LKID2. The former is simpler in the sense of having smaller number of rules and, after small change, satisfies cut elimination but fails to (...) satisfy the subformula property. In LKID2 an additional analysis of different kinds of identities leads to proliferation of rules but yields the subformula property. This refined proof theoretic analysis leading to fully analytic calculus with constructive proof of cut elimination is the main contribution of the paper. (shrink)

I sketch an application of a semantically anti-realist understanding of the classical sequent calculus to the topic of mathematics. The result is a semantically anti-realist defence of a kind of mathematical realism. In the paper, I begin the development of the view and compare it to orthodox positions in the philosophy of mathematics.

Free logics are a family of first-order logics which came about as a result of examining the existence assumptions of classical logic (Hintikka _The Journal of Philosophy_, _56_, 125–137 1959 ; Lambert _Notre Dame Journal of Formal Logic_, _8_, 133–144 1967, 1997, 2001 ). What those assumptions are varies, but the central ones are that (i) the domain of interpretation is not empty, (ii) every name denotes exactly one object in the domain and (iii) the quantifiers have existential import. Free (...) logics reject the claim that names need to denote in (ii). _Positive_ free logic concedes that some atomic formulas containing non-denoting names (including self-identity) are true, _negative_ free logic treats them as uniformly false, and _neutral_ free logic as taking a third value. There has been a renewed interest in analyzing proof theory of free logic in recent years, based on intuitionistic logic in Maffezioli and Orlandelli (_Bulletin of the Section of Logic_, _48_(2), 137–158 2019 ) as well as classical logic in Pavlović and Gratzl (_Journal of Philosophical Logic_, _50_, 117–148 2021 ), there for the positive and negative variants. While the latter streamlines the presentation of free logics and offers a more unified approach to the variants under consideration, it does not cover neutral free logic, since there is some lack of both clear formal intuitions on the semantic status of formulas with empty names, as well as a satisfying account of the conditional in this context. We discuss extending the results to this third major variant of free logics. We present a series of G3 sequent calculi adapted from Fjellstad (_Studia Logica_, _105_(1), 93–119 2017, _Journal of Applied Non-Classical Logics_, _30_(3), 272–289 2020 ), which possess all the desired structural properties of a good proof system, including admissibility of contraction and all versions of the cut rule. At the same time, we maintain the unified approach to free logics and moreover argue that greater clarity of intuitions is achieved once neutral free logic is conceptualized as consisting of two sub-varieties. (shrink)

We develop a bottom-up approach to truth-value semantics for classical logic of partial terms based on equality and apply it to prove the conservativity of the addition of partial description and selection functions, independently of any strictness assumption.

Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel set theory for reasoning about sets, proper (...) classes, and partial functions represented as classes of ordered pairs. The underlying logic of the system is a partial first-order logic, so class-valued terms may be nondenoting. Functions can be specified using lambda-notation, and reasoning about the application of functions to arguments is facilitated using sorts similar to those employed in the logic of the IMPS Interactive Mathematical Proof System. The set theory is intended to serve as a foundation for mechanized mathematics systems. (shrink)

If concepts are explicated as abstract procedures, then we can easily show that each empirical concept is a not an effective procedure. Some, but not all empirical concepts are shown to be of a special kind: they cannot in principle guarantee that the object they identify satisfies the intended conditions.

A free logic is one in which a singular term can fail to refer to an existent object, for example, `Vulcan' or `5/0'. This essay demonstrates the fruitfulness of a version of this non-classical logic of terms (negative free logic) by showing (1) how it can be used not only to repair a looming inconsistency in Quine's theory of predication, the most influential semantical theory in contemporary philosophical logic, but also (2) how Beeson, Farmer and Feferman, among others, use it (...) to provide a natural foundation for partial functions in programming languages. Vis à vis (2), the question is raised whether the Beeson-Farmer-Feferman approach is adequate to the treatment of partial functions in all programming languages. Gumb and the author say No, and suggest a way of handling the refractory cases by means of positive free logic. Finally, Antonelli's solution of a problem associated with the Gumb-Lambert proposal is mentioned. (shrink)

The Suslin operator is a type-2 functional testing for the well-foundedness of binary relations on the natural numbers. In the context of applicative theories, its proof-theoretic strength has been analyzed in Jäger and Strahm [18]. This article provides a more direct approach to the computation of the upper bounds in question. Several theories featuring the Suslin operator are embedded into ordinal theories tailored for dealing with non-monotone inductive definitions that enable a smooth definition of the application relation.

The Logic of Partial Terms LPT is a strict negative free logic that provides an economical framework for developing many traditional mathematical theories having partial functions. In these traditional theories, all functions and predicates are strict. For example, if a unary function (predicate) is applied to an undefined argument, the result is undefined (respectively, false). On the other hand, every practical programming language incorporates at least one nonstrict or lazy construct, such as the if-then-else, but nonstrict functions cannot be either (...) primitive or introduced in definitional extensions in LPT. Consequently, lazy programming language constructs do not fit the traditional mathematical mold inherent in LPT. A nonstrict (positive free) logic is required to handle nonstrict functions and predicates. Previously developed nonstrict logics are not fully satisfactory because they are verbose in describing strict functions (which predominate in many programming languages), and some logicians find their semantics philosophically unpalatable. The newly developed Lazy Logic of Partial Terms LL is as concise as LPT in describing strict functions and predicates, and strict and nonstrict functions and predicates can be introduced in definitional extensions of traditional mathematical theories. LL is "built on top of" LPT, and, like LPT, admits only one domain in the semantics. In the semantics, for the case of a nonstrict unary function h in an LL theory T, we have $\models_T h(\perp) = y \longleftrightarrow \forall x(h(x) = y)$ , where $\perp$ is a canonical undefined term. Correspondingly, in the axiomatization, the "indifference" (to the value of the argument) axiom $h(\perp) = y \longleftrightarrow \forall x(h(x) = y)$ guarantees a proper fit with the semantics. The price paid for LL's naturalness is that it is tailored for describing a specific area of computer science, program specification and verification, possibly limiting its role in explicating classical mathematical and philosophical subjects. (shrink)

One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.