The topics of structural proof theory and logic programming have influenced each other for more than three decades. Proof theory has contributed the notion of sequent calculus, linear logic, and higher-order quantification. Logic programming has introduced new normal forms of proofs and forced the examination of logic-based approaches to the treatment of bindings. As a result, proof theory has responded by developing an approach to proof search based on focused proof systems in which introduction rules are organized into two alternating (...) phases of rule application. Since the logic programming community can generate many examples and many design goals, the close connections with proof theory have helped to keep proof theory relevant to the general topic of computational logic. (shrink)

Leon Henkin (1921–2006) was not only an extraordinary logician, but also an excellent teacher, a dedicated professor and an exceptional person. The first two sections of this paper are biographical, discussing both his personal and academic life. In the last section we present three aspects of Henkin’s work. First we comment part of his work fruit of his emphasis on teaching. In a personal communication he affirms that On mathematical induction, published in 1969, was the favourite among his articles with (...) a somewhat panoramic nature and not meant exclusively to specialists. This subject is covered in the first subsection. Needless to say that we also analyse Henkin’s better known contribution: his completeness method. His renowned results on completeness for both type theory and first order logic were part of his thesis, The Completeness of Formal Systems, presented at Princeton in 1947 under the advise of Alonzo Church. It is interesting to note that he obtained the proof of completeness for first order logic readapting the argument for the theory of types. The last subsection is devoted to philosophy. The work most directly related to philosophy is an article entitled: Some Notes on Nominalism which appeared in the Journal of Symbolic Logic in 1953. Unfortunately, we are not covering his contribution to the field of cylindric algebras. As a matter of fact, Henkin spent many years investigating algebraic structures with Alfred Tarski and Donald Monk, among others. (shrink)

This article is an extended promenade strolling along the winding roads of identity, equality, nameability and completeness, looking for places where they converge. We have distinguished between identity and equality; the first is a binary relation between objects while the second is a symbolic relation between terms. Owing to the central role the notion of identity plays in logic, you can be interested either in how to define it using other logical concepts or in the opposite scheme. In the first (...) case, one investigates what kind of logic is required. In the second case, one is interested in the definition of the other logical concepts in terms of the identity relation, using also abstraction. The present paper investigates whether identity can be introduced by definition arriving to the conclusion that only in full higher-order logic a reliable definition of identity is possible. However, the definition needs the standard semantics and we know that with this semantics completeness is lost. We have also studied the relationship of equality with comprehension and extensionality and pointed out the relevant role played by these two axioms in Henkin’s completeness method. We finish our paper with a section devoted to general semantics, where the role played by the nameable hierarchy of types is the key in Henkin’s completeness method. (shrink)

English distinguishes between singular quantifiers like "a donkey" and plural quantifiers like "some donkeys". Pluralists hold that plural quantifiers range in an unusual, irreducibly plural, way over common objects, namely individuals from first-order domains and not over set-like objects. The favoured framework of pluralism is plural first-order logic, PFO, an interpreted first-order language that is capable of expressing plural quantification. Pluralists argue for their position by claiming that the standard formal theory based on PFO is both ontologically neutral and really (...) logic. These properties are supposed to yield many important applications concerning second-order logic and set theory that alternative theories supposedly cannot deliver. I will show that there are serious reasons for rejecting at least the claim of ontological innocence. Doubt about innocence arises on account of the fact that, when properly spelled out, the PFO-semantics for plural quantifiers is committed to set-like objects. The correctness of my worries presupposes the principle that for every plurality there is a coextensive set. Pluralists might reply that this principle leads straight to paradox. However, as I will argue, the true culprit of the paradox is the assumption that every definite condition determines a plurality. (shrink)

