Na teoria quântica não são válidos todos os princípios clássicos de inferência, e as lógicas quânticas procuram estabelecer sistemas lógicos mais adequados para raciocinar sobre as proposições dos sistemas quânticos. Garrett Birkhoff e John von Newmann, em 1936, foram os primeiros a propor o que se poderia chamar de "lógica da mecânica quântica". Atualmente há muitos sistemas alternativos de lógicas quânticas, concebidos dentro das mais diversas perspectivas. Nesta apresentação descrevemos duas propostas para as lógicas quânticas (a ?orthologic? e a ?orthomodular quantum logic?), propostas em conformidade com as idéias de Birkhoff e de von Newmann.

               In this talk we point out that possible worlds are not an essential feature ofKripke structures. We show how to construct Kripke structures without possible worlds and show how this is useful to extend Kripke semantics (e.g. with many values) to develop a wide range of logics in particular paraconsistent ones.

               We consider new implicit connectives in non-classical logics not necessarily given by axioms. In particular, we pay attention to the successor connective.

        According to the modal realist, possible worlds exist, and in terms of them, it’s possible to articulate a systematic approach to the theory of modality (Lewis [1986]). Given, however, that we have no access to such worlds, how can we know that they in fact exist? To answer this question, Lewis developed two modal epistemological strategies. First, he explored an analogy with mathematics, noting that we do have mathematical and modal knowledge, both being cases of a priori knowledge. Second, he defended a theoretical utility argument, insisting that the theoretical utility of postulating possible worlds is a good reason to believe in the existence of these objects. In this paper, we examine critically both strategies, and argue that they fail. We then sketch an alternative way of developing a modal epistemology, and argue that, because it’s not committed to possible worlds, it doesn’t face the problems faced by Lewis’ proposal.

     I show here simplified axiomatizations for the hierarchies of propositional logics Pn and In, started  by Sette and Carnielli, and developed by Fernandez and Coniglio. Pn is a generalization of the three-valued paraconsistent logic P1 proposed  by Sette, and In is a generalization of the 3-valued  intuitionistic logic I1 proposed  by Sette and Carnielli.
      It is also  shown that the finite algebrazability for P1 and I1 can be generalized in a natural way for Pn and In. Although the varieties that algebrize  P1 and I1 are the same, this is  not true for the whole hierarchy. I discuss this question, as well as the possibilities of algebraizing other generalizations of these hierarchies.

     The "Logics of Formal Inconsistency" (LFIs) constitute a wide class of paraconsistent logics, and many of them can be semantically characterized by the "possible-translations semantics", a formal semantics devised by myself some years ago and widely investigated in cooperation with J. Marcos and M. E. Coniglio. LFIs can be naturally extended to modal logics, minimal in the sense of involving the minimum properties of negation.
       I discuss here how modal extensions of LFIs can offer a fresh approach to questions involving certain difficulties in the notion of knowability. It is shown (in a joint work with A. Costa-Leite and M. E. Coniglio) how modal logics based upon subclassical logics which control the effects of negation can be characterized by Kripke structures, and how they can be applied to offer a solution to Fitch's Paradox of Knowability.

        In our research project, we intend to introduce a new hierarchy of quantificational analytical tableaux systems TNDCn*, Cn*, 1?n<?, for da Costa´s hierarchy of quantificational paraconsistent logics Cn*, 1?n<?. As in  our tableaux formulation for da Costa's propositional paraconsistent systems, we will introduce da Costa's "ball" operator "o", the generalized operators "k" and "(k)", for1?k, and the negations "~k", for k?1, as primitive operators, differently to what has been done in the literature, where these operators are usually defined operators. We will try to prove a version of Cut Rule for the TNDCn*, 1?n<?, and also prove that these systems are logically equivalent to the corresponding systems Cn*, 1?n<?. We also intend to introduce the hierarchies of sequent calculus sequent calculus SNDCn and SNDCn * for da Costa's hierarchy of propositional paraconsistent and quantificational logics Cn and Cn *, 1?n<?, respectively. We will try to obtain a Cut Rule for each one of the sequent calculus of these hierarquies. 

        I will present an interpretation of Frege's theory of senses for proper names and natural kind terms, and argue that it is compatible with, and indeed can be combined with, Kripke's theory of reference fixing and transmission.

        In this talk (based on a joint work with W. Carnielli) the question of factoring a logic into a family of generally simpler logics is addressed. Three methods are analyzed and compared: Possible-Translations Semantics, Non-Deterministic Semantics and Plain fribring (together with its particularization direct union of matrices). The possibility of inter-definability between these methods is also studied. Finally, applications to some well-known logic systems are given and their significance evaluated.

