It is well known that infinite minimal sets for continuous functions on the interval are Cantor sets; that is, compact zero dimensional metrizable sets without isolated points. On the other hand, it was proved in Alcaraz and Sanchis (Bifurcat Chaos 13:1665–1671, 2003) that infinite minimal sets for continuous functions on connected linearly ordered spaces enjoy the same properties as Cantor sets except that they can fail to be metrizable. However, no examples of such subsets have been known. In this (...) note we construct, in ZFC, ${2^{\mathfrak{c}}}$ non-metrizable infinite pairwise non-homeomorphic minimal sets on compact connected linearly ordered spaces. (shrink)

Zero pronominals challenge Type Logical Grammar in two ways. One, TLG displays a linear resource management regime for semantic composition, meaning that pronominals call for special treatment if they want to do resource multiplication. Two, as a grammar of lexicalism, TLG applies to phonologically realized lexical entries only, illegitimating the phonetically null items during syntactic derivation. Jägor extends the inventory of category-forming connectives of TLG by a third kind of implication that creates categories of anaphoric items and solves (...) the first problem above. This article goes a step further to tackle the second one. In order to formalize the constructions with zero pronominals, we design a ternary category A B C and include the latter into Jägor’s system. The proposed system is proof-theoretically well-behaved. It is complete, sound, and decidable. More importantly, zero pronominals of various forms can be derived in the system. (shrink)

We develop a set-theoretic semantics for Cocchiarella's second-order logical system . Such a semantics is a modification of the nonstandard sort of second-order semantics described, firstly, by Simms and later extended by Cocchiarella. We formulate a new second order logical system and prove its relative consistency. We call such a system and construct its set-theoretic semantics. Finally, we prove completeness theorems for proper normal extensions of the two systems with respect to certain (...) notions of validity provided by the semantics. (shrink)

Deleuze (1925–1995), in the early 1980s, adopts Peirce’s (1839–1914) semiotics in order to classify the signs that the images of the cinema display. Aiming at insufflating the Peircean principles with the movement that animates the images of cinema, he provides Peirce’s triadic logic with a new category – Zeroness – which stands for the semiotic movement of cinematic images. Deleuze’s new category has impacts on the main domains of Peirce’s philosophy. Accordingly, our inquiry will focus on the irradiation of (...) Zeroness over the (a) system of categories, the (b) Peircean phenomenology (phaneroscopy), the (c) generative categorial role, the (d) semiotic effectiveness, the (e) doctrine of continuity, and the (f) logic of relatives. This article will show that for Deleuze nearly like more recent Peircean scholarship: (a) zeroth state holds a categorial status, (b) some phenomenon instantiates zeroth state, (c) zeroth state plays a generative role regarding Peirce's categories, (d) zeroth state as a phenomenological category is semiotically effective, (e) zeroth state and the doctrine of continuity, and (f) zeroth state is a “medad.” In order to assess these topics, we recover Deleuze’s advances on Peirce’s philosophy and confront them with the Peircean studies on the zeroth state. Finally, we will see that Deleuze, far from being a Peircean scholar, developed the importance of the zeroth state for Peirce’s semiotics in advance to the subsequent Peircean scholarship. Reciprocally, most of Deleuzian scholars understimate the importance of Peirce for Deleuze’s semiotics. (shrink)

“Second-order Logic” in Anderson, C.A. and Zeleny, M., Eds. Logic, Meaning, and Computation: Essays in Memory of Alonzo Church. Dordrecht: Kluwer, 2001. Pp. 61–76. -/- Abstract. This expository article focuses on the fundamental differences between second- order logic and first-order logic. It is written entirely in ordinary English without logical symbols. It employs second-order propositions and second-order reasoning in a natural way to illustrate the fact that second-order logic is actually a familiar part (...) of our traditional intuitive logical framework and that it is not an artificial formalism created by specialists for technical purposes. To illustrate some of the main relationships between second-order logic and first-order logic, this paper introduces basic logic, a kind of zero-order logic, which is more rudimentary than first-order and which is transcended by first-order in the same way that first-order is transcended by second-order. The heuristic effectiveness and the historical importance of second-order logic are reviewed in the context of the contemporary debate over the legitimacy of second-order logic. Rejection of second-order logic is viewed as radical: an incipient paradigm shift involving radical repudiation of a part of our scientific tradition, a tradition that is defended by classical logicians. But it is also viewed as reactionary: as being analogous to the reactionary repudiation of symbolic logic by supporters of “Aristotelian” traditional logic. But even if “genuine” logic comes to be regarded as excluding second-order reasoning, which seems less likely today than fifty years ago, its effectiveness as a heuristic instrument will remain and its importance for understanding the history of logic and mathematics will not be diminished. Second-order logic may someday be gone, but it will never be forgotten. Technical formalisms have been avoided entirely in an effort to reach a wide audience, but every effort has been made to limit the inevitable sacrifice of rigor. People who do not know second-order logic cannot understand the modern debate over its legitimacy and they are cut-off from the heuristic advantages of second-order logic. And, what may be worse, they are cut-off from an understanding of the history of logic and thus are constrained to have distorted views of the nature of the subject. As Aristotle first said, we do not understand a discipline until we have seen its development. It is a truism that a person's conceptions of what a discipline is and of what it can become are predicated on their conception of what it has been. (shrink)