ABSTRACT Backwards-looking operators Saarinen, E. [1979. “Backwards-Looking Operators in Tense Logic and in Natural Language.” In Essays on Mathematical and Philosophical Logic, edited by J. Hintikka, I. Niiniluoto, and E. Saarinen, 341–367. Dordrecht: Reidel] that have the material in their scope depend on higher intensional operators, are known to increase the expressivity of some intensional languages and have thus played a central role in debates about approaches to intensionality in terms of implicit parameters vs. variables explicitly quantifying over them. The (...) current contribution takes a look at these operators from a type-logical perspective. It is shown that extending Gallin's translation from intensional type logic to two-sorted type theory so as to include a version of Yanovich's backwards-looking operators, does not increase the expressive power of formulae with exclusively intensional parameters. The result, which makes use of a theorem by Zimmermann : 65–77]), is illustrated by pertinent examples from the literature. The paper closes by indicating alternative strategies of incorporating backwards-looking operators. (shrink)

I present an analysis according to which the current state of the definition of substitution leads to a contradiction in the system of Transparent Intensional Logic. I entail the contradiction using only the basic definitions of TIL and standard results. I then analyse the roots of the contradiction and motivate the path I take in resolving the contradiction. I provide a new amended definition of collision-less substitution which blocks the contradiction in a non-ad hoc way. I elaborate on the consequences (...) of the amended definition, namely the invalidity of the Church-Rosser theorem. I present a counterexample to the validity of the theorem in TIL with an amended definition of substitution. (shrink)

Cooper storage is a widespread technique for associating sentences with their meanings, used in diverse linguistic and computational linguistic traditions. This paper encodes the data structures and operations of cooper storage in the simply typed linear \-calculus, revealing the rich categorical structure of a graded applicative functor. In the case of finite cooper storage, which corresponds to ideas in current transformational approaches to syntax, the semantic interpretation function can be given as a linear homomorphism acting on a regular set of (...) trees, and thus generation can be done in polynomial time. (shrink)

A standard formalization of a scientific theory is a system of axioms for that theory in a first-order language (possibly many-sorted; possibly with the membership primitive $$\in$$ ). Suppes (in: Carvallo M (ed) Nature, cognition and system II. Kluwer, Dordrecht, 1992) expressed skepticism about whether there is a “simple or elegant method” for presenting mathematicized scientific theories in such a standard formalization, because they “assume a great deal of mathematics as part of their substructure”. The major difficulties amount to these. (...) First, as the theories of interest are mathematicized, one must specify the underlying applied mathematics base theory, which the physical axioms live on top of. Second, such theories are typically geometric, concerning quantities or trajectories in space/time: so, one must specify the underlying physical geometry. Third, the differential equations involved generally refer to coordinate representations of these physical quantities with respect to some implicit coordinate chart, not to the original quantities. These issues may be resolved. Once this is done, constructing standard formalizations is not so difficult—at least for the theories where the mathematics has been worked out rigorously. Here we give what may be claimed to be a simple and elegant means of doing that. This is for mathematicized scientific theories comprising differential equations for $$\mathbb{R}$$ -valued quantities Q (that is, scalar fields), defined on n (“spatial” or “temporal”) dimensions, taken to be isomorphic to the usual Euclidean space $$\mathbb{R}^n$$. For illustration, I give standard (in a sense, “text-book”) formalizations: for the simple harmonic oscillator equation in one-dimension and for the Laplace equation in two dimensions. (shrink)

We formulate a Curry-typed logic with fine-grained intensionality within Turner’s typed predicate logic. This allows for an elegant presentation of a theory that corresponds to Fox and Lappin’s property theory with curry typing, but without the need for a federation of languages. We then consider how the fine-grained intensionality of this theory can be given an operational interpretation. This interpretation suggests itself as expressions in the theory can be viewed as terms in the untyped lambda-calculus, which provides a model of (...) computation. (shrink)

The restrictive grammatical format suggested in GPSG provides an extremely interesting alternative to transformational approaches to grammar. However, we have seen that the way the grammar is currently organized, it will in certain cases fail to give the correct interpretation to sentences with displaced constituents. Whenever a left or rightward displaced constituent contains an element that can stand in an anaphoric relation with some other element in the sentence, i.e. contains a quantifier or a pronoun, the semantic rules as given (...) do not provide the intended reading. It should be made clear, however, that this shortcoming pertains to one particular type of GPSG, namely one whose interpretation procedures make use of lambda abstraction. The problematic cases addressed here do not by themselves invalidate the syntactic framework of a GPSG. It seems quite plausible that one could construct a semantics that does not depend on lambda conversion, in which case the problem addressed in this note is presumably no longer relevant. One such proposal is put forward in Cooper (forthcoming) where a non-movement syntax is combined with interpretation procedures that do not involve translation into a lambda calculus. (shrink)

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program of Friedman and Simpson. We look in particular at: (i) the long arc from Poincar\'e to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles equivalent to Weak K\"onig's (...) Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others. (shrink)

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

