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)

Equational hybrid propositional type theory ) is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra and a Kripke frame. The main result in this paper is the proof of completeness of a calculus specifically defined for this logic. The completeness proof is based on the three proofs Henkin published last century: Completeness in type theory, The completeness of the first-order functional calculus (...) and Completeness in propositional type theory. More precisely, from and we take the idea of building the model described by the maximal consistent set; in our case the maximal consistent set has to be named, \-saturated and extensionally algebraic-saturated due to the hybrid and equational nature of \. From, we use the result that any element in the hierarchy has a name. The challenge was to deal with all the heterogeneous components in an integrated system. (shrink)

This paper focuses on the evolution of the notion of completeness in contemporary logic. We discuss the differences between the notions of completeness of a theory, the completeness of a calculus, and the completeness of a logic in the light of Gödel's and Tarski's crucial contributions.We place special emphasis on understanding the differences in how these concepts were used then and now, as well as on the role they play in logic. Nevertheless, we can still observe a certain ambiguity in (...) the use of the close notions of completeness of a calculus and completeness of a logic. We analyze the state of the art under which Gödel's proof of completeness was developed, particularly when dealing with the decision problem for first-order logic. We believe that Gödel had to face the following dilemma: either semantics is decidable, in which case the completeness of the logic is trivial or, completeness is a critical property but in this case it cannot be obtained as a corollary of a previous decidability result. As far as first-order logic is concerned, our thesis is that the contemporary understanding of completeness of a calculus was born as a generalization of the concept of completeness of a theory. The last part of this study is devoted to Henkin's work concerning the generalization of his completeness proof to any logic from his initial work in type theory. (shrink)

We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and first-order hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)

Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, e (...) Manzano [no prelo]), e sim nos instrumentos subjacentes e no modo como trabalham em conjunto. Esperamos que o leitor fique tentado a cantar junto. DOI:10.5007/1808-1711.2011v15n2p225. (shrink)

Professor Bunge makes the distinction between the logical concept of existence and the ontological one. I agree with him and in this paper I am formalizing his existence predicate into the powerful language of type theory.I am also proving the logical equivalence of this for mulation with a briefer one, which says that to exist conceptually is the same as to be a conceptual object. Accordingly, from this point on I investigate what conceptual objects are. I reach the conclusion that (...) it is better to study a restricted area each time, where existence could even be assigned in different degrees. For instance, in set theory -like in Animal Farm of Orwell every set exists but so me “exist more” than others. Of course, in relating degrees of existence to degrees of definability I am not following Bunge. (shrink)

In this paper we will discuss the active part played by certain diagonal arguments in the genesis of computability theory. 1?In some cases it is enough to assume the enumerability of Y while in others the effective enumerability is a substantial demand. These enigmatical words by Kleene were our point of departure: When Church proposed this thesis, I sat down to disprove it by diagonalizing out of the class of the ??definable functions. But, quickly realizing that the diagonalization cannot be (...) done effectively, I became overnight a supporter of the thesis. (1981, p. 59) The title of our paper alludes to this very work, a task on which Kleene claims to have set out after hearing such a remarkable statement from Church, who was his teacher at the time. There are quite a few points made in this extract that may be surprising. First, it talks about a proof by diagonalization in order to test?in fact to try to falsify?a hypothesis that is not strictly formal. Second, it states that such a proof or diagonal construction fails. Third, it seems to use the failure as a support for the thesis. Finally, the episode we have just described took place at a time, autumn 1933, in which many of the results that characterize Computability Theory had not yet materialized. The aim of this paper is to show that Church and Kleene discovered a way to block a very particular instance of a diagonal construction: one that is closely related to the content of Church's thesis. We will start by analysing the logical structure of a diagonal construction. Then we will introduce the historical context in order to analyse the reasons that might have led Kleene to think that the failure of this very specific diagonal proof could support the thesis. This is a joint paper. We have both attempted to add a small piece to an amazing historical jigsaw puzzle at a juncture we feel to be appropiate. In the paper by Manzano 1997 the aforementioned words by Kleene were quoted, and since then several logicians, Enrique Alonso first and foremost, have questioned her on this issue. Here we both submit our reply. (1999, pp. 249--273). (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)