Abstract: In his thesis “Para uma Teoria Geral dos Humanismos” the Portuguese mathematician José Sebastião e Silva constructed an abstract or generalized Galois theory, that is intimately linked to F. Klein´s Erlangen Programe and that foreshadowed some notions and results of today Model Theory. An analogous theory was independelly worked out by M. Krasner in 1938.
Da Silva´s work on the subject is neither wholly clear nor sufficiently rigorous. In this work a rigorous version  of the theory, correcting the shortcoming´s of Silva´s exposition and extending some of its main results is investigated.
We also study the interrelation between Silva´s and Krasner´s approaches.

In this paper we introduce da Costa's paraconsistent differencial calculus and some of its main results. We prove a transference theorem from classical differential calculus into paraconsistent differential calculus.

           A lógica do plausível é uma extensão da lógica de primeira ordem clássica através da inclusão de um novo quantificador (generalizado), que procura caracterizar no ambiente formal  noções de plausibilidade, mais especificamente, através da seguinte quantificação: 'uma boa parte dos indivíduos do universo de discurso admitem uma dada propriedade'.
    Como estrutura matemática destinada à interpretação deste novo quantificador, a pesquisadora Maria Claudia Cabrini Gracio propôs o conceito de topologia reduzida, o qual temos denominado, mais recentemente, de pseudo-topologia, que é uma variação do conceito usual, dada por meio de duas cláusulas: (i) o conjunto vazio não é um pseudo aberto e (ii) apenas uma intersecção finita de pseudo-abertos é um pseudo-aberto. Apesar desta versão de primeira ordem estendida, imaginamos que podemos tratar  com a versão da pseudo-topologia num contexto algébrico e, então, construir uma lógica do plausível proposicional.
            Este trabalho apresenta os primeiros passos nesta direção.

               In this work we study an extension of classical sequent calculus
with a substitution rule, which is normally admissible in classical logic.  The structure of proofs is also extended to permit DAG shaped proofs.  We analyse several properties of this system, such  as the complexity of cut-elimination, and propose an extended tableau proof system, called s-tableaux, that corresponds to the DAG-sequent calculus.  We show how the pigeon hole principle can be solved linearly solved in s-tableaux.

        O conceito de teoria de Galois é um padrão recorrente, aparecendo em contextos diversos da matemática atual. Esta apresentação será destinada a esboçar as motivações e métodos de algumas teorias de Galois e suas ligações com a Lógica, à luz dos trabalhos de José Sebastião e Silva, Marc Krasner e Alexander Grothendieck. 

        Newton C.A. da Costa estabelece uma demarcação entre "interpretações filosóficas" e "definições formais" de verdade. Entre as interpretações filosóficas encontramos as teorias da verdade como correspondência, as teorias pragmatistas e as teorias deflacionárias, enquanto entre as definições formais temos a concepção semântica de verdade de Alfred Tarski e a definição de quase-verdade de da Costa. Neste trabalho apresentaremos algumas considerações gerais sobre as teorias da verdade, verdade correspondencial , verdade pragmática, a definição de quase-verdade de da Costa e uma lógica adequada para esta definição.

        A proposta é explorar a tradutibilidade entre a semântica de valorações e os modelos de Kripke. A primeira trabalha com sequências de fórmulas onde cada uma é precedida todas as suas subfórmulas e estipula condições necessárias (nem sempre suficientes) para a verdade ou falsidade das mesmas levando em conta os comportamentos veritativos que certas fórmulas precedentes na sequência apresentam em toda a classe das valorações. Os modelos de Kripke, por outro lado, trabalham com condições necessárias e suficientes, mas levam em consideração apenas determinadas valorações (mundos possíveis) que mantêm entre si uma determinada relação, dita de acessibilidade.
      No entanto, pode-se mostrar que há uma correspondência biunívoca entre os mundos integrantes dos modelos de Kripke de um sistema modal e as valorações para o mesmo sistema.

        This paper starts by showing that the Kantian program of the critique of pure reason can be summed up by the following question: how theoretical synthetic a priori judgments are possible? Considered by Kant as the ?general? or the ?main? task of transcendental philosophy, this question requires that be determined conditions in which judgments of this kind are objectively valid. In modern language, it is required to ensure the meaning of theoretical a priori terms and the truth conditions of theoretical a priori judgments, philosophic as well as scientific, in the domain of interpretation constituted by objects of possible representational experience. Accordingly, the transcendental logic of Kant´s, which is the initial form of his transcendental philosophy, can be interpreted as being, in essence, an a priori theory of meaning and truth, that is, as an a priori semantics. In its second part, the paper studies the different ways in which Kant extended this program of the critique of pure reason to a priori judgments belonging to non theoretic domains of philosophical discourse. Is shows, in a schematic manner, how are raised and answered questions about the possibility of synthetic judgments a priori of doctrines of morals, esthetics, of law, of virtue and of history, especial attention being given to the multiplicity of domains of interpretation and the subsequent modification of the concept of objective validity. These considerations provide the conclusive evidence that transcendental semantics of synthetic a priori judgments in general is an essential component of Kant´s transcendental philosophy, taken not just as being a transcendental logic, but in the amplified sense as the whole of results obtained by Kant in the course of his progressive extension of his program of the critique of pure reason.

