Online research in philosophy

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)

Classical logic has proved inadequate in various areas of computer science, artificial intelligence, mathematics, philosopy and linguistics. This is an introduction to extensions of first-order logic, based on the principle that many-sorted logic (MSL) provides a unifying framework in which to place, for example, second-order logic, type theory, modal and dynamic logics and MSL itself. The aim is two fold: only one theorem-prover is needed; proofs of the metaproperties of the different existing calculi can be (...) avoided by borrowing them from MSL. To make the book accessible to readers from different disciplines, whilst maintaining precision, the author has supplied detailed step-by-step proofs, avoiding difficult arguments, and continually motivating the material with examples. Consequently this can be used as a reference, for self-teaching or for first-year graduate courses. (shrink)

Well-written undergraduate-level introduction begins with symbolic logic and set theory, followed by presentation of statement calculus and predicate calculus. First-order theories are discussed in some detail, with special emphasis on number theory. After a discussion of truth and models, the completeness theorem is proved. "...an excellent text."—Mathematical Reviews. Exercises. Bibliography.

Introduction This is an elementary logic book designed for people who have no technical familiarity with modern logic but who have been reasoning, ...

This completely self-contained study, widely considered the best book in the field, is intended to serve both as an introduction to quantification theory and as ...

This work makes available to readers without specialized training in mathematics complete proofs of the fundamental metatheorems of standard (i.e., basically ...

We extend first-order logic to include variadic function symbols, and prove a substitution lemma. Two applications are given: one to bounded quantifier elimination and one to the definability of certain Borel sets.

This is part I of a two-part essay introducing case-intensional first order logic (CIFOL), an easy-to-use, uniform, powerful, and useful combination of first-order logic with modal logic resulting from philosophical and technical modifications of Bressan’s General interpreted modal calculus (Yale University Press 1972 ). CIFOL starts with a set of cases; each expression has an extension in each case and an intension, which is the function from the cases to the respective case-relative extensions. Predication is intensional; (...) identity is extensional. Definite descriptions are context-independent terms, and lambda-predicates and -operators can be introduced without constraints. These logical resources allow one to define, within CIFOL, important properties of properties, viz., extensionality (whether the property applies, depends only on an extension in one case) and absoluteness, Bressan’s chief innovation that allows tracing an individual across cases without recourse to any notion of “rigid designation” or “trans-world identity.” Thereby CIFOL abstains from incorporating any metaphysical principles into the quantificational machinery, unlike extant frameworks of quantified modal logic. We claim that this neutrality makes CIFOL a useful tool for discussing both metaphysical and scientific arguments involving modality and quantification, and we illustrate by discussing in diagrammatic detail a number of such arguments involving the extensional identification of individuals via absolute (substance) properties, essential properties, de re vs. de dicto , and the results of possible tests. (shrink)

We present a compositional semantics for first-order logic with imperfect information that is equivalent to Sevenster and Sandu’s equilibrium semantics (under which the truth value of a sentence in a finite model is equal to the minimax value of its semantic game). Our semantics is a generalization of an earlier semantics developed by the first author that was based on behavioral strategies, rather than mixed strategies.

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 Lukasiewicz'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)

What has been the historical relationship between set theory and logic? On the óne 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 question 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)

We consider a new fragment of first-order logic with two variables. This logic is defined over interval structures. It constitutes unary predicates, a binary predicate and a function symbol. Considering such a fragment of first-order logic is motivated by defining a general framework for event-based interval temporal logics. In this paper, we present a sound, complete and terminating decision procedure for this logic. We show that the logic is decidable, and provide a NEXPTIME (...) complexity bound for satisfiability. This result shows that even a simple decidable fragment of first-order logic has NEXPTIME complexity. (shrink)

Van Lambalgen (1990) proposed a translation from a language containing a generalized quantifierQ into a first-order language enriched with a family of predicatesR i, for every arityi (or an infinitary predicateR) which takesQxg(x, y1,..., yn) to x(R(x, y1,..., y1) (x,y1,...,yn)) (y 1,...,yn are precisely the free variables ofQx). The logic ofQ (without ordinary quantifiers) corresponds therefore to the fragment of first-order logic which contains only specially restricted quantification. We prove that it is decidable using the method (...) of analytic tableaux. Related results were obtained by Andréka and Németi (1994) using the methods of algebraic logic. (shrink)

