Tarskian Structured Consequence Relations and Functional Completeness

  • Heinrich Wansing
Part of the Trends in Logic book series (TREN, volume 3)


Many proofs of functional completeness for intuitionistic propositional logic and related systems make use of a higher-level natural deduction or sequent-style proof-theoretic semantics, see e.g. [8], [96], [97], [151], [178], and [180]. The idea now is to apply this kind of approach to Gabbay’s [67] notion of a Tarski-type structured consequence relation |~ between structured databases Δ and single formulas A. This concept generalizes the ordinary notion of single-conclusion consequence relations and is intended to capture a broad range of non-monotonic reasoning systems, like Defeasible Logic and Probabilistic Nets (for concrete examples and motivation see [67]). Intuitively speaking, a structured database is a structure τ together with an assignment of formulas to the elements of the domain of τ. Working within a sequent calculus framework we assume that a structured database Δ is always finite. With every Tarski-type structured consequence relation |~ we shall associate a certain positive propositional logic |~+ by specifying introduction rules for various propositional connectives and constants which naturally arise in the context of structured databases. The main novelty here is Gabbay’s idea to conceive of implication as depending on a contraction mapping operating on the underlying structures. It is then shown that this collection of connectives and constants is expressively complete with respect to a semantics in terms of rather natural introduction schemata. In a second step this approach is extended to constructive propositional logics associated with Tarskian structured consequence relations. The constructive negation ~ of these systems is motivated by the idea of taking refutations seriously and therefore considering the notion of disproof as primitive and of equal importance as the positive notion of proof; see also Chapter 9. Cut-elimination and functional completeness of the extended set of operations will be established.


Propositional Logic Sequent Calculus Introduction Rule Constructive Logic Intuitionistic Propositional Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 1998

Authors and Affiliations

  • Heinrich Wansing
    • 1
  1. 1.Institute of Logic and Philosophy of ScienceUniversity of LeipzigLeipzigGermany

Personalised recommendations