Tarskian Structured Consequence Relations and Functional Completeness
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. , , , , , and . The idea now is to apply this kind of approach to Gabbay’s  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 ). 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.
KeywordsPropositional Logic Sequent Calculus Introduction Rule Constructive Logic Intuitionistic Propositional Logic
Unable to display preview. Download preview PDF.