In [2] we have presented sequent formulations of the modal logics S5 and S4 based on sequents of higher levels: sequents of level 1 are like ordinary sequents, sequents of level 2 have collections of sequents of level 1 on the left and right of the turnstile, etc. The rules we gave for modal constants involved sequents of level 2, whereas rules for other customary logical constants of first–order logic involved only sequents of level 1. Here we show (...) starting from the same sequent rules of higher level we can obtain sequent formulations of intuitionistic analogues of S5 and S4. We presuppose for this paper an acquaintance with [2]. (shrink)

We present the first-order logic of change, which is an extension of the propositional logic of change $\textsf {LC}\Box $ developed and axiomatized by Świętorzecka and Czermak. $\textsf {LC}\Box $ has two primitive operators: ${\mathcal {C}}$ to be read it changes whether and $\Box $ for constant unchangeability. It implements the philosophically grounded idea that with the help of the primary concept of change it is possible to define the concept of time. One of the characteristic axioms for ${\mathcal (...) {C}}$ is ${\mathcal {C}} A \to {\mathcal {C}}\neg A$ and one of the primitive rules is $\omega $-rule introducing $\Box $. It turns out that the next operator is definable in $\textsf {LC}\Box $. Logic $\textsf {LC}\Box $ with next is equivalent to certain fragment of $\textsf {LTL}$ extended by the appropriate definition of ${\mathcal {C}}$. Recently, $\textsf {LC}\Box $ has also been modified to the propositional logic of ‘branching’ changes $\textsf {BTC}$ by Łyczak and the logic of ‘parallel’ changes $\textsf {LC}\Box $ ↳ by Świętorzecka and Łyczak. Extended in an appropriate manner, $\textsf {BTC}$ is equivalent to a certain fragment of logic $\textsf {CTL}$ to which definitions of two kinds of changes have been added. Here we propose an extension of $\textsf {LC}\Box $ to first-order logic in which, again, the only primitive modal operators are ${\mathcal {C}}$ and $\Box $. We interpret our logic in the semantics of histories of changes. We give an axiomatic system $\textsf {LC}\Box Q$ for the considered logic, and we show selected theses about some relationships between ${\mathcal {C}}$, $\Box $ and $\forall $. Then we prove the completeness of $\textsf {LC}\Box Q$. Finally, we compare our logic with $\textsf {FOLT}$ and show the relation between $\textsf {LC}\Box Q$ and a certain fragment of the Kröger system $\varSigma $ to which the definition of ${\mathcal {C}}$ was added. (shrink)

We prove that every monadic second-order property of the unfolding of a transition system is a monadic second-order property of the system itself. An unfolding is an instance of the general notion of graph covering. We consider two more instances of this notion. A similar result is possible for one of them but not for the other.

J. D. Monk has shown that for first order languages with finitely many variables there is no finite set of schema which axiomatizes the universally valid formulas. There are such finite sets of schema which axiomatize the formulas valid in all structures of some fixed finite size.