Key Words: Kant, critique of pure reason, transcendental philosophy, a priori judgments, transcendental semantics.

Investigating the connections between Galois theory and Logic we found in Borceux & Janelidze's "Galois Theories" [BJ] an expanded version of the classical Galois Theorem, expressed as an equivalence of categories between Split(L:K) (finite dimensional K-algebras split by L and morphisms) and Gal(L:K)-fsets (finite G-sets and morphisms),where G is the Galois group of L over K (here L is a finite dimensional Galois extension of K).
The point of the present talk is to explain how it is possible to complete the above equivalence with a Hom-functor (the reason for "Hom sweet Hom" in the title) in the opposite direction (from Gal(L:K) to Split(L:K)), which is absent in [BJ]. We also reshape the proof of the equivalence in a more elementary and direct form, noting that the argument of [BJ] uses only part of the inherent naturality of Hom functors, or the sweetness of Home: this requires much more preparatory material.

            What is the fundamental insight behind truth-functionality? When is a logic interpretable by way of a truth-functional semantics? To answer such questions in a satisfactory way, a formal definition of truth-functionality from the point of view of abstract logics is clearly called for. As a matter of fact, such a definition is available at least since the 70s, though maybe not very widely well-known.
        There is a clear difference between logics characterizable through: (1) genuine finite-valued tabular semantics; (2) no finite-valued but only an infinite-valued tabular semantics; (3) no tabular semantics at all. Any of those logics, however, can in principle be characterized through non-truth-functional valuation semantics, at least as soon as their associated consequence relations are governed by the usual tarskian axioms. So, paradoxical as that might seem at first, truth-functional logics may surely have adequate non-truth-functional semantics. Now, what feature of a given logic would allow it to live in class (1) or in class (2)?
        The present talk will recall the basic definitions and results concerning truth-functionality of logics, and give examples of logics indigenous to each of the aforementioned classes. If there is time and interest, some problems pertaining to those definitions and to their possible generalizations will be touched.

        We show that the category of Blok-Pigozzi algebraizable logics, with morphisms taken as the induced formula algebra functions that are consequence preserving and also preserve the defining equations and the equivalence formulas, has all filtered colimits. This also gives some information about the equivalent quasivariety semantics for the colimits.

        Em 1972 apresentamos um trabalho sob o título acima onde propusemos a aplicação de modelos de Kripke à lógica discussiva de Jaskowski, baseada no sistema S5 de Lewis e de teoremas de correção e completude.

        After some unsuccessfully atempts to implement a parser for Categorial Grammars, due to computational complexities imposed by strutural complexity and spurious ambiguity (which, in the worst case, allows infinitely many analysis for a single unambiguous well-formed sentence), I decided to change from a theorem proving perspective to a proof assistant account. Contrary to the parser as a theorem prover, the parsing assistant is not the only responsible for constructing the phrase marker. So, instead of a program for automatic analysis, we can build a didatic tool in which the user has the the complete control over the strruture construction.

        The distinction between a General Proof Theory and a Reductive Proof Theory was introduced by Dag Prawitz [1]. According to Prawitz, among the main problems in General Proof Theory we find the Identity Problem: 

2.3. The Representation of proofs by formal derivations. In the same way as one asks when two formulas define the same set or two sentences express the same proposition, one asks whe two derivations represent the same proof; in other words, one asks for identity criteria for proofs or for a ?synonimity? (or equivalence) relation between derivations. (Prawitz [1], p.237) 

