Jaime Ramos

Usually in logic, proof systems are defined having in mind proving properties like validity and semantic consequence. It seems worthwhile to address the problem of having proof systems where satisfiability is a primitive notion in the sense that a formal derivation means that a finite set of formulas is satisfiable. Moreover, it would be useful to cover within the same framework as many logics as possible. We consider Kripke semantics where the properties of the constructors are provided by valuation constraints as the common ground of those logics. This includes for instance intuitionistic logic, paraconsistent Nelson’s logic ${\textsf{N4}}$, paraconsistent logic ${\textsf{imbC}}$ and modal logics among others. After specifying a logic by those valuation constraints, we show how to induce automatically and from scratch an existential proof system for that logic. The rules of the proof system are shown to be invertible. General results of soundness and completeness are proved and then applied to the logics at hand.

We show how to obtain a probabilistic semantics and calculus for a logic presented by a valuation specification. By identifying general forms of valuation constraints we are able to accommodate a wide class of propositional based logics encompassing multi-valued logics like Łukasiewicz 3-valued logic and the Belnap–Dunn four-valued logic as well as paraconsistent logics like $${\textsf{mbC}}$$ and $${\textsf{LFI1}}$$. The probabilistic calculus is automatically generated from the valuation specification. Although not having explicit probability constructors in the language, the rules of the calculus reflect the valuation constraints in a probabilistic way. Indeed the probability of the premises of each rule coincides with the probability of the conclusions. Moreover, a failed exhaustive attempt of proving a formula in this calculus means non-derivability. Nevertheless when the non-derived formula is consistent then it is possible to extract a satisfying valuation from the failed exhaustive attempt. Soundness and completeness of the calculi are established with respect to the probabilistic semantics consisting of probability spaces also induced by the valuation specification. Furthermore we prove the equivalence between the probabilistic and the valuation semantics.

The distributed temporal logic (DTL) is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been provided over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose an automata-theoretic model checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Büchi automaton and of distributed Büchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case.

Mediante un examen crítico de los ensayos publicados en Ideas y Valores acerca de la filosofía de Ludwig Wittgenstein, el escrito busca establecer qué tan rica es nuestra asimilación del pensamiento de uno de los grandes filósofos de la historia, si tal trabajo muestra una evolución a lo largo del devenir de la revista y si el examen que hago aquí puede darnos algún indicio acerca de nuestro desarrollo filosófico. Finalmente, se hacen algunas breves consideraciones acerca de lo que significa hacer filosofía desde la periferia y algunas posibles ventajas que eso tiene, así como señalar la necesidad de realizar una labor más colectiva.

The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity of a schema formula. Based on these concepts we prove general robustness results that relate the complexity of introducing a logical constructor with the complexity of the component schema formulas as well as the complexity of a schema formula across different schema calculi.

This is a critical examination of Jerry Fodor's language of thought hypothesis . Fodor postulated a system of mental representations in which mental processes are supposed to be coded. The language of thought is alleged to be a discrete representational system which has a finite vocabulary, a compositional syntactic structure and a set of semantic rules that determine the meanings of the expressions. This mental language is supposed to be innate and instantiated in the brain, where neural objects or processes serve as the physical signs of the language. In the first chapter I trace the origins of the LOT hypothesis, showing the influence of generative grammar and Turing's algorithms on Fodor's work. I also show how functionalist philosophy of mind arose as an alternative to philosophical behaviorism and reductionistic materialism. In the second chapter I argue against Fodor's computational theory of propositional attitudes by questioning the very idea of physical symbols that have intrinsic semantic content and showing that his theory does not capture our normal notions of belief and desire. In chapter three I examine in some detail the hypothetical structure of LOT and I argue that there cannot be a language where the syntax perfectly mirrors the semantics, a language where there is no place for vagueness or ambiguity. I examine in chapter four the alleged innate character of LOT, and I argue that Chomsky's poverty of the stimulus argument does not support the thesis of innate concepts. Moreover, I argue that Fodor's innatism is inconsistent with his causal theory of meaning for LOT terms. In chapter five, I examine Fodor's arguments against connectionism, the main rival of the LOT hypothesis in contemporary cognitive science, and I argue that Fodor is wrong in believing that thought has the characteristics of constituency, productivity and systematicity in virtue of some natural law, but that it is rather a conceptual, or grammatical, truth that thought has those characteristics. It is not a factual issue whether thought has a symbolist or a connectionist structure

. The semantic collapse problem is perhaps the main difficulty associated to the very powerful mechanism for combining logics known as fibring. In this paper we propose cryptofibred semantics as a generalization of fibred semantics, and show that it provides a solution to the collapsing problem. In particular, given that the collapsing problem is a special case of failure of conservativeness, we formulate and prove a sufficient condition for cryptofibring to yield a conservative extension of the logics being combined. For illustration, we revisit the example of combining intuitionistic and classical propositional logics.

The modern view of logical reasoning as modeled by a consequence operator has allowed for huge developments in the study of logic as an abstract discipline. Still, it is unable to explain why it is often the case that the same designation is used, in an ambiguous way, to describe several distinct modes of reasoning over the same logical language. A paradigmatic example of such a situation is ‘modal logic’, a terminology which can encompass reasoning over Kripke frames, but also over Kripke models, and in any case either locally or globally. Herein, we adopt a novel abstract notion of logic presented as a lattice-structured hierarchy of consequence operators, and explore some common proof-theoretic and model-theoretic ways of presenting such hierarchies through a collection of meaningful examples. In order to illustrate the usefulness of the notion of hierarchical consequence operators we address a few questions in the theory of combined logics, where a suitable abstract presentation of the logics being combined is absolutely essential. We show how to define the operation, in general, and we achieve a number of interesting preservation results for fibring within the context of 2-hierarchies.