The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO 2 over ordered, respectively wellordered, domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems (...) is essentially the same as for plain unconstrained FO 2 , namely non-deterministic exponential time. In contrast FO 2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO 2 and computation tree logic CTL. (shrink)

There are properties of finite structures that are expressible with the use of Hilbert's ε-operator in a manner that does not depend on the actual interpretation for ε-terms, but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power (...) of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide (...) regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it (...) has a finite model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

The aim of this paper is to give a new proof for the decidability and finite model property of first-order logic with two variables (without function symbols), using a combinatorial theorem due to Herwig. The results are proved in the framework of polyadic equality set algebras of dimension two (Pse 2 ). The new proof also shows the known results that the universal theory of Pse 2 is decidable and that every finite Pse 2 can be represented on (...) a finite base. Since the class Cs 2 of cylindric set algebras of dimension 2 forms a reduct of Pse 2 , these results extend to Cs 2 as well. (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.1 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)

Continuous first-order logic has found interest among model theorists who wish to extend the classical analysis of “algebraic” structures (such as fields, group, and graphs) to various natural classes of complete metric structures (such as probability algebras, Hilbert spaces, and Banach spaces). With research in continuous first-order logic preoccupied with studying the model theory of this framework, we find a natural question calls for attention. Is there an interesting set of axioms yielding a completeness result? The (...) primary purpose of this article is to show that a certain, interesting set of axioms does indeed yield a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies an approximated form of strong completeness, whereby Σ⊨φ (if and) only if Σ⊢φ∸ 2-n for all n < ω. This approximated form of strong completeness asserts that if Σ⊨φ, then proofs from Σ, being finite, can provide arbitrarily better approximations of the truth of φ. Additionally, we consider a different kind of question traditionally arising in model theory—that of decidability. When is the set of all consequences of a theory (in a countable, recursive language) recursive? Say that a complete theory T is decidable if for every sentence φ, the value φT is a recursive real, and moreover, uniformly computable from φ. If T is incomplete, we say it is decidable if for every sentence φ the real number φT∘ is uniformly recursive from φ, where φT∘ is the maximal value of φ consistent with T. As in classical first-order logic, it follows from the completeness theorem of continuous first-order logic that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable. (shrink)

Applying first-order logic to derive the consequences of laws that are only approximately true of empirical phenomena involves idealization of a kind that is akin to applying arithmetic to calculate the area of a rectangular surface from approximate measures of the lengths of its sides. Errors in the data, in the exactness of the lengths in one case and in the exactness of the laws in the other, are in some measure transmitted to the consequences deduced from them, (...) and the aim of a theory of idealization is to describe this process. The present paper makes a start on this in the case of applied first-order logic, and relates it to Plato's picture of a world or model of 'appearances' in which laws are only approximately true, but which to some extent resembles an ideal world or model in which they are exactly true. (shrink)

‘Quantified pure existentials’ are sentences (e.g., ‘Some things do not exist’) which meet these conditions: (i) the verb EXIST is contained in, and is, apart from quantificational BE, the only full (as against auxiliary) verb in the sentence; (ii) no (other) logical predicate features in the sentence; (iii) no name or other sub-sentential referring expression features in the sentence; (iv) the sentence contains a quantifier that is not an occurrence of EXIST. Colin McGinn and Rod Girle have alleged that standard (...) first-order logic cannot adequately deal with some such existentials. The article defends the view that it can. (shrink)

