The novel notion of importing logics is introduced, subsuming as special cases several kinds of asymmetric combination mechanisms, like temporalization [8, 9], modalization [7] and exogenous enrichment [13, 5, 12, 4, 1]. The graph-theoretic approach proposed in [15] is used, but formulas are identified with irreducible paths in the signature multi-graph instead of equivalence classes of such paths, facilitating proofs involving inductions on formulas. Importing is proved to be strongly conservative. Conservative results follow as corollaries for temporalization, modalization and exogenous (...) enrichment. (shrink)

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...) logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

Arrow and turnstile interpolations are investigated in UCL [introduced by Sernadas et al. ], a logic that is a complete extension of classical propositional logic for reasoning about connectives that only behave as expected with a given probability. Arrow interpolation is shown to hold in general and turnstile interpolation is established under some provisos.

A new technique is presented for proving that a consequence system enjoys Craig interpolation or Maehara interpolation based on the fact that these properties hold in another consequence system. This technique is based on the existence of a back and forth translation satisfying some properties between the consequence systems. Some examples of translations satisfying those properties are described. Namely a translation between the global/local consequence systems induced by fragments of linear logic, a Kolmogorov-Gentzen-Gödel style translation, and a new translation between (...) the global consequence systems induced by full Lambek calculus and linear logic, mixing features of a Kiriyama-Ono style translation with features of a Kolmogorov-Gentzen-Gödel style translation. These translations establish a strong relationship between the logics involved and are used to obtain new results about whether Craig interpolation and Maehara interpolation hold in that logics . (shrink)

Satisfaction systems and reductions between them are presented as an appropriate context for analyzing the satisfiability and the validity problems. The notion of reduction is generalized in order to cope with the meet-combination of logics. Reductions between satisfaction systems induce reductions between the respective satisfiability problems and (under mild conditions) also between their validity problems. Sufficient conditions are provided for relating satisfiability problems to validity problems. Reflection results for decidability in the presence of reductions are established. The validity problem in (...) the meet-combination is proved to be decidable whenever the validity problem for the components are decidable. Several examples are discussed, namely, involving modal and intuitionistic logics, as well as the meet-combination of modal logic and intuitionistic logic. (shrink)

We address the problem of combining intuitionistic and S4 modal logic in a non-collapsing way inspired by the recent works in combining intuitionistic and classical logic. The combined language includes the shared constructors of both logics namely conjunction, disjunction and falsum as well as the intuitionistic implication, the classical implication and the necessity modality. We present a Gentzen calculus for the combined logic defined over a Gentzen calculus for the host S4 modal logic. The semantics is provided by Kripke structures. (...) The calculus is proved to be sound and complete with respect to this semantics. We also show that the combined logic is a conservative extension of each component. Finally we establish that the Gentzen calculus for the combined logic enjoys cut elimination. (shrink)

Fibring is recognized as one of the main mechanisms in combining logics, with great signicance in the theory and applications of mathematical logic. However, an open challenge to bring is posed by the collapsing problem: even when no symbols are shared, certain combinations of logics simply collapse to one of them, indicating that bring imposes unwanted interconnections between the given logics. Modulated bring allows a ner control of the combination, solving the collapsing problem both at the semantic and deductive levels. (...) Main properties like soundness and completeness are shown to be preserved, comparison with bring is discussed, and some important classes of examples are analyzed with respect to the collapsing problem. (shrink)

The main objective of this paper is to define a logic for reasoning about distributed time-stamped claims. Such a logic is interesting for theoretical reasons, i.e. as a logic per se, but also because it has a number of practical applications, in particular when one needs to reason about a huge amount of pieces of evidence collected from different sources, where some of the pieces of evidence may be contradictory and some sources are considered to be more trustworthy than others. (...) We introduce the time-stamped claim logic including a sound and complete sequent calculus. In order to show how time-stamped claim logic can be used in practice, we consider a concrete cyber-attribution case study. (shrink)

We give an axiomatization of first‐order logic enriched with the almost‐everywhere quantifier over finitely additive measures. Using an adapted version of the consistency property adequate for dealing with this generalized quantifier, we show that such a logic is both strongly complete and enjoys Craig interpolation, relying on a (countable) model existence theorem. We also discuss possible extensions of these results to the almost‐everywhere quantifier over countably additive measures.

Fusion is a well-known form of combining normal modal logics endowed with a Hilbert calculi and a Kripke semantics. Herein, fusion is studied over logic systems using sequent calculi labelled with truth values and with a semantics based on a two-sorted algebra allowing, in particular, the representation of general Kripke structures. A wide variety of logics, including non-classical logics like, for instance, modal logics and intuitionistic logic can be presented by logic systems of this kind. A categorical approach of fusion (...) is defined in the context of these logic systems. Preservation of soundness and completeness by fusion is studied. Soundness is preserved without further requirements, completeness is preserved under mild assumptions. (shrink)

