Prawitz suggested expanding a natural deduction system for intuitionistic logic to include rules for classical logic constructors, allowing both intuitionistic and classical elements to coexist without losing their inherent characteristics. Looking at the added rules from the point of view of the Gödel-Gentzen translation, led us to propose a general method for the coexistent combination of two logics when a conservative translation exists from one logic (the source) to another (the host). Then we prove that the combined logic is a conservative extension of the original logics, thereby preserving the unique characteristics of each component logic. In this way there is no collapse of one logic into the other in the combination. We also demonstrate that a Gentzen calculus for the combined logic can be induced from a Gentzen calculus for the host logic by considering the translation. This approach applies to semantics as well. We then establish a general sufficient condition for ensuring that the combined logic is both sound and complete. We apply these principles by combining classical and intuitionistic logics capitalizing on the Gödel-Gentzen conservative translation, intuitionistic and S4 modal logics relying on the Gödel-McKinsey-Tarski conservative translation, and classical and Jaśkowski’s paraconsistent logics taking into account the existence of a conservative translation.

Particular reasoning enables the deductive proof of existential properties, such as the satisfiability/consistency of a set of formulas. In this work, we consider particular reasoning in the context of a theory of a given logic. The logic is presented by a semantic constraint specification. From this specification, we induce a particular calculus for the logic at hand. In this calculus we define what is a particular derivation in the context of a theory and show how to extract a model of the theory that satisfies the assertions within the derivation. We demonstrate that the induced particular calculus is both sound and complete with regard to the intended semantics. Our results are applicable to logics with a strong finite model property, including classical, intuitionistic, certain modal logics, and Nelson's N4 logic, among others.

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 N4, paraconsistent logic 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 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.

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 and . 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.

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.

We present a technique for obtaining a logic with abductive reasoning extending a given propositional logic. Abduction, along with deduction and induction, is recognized as important for machine learning, namely in identifying possible causes that may lead to the occurrence of an event and in providing new ways for a computational device to achieve a certain objective. Each rule in the original calculus induces a set of multiple-conclusion abductive rules. Moreover, rules stating generic properties of abduction have to be added. In the induced logic, the deductive mechanism of the base logic coexists with this abductive component. A new notion of a multiple-conclusion derivation had to be developed. Due to the canonical nature of obtaining such a logic, we prove the preservation of soundness, completeness, decidability and computational complexity. These concepts and results are illustrated in a robot navigation problem using a multimodal logic.

We provide sufficient conditions for the existence of a conservative translation from a consequence system to another one. We analyze the problem in many settings, namely when the consequence systems are generated by a deductive calculus or by a logic system including both proof-theoretic and model-theoretic components. We also discuss reflection of several metaproperties with the objective of showing that conservative translations provide an alternative to proving such properties from scratch. We discuss soundness and completeness, disjunction property and metatheorem of deduction among others. We provide several illustrations of conservative translations.

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.

The essential structure of derivations is used as a tool for measuring the complexity of schema consequences in propositional-based logics. Our schema derivations allow the use of schema lemmas and this is reflected on the schema complexity. In particular, the number of times a schema lemma is used in a derivation is not relevant. We also address the application of metatheorems and compare the complexity of a schema derivation after eliminating the metatheorem and before doing so. As illustrations, we consider a propositional modal logic presented by a Hilbert calculus and an intuitionist propositional logic presented by a Gentzen calculus. For the former, we discuss the use of the metatheorem of deduction and its elimination, and for the latter, we analyze the cut and its elimination. Furthermore, we capitalize on the result for the cut elimination for intuitionistic logic, to obtain a similar result for Nelson’s logic via a language translation.

AbstractSatisfaction 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$\textrm {K}$modal logic and intuitionistic logic.

The Event-Based Time-Stamped Claim Logic that we define in this paper allows one to reason about distributed time-stamped claims that can change through time by the occurrence of events. Such a logic is interesting for theoretical reasons, i.e., as a logic per se, but also because it can be applied in a number of different disciplines and application domains (e.g., history, crime forensics or cyber forensics) as it allows one to reason about a huge amount of pieces of evidence collected from different sources over time, where some of the pieces of evidence may be contradictory and some sources considered to be more trustworthy than others. We formalize the language and the semantics of the Event-Based Time-Stamped Claim Logic, provide a sound and complete Hilbert calculus, and consider some concrete examples. We also show that the validity problem for the logic is decidable by providing a tableau-like decision algorithm.

The objective of the chapter is to discuss decidability of combination of theories sharing only equality. We start by relating the decidability problem with the satisfiability problem in the context of a theory. This relationship is relevant since we prove preservation of decidability relying on preservation of satisfiability. We follow the Nelson-Oppen technique for establishing the preservation of satisfiability. So the theories considered for combination only share equality and are stably infinite.

The objective of the chapter is to provide a usable way to deduce logical consequences from a given theory. We adopt Gentzen calculus (other alternatives for reasoning with theories are, namely, natural deduction and tableaux, see [, ] and [], respectively) inspired by the presentation in [] and in [] (see also []) and analyze how to use the calculus for reasoning with theories. After proving some technical lemmas and providing several examples, we show that the calculus is sound and, based on Hintikka sets (see [, ]), we also prove completeness. Then we establish in detail Gentzen’s Hauptsatz, i.e., the Cut Elimination Theorem (see [, ] and for more advanced topics on cut elimination see also [, , ]). Finally, we conclude the chapter with a constructive proof of Craig’s Interpolation Theorem (see [, , ]).

In this chapter, after some introductory concepts and results, we present sufficient conditions for a theory to be decidable. We start by considering theories with computable quantifier elimination and show that the decidability of such theories is equivalent to the decidability of their quantifier-free sentence fragment.

Provides a comprehensive, self-contained introduction to decidability of first-order theories, using detailed proofs and examples to illustrate and clarify complex concepts Incorporates computability theory and reduction techniques to determine the decidability of theories Illustrates a variety of ways to deduce logical consequences from a theory, including the use of Gentzen calculus for first-order logic

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.