This is Part I of a two-part essay introducing case-intensional first-order logic (CIFOL), an easy-to-use, uniform, powerful, and useful combination of first order logic with modal logic resulting from philosophical and technical modifications of Bressan’s General interpreted modal calculus (Yale University Press 1972). CIFOL starts with a set of cases; each expression has an extension in each case and an intension, which is the function from the cases to the respective case-relative extensions. Predication is intensional; identity (...) is extensional. Definite descriptions are context-independent terms, and lambda-predicates and -operators can be introduced without constraints. These logical resources allow one to define, within CIFOL, important properties of properties, viz., extensionality (whether the property applies, depends only on an extension in one case) and absoluteness, Bressan’s chief innovation that allows tracing an individual across cases without recourse to any notion of “rigid designation” or “trans-world identity.” Thereby CIFOL abstains from incorporating any metaphysical principles into the quantificational machinery, unlike extant frameworks of quantified modal logic. We claim that this neutrality makes CIFOL a useful tool for discussing both metaphysical and scientific arguments involving modality and quantification, and we illustrate by discussing in diagrammatic detail a number of such arguments involving the extensional identification of individuals via absolute (substance) properties, essential properties, de re vs. de dicto, and the results of possible tests. (shrink)

We show that the loosely guarded and packed fragments of first-order logic have the finite model property. We use a construction of Herwig and Hrushovski. We point out some consequences in temporal predicate logic and algebraic logic.

to a number of issues related to testing and specification. Brief review of first order logic. Use of first order logic for specification, in the specification tool Alloy.

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)

This paper responds to criticism of the Kripkean account of logical truth in first-order modal logic. The criticism, largely ignored in the literature, claims that when the box and diamond are interpreted as the logical modality operators, the Kripkean account is extensionally incorrect because it fails to reflect the fact that all sentences stating truths about what is logically possible are themselves logically necessary. I defend the Kripkean account by arguing that some true sentences about logical possibility are (...) not logically necessary. (shrink)

This paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01]. We introduce an operation $esists_{n}(S)$ on properties S that says "there are n components having S". We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a (...) corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict. We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W. We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that $\prod_{n}\nsubseteq FO(\Sigma_{n})$ , $\Sigma_{n} \nsubseteq FO(\delta_{n})$ , and $\delta_{n+1} \nsubseteq FOB(\Sigma_{n})$ , solving some open problems raised in [Mat98]. (shrink)

This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established for (...) the Gentzen-type system, and then transferred to resolution. The propositional resolution system was implemented by T. Tammet. (shrink)

In this paper we will discuss the first order multiplicative intuitionistic fragment of linear logic, MILL1, and its applications to linguistics. We give an embedding translation from formulas in the Lambek Calculus to formulas in MILL1 and show this translation is sound and complete. We then exploit the extra power of the first order fragment to give an account of a number of linguistic phenomena which have no satisfactory treatment in the Lambek Calculus.

Provided here is an account, both syntactic and semantic, of first-order and monadic second-order quantification theory for domains that may be non-atomic. Although the rules of inference largely parallel those of classical logic, there are important differences in connection with the identification of argument places and the significance of the identity relation.

In the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic. All results included here, but a part of the proposition (a) below, are new. This work is, (...) ideally, a continuation of a paper by McCarty, who considered intuitionistic completeness mostly for first order intuitionistic logic. (shrink)

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we (...) prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic. (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)

As McKinsey and Tarksi showed, the Stone representation theorem for Boolean algebras extends to algebras with operators to give topological semantics for (classical) propositional modal logic, in which the "necessity" operation is modeled by taking the interior of an arbitrary subset of a topological space. in this paper the topological interpretation is extended in a natural way to arbitrary theories of full first-order logic. The resulting system of S4 first-order modal logic is complete with respect (...) to such topological semantics. (shrink)

Jaakko Hintikka has argued that ordinary first-order logic should be replaced byindependence-friendly first-order logic, where essentially branching quantificationcan be represented. One recurring criticism of Hintikka has been that Hintikka''ssupposedly new logic is equivalent to a system of second-order logic, and henceis neither novel nor first-order. A standard reply to this criticism by Hintikka andhis defenders has been to show that given game-theoretic semantics, Hintikka''sbranching quantifiers receive the exact same treatment as the regular first-orderones. (...) We develop a different reply, based around considerations concerning thenature of logic. In particular, we argue that Hintikka''s logic is the logic that bestrepresents the language fragment standard first-order logic is meantto represent. Therefore it earns its keep, and is also properly regarded as first-order. (shrink)