Second-order logic has a number of attractive features, in particular the strong expressive resources it offers, and the possibility of articulating categorical mathematical theories (such as arithmetic and analysis). But it also has its costs. Five major charges have been launched against second-order logic: (1) It is not axiomatizable; as opposed to first-order logic, it is inherently incomplete. (2) It also has several semantics, and there is no criterion to choose between them (Putnam, J Symbol Logic 45:464–482, (...) 1980 ). Therefore, it is not clear how this logic should be interpreted. (3) Second-order logic also has strong ontological commitments: (a) it is ontologically committed to classes (Resnik, J Phil 85:75–87, 1988 ), and (b) according to Quine (Philosophy of logic, Prentice-Hall: Englewood Cliffs, 1970 ), it is nothing more than “set theory in sheep’s clothing”. (4) It is also not better than its first-order counterpart, in the following sense: if first-order logic does not characterize adequately mathematical systems, given the existence of non - isomorphic first-order interpretations, second-order logic does not characterize them either, given the existence of different interpretations of second-order theories (Melia, Analysis 55:127–134, 1995 ). (5) Finally, as opposed to what is claimed by defenders of second-order logic [such as Shapiro (J Symbol Logic 50:714–742, 1985 )], this logic does not solve the problem of referential access to mathematical objects (Azzouni, Metaphysical myths, mathematical practice: the logic and epistemology of the exact sciences, Cambridge University Press, Cambridge, 1994 ). In this paper, I argue that the second-order theorist can solve each of these difficulties. As a result, second-order logic provides the benefits of a rich framework without the associated costs. (shrink)

Beginning with a survey of the shortcoming of theories of organology/media-as-externalization of mind/body—a philosophical-anthropological tradition that stretches from Plato through Ernst Kapp and finds its contemporary proponent in Bernard Stiegler—I propose that the phenomenological treatment of media as an outpouching and extension of mind qua intentionality is not sufficient to counter the ̳black-box‘ mystification of today‘s deep learning‘s algorithms. Focusing on a close study of Simondon‘s On the Existence of Technical Objectsand Individuation, I argue that the process-philosophical work of Gilbert (...) Simondon, with its critique of Norbert Wiener‘s first-order cybernetics, offers a precursor to the conception of second-order cybernetics (as endorsed byFrancisco Varela, Humberto Maturana, and Ricardo B. Uribe) and, specifically, its autopoietic treatment of information. It has been argued by those such as Frank Pasquale that neuro-inferential deep learning systems premised on predictive patterning, suchas AlphaGo Zero, have a veiled logic and, thus, are ̳black boxes‘. In detailing a philosophical-historical approach to demystify predictive patterning/processing and the logic of such deep learning algorithms, this paper attempts to shine a light on such systems and their inner workingsàla Simondon. (shrink)

This paper begins the study of first-order functions, which are a generalization of truth-functions. The concepts of truth-table and systems of truth-functions, both introduced in propositional logic by Post, are also generalized and studied in the quantificational setting. The general facts about these concepts are given in the first five sections, and constitute a “general theory” of first-order functions. The central theme of this paper is the relation of definition among notions expressed by formulas of first-order logic. (...) We emphasize that logic is not concerned only with the consequence relation among notions expressed by formulas. It also attends to the relation of definition among notions, where a notion is defined from other notions. Sections 5 and 6 deal exclusively with the relation of definition among notions expressed by formulas of first-order logic. In these sections, we study the systems of first-order functions, which are the sets of first-order functions closed under definitions. Sections 7 and 8 are concerned with the relativization of first-order functions to a class of structures. The relativization to a class of structures is a fundamental operation which is used in order to relate the theory of first-order functions with set theory and first-order model theory, a subject which we have barely scratched the surface. The apparatus developed in this paper enables us to define what is a vehicle for the foundation of classical mathematics in set theory, and, in Sect. 8, we prove that first-order logic with one binary predicate variable is not a minimal vehicle for the foundation of classical mathematics in set theory. Sections 9 and 10 introduce further operations and ideals of first-order functions. Besides some results on the influence of the arguments of a first-order function, a result about definability is proved in Sect. 10.1. It is this theorem that provides necessary and sufficient conditions for a first-order function to be in a finitely generated ideal. In Sect. 11, this result is applied to the problem of predicate definability in classes of structures, the problem with which Beth’s theorem dealt in the case of elementary classes. (shrink)

This paper investigates the claim that the second-order consequence relation is intractable because of the incompleteness result for SOL. The opponents’ claim is that SOL cannot be proper logic since it does not have a complete deductive system. I argue that the lack of a completeness theorem, despite being an interesting result, cannot be held against the status of SOL as a proper logic.

