Novo blog dos Semináros de Lógica!

Nosso blog mudou de endereço!

O antigo permanecerá no ar como registro dos últimos anos.

Agradecemos a todos que ajudaram na organização nestes anos.

http://www.seminarioscle.wordpress.com

 

 

03/06 - Pedro Carrasqueira

On the foundations of a theory of deliberative reason: A logical survey of the general principles of the theory of rational choices and coherent preferences

Last century witnessed a great development of the mathematical foundations of social sciences, due to the rapid growth of research in decision theory, game theory and social choice theory and to the astounding results obtained in those fields. Such studies seem to me to point towards a more general theory of rationality in practical contexts, and, in particular, to a mathematical theory of deliberative reason. Such a possibility, however, presupposes a (to the best of my knowledge) not yet systematically undertaken philosophical inquiry of the principles underlying those theories, --- one that would explore their pertinence to settings broader than those proper to the social sciences.

My exposition shall be divided in three parts.

In the first part I shall present the main concepts common to all those theories --- to wit, the notions of choice, preference, welfare, norm and strategy --- and discuss in very broad strokes how they relate, with special attention to the relation between the more fundamental concepts of choice and preference. (I say they are more fundamental because they seem to me to be the ones that characterize, minimally, a deliberative setting.)

In the second part I shall briefly discuss what contributions (beyond the already well-known use of games in model theory) I believe such an enlargement of the field of application of those concepts would have to offer to logic in general, and to logic in practical contexts in particular.

In the third part I shall present a few questions about how already well-established logic, and modal logic in particular, could contribute to the understanding of those fundamental concepts of deliberative reason. I shall also present, if time allows it, some still very sketchy proposals of mine towards such a contribution.

Colloquium Logicae: Prof. Stefano Predelli

Meaning Without Truth

Stefano Predelli (da Universidade de Nottingham) apresentará as principais ideias e resultados de seu recente livro "Meaning Without Truth" (Oxford UP 2013). Trata-se de uma interessante tentativa de tratar de forma rigorosa e sistemática aspectos do significado que não são capturáveis na semântica verifuncional (estendendo de algumas formas relevantes a semântica de Kaplan em termos de caráter e conteúdo). Teremos também como comentadora Eleonora Orlando (da Universidad de Buenos Aires).

Três sessões. Sala Kurt Gödel, CLE-UNICAMP.

25 de maio (segunda-feira), 16h: Meaning Without Truth I

27 de maio (quarta-feira), 16h: Meaning Without Truth II

3 de junho (quarta-feira), 14h: Meaning Without Truth III

06/05 - Marco Ruffino

A Puzzle About Frege’s Singular Senses

In this paper I discuss what seems to be a puzzle for Frege’s notion of singular senses (i.e., the senses of singular terms) assuming the interpretation that, for him, every singular term is reducible to (or express the same sense as) some definite description. Singular senses are supposed to be complete (or saturated), but they are composed of the incomplete (unsaturated) senses of the concept-words of the descriptions. I ask how the definite article (or what it expresses) “transforms” an unsaturated sense into a saturated one, and review some attempted explanations in the literature. I argue that none of them is compatible with Frege’s broader views in semantics. Next I discuss one alternative that Frege himself endorses (the definite article indicating an attitude on the speaker’s part). This alternative, I argue, is also incompatible with his semantics. I conclude that Frege has no coherent view on singular senses.

*DF-IFCH and CLE-UNICAMP

Colloquium Logicae: Prof. Dr. Wolfgang Lenzen

"Leibniz Logic" on Wednesday April 15th, 16:30, Gödel Room at CLE- UNICAMP

"A Survey on Epistemic Logic" on Thursday 16th, 14:00, Gödel Room at CLE- UNICAMP

Biography and eulogy: Prof. Wolfgang Lenzen (in German)

http://www.lumer.info/wp-content/uploads/2012/04/C005_LumerMeyer_VorwortFSLenzen.pdf

Department of Philosophy, Universität Osnabrück, Germany

25/03 - Lucas Rosenblatt (Colloquium Logicae)

Capturing Naive Validity in the Strict-Tolerant Approach

Rejecting the structural rule of Cut has been recently proposed as a strategy to avoid both the usual semantic paradoxes and the so-called Validity Paradox. In this paper we consider if a theory that rejects Cut is capable of accurately representing its own notion of validity. We claim that the standard rules governing a naive validity predicate are too weak for this purpose and we show that although it is possible to strengthen these rules, the most obvious way of doing so brings with it a serious problem: an internalized version of Cut can be proved. We also evaluate a number of possible ways of escaping this difficulty.