The paper focuses on extending to the first order case the semantical program for modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer in the first part of the paper a series of new completeness results for salient classical systems of first order modal logic. Among other results we show that it is possible to prove strong completeness results for normal systems without the Barcan Formula (...) (like FOL + K)in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. Models of this type are either difficult of impossible to build in terms of relational Kripkean semantics [40].We conclude by introducing general first order neighborhood frames with constant domains and we offer a general completeness result for the entire family of classical first order modal systems in terms of them, circumventing some well-known problems of propositional and first order neighborhood semantics (mainly the fact that many classical modal logics are incomplete with respect to an unmodified version of either neighborhood or relational frames). We argue that the semantical program that thus arises offers the first complete semantic unification of the family of classical first order modal logics. (shrink)

We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.We also add a few axioms to find a sound and complete axiomatisation for the first order temporal logic of Until and Since over rational numbers time.

This paper focuses on extending to the first order case the semantical program for modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer in the first part of the paper a series of new completeness results for salient classical systems of first order modal logic.

We consider the decision problem for cases of first-order temporal logic with function symbols and without equality. The monadic monodic fragment with flexible functions can be decided with EXPSPACE-complete complexity. A single rigid function is sufficient to make the logic not recursively enumerable. However, the monadic monodic fragment with rigid functions, where no two distinct terms have variables bound by the same quantifier, is decidable and EXPSPACE-complete.

This paper is an attempt to develop the many-valued first-order fuzzy logic. The set of its truth, values is supposed to be either a finite chain or the interval 0, 1 of reals. These are special cases of a residuated lattice L, , , , , 1, 0. It has been previously proved that the fuzzy propositional logic based on the same sets of truth values is semantically complete. In this paper the syntax and semantics of the (...) first-order fuzzy logic is developed. Except for the basic connectives and quantifiers, its language may contain also additional n-ary connectives and quantifiers. Many propositions analogous to those in the classical logic are proved. The notion of the fuzzy theory in the first-order fuzzy logic is introduced and its canonical model is constructed. Finally, the extensions of Gödel's completeness theorems are proved which confirm that the first-order fuzzy logic is also semantically complete. (shrink)

First-order modal logic is very much under current development, with many different semantics proposed. The use of rigid objects goes back to Saul Kripke. More recently several semantics based on counterparts have been examined, in a development that goes back to David Lewis. There is yet another line of research, using intensional objects, that traces back to Richard Montague. I have been involved with this line of development for some time. In the present paper I briefly sketch (...) several of the approaches to first-order modal logic. Then I present one that I call FOIL (for first-order intensional logic) in the Montague tradition that, I believe, is both expressive and natural. I briefly discuss in what sense it can be made to encompass the other approaches. Finally I provide tableau rules to go with the FOIL semantics. (shrink)

Horacio Arlo-Costa. First Order Extensions of Classical Systems of Modal Logic: The Role of Barcan Schemas.

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.

It is a popular view amongst some philosophers, most notably those with Quinean views about ontological commitment, that scientific theories are first-orderizable; that we can regiment all such theories in an extensional first-order language. I argue that this view is false, and that any acceptable account of science needs to take some modal notion as primitive.

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).

Features are unary operators used to build record-like expressions. The resulting term algebras are encountered in linguistic computation and knowledge representation. We present a general description of feature logic and of a slightly restricted version, called record logic. It is shown that every first-order theory can be faithfully interpreted in a record logic with various additional axioms. This fact is used elsewhere [15] to extend a result of Tarski and Givant [14] on expressing first order theories (...) in relation algebra. (shrink)

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.

We prove that for a natural class of first-order formulas the validity problem is Π p 2 -complete.

This paper provides finitary jointly necessary and sufficient acceptance and rejection conditions for the logical constants of a first order quantificational language. By introducing the notion of making an assignment as a distinct object level practice—something you do with a sentence—(as opposed to a meta-level semantic notion) and combining this with the practice of (hypothetical and categorical) acceptance and rejection and the practice of making suppositions one gains a structure that is sufficiently rich to fully characterize the class of classical (...) first order theories. The analysis thus provides a way of characterizing classical first order quantification by expressivist means. (shrink)