In an earlier defense of the view that the fundamental logical properties of logical truth and logical consequence obtain or fail to obtain only relative to contexts, I focused on a variation of Kaplan’s own modal logic of indexicals. In this paper, I state a semantics and sketch a system of proof for a first-order logic of demonstratives, and sketch proofs of soundness and completeness. (I omit details for readability.) That these results obtain for the (...) first-order logic of demonstratives shows that the significance of demonstratives for logic exceeds their behavior as rigid designators in counterfactual reasoning, or reasoning about alternative possibilities. Furthermore, the results in this paper help address one common objection to the view that logical truth and consequence obtain only relative to contexts. According to this objection, the view entails that logical consequence is not formal. (shrink)

A classical reconstruction of Wright’s first-order logic of strict finitism is presented. Strict finitism is a constructive standpoint of mathematics that is more restrictive than intuitionism. Wright sketched the semantics of said logic in Wright (Realism, Meaning and Truth, chap 4, 2nd edition in 1993. Blackwell Publishers, Oxford, Cambridge, pp.107–75, 1982), in his strict finitistic metatheory. Yamada (J Philos Log. https://doi.org/10.1007/s10992-022-09698-w, 2023) proposed, as its classical reconstruction, a propositional logic of strict finitism under an auxiliary condition that makes the (...) logic correspond with intuitionistic propositional logic. In this paper, we extend the propositional logic to a first-order logic that does not assume the condition. We will provide a sound and complete pair of a Kripke-style semantics and a natural deduction system, and show that if the condition is imposed, then the logic exhibits natural extensions of Yamada (2023)’s results. (shrink)

This paper presents a new system of logic, LF, that is intended to be used as the foundation of the formalization of science. That is, deductive validity according to LF is to be used as the criterion for assessing what follows from the verdicts, hypotheses, or conjectures of any science. In work currently in progress, we argue for the unique suitability of LF for the formalization of logic, mathematics, syntax, and semantics. The present document specifies the language and rules (...) of LF, lays out some notational conventions, and states some basic technical facts about the system. (shrink)

In my response to Guillermo Rosado-Haddock I discuss the two main issues raised in his paper. The first is that by allowing Henkin’s general models as a legitimate model-theoretic interpretation of second-order logic, I undermine my defense of second-order logic against Quine’s views concerning the primacy of first-order logic. The second is that my treatment of logical truth and logical properties does not take into account various systems of logic and properties of systems of logic (...) such as the Löwenheim-Skolem property.Em minha réplica à Guillermo Rosado-Haddock discuto as duas questões centrais levantadas em seu artigo. A primeira é que ao permitir modelos gerais de Henkin como uma interpretação legítima da lógica de segunda ordem, desvirtuo minha defesa da lógica de segunda ordem contra a visão de Quine respeito à primazia da lógica de primeira ordem. A segunda é que meu tratamento da verdade lógica e das propriedades lógicas não leva em consideração diversos sistemas de lógica e propriedades de sistemas de lógica tais como a propriedade de Löwenheim-Skolem. (shrink)

First, we describe a psychological experiment in which the participants were asked to determine whether sentences of first-order logic were true or false in finite graphs. Second, we define two proof systems for reasoning about truth and falsity in first-order logic. These proof systems feature explicit models of cognitive resources such as declarative memory, procedural memory, working memory, and sensory memory. Third, we describe a computer program that is used to find the smallest proofs in the aforementioned proof (...) systems when capacity limits are put on the cognitive resources. Finally, we investigate the correlation between a number of mathematical complexity measures defined on graphs and sentences and some psychological complexity measures that were recorded in the experiment. (shrink)

What has been the historical relationship between set theory and logic? On the one hand, Zermelo and other mathematicians developed set theory as a Hilbert-style axiomatic system. On the other hand, set theory influenced logic by suggesting to Schröder, Löwenheim and others the use of infinitely long expressions. The questions of which logic was appropriate for set theory - first-order logic, second-order logic, or an infinitary logic - culminated in a vigorous exchange between Zermelo and Gödel around (...) 1930. (shrink)

One is often said to be reasoning well when they are reasoning logically. Many attempts to say what logical reasoning is have been proposed, but one commonly proposed system is first-order classical logic. This Element will examine the basics of first-order classical logic and discuss some surrounding philosophical issues. The first half of the Element develops a language for the system, as well as a proof theory and model theory. The authors provide theorems about the (...) system they developed, such as unique readability and the Lindenbaum lemma. They also discuss the meta-theory for the system, and provide several results there, including proving soundness and completeness theorems. The second half of the Element compares first-order classical logic to other systems: classical higher order logic, intuitionistic logic, and several paraconsistent logics which reject the law of ex falso quodlibet. (shrink)

This paper aims at clarifying the nature of Frege's system of logic, as presented in the first volume of the Grundgesetze. We undertake a rational reconstruction of this system, by distinguishing its propositional and predicate fragments. This allows us to emphasise the differences and similarities between this system and a modern system of classical second-order logic.

In this fourth paper in a series on stochastic electrodynamics (SED), the harmonic oscillator-zero-point field system in the presence of an arbitrary applied classical radiation field is studied further. The exact closed-form expressions are found for the time-dependent probability that the oscillator is in the nth eigenstate of the unperturbed SED Hamiltonian H 0 , the same H 0 as that of ordinary quantum mechanics. It is shown that an eigenvalue of H 0 is the average energy that (...) the oscillator would have if its wave function could be just the corresponding eigenstate. The level shift for each unperturbed eigenvalue is found and shown to be unobservable for a different reason than in the corresponding QED treatment. Perturbation theory is applied to the SED Schrödinger equation to derive first-order transition rates for spontaneous emission and resonance absorption. The results agree with those of quantum electrodynamics, but the mathematics is strikingly different. It is shown that SED demands discarding the ideas of quantized energies, photons, and completeness of the Schrödinger equation, Finally, an intuitive physical SED model is suggested for the photoeffect and for Clauser's (2) coincidence experiment. (shrink)

This chapter provides an overview of second-order logic and higher-order logic generally. It provides the basic formal languages, deductive systems, and model-theoretic semantics, including a brief account of George Boolos’s interpretation of second-order languages in terms of the plural construction. It then goes into some of the arguments in favor of second-order logic.

Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces- so -called "topological semantics." The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.

Starting from certain metalogical results, I argue that first-order logical truths of classical logic are a priori and necessary. Afterwards, I formulate two arguments for the idea that first-order logical truths are also analytic, namely, I first argue that there is a conceptual connection between aprioricity, necessity, and analyticity, such that aprioricity together with necessity entails analyticity; then, I argue that the structure of natural deduction systems for FOL displays the analyticity of its truths. Consequently, each (...) philosophical approach to these truths should account for this evidence, i.e., that first-order logical truths are a priori, necessary, and analytic, and it is my contention that the semantic account is a better candidate. (shrink)

We present Property Theory with Curry Typing (PTCT), an intensional first-order logic for natural language semantics. PTCT permits fine-grained specifications of meaning. It also supports polymorphic types and separation types. We develop an intensional number theory within PTCT in order to represent proportional generalized quantifiers like “most.” We use the type system and our treatment of generalized quantifiers in natural language to construct a type-theoretic approach to pronominal anaphora that avoids some of the difficulties that undermine previous (...) type-theoretic analyses of this phenomenon. (shrink)

Two thoughts about the concept of number are incompatible: that any zero or more things have a number, and that any zero or more things have a number only if they are the members of some one set. It is Russell's paradox that shows the thoughts incompatible: the sets that are not members of themselves cannot be the members of any one set. The thought that any things have a number is Frege's; the thought that things have a (...) number only if they are the members of a set may be Cantor's and is in any case a commonplace of the usual contemporary presentations of the set theory that originated with Cantor and has become ZFC.In recent years a number of authors have examined Frege's accounts of arithmetic with a view to extracting an interesting subtheory from Frege's formal system, whose inconsistency, as is well known, was demonstrated by Russell. These accounts are contained in Frege's formal treatise Grundgesetze der Arithmetik and his earlier exoteric book Die Grundlagen der Arithmetik. We may describe the two central results of the recent re-evaluation of his work in the following way: Let Frege arithmetic be the result of adjoining to full axiomatic second-order logic a suitable formalization of the statement that the Fs and the Gs have the same number if and only if the F sand the Gs are equinumerous. (shrink)

This paper follows Part I of our essay on case-intensional first-order logic (CIFOL; Belnap and Müller (2013)). We introduce a framework of branching histories to take account of indeterminism. Our system BH-CIFOL adds structure to the cases, which in Part I formed just a set: a case in BH-CIFOL is a moment/history pair, specifying both an element of a partial ordering of moments and one of the total courses of events (extending all the way into the future) that (...) that moment is part of. This framework allows us to define the familiar Ockhamist temporal/modal connectives, most notably for past, future, and settledness. The novelty of our framework becomes visible in our discussion of substances in branching histories, i.e., in its first-order part. That discussion shows how the basic idea of tracing an individual thing from case to case via an absolute property is applicable in a branching histories framework. We stress the importance of keeping apart extensionality and moment-definiteness, and give a formal account of how the specification of natural sortals and natural qualities turns out to be a coordination task in BH-CIFOL. We also provide a detailed answer to Lewis’s well-known argument against branching histories, exposing the fallacy in that argument. (shrink)

This paper deals with the translation of first order formulas to predicate S5 formulas. This translation does not bring the first order formula itself to a modal system, but modal interpretation of the first order formula can be given by the translation. Every formula can be translated, and the additional condition such as formula's having only one variable, or having both world domain and individual domain is not required. I introduce an indexical predicate 'E' for the (...) translation. The meaning that 'E(a)' is true is 'this world is 'a' '. Because of this meaning, I call 'E' an indexical predicate. 'E' plays an important role for the translation. In addition that the modal formulas can be translated into first order formulas, we can conclude that the first order logic and modal predicate logic isintertranslatable. (shrink)

In theTractatus, Wittgenstein advocates two major notational innovations in logic. First, identity is to be expressed by identity of the sign only, not by a sign for identity. Secondly, only one logical operator, called “N” by Wittgenstein, should be employed in the construction of compound formulas. We show that, despite claims to the contrary in the literature, both of these proposals can be realized, severally and jointly, in expressively complete systems of first-order logic. Building on early work of (...) Hintikka’s, we identify three ways in which the first notational convention can be implemented, show that two of these are compatible with the text of theTractatus, and argue on systematic and historical grounds, adducing posthumous work of Ramsey’s, for one of these as Wittgenstein’s envisaged method. With respect to the second Tractarian proposal, we discuss how Wittgenstein distinguished between general and non-general propositions and argue that, claims to the contrary notwithstanding, an expressively adequate N-operator notation is implicit in theTractatuswhen taken in its intellectual environment. We finally introduce a variety of sound and complete tableau calculi for first-order logics formulated in a Wittgensteinian notation. The first of these is based on the contemporary notion of logical truth as truth in all structures. The others take into account the Tractarian notion of logical truth as truth in all structures over one fixed universe of objects. Here the appropriate tableau rules depend on whether this universe is infinite or finite in size, and in the latter case on its exact finite cardinality.As it is obviously easy to express how propositions can be constructed by means of this operation and how propositions are not to be constructed by means of it, this must be capable of exact expression.5.503. (shrink)

Some internal and philosophical remarks are made regarding a system of a second order logic of existence axiomatized by the author. Attributes are distinguished in the system according as their possession entails existence or not, The former being called e-Attributes. Some discussion of the special principles assumed for e-Attributes is given as well as of the two notions of identity resulting from such a distinction among attributes. Non-Existing objects are of course indiscernible in terms of e-Attributes. In (...) addition, However, Existing objects indiscernible in terms of e-Attributes are indiscernible in terms of all attributes. (shrink)

We define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a (...) cut-elimination proof for the proof system. We also give examples showing what formulas can and cannot be used in the logic. (shrink)

Inquisitive first-order logic, InqBQ, is a system which extends classical first-order logic with formulas expressing questions. From a mathematical point of view, formulas in this logic express properties of sets of relational structures. This paper makes two contributions to the study of this logic. First, we describe an Ehrenfeucht–Fraïssé game for InqBQ and show that it characterizes the distinguishing power of the logic. Second, we use the game to study cardinality quantifiers in the inquisitive setting. That is, (...) we study what statements and questions can be expressed in InqBQ about the number of individuals satisfying a given predicate. As special cases, we show that several variants of the question how many individuals satisfy α(x) are not expressible in InqBQ, both in the general case and in restriction to finite models. (shrink)

Nous proposons dans cet article un développement de l’idée proposée par F.A. Hayek selon laquelle l’ordre du droit coutumier est un ordre d’action, une coordination des plans individuels dans un système d’échange régi par ce droit. Cette conception s’oppose à l’idée suivant laquelle l’ordre légal doit être avant tout fondé sur la cohérence logique des concepts et doctrines de ce droit. Un exemple important de cette approche est celui de la structure de maximisation des richesses de William Landes et Richard (...) Posner. L’article montre que la cohérence logique n’est ni nécessaire ni suffisante pour un ordre de plans ou pour une “cohérence praxéologique”. Nous défendons la position du droit coutumier classique suivant laquelle le droit se développe en accord avec les anticipations marginales des parties en présence. Dans la mesure où le droit se développe dans ce sens, il est possible d’approcher des objectifs jumelés du droit coutumier : la certitude relative et l’adaptation aux circonstances particulières.This article is a development of the idea, proposed by F.A. Hayek, that the order of common law is an order of actions, that is, a coordination of the plans of individuals in a system of exchanges governed by that law. This is in contrast to the idea that legal order is primarily to be found in the logical coherence of the law’s doctrines and concepts. The article shows that logical coherence is neither necessary nor sufficient for an order of plans, or “praxeological coherence”. It argues for the classic common law position that the law develops in accordance with the marginal expectations of the relevant parties. To the extent that the law develops in this way, it is possible for the twin goals of the common law to be approximated: relative certainty and adaptation to novel circumstances. (shrink)

Higher-Order Logic (HOL) is a proof development system intended for applications to both hardware and software. It is principally used in two ways: for directly proving theorems, and as theorem-proving support for application-specific verification systems. HOL is currently being applied to a wide variety of problems, including the specification and verification of critical systems. Introduction to HOL provides a coherent and self-contained description of HOL containing both a tutorial introduction and most of the material that is needed for (...) day-to-day work with the system. After a quick overview that gives a "hands-on feel" for the way HOL is used, there follows a detailed description of the ML language. The logic that HOL supports and how this logic is embedded in ML, are then described in detail. This is followed by an explanation of the theorem-proving infrastructure provided by HOL. Finally two appendices contain a subset of the reference manual, and an overview of the HOL library, including an example of an actual library documentation. (shrink)

The systems Kα of transfinite cumulative types up to α are extended to systems K∞α that include a natural infinitary inference rule, the so-called limit rule. For countable α a semantic completeness theorem for K∞α is proved by the method of reduction trees, and it is shown that every model of K∞α is equivalent to a cumulative hierarchy of sets. This is used to show that several axiomatic first-order set theories can be interpreted in K∞α, for suitable α.

An algebraization of multi-signature first-order logic without terms is presented. Rather than following the traditional method of choosing a type of algebras and constructing an appropriate variety, as is done in the case of cylindric and polyadic algebras, a new categorical algebraization method is used: The substitutions of formulas of one signature for relation symbols in another are treated in the object language. This enables the automatic generation via an adjunction of an algebraic theory. The algebras of this theory (...) are then used to algebraize first-order logic. (shrink)

A classical reconstruction of Wright’s first-order logic of strict finitism is presented. Strict finitism is a constructive standpoint of mathematics that is more restrictive than intuitionism. Wright sketched the semantics of said logic in Wright (Realism, Meaning and Truth, chap 4, 2nd edition in 1993. Blackwell Publishers, Oxford, Cambridge, pp.107-75, 1982), in his strict finitistic metatheory. Yamada (J Philos Log. [doi-url omitted], 2023) proposed, as its classical reconstruction, a propositional logic of strict finitism under an auxiliary condition that makes (...) the logic correspond with intuitionistic propositional logic. In this paper, we extend the propositional logic to a first-order logic that does not assume the condition. We will provide a sound and complete pair of a Kripke-style semantics and a natural deduction system, and show that if the condition is imposed, then the logic exhibits natural extensions of Yamada (2023)’s results. (shrink)

The paper presents Property Theory with Curry Typing (PTCT) where the language of terms and well-formed formulæ are joined by a language of types. In addition to supporting fine-grained intensionality, the basic theory is essentially first-order, so that implementations using the theory can apply standard first-order theorem proving techniques. Some extensions to the type theory are discussed, type polymorphism, and enriching the system with sufficient number theory to account for quantifiers of proportion, such as “most.”.

Regarding strictly monadic second‐order logic (SMSOL), which is the fragment of monadic second‐order logic in which all predicate constants are unary and there are no function symbols, we show that a standard deductive system with full comprehension is sound and complete with respect to standard semantics. This result is achieved by showing that in the case of SMSOL, the truth value of any formula in a faithful identity‐standard Henkin structure is preserved when the structure is “standardized”; that (...) is, the predicate domain is expanded into the set of all unary relations. In addition, we obtain a simpler proof of the decidability of SMSOL. (shrink)

In recent years large amounts of electronic texts have become available. While the first of these corpora had only a low level of annotation, the more recent ones are annotated with refined syntactic information. To make these rich annotations accessible for linguists, the development of query systems has become an important goal. One of the main difficulties in this task consists in the choice of the right query language, a language which at the same time should be powerful enough to (...) let users formulate the queries they want and which should be efficiently evaluable to keep query response times short. There is a widespread belief that such a query language does not exist. It is therefore the aim of this paper to show that there is indeed a powerful query language that can be efficiently evaluated. We propose the use of monadic second-order logic as a query language. We show that a query in this language can be evaluated in linear time in the size of a tree in the corpus. We also provide examples of complicated linguistic queries expressed in monadic second-order logic thereby demonstrating the high expressive power of the language. (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations (...) are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)

The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical (...) system of the Grundgesetze and the one given by Martin-Löf for the intuitionistic type theory with a type of all types.The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast domain for foundational research. (shrink)

This article studies the mathematical properties of two systems that model Aristotle's original syllogistic and the relationship obtaining between them. These systems are Corcoran's natural deduction syllogistic and ?ukasiewicz's axiomatization of the syllogistic. We show that by translating the former into a first-order theory, which we call T RD, we can establish a precise relationship between the two systems. We prove within the framework of first-order logic a number of logical properties about T RD that bear upon (...) the same properties of the natural deduction counterpart ? that is, Corcoran's system. Moreover, the first-order logic framework that we work with allows us to understand how complicated the semantics of the syllogistic is in providing us with examples of bizarre, unexpected interpretations of the syllogistic rules. Finally, we provide a first attempt at finding the structure of that semantics, reducing the search to the characterization of the class of models of T RD. (shrink)

In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this paper, we consider logic systems called L'T without this kind of constants but limited to the case where T is a finite poset. We study the tableau method for this system and we prove its completeness for a class of formulas with respect to (...) an algebraic semantics. (shrink)

We consider one aspect of the problem of specification and verification of reactive real-time systems which involve operations and constraints concerning time. Time is continuous what is motivated by specifications of hybrid systems. Our goal is to try to find a framework that is based on applied first order logic that permits to represent the verification problem directly, completely and conservatively , and that is apt to describe interesting decidable classes, maybe showing way to feasible algorithms. To achieve this (...) goal we use a first order timed logic that is an extension of a decidable theory of reals with timed functions. This logic permits, on the one hand, to rewrite directly and completely requirements and, on the other hand, to describe executions of various timed algorithms—here we consider block Gurevich abstract state machines because of their theoretical clarity and sufficient expressive power. Then we describe one decidable class of the verification problem that is based on notions reflecting finiteness properties of systems of control. These notions may be of independent interest, as, in particular, they give a way to describe a limited usage of arithmetics preserving decidability that is not covered by existing model-theoretic approaches. As an example we consider the generalized railroad crossing problem that we analyze in its entirety. (shrink)

This paper follows Part I of our essay on case-intensional first-order logic ). We introduce a framework of branching histories to take account of indeterminism. Our system BH-CIFOL adds structure to the cases, which in Part I formed just a set: a case in BH-CIFOL is a moment/history pair, specifying both an element of a partial ordering of moments and one of the total courses of events that that moment is part of. This framework allows us to define (...) the familiar Ockhamist temporal/modal connectives, most notably for past, future, and settledness. The novelty of our framework becomes visible in our discussion of substances in branching histories, i.e., in its first-order part. That discussion shows how the basic idea of tracing an individual thing from case to case via an absolute property is applicable in a branching histories framework. We stress the importance of keeping apart extensionality and moment-definiteness, and give a formal account of how the specification of natural sortals and natural qualities turns out to be a coordination task in BH-CIFOL. We also provide a detailed answer to Lewis’s well-known argument against branching histories, exposing the fallacy in that argument. (shrink)

The paper studies first order extensions of classical systems of modal logic (see (Chellas, 1980, part III)). We focus on the role of the Barcan formulas. It is shown that these formulas correspond to fundamental properties of neighborhood frames. The results have interesting applications in epistemic logic. In particular we suggest that the proposed models can be used in order to study monadic operators of probability (Kyburg, 1990) and likelihood (Halpern-Rabin, 1987).