Cut elimination is shown, in a constructive way, to hold in sequent calculi labelled with truth values for a wide class of normal modal logics, supporting global and local reasoning and allowing a general frame semantics. The complexity of cut elimination is studied in terms of the increase of logical depth of the derivations. A hyperexponential worst case bound is established. The subformula property and a similar property for the label terms are shown to be satisfied by that class of (...) modal sequent calculi. Modal logics presented by these calculi are proven to be globally and locally consistent. (shrink)

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. (shrink)

We introduce a general recipe for presenting non-classical logics in a modular and uniform way as labelled deduction systems. Our recipe is based on a labelling mechanism where labels are general entities that are present, in one way or another, in all logics, namely truth-values. More specifically, the main idea underlying our approach is the use of algebras of truth-values, whose operators reflect the semantics we have in mind, as the labelling algebras of our labelled deduction systems. The “truth-values as (...) labels” approach allows us to give generalized systems for multiple-valued logics within the same formalism: since we can take multiple-valued logics as meaning not only finitely or infinitely many-valued logics but also power-set logics, i.e. logics for which the denotation of a formula can be seen as a set of worlds, our recipe allows us to capture also logics such as modal, intuitionistic and relevance logics, thus providing a first step towards the fibring of these logics with many-valued ones. (shrink)

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. (shrink)

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. (shrink)

We extend meet-combination of logics for capturing the consequences that are common to both logics. With this purpose in mind we define meet-combination of consequence systems. This notion has the advantage of accommodating different ways of presenting the semantics and the deductive calculi. We consider consequence systems generated by a matrix semantics and consequence systems generated by Hilbert calculi. The meet-combination of consequence systems generated by matrix semantics is the consequence system generated by their product. On the other hand, the (...) meet-combination of consequence systems generated by Hilbert calculi is the consequence system generated by their interconnection. We investigate preservation of several properties. Capitalizing on these results we show that interconnection provides an axiomatization for the product. Illustrations are given for intuitionistic and modal logics, Łukasiewicz logic and some paraconsistent logics. (shrink)

Linear temporal logic with Since and Until modalities is expressively equivalent, over the class of complete linear orders, to a fragment of first-order logic known as FOMLO. It turns out that LTL, under some basic assumptions, is expressively complete if and only if it has the property, called separation, that every formula is equivalent to a Boolean combination of formulas that each refer only to the past, present or future. Herein we present simple algorithms and their implementations to perform separation (...) of the LTL with Since and Until, over discrete and complete linear orders, and translation from FOMLO formulas into equivalent temporal logic formulas. We additionally show that the separation of a certain fragment of LTL results in at most a double exponential size growth. (shrink)

In recent years, there has been a growing interest in the application of foundational ontologies, i.e., formal ontological theories in the philosophical sense, to provide a theoretically sound foun...

This book symposium comprises a précis of Nuno Venturinha’s Description of Situations: An Essay in Contextualist Epistemology together with four critical commentaries on different aspects of the book by Marcelo Carvalho, João Vergílio Gallerani Cuter, Marcos Silva and Darlei Dall’Agnol, and the author’s replies.

Esports, including virtual football, are a worldwide phenomenon. Yet, little is known about the physical activity levels of individuals engaged in virtual football game play. Therefore, we aimed to perform a preliminary evaluation of the levels of physical activity, sedentarism, and habits of physical training of adults engaged with virtual football in Portugal. This was a cross-sectional investigation based on a structured online survey using the International Physical Activity Questionnaire and a set of questions regarding habits of physical training. The (...) participants reported spending a median of 5,625 MET-min⋅week−1 being physically active. Still, the participants spent 320 min/day sitting, and 150 min/day practicing virtual football. According to the IPAQ scores, high physical activity levels were reported by 84.5% of the participants, and 87.1% were considered physically active considering the WHO guidelines on physical activity and sedentary behavior. Overall, 60.0% of the participants reported planning their own physical training. Maintaining or improving overall physical health was one of the main reasons for doing physical training, with only 6.1% responding being active to improve virtual football performance. Overall, the results showed that virtual football players accomplished the standard recommendations for physical activity, with high levels of physical activity, and encompassing regular physical training focused mostly on health promotion, rather than improved virtual football performance. (shrink)