11/03 - Emiliano Boccardi

If it ain’t Moving it shall not be Moved: real passage for A-theorists

Imagine two friends sitting on a beach, looking at a ship far away. Because of the distance, they cannot just tell by looking at it whether the ship is moving or not. “I bet it’s moving” says one. “No it’s not!”, says the other. Do they disagree about something? And if yes, what is the disagreement exactly about?

After some time the two friends look again and the ship has obviously moved, although it looks to them just as still as it looked before: its position (relative to them) has changed. “Aha!”, says the first, “I told you it was moving!” “You were right, it was moving. I lost the bet!”, says the other. What was this bet about?

Physics and mathematics  textbooks  follow  Bertrand  Russell  in accounting  for  a  body‘s instantaneous velocity not merely as equal to, but moreover as identical to the time-derivative of its trajectory. On this view, a body’s instantaneous velocity is ontologically parasitic on its trajectory. This deflationist understanding of change was heavily inspired by Weierstrass’ and Cantor’s understanding of limit and infinity. According to Weierstrass’ conception of limits and infinitesimals (now the received view), variables are just denotational schemas: they contribute to the sole purpose of denoting large numbers of (unchanging) facts about their values. The values of the variables do not themselves vary: they do not “approach”, let alone “reach” their limits, or change in any sense, contrary to what they were ambiguously alleged to be doing in prior formulations (since Newton’s and Leibniz’s). Of course, according to this conception, neither do variables themselves vary or change, in spite of their evocative name. It was this reconceptualization of the notion of limit that inspired Russell’s treatment of the antinomies involved in the notion of indefinitely growing series of things (such as those involved in Zeno’s paradoxes): “Weierstrass”, he says, “by strictly banishing all infinitesimals has at last shown that we live in an unchanging world, and that [Zeno’s] arrow, at every moment of its flight, is truly at rest” (POM, p. 347).

Likewise, many philosophers of time argue that the passage of time is identical with the fact that different times subsequently instantiate presentness.

However, I shall argue in the first part of this talk, it is tempting to think that the initial disagreement between the two friends is about a property instantiated by the ship at (and only at) the time of the bet (t1). What they observe at the time of the assessment of the bet (t2), according to this intuitive view, is the comparative fact that the ship’s location at t1 is different from its location at t2. They agree that this provides indirect evidence for the further (non-comparative) fact that the ship was moving at t1. If the ship is found at different positions at times right after t1, this must be because at t1 it possessed an intrinsic kinematic quantity in addition to its position.

If this explanatory pattern is sound, then the comparative fact that (a) the location of the ship at t1 is different from its location at t2, must be ontologically distinct from the (non-comparative) fact that (b) the object has been in motion for enough times between t1 and t2. In short, according to this view, the displacement of the ship is a posthumous consequence of its state of motion (velocity) throughout the time interval considered, hence fact b (the explanans) cannot be identical to fact a (the explanandum). Analogously, I shall defend the thesis that yesterday became past because time passes. The passage of time ought to explain the ensuing comparative fact that Today’s presentness followed Yesterday’s presentness, so it cannot be thought of as identical with it. The ensuing view construes passage as an intrinsic, non-comparative feature of time instants.

In the second, more tentative part of the talk, I shall bring this issue to bear on the formal semantics of axiomatic treatments of aspect. In particular, I shall consider different solutions to the so called Imperfective Paradox, and test them against the desiderata put forward in the first part of the talk.

References

Arntzenius, F. (2000) Are there really instantaneous velocities? Monist 83:187–208

Bach, E. (1986) The algebra of events, Linguistics and Philosophy, 9(1):5–16

Bigelow, J. (1991) Worlds enough for time. Nouˆs 25:1–19
. Bigelow J, Pargetter R (1990) Science and necessity. Cambridge University Press, Cambridge

Boccardi, E. (2015) If it ain't Moving it shall not be Moved, Topoi, 34(1): 171-185

Dowty, D. (1979) Word Meaning and Montague Grammar, Dordrecht: Reidel

Hall, N. (2004) Two concepts of causation. In: Collins, Hall N, Paul, LA (eds)

Causation and counterfactuals. The MIT Press, Cambridge, pp 225–276

James, W. (1987) Writings 1902–1910. Literary Classics of the United States inc., New York

Lange, M. (2005) How can instantaneous velocity fulfill its causal role? Philos Rev 114(4): 433–468