Když jsem v roce 1992 začínal na filosofické fakultě UK přednášet teorii sémantiky, cítil jsem intenzivní potřebu poskytnout studentům nějaký učební text. O překotném vývoji tohoto interdisciplinárního oboru, který odstartovalo v sedmdesátých letech úspěšné “zkřížení logiky s lingvistikou” Richardem Montaguem a dalšími a který se nezpomalil dodnes, totiž v češtině neexistovaly prakticky žádné zprávy (s čestnou výjimkou přístupu tzv. transparentní intenzionální logiky, který byl dílem českého emigranta Pavla Tichého a o kterém u nás psal Pavel Materna). Přehledové publikace, jaké jsou (...) potřeba pro někoho, kdo se chce v dané problematice zorientovat, se ovšem v té době i po světě teprve začínaly objevovat: v roce 1990 vyšla kniha An Introduction to Semantics Gennara Chierchii a Sally McConell-Ginnetové a v roce 1991 vydala skupina holandských logiků pod kolektivním pseudonymem L.T.F. Gamut dvousvazkovou knihu Language and Meaning. Za této situace jsem se pokusil co nejrychleji sepsat učební text, který by moji studenti i jiní zájemci o sémantiku mohli použít; a protože o jeho vydání paradoxně projevila větší zájem filosofická fakulta Masarykovy univerzity v Brně (kde jsem já osobně nikdy neučil; ale zájem o sémantiku tam neúnavně podněcoval a vydání mého textu tam zprostředkoval kolega Materna) než filosofická fakulta mojí domovské Karlovy univerzity, vyšel tento text v Brně, a to pod názvem Úvod do teoretické sémantiky. (shrink)

In this paper, we will briefly look at the history of mathematical fuzzy logic in Czechoslovakia starting from the 1970s and extending until 2009. The role of P. Ha ́jek in the development of fuzzy logic is especially emphasized.

An axiomatic theory of abstract objects is developed and used to construct models of Plato's Forms, Leibniz's Monads, Possible Worlds, Frege's Senses, stories, and fictional characters. The theory takes six primitive metaphysical notions: object ; n-place relations ,G,...); x,...x exemplify F x...x); x exists ; it is necessary that "); and x encodes F "). Properties and propositions are one place and zero place relations, respectively.objects are objects which necessarily fail to exist E!x"). The two most important proper axioms are (...) that no possibly existing object encodes any properties E!x F)xF)), and for every expressible condition on properties, there is an abstract object which encodes just the properties satisfying the condition x) )), where has no free x's). Semantically, an abstract object encodes a property iff the property is an element of the set of properties correlated with the object. Two abstract objects will be identical just in case they encode the same properties. Abstract objects may exemplify properties as well--being non-red, not having spatial location, etc. ;The models of Forms, Monads, and Possible Worlds consist in: identifying these philosophical entities as different species of abstract objects through definitions of the object language, and either showing that there are consequences of the theory which are reasonable facsimiles of assertions made by important philosophers or showing that there are many interesting theorems which capture our own intuitions about these entities . The model for Frege's Senses consists in: developing a language in which the abstract objects generated by the theory serve as the senses of names and descriptions, and showing that the data may be consistently translated into the language preserving truth. Finally, the model for fictional characters consists in: assigning abstract objects to serve as the denotations of names of stories and characters, and showing that such an assignment allows us to understand how the intuitively true sentences about stories and characters have the truth value that they do. ;The material is structured as follows. In Chapters I, III, and V, the elementary, modal, and typed theories of abstract objects are developed, respectively. In Chapters II, IV, and VI, these theories are applied, respectively. Each of the theoretical chapters is subdivided as follows: 1--The Language; 2--The Semantics; 3--The Logic; and 4--The Proper Axioms. Thus, the proper axioms of the theory are couched in a precisely defined and interpreted language, and the logic allow us to prove the consequences of the theory. (shrink)