Neste trabalho são apresentados dados e reflexões sobre a proposta pedagógica de Ensino Médio Politécnico, implantada desde 2012 nas escolas públicas estaduais do Rio Grande do Sul, Brasil. Tendo como pano de fundo as concepções do Educar pela Pesquisa e da Interdisciplinaridade - eixos norteadores da parte diversificada denominada Seminário Integrado -, a investigação teve cunho qualitativo, apresentando inferências sobre as compreensões acerca do conceito de pesquisa alcançadas pelos estudantes. As intervenções pedagógicas da investigação foram desenvolvidas em quatro turmas de (...) uma escola em Porto Alegre, capital do Rio Grande do Sul, encaminhadas no início do ano letivo de 2015. Por meio da análise qualitativa das falas dos alunos, da identificação da ampliação da complexidade dos seus respectivos mapas conceituais, confeccionados no software CmapTools, assim como da avaliação quanto à profundidade dos projetos encaminhados, pôde-se evidenciar ampla evolução nas compreensões dos alunos quanto ao conceito de pesquisa, percebendo-se assim que a metodologia aplicada nessa investigação foi profícua. (shrink)

The Second Vatican Council was built within a solidly constituted tradition in the Catholic Church. All councils were held within the traditional and legal parameters of the Church. The question about the condition of possibility of a renewal Council under this tradition shows relevant. The Vatican II is the result of a negotiation between renewal and preservation. Pope John XXIII personally coordinated the construction of the legitimacy of the new event, following steps which may be rescued during the preparatory stages (...) of the great assembly. The reading of this process from sociological parameters may elucidate its plausibility within the tradition and the Church's bureaucratic organization. Pope John started ably a church renewal process, opening a new phase in the long Catholic tradition. Under his Pope condition, he knew how to seed the idea of a revamping event in the name of a divine inspiration and with the set of bishops’ participation of the Church. (shrink)

Our present moral traits are unable to provide the level of large-scale co-operation necessary to deal with risks such as nuclear proliferation, drastic climate change and pandemics. In order to survive in an environment with powerful and easily available technologies, some authors claim that we need to improve our moral traits with moral enhancement. But this is prone to produce paradoxical effects, be self-reinforcing and harm personal identity. The risks of moral enhancement require the use of a safety framework; such (...) a framework should guarantee practical robustness to moral uncertainty, empirical adequacy, correct balance between dispositions, preservation of identity, and be sensitive to practical considerations such as emergent social effects. A virtue theory can meet all these desiderata. Possible frameworks incorporate them to variable degrees. The social value orientations framework is one of the most promising candidates. (shrink)

O objetivo deste trabalho é compreender os interesses teórico e prático da ideia kantiana de história como progresso. Nesse passo, pretende-se examinar como o interesse teórico da razão relaciona-se com a filosofia da história de Kant e em que medida ele diferencia-se do interesse teórico referente ao conhecimento objetivo, ao assumir a forma de ideias heurístico-regulativas. Contra aqueles que não admitem o interesse teórico na filosofia da história de Kant, pretende-se defender não somente a sua ocorrência, mas também a sua (...) necessidade quando se tem em vista os horizontes do interesse prático da ideia de progresso histórico. Com isso, passa-se a estudar a convergência dos interesses prático e teórico na ideia kantiana de história e como Kant investiga os elementos fáticos da história à procura de motores empíricos para guiar o progresso humano. (shrink)

The Foundations of Cognitive Science is a set of thirteen new essays on key topics in this lively interdisciplinary field, by a stellar international line-up of authors. Philosophers, psychologists, and neurologists here come together to investigate such fascinating subjects as consciousness; vision; rationality; artificial life; the neural basis of language, cognition, and emotion; and the relations between mind and world, for instance our representation of numbers and space. The contributors are Ned Block, Margaret Boden, Susan Carey, Patricia Churchland, Paul Churchland, (...) Antonio Damasio, Hanna Damasio, Donald Davidson, Daniel Dennett, Ilya Farber, James Higginbotham, Christopher Peacocke, Will Peterman, Zenon Pylyshyn, John Searle. Anyone interested in the exploration of the human mind will enjoy this book. (shrink)

O artigo tenta reconstruir alguns elementos acerca da passagem da Lógica da essência para a Lógica do conceito, da necessidade para a liberdade, na Ciência da Lógica hegeliana. No contexto da publicação dos duzentos anos dessa obra filosófica, a explicitação dessa passagem é referencial para a compreensão da Ciência da Lógica e de todo o pensamento hegeliano. O artigo procura sustentar que o binômio necessidade/contingência, um dos pares categoriais da Lógica da essência, não é adequado para a articulação da filosofia (...) hegeliana. Como Hegel afirma reiteradas vezes, é preciso superar a dura necessidade para dar lugar à lógica da liberdade. Para a discussão da problemática, a confrontação entre algumas categorias da essência, tais como substancialidade, necessidade, contingência e causalidade, e algumas categorias do conceito, tais como universalidade, particularidade e singularidade é o foco da exposição. Dessa discussão brota a noção hegeliana de liberdade e a sua relação com o sistema. (shrink)