Prawitz not only formulates the problem, but he also proposes a solution: two derivations represent the same proof if and only if they are equivalent. The equivalence relation envisaged by Prawitz is defined in terms of operational reductions for detours of different logical forms. The aim of this paper is to study the relationship between structural reductions and the identity problem. Special emphasis will be given to structural reductions related to the constant ? and their connection with the well known collapse of the initial object in category theory. 

[1] Prawitz, Dag - Ideas and Results in Proof Theory, in Proceedings of the Second Scandinavian Logic Symposium, ed. by J.E. Fenstad, North-Holland, Amsterdam, 1971, pp.235-307.

[2] Widebäck, Filip - Identity of Proofs, Almqvist & Wiksell International, 2001.

        As lógicas moduladas introduzidas por W. A. Carnielli, A. M. Sette e P.A.S. Veloso constituem   a família dos sistemas lógicos que se ocupam da formalização de argumentos indutivos de forma puramente qualitativa.. Por outro lado, as chamadas lógicas difusas e a noção de conjuntos  difusos introduzidas por L. Zadeh vêem sendo usados nas situações onde o ‘raciocínio binário’ (incluindo a lógica clássica e a matemática usual) não parece adequado. O paradigma difuso tem sido extensamente aplicado mesmo sem um embasamento lógico satisfatório. O objetivo deste trabalho é propor uma fundamentação, totalmente qualitativa, para o raciocínio difuso, utilizando-se das lógicas moduladas visando uma nova abordagem ao problema do Paradoxo dos Sorites.

        Lançando mão da teoria local de conjuntos, demonstramos que a estrutura ordenada dos reais de Dedekind é (efetivamente) homogênea em qualquer topos com objeto dos números naturais, isto é, todo isomorfismo parcial finito pode ser estendido a um automorfismo da estrutura. Ilustramos matematicamente o resultado obtido através do topos dos feixes sobre um espaço topológico.

      In our exposition we are going to present natural deduction rules for preserving falsity. Usually deduction rules are thought as truth preserving devices. Curiously, it happens that all structures representing truth preservation can be read as representing falsity preservation. As natural deduction systems correspond closely to the logistic systems, also logistic systems can be interpreted alike as falsity preserving devices. To sum up, it seems that a whole bunch of questions can be worked from such a perspective. We are going to touch one or two of them in our exposition.

      We will describe the motivation and implementation of a Multi-Strategy Tableau Prover. Strategies are responsible for the control of (nondeterministic) inference rules of automated deduction systems.
        Our prover allows us to vary the strategy without modifying the core of the implementation.
        Generating Definable Relations in an Infinitary

            To judge is to represent a possible fact and, moreover, to represent it as a possible content of evidence. This means that proper judging involves a presupposition, namely, that judgments can be verified. I will analyze in this paper the character of this presupposition and the sense of these modalities. I will argue that the possibility of verification that judging presupposes cannot be understood as the hypothesis that any proper judgment can be effectively verified. Rather, the underlying presupposition that accompanies any judgment is an ideal that plays a regulative role. Particular attention will be given to necessarily false judgments and contingent assertions referring to future events.

            O objetivo do trabalho é desenvolver o esboço de um argumento a favor de uma filosofia da consciência e da significação que possa ser posta como fundamento da Lógica e da Matemática, i.e., por a vista a existência da Idéia que se pensa a si própria, unidade inteligente e inteligível, que é, ao mesmo tempo, fundamento da existência dos diversos sistemas lógicos, na medida em que contém todas as possibilidades de sistemas formais.
            A partir de uma análise da Lógica atual, argumenta-se, inicialmente, que significados e significantes formam uma totalidade de mesma natureza, um universo. Nesse contexto, define-se o termo ‘Idéia’, argumenta-se a favor da preexistência da Idéia, enquanto fundamento das diversas teorias, e se explicita como, de suas características essenciais, isto é, necessárias a partir da definição, pode-se concluir pela sua unicidade e inteligibilidade. Por fim, apresenta-se então o caráter inteligente da Idéia como totalidade que se pensa a si própria, concluindo-se então pela existência da Idéia que se pensa a si própria, unidade inteligente e inteligível, que é também fundamento da Lógica e da Matemática.

            One of the main problems in using logic for solving problems is the high computational costs involved in inference. In this paper, we propose the use of a notion of relevance in order to cut the search space for a solution. Instead of trying to infer a formula $\alpha$ directly from a large knowledge base $K$, we consider first only the most relevant sentences in $K$ for the proof. If those are not enough, the set can be increased until, at the worst case, we consider the whole base $K$.
We show how to define a notion of relevance for first-order logic with equality and analyze the results of implementing the method and testing it over more than 700 problems from the TPTP problem library.