Desde que Tarski publicó su estudio sobreel concepto de verdad en los años 30, hasido una práctica ortodoxa el considerarque t oda i nst anci a del esquema T esverdadera. Sin embargo, algunas instanciasdel esquema son falsas. Éstas incluyen lasi nst anci as paradój i cas ej empl i f i cadaspor la oración del mentiroso. Aquí sedemuestra que un esquema mejor permiteun tratamiento uniforme de la verdad enel que las paradojas semánticas resultanser simplemente falsas.Si nc e Ta r s (...) ki publ i s he d hi s s t udy ofthe concept of truth in the 1930s, it hasbeen orthodox practice to suppose thatevery instance of the T-schema is true.However, some instances of the schemaare false. These include the paradoxicalinstances exemplified by the Liar sentence.It is shown that a better schema allows auniform treatment of truth in which thesemantic paradoxes turn out to be simplyfalse. (shrink)

A shallow semantic embedding of an intensional higher-order modal logic in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in his textbook Types, Tableaus and Gödel’s God in order to discuss his emendation of Gödel’s ontological argument for the existence of God. Utilizing IHOML, the most interesting parts of Fitting’s textbook are formalized, automated and verified in the Isabelle/HOL proof assistant. A particular focus thereby is on three variants of the ontological argument (...) which avoid the modal collapse, which is a strongly criticized side-effect in Gödel’s resp. Scott’s original work. (shrink)

Classical higher-order logic, when utilized as a meta-logic in which various other logics can be shallowly embedded, is well suited for realising a universal logic reasoning approach. Universal logic reasoning in turn, as envisioned already by Leibniz, may support the rigorous formalisation and deep logical analysis of rational arguments within machines. A respective universal logic reasoning framework is described and a range of exemplary applications are discussed. In the future, universal logic reasoning in combination with appropriate, controlled forms of rational (...) argumentation may serve as a communication layer between humans and intelligent machines. (shrink)

With material on his early philosophical views, his contributions to set theory and his work on nominalism and higher-order quantification, this book offers a uniquely expansive critical commentary on one of analytical philosophy’s great ...

The quest for a most general framework supporting universal reasoning is very prominently represented in the works of Leibniz. He envisioned a scientia generalis founded on a characteristica universalis, that is, a most universal formal language in which all knowledge about the world and the sciences can be encoded. A quick study of the survey literature on logical formalisms suggests that quite the opposite to Leibniz’ dream has become reality. Instead of a characteristica universalis, we are today facing a very (...) rich and heterogenous zoo of different logical systems, and instead of converging towards a single superior logic, this logic zoo is further expanding, eventually even at accelerated pace. As a consequence, the unified vision of Leibniz seems farther away than ever before. However, there are also some promising initiatives to counteract these diverging developments. Attempts at unifying approaches to logic include categorial logic algebraic logic and coalgebraic logic. (shrink)

This paper develops a semantics for a fragment of English that is based on the idea of `impossible possible worlds'. This idea has earlier been formulated by authors such as Montague, Cresswell, Hintikka, and Rantala, but the present set-up shows how it can be formalized in a completely unproblematic logic---the ordinary classical theory of types. The theory is put to use in an account of propositional attitudes that is `hyperfine-grained', i.e. that does not suffer from the well-known problems involved with (...) replacing expressions by logical equivalents. (shrink)

The paper reconstructs three main stages in the development of Carnap’s approach to language in the years 1931 – 1947. It starts with Carnap’s approach to metalogic in his Viennese Zirkelprotokolle and his Logische Syntax der Sprache from the point of view of one-level approach to the relation between metalanguage and its object-language. It then analyzes Tarski’s turn to semantics in his paper presented at the Paris conference in September 1935, as well as the implications of his view for Carnap’s (...) approach to semantics from 1935 until 1943. Finally, it analyzes Church’s rediscovery of Frege and its impact on Carnap’s shift to the extension/intension distinction in his semantics in the years 1943 – 1947. (shrink)