Le Poidevin, R. (2002) Zeno’s arrow and the significance of the present. In: Callender

Craig, University Cambridge (eds) Time, reality and experience. Press, Cambridge


Parsons, T., 1989, “The progressive in English: Events, states and processes”, Linguistics and Philosophy, 12(2): 213–241

–––, 1990, Events in the Semantics of English, Cambridge MA: MIT Press.

Prior, A., 1967, Past, Present, and Future, Oxford: Oxford University Press.

Russell, B. (1938) Principles of mathematics. W.W. Norton & Company, inc, New York


Tooley, M. (1988) In defense of the existence of states of motion. Philos Top 16:225–254

03/12 - Rodolfo Ertola

Adding connectives to non-classical logics

Already in 1919 Skolem studied, from an algebraic point of view, certain operations that appear afterwards from a logical point of view, for example in 1942 in a work by Moisil. This is done in the context of a logic that, more recently, has been called bi-intuitionistic. Some decades afterwards, there also appear many papers by the polish logician Rauszer on the same logic. More recently, in 2009, Priest gave a paraconsistent version of some kind of bi-intuitionistic logic. We have proved that, in fact, using a notion by Urbas, it is strictly paraconsistent. Approximately in the same tradition appears the connective ∆ of fuzzy logic. We have proved that, added to a Heyting algebra, the result is an equational class.

Another tradition was started in Russia by Novikov in the Fifties and corresponds to the notion of intuitionistic connective. These connectives are supposed to give conservative expansions and enjoy the Disjunction Property. Regarding this, we consider some problems that arise in the case of first-order intuitionistic logic for connectives suggested by Smetanich, Kuznetsov, Gabbay, and Humberstone.

Axioms may not be enough for the axiomatization, i.e. in some cases it is necessary to add a rule. From a semantical point of view, the choice is between a truth-preserving or a truth-degree-preserving consequence.

Unicamp - Brazil

19/11 - Esko Turunen, PhD*

A Paraconsistent Version of Pavelka's Fuzzy Logic

In 1979 Jan Pavelka introduced a very general framework to deal with many valued logics. Pavelka's  idea was to process Zadeh's Fuzzy Sets such that theories, rules of inference, proofs as well as  tautologies may be only partial, i.e. fuzzy. Pavelka defined all his concepts in complete residuated lattices. The main issue was to study the circumstances under which the fuzzy semantic consequence operation and fuzzy syntactic operation coincide; such a property is called Pavelka style completeness.  Pavelka solved the problem in the special case that the set of truth values is the Lukasiewicz sturucure, i.e. the real unit interval equipped with standard MV-structure. The present author has recently proved that Pavelka style completeness holds if, and only if the set of truth values is a complete MV-algebra. Thus, if in particular ,the set M of truth values is a certain collection of 2x2-matrices equipped with suitable operations, then M is a complete MV-algebra. In fact, the set M extends Belnap's four valued para consistent logic. Such an approach results a complete many-valued logic that behaves consistently when looking from outside: the structure in related to Lukasiewicz logic which is a consistent logic. However, looking the logic from inside, i.e. a single 2x2-matrix, para consistency steps in. Truth and falsehood are not opposites of each other, and also contradictions and lack of knowledge is involved.

*Tampere University of Technology (Tampere, Finland)

12/11 - Francesc Esteva* & Lluis Godo*

On paraconsistent fuzzy logics

Paraconsistent logics are specially tailored to deal with inconsistency, while fuzzy logics primarily deal with graded truth and vagueness. Aiming at studying logics that can handle inconsistency and graded truth at once, this talk will report about recent investigations on how a notion of paraconsistent fuzzy logic can be cast within the framework of the so-called logics of formal inconsistency (LFIs).

As in classical logic, it is clear that the notion of truth-preserving deduction commonly used in systems of mathematical fuzzy logic is incompatible with any form of paraconsistency. However, in the first part of the seminar we will show that, instead, some degree-preserving fuzzy logics exhibit interesting paraconsistency features. We will also consider expansions of these logics with additional negation connectives and study their paraconsistency properties as LFIs.

In the second part of the seminar, we will address a kind of converse problem, namely how to extend a given fuzzy logic with a new “consistency” operator in the style of the LFIs. We will introduce a set of postulates for this type of operators over the corresponding algebras, leading to the definition and axiomatization of a family of logics, expansions of MTL, whose degree-preserving counterpart are paraconsistent and moreover LFIs.

 