Importing subsumes several asymmetric ways of combining logics, including modalization and temporalization. A calculus is provided for importing, inheriting the axioms and rules from the given logics and including additional rules for lifting derivations from the imported logic. The calculus is shown to be sound and concretely complete with respect to the semantics of importing as proposed in J. Rasga et al. (100(3):541–581, 2012) Studia Logica.

In this paper, we investigate the rules that should underlie a computer program that is capable of revising its beliefs or opinions. Such a program maintains a model of its environment, which is updated to reflect perceived changes in the environment. This model is stored in a knowledge base, and the program draws logical inferences from the information in the knowledge base. All the inferences drawn are added to the knowledge base. Among the propositions in the knowledge base, there are (...) some in which the program believes, and there may be others in which the program does not believe. Inputs from the outside world or reasoning carried out by the program may lead to the detection of contradictions, in which case the program has to revise its beliefs in order to get rid of the contradiction and to accommodate the new information. (shrink)

This paper tries to characterize the factors determining human relations with its environment and to identify the drives of those behavioral patterns and “praxis”. One scrutinizes the physiological and psychological factors that influence those drives, and tries to determine ways of overriding instinctive drives in favor of rational, sustainable ones. It focuses its attention on the way the different ecosystemic, economic and socio-cultural systems work, and pin-points the critical issues in view of the development of sustainable behavioral patterns. Also the (...) values that must build the new behavioral paradigm, as well as the ways to ensure the evolutionary quantum-leap necessary to ensure this sustainable condition, and the fulfilment, at every level, the different needs of humans and human societies, are analyzed. In conclusion, it stresses the fact that any reliable and long lasting change towards a sustainable behavior must start at the individual and the close social groups levels, and of the development of new factors of self-fulfillment and gratification, able to support and foster that change. The proposed epistemological approach is particularly innovative, precisely because of this emphasis on the individual drives and the way they determine the global patterns of environmental use, as well as the way they can evolve into a more rational character. In short, the paper focuses itself in the way man can evolve from its natural animal instincts and drives toward more rational ones, humanizing its behavior and turning, therefore, into an able actor of the process of sustainability building. (shrink)

Following logicism, Frege famously held that logic is a science on its own. Particularly, he held the informativity thesis, viz., that logic is a science because it is deductively informative. This paper aims to understand Frege’s informativity thesis and its connection with the conception of logic as science. For such, it focuses on some features of Frege’s philosophy that are key for understanding this connection, particularly his conception of analyticity, the role of judgments in inferential reasoning, and the use of (...) decomposition of functions as a means for concept-formation, which Frege names as fruitful definitions. Keywords: Gottlob Frege; Informativity of Logic; Judgements; Fruitful Definitions. (shrink)

O texto é uma resenha da Doutrina do Conceito hegeliana recém editada e publicada em português. O terceiro livro da Ciência da Lógica é estruturado em subjetividade, objetividade e ideia, com cada uma destas partes também desenvolvida numa estrutura tripartite. Nesta exposição, merece destaque o movimento contraditório de autodeterminação do conceito, no qual a universalidade se autodiferencia imanentemente em particularidade e o conceito retorna a si mesmo na forma da universalidade concreta. O conceito passa pelas diferentes formas de mediação na (...) teoria do silogismo, especialmente com a mediação da universalidade, quando o conceito se transforma em objetividade. Esta começa com a relação externa do mecanismo, avança para a relação interna do quimismo e conclui na teleologia, onde a liberdade é mais elevada que a necessidade. A Ideia, última parte da Doutrina do Conceito, é a unidade sintética entre conceito e objetividade, com destaque no capítulo da Ideia absoluta na qual Hegel formula uma noção de método como estrutura e movimento do conteúdo e da racionalidade. (shrink)

The exchange of goods and services between individuals is often formalised by a contract in which the parties establish norms to define what is expected of each one. Norms use deontic statements of obligation, prohibition, and permission, which may be in conflict. The task of manually detecting norm conflicts can be time–consuming and error-prone since contracts can be vast and complex. To automate such tasks, we develop an approach to identify potential conflicts between norms. We show the effectiveness of our (...) approach and its individual components empirically using two publicly available corpora, and contribute with a new annotated test corpus for norm conflict identification. (shrink)