Restricted to first-order formulas, the rules of inference in the Curry-Howard type theory are equivalent to those of first-order predicate logic as formalized by Heyting, with one exception: ∃-elimination in the Curry-Howard theory, where ∃x : A.F (x) is understood as disjoint union, are the projections, and these do not preserve firstorderedness. This note shows, however, that the Curry-Howard theory is conservative over Heyting’s system.

The purpose of this article is to delimit what can and cannot be claimed on behalf of second-order logic. The starting point is some of the discussions surrounding my Foundations without Foundationalism: A Case for Secondorder Logic.

From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time.

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.”.

We de ne an executable process interpretation for dynamic rst order logic and show that it is a faithful approximation of a dynamic interpre tation procedure for rst order formulas familiar from natural language semantics extended with constructs for bounded choice and bounded it eration This new interpretation of extended dynamic FOL is inspired by an executable interpretation for standard FOL proposed by Apt and Bezem The relation to the Apt Bezem style execution process and the advantages of taking (...) dynamic FOL rather than standard FOL as one s point of reference are discussed at some length Our results relate computational interpretation of FOL to a research tra dition from natural language semantics We discuss some example pro grams in Dynamo a simple language for dynamic logic programming based on the executable process interpretation for dynamic FOL.. (shrink)

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

For first order languages with no individual constants, empty structures and truth values (for sentences) in them are defined. The first order theories of the empty structures and of all structures (the empty ones included) are axiomatized with modus ponens as the only rule of inference. Compactness is proved and decidability is discussed. Furthermore, some well known theorems of model theory are reconsidered under this new situation. Finally, a word is said on other approaches to the whole problem.

A BSTRACT. 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.1 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 typetheoretic approach to pronominal anaphora that avoids some of the difficulties that (...) undermine previous type-theoretic analyses of this phenomenon. (shrink)

The theorem to the effect that the languageL introduced in [2] is mutually interpretable with the first order language is proved. This yields several model-theoretical results concerningL.

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.1 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)

We describe a new way in which theories about the deontic status of actions can be represented in terms of the standard two-sorted first-order extensional predicate calculus. Some of the resulting formal theories are easy to implement in Prolog; one prototype implementation—R. M. Lee's deontic expert shell DX—is briefly described.

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.