In the third and final part of the seminar, we will talk about some remarks on ongoing work on the study on intermediate paraconsistent fuzzy logics between the truth-preserving and degree-preserving logics.

 

*IIIA - CSIC, Barcelona, Spain

05/11 - Gabriele Pulcini

A Uniform Setting for Classical, Non-Monotonic and Paraconsistent Logic

In this talk, we propose a uniform syntactical framework encompassing classical, non monotonic and paraconsistent logic. Such a uniform framework is obtained by means of the control sets logical device. Control sets leave the underlying syntax unchanged, while affecting the very combinatorial structure of sequents and proofs. Moreover, we prove the cut-elimination theorem for a version of controlled propositional classical logic, i.e. the sequent calculus for classical propositional logic to which a control sets system is applied. Our goals are two-folds: i) to overcome the conceptual gap between classical and non-classical logics; ii) to give, in particular, a new (positive) account of paraconsistency (and non-monotonicity) in terms of concurrency.

22/10 - Rodrigo Freire

Funções de primeira ordem, Parte 2

Esta apresentação é dedicada às funções de primeira ordem, que são uma generalização das funções de verdade. Os conceitos de tabela de verdade e de sistema de funções de verdade, ambos introduzidos na lógica proposicional por Emil Post, são também generalizados e estudados no caso quantificacional. O tema central desta exposição é a relação de definição entre noções expressas por fórmulas da lógica de primeira ordem. Enfatizamos que a lógica não se ocupa apenas da relação de consequência entre noções expressas por fórmulas, em que uma noção é consequência de outras. A lógica também se ocupa da relação de definição entre noções, em que uma noção é definida a partir de outras. Em uma segunda parte, vamos analisar a relação de definição entre noções expressas por fórmulas da lógica de primeira ordem. Nós vemos a lógica de primeira ordem como uma estrutura matemática cujo domínio é o sistema de todas as funções e primeira ordem, munida das operações básicas e da relação de consequência entre funções de primeira ordem. Em particular, os domínios de subestruturas da lógica de primeira ordem são os sistemas de funções de primeira ordem.

01/10 - Rodrigo Freire

Funções de primeira ordem, Parte 1

Esta apresentação é dedicada às funções de primeira ordem, que são uma generalização das funções de verdade. Os conceitos de tabela de verdade e de sistema de funções de verdade, ambos introduzidos na lógica proposicional por Emil Post, são também generalizados e estudados no caso quantificacional. O tema central desta exposição é a relação de definição entre noções expressas por fórmulas da lógica de primeira ordem. Enfatizamos que a lógica não se ocupa apenas da relação de consequência entre noções expressas por fórmulas, em que uma noção é consequência de outras. A lógica também se ocupa da relação de definição entre noções, em que uma noção é definida a partir de outras. Em uma segunda parte, vamos analisar a relação de definição entre noções expressas por fórmulas da lógica de primeira ordem. Nós vemos a lógica de primeira ordem como uma estrutura matemática cujo domínio é o sistema de todas as funções e primeira ordem, munida das operações básicas e da relação de consequência entre funções de primeira ordem. Em particular, os domínios de subestruturas da lógica de primeira ordem são os sistemas de funções de primeira ordem.

24/09 - Mathieu Beirlaen*

Inconsistency-adaptive dialogical logic, or how to dialogue sensibly in the presence of inconsistencies

Even when inconsistencies are present, we can sensibly distinguish between good and bad arguments relying on these premises. Not anything goes: the mere presence of inconsistencies does not warrant the inference to any conclusion whatsoever. In order to separate good and bad inferences in the possible presence of inconsistency, we nowadays have a wide range of paraconsistent logics to our disposal.

Many of these logics, however, lack the inferential power and the dynamics to model how we actually treat information tainted by inconsistency. An exception in this respect is Batens’ inconsistency-adaptive approach, in which all rules of classical logic are applicable to those parts of our premise set which we can safely consider untainted by inconsistency, without having to specify beforehand which parts of our premises behave consistently.

In order to bring this dynamic approach to paraconsistency closer to our actual argumentative practice, we use its machinery to extend the paraconsistent approach to dialogical logic as developed by Rahman and Carnielli. This way, we obtain a very powerful formalism for the systematic study of dialogues in which two parties exchange arguments over a central claim, in the possible presence of inconsistent information.

* Instituto de Investigaciones Filosóficas (IIF) - Universidad National Autonoma de México (UNAM)

Joint work with Matthieu Fontaine (IIF-UNAM)

Raymundo Morado's Talks at GTAL-CLE Seminars

In 1800, Kant famously declared exhausted our research into logic. According to him, “we do not require any new discoveries in Logic” (“wir brauchen auch zur Logik keine neuen Erfindungen”). Mankind had found practically all there was to find about inference and validity. Turned out the news of the end of logic were greatly exaggerated. So, are there any limits to logic? Certainly, we do very little syllogistic logic anymore, and we expect no big surprises from classical propositional calculus. Maybe logic ended in 1879, with the publication of the first complete system of first-order quantificational logic; maybe in 1932 with the normal systems of strict implication. Yet, logic keeps expanding both its depth and its breadth. We have discovered truths about the logical connectives that intrigued the stoics, and we have expanded the power of classical logic with amazing conservative extensions. Still, some developments seem to challenge our very notion of logicality. Kant was talking from a certain perspective of what logic is that excluded from the set go many recent developments. If logic is the science of necessary inference, non-deductive forms of reasoning must fall outside its realm; mathematical induction is in, induction in zoology is out. If logic is the science of abstract concepts, there can be a logical theory of classical quantifiers, but not of all fallacies. Each idea of logic sets its limits. Limits can be good, as Kant’s dove attests. But there can be also good reasons to evolve our concepts out of the old limits and to allow them to encompass new or unsuspected facets of reality.

September 10

I propose to see if we can find a principled extension of our ideas of logic when confronted with non-classical systems, especially with rival logics. I believe there are important lessons for the philosophy of logic to be gleaned from the examination of logics such as the intuitionistic, free, or quantum ones.

September 17

I will illustrate this with the case of the paraconsistent logics of relevance which are of great importance both theoretical and practical.

October 8

Then we shall examine some of the general problems of constraining excessively our notion of logicality and illustrate this with a discussion of the family of non-monotonic formalisms. This will lead us to consider some formal questions that can help us hone pertinent concepts.

October 15

And this in turn will be useful to tackle the ultimate limit: the general issue of what justifies logic itself. We shall finally mention some open problems in this area of the philosophy of logic(s). These are mostly fundamental topics, and we shall only require the minimal symbolic apparatus of a first semester in logic.

28/05 - Tony Marmo

Comparison of Logics: Some Issues and Perspectives

Throughout the recent history of logic, many logic systems have been proposed in accordance with their proponents’ philosophical standpoints. Additionally, the comparative endeavours require that one firstly defines the sense in which one system contains the other (specially when logics of different valences are at stake). In this talk we shall present some comparative methods available in the literature and, inasmuch as possible, some pertinent issues. We shall briefly try to show how philosophical arguments/objections reflect in different results, perhaps yielding unexpected results.

One of such issues will be Suszko’s claim against many-valuedness and his reduction method. Time permitting; we shall try to present Gehrke and Walker theorem, a proven result that goes in the opposite direction of Suszko’s arguments.

14/05 - Peter Verdée

(Paraconsistent) adaptive logics: a logico-philosophical introduction

In this talk I will introduce adaptive logics as models for rational defeasible reasoning. First I will explain what defeasible reasoning is and why is useful to distinguish rational from irrational defeasible reasoning patterns. I will illustrate that there exist very different forms of defeasible reasoning (induction, abduction, vagueness, inconsistency handling, belief merging, etc.) but that they nevertheless have some formal aspects in common.

Next, I will introduce the Standard Format of Adaptive Logic (SF). I will give a short introduction to the semantics and proof theory of (SF) and will give some examples of adaptive logics within the format of the SF, with special attention for paraconsistent adaptive logics. I will argue why adaptive logics defined within SF are good unifying formalisations of many aspects of defeasible reasoning.

Finally, I will discuss some issues concerning the (computational) complexity of adaptive logics.

30/04 - Rafael Testa

A system of Belief Revision based on the formal consistency operator

The Belief Revision studies how rational agents change their beliefs when they receive new information. The AGM system, most influential work in this area of study presented by Alchourrón, Gärdenfos and Makinson, postulates rationality criteria for different types of belief change and provides explicit constructions for such -- the equivalence between the postulates and operations is called the representation theroem. Recent studies show how the AGM paradigm can be compliant with different non-classical logics, which is called the AGM-compliance -- this is the case of the paraconsistent logics family that we analyzed, the Logics of Formal Inconsistency (LFIs).