Classical first-order logic can be extended in two different ways to serve as a foundation for mathematics: introduce higher orders, type theory, or introduce sets. As it happens, both approaches have natural analogs for quantified modal logics, both approaches date from the 1960’s, one is not very well-known, and the other is well-known as something else. I will present the basic semantic ideas of both higher order intensional logic, and intensional set theory. Before doing so, I’ll quickly (...) sketch some necessary background material from quantified modal logic. Except for standard material concerning propositional modal logics, the paper is essentially self-contained. (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. The paper sketches a system of tableau rules that implement the theory. Some extensions to the type theory are discussed, including type polymorphism, which provides a useful analysis of conjunctive (...) terms. Such terms can be given a single polymorphic type that expresses the fact that they can conjoin phrases of any one type, yielding an expression of the same type. (shrink)

Certain extensions of Nelson's constructive logic N with strong negation have recently become important in arti.cial intelligence and nonmonotonic reasoning, since they yield a logical foundation for answer set programming (ASP). In this paper we look at some extensions of Nelson's .rst-order logic as a basis for de.ning nonmonotonic inference relations that underlie the answer set programming semantics. The extensions we consider are those based on 2-element, here-and-there Kripke frames. In particular, we prove completeness for .rst-order here-and-there logics, (...) and their minimal strong negation extensions, for both constant and varying domains. We choose the constant domain version, which we denote by QNc5, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic properties of QNc5, including Skolem forms and Herbrand theorems and Interpolation, and show that the .rst-oder version of equilibrium logic can be used as a foundation for answer set inference. (shrink)

It is almost universally acknowledged that first-order logic (FOL), with its clean, well-understood syntax and semantics, allows for the clear expression of philosophical arguments and ideas. Indeed, an argument or philosophical theory rendered in FOL is perhaps the cleanest example there is of “representing philosophy”. A number of prominent syntactic and semantic properties of FOL reflect metaphysical presuppositions that stem from its Fregean origins, particularly the idea of an inviolable divide between concept and object. These presuppositions, taken at (...) face value, reflect a significant metaphysical viewpoint, one that can in fact hinder or prejudice the representation of philosophical ideas and arguments. Philosophers have of course noticed this and have, accordingly, sought to alter or extend traditional FOL in novel ways to reflect a more flexible and egalitarian metaphysical standpoint. The purpose of this paper, however, is to document and discuss how similar “adaptations” to FOL—culminating in a standardized framework known as Common Logic —have evolved out of the more practical and applied encounter of FOL with the problem of representing, sharing, and reasoning upon information on the World Wide Web. (shrink)

Dependence is a common phenomenon, wherever one looks: ecological systems, astronomy, human history, stock markets - but what is the logic of dependence? This book is the first to carry out a systematic logical study of this important concept, giving on the way a precise mathematical treatment of Hintikka’s independence friendly logic. Dependence logic adds the concept of dependence to first order logic. Here the syntax and semantics of dependence logic are studied, dependence logic (...) is given an alternative game theoretic semantics, and results about its complexity are proven. This is a graduate textbook suitable for a special course in logic in mathematics, philosophy and computer science departments, and contains over 200 exercises, many of which have a full solution at the end of the book. It is also accessible to readers, with a basic knowledge of logic, interested in new phenomena in logic. (shrink)

The main tool of the arithmetization and logization of analysis in the history of nineteenth century mathematics was an informal logic of quantifiers in the guise of the “epsilon–delta” technique. Mathematicians slowly worked out the problems encountered in using it, but logicians from Frege on did not understand it let alone formalize it, and instead used an unnecessarily poor logic of quantifiers, viz. the traditional, first-order logic. This logic does not e.g. allow the definition and (...) study of mathematicians’ uniformity concepts important in analysis. Mathematicians’ stronger logic was rediscovered around 1990 as the form of independence-friendly logic which hence is not a new logic nor a further development of ordinary first-order logic but a richer version of it. (shrink)

1. Logic programming did not seize the attention of most programmers until the Japanese announced that they had chosen Prolog for their ambitious Fifth Generation Computer Systems project. While that project appeàrs now to be hampered by bureaucratic difficulties, the interest it aroused in Prolog lives on. Part of the attraction of Prolog stems from the fact that the beginner will very quickly be able to write toy programs, even spectacular ones. Difficulties in creating larger programs, however, seem to (...) bring back Prolog to the level of other programming languages. Such difficulties arise from numerous defects of Prolog, some of which are purely logicai in nature. Among the latter at least two should be mentioned: (a) the peculiar meaning of negation; (b) the fact that reduction to clausal form is not part of the language. As to (a), strictly speaking Prolog has no negation. Its notion ot.negation- as-failure - by which -i <p is inferred from fatture to infer y - is a tricky one. For instance, suppose that the goal likes (John, X ) succeeds with X instantiated to mary. Then not (likes (John, X )) fails, so X becomes uninstantiated and hence has no value. However not (not (likes (John, X ))) succeeds with X instantiated to mary. This makes the meaning of negation almost incomprehensible. As to (b), for efficiency Prolog uses the programmer, as it were, as a preprocessor for reduction to clausal form: with the gain in efficiency that one can very well imagine. Of course reduction to clausal form can be implemented in Prolog and bùilt up within every Prolog program together with a suitable user interface, but this is very much like designing a new programming language. (shrink)

Though regarded today as one of the most important results in logic, the compactness theorem was largely ignored until nearly two decades after its discovery. This paper describes the vicissitudes of its evolution and transformation during the period 1930-1970, with special attention to the roles of Kurt Gödel, A. I. Maltsev, Leon Henkin, Abraham Robinson, and Alfred Tarski.

We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.

Motivation and perspective for an exciting new research direction interconnecting logic, spacetime theory, relativity--including such revolutionary areas as black hole physics, relativistic computers, new cosmology--are presented in this paper. We would like to invite the logician reader to take part in this grand enterprise of the new century. Besides general perspective and motivation, we present initial results in this direction.

Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HA ω into a type theory WL, that can be described as Troelstra's system ML 1 0 with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HA ω if and only if its corresponding type in WL is inhabited. Analogous results are proved for Diller's so-called (...) restricted system and for a type theory based on predicate logic instead of arithmetic. (shrink)