Despite the AGM-compliance, when we consider a new logic its underlying rationality must be understood and its language should be used in fact. In this work, we redefine the AGM operations and propose new constructions, which actually captures the intuition of LFIs -- this is what we call the
AGM° system. Thus we provide an interesting interpretation for these logics, more in line with formal epistemology. In an alternative approach, by considering the AGM-compatibility, the AGM results can be directly applied to LFIs (as we presented in the previous seminar). In both approaches, we prove the corresponding theorems of representation where needed.


This is part of my doctoral thesis supervised by Professor Dr. Marcelo Esteban Coniglio (Unicamp) and by Professor Dr. Márcio Moretto Ribeiro (USP).

02/04 - Olivier Rioul

A mathematical analysis of Fitts' law

Fitts' law is a well-known empirical regularity which predicts the average movement time T it takes people, under time pressure, to reach a target of width W located at distance D with some pointer. This model has proven useful in several fields of applied psychology such as Human-Computer Interaction and Ergonomics. Whether Fitts' law is a logarithmic law or a power law has remained unclear so far: In two widely cited papers, Meyer & al. have claimed that the power model they derived from their celebrated stochastic optimized sub-movement theory encompasses the logarithmic model as a limiting case, when the number of submovements grows large. We review the Meyer & al. sub-movement theory and show that this claim is questionable mathematically. Our analysis reveals that the traditional theory implies in fact a quasi-logarithmic, rather than quasi-power model, the two models not being equivalent. Incidentally, the original logarithmic model was derived by Fitts (1954) in analogy with Shannon's information capacity formula (1948); we conclude this talk by discussing recent advances on a sub-movement model that justifies the information theoretic approach. At any rate, awareness that the two classes of candidate mathematical descriptions of Fitts' law are not equivalent should stimulate experimental research in the field.

Joint work with Yves Guiard (CNRS LTCI, France). This work was presented at the 2012 Meeting of the European Mathematical Psychology Group (see also [1], [2]).

Bio

Olivier Rioul (PhD, HDR) is professor at Telecom ParisTech and Ecole Polytechnique, France. His research interests [3] are in applied mathematics and include various, sometimes unconventional, applications of information theory such as in Bayesian dynamic estimation, hardware security, and experimental psychology. He has been teaching information theory at various French universities for almost twenty years. He has published a textbook [4] which has become a classical French reference in the field. A Brazilian edition of the book is scheduled to be published by Editora da Unicamp in the future.

References

[1] O. Rioul and Y. Guiard, "Power vs. logarithmic model of Fitts' law: A mathematical analysis," Math. Sci. hum. / Mathematics and Social Sciences, No. 199, 2012(3), p. 85-96.

[2] O. Rioul and Y. Guiard, "The power model of Fitts' law does not encompass the logarithmic model," Electronic Notes in Discrete Mathematics, Elsevier, Vol. 42, June 2013, pp. 65-72.

http://authors.elsevier.com/sd/article/S1571065313001509

[3] http://perso.telecom-paristech.fr/~rioul/research.html 

[4] O. Rioul, Théorie de l'Information et du Codage, Hermes Science, 2007.

26/03 - Dante Cardoso Pinto de Almeida

Dedução Natural Rotulada para Lógicas Modais e Multimodais

Dedução Natural é um sistema de prova desenvolvido independentemente por Gentzen e Jaśkowski. Caracteriza-se por conter diversas regras de inferência, em geral duas para cada operador (uma para introduzi-lo e outra para eliminá-lo) em contraste com a presença de pouquíssimos ou nenhum axioma; além do mais, caracteriza-se por conter regras de inferência hipotéticas. Assim, o sistema de Dedução Natural passou a ser reconhecido como o que mais se aproxima da forma como se raciocina em matemática.

Contudo, a despeito deste sistema de prova ser aplicado com sucesso a diversos sistemas de lógica (ex: clássica, intuicionista, minimal, algumas lógicas relevantes, alguns poucos sistemas modais etc), tem-se encontrado diversas dificuldades para aplicá-lo em diversos outros sistemas. Recentemente estas dificuldades vem sendo contornadas por autores como Simpson e Gabbay, com a adoção de sistemas de provas rotulados. Rótulos (ou etiquetas) são marcações atribuídas às formulas em um sistema de provas, geralmente expressando propriedades semânticas dessas.

Neste seminário, mostrarei como a dedução natural rotulada funciona para diversos sistemas de lógica modal e multimodal, discutirei o que ainda há para ser estudado na área e como esse sistema pode ser utilizado para formalizar raciocínios e argumentos envolvendo termos modais.