Definitional reflection and basic logic
type: Item
instance of: scholarly article
title: Definitional reflection and basic logic
zbMATH Open document ID: 1263.03052
author: Peter Schroeder-Heister
published in: Annals of Pure and Applied Logic
publication date: 2013-03-15T00:00:00Z
review text: In the paper, two general approaches towards generating logical rules are comparised: Basic Logic (BL) due to Sambin, Battiglioni and Faggian, and Definitional Reflection (DL) due to Schroeder-Heister and Hallnäs. Both approaches belong to the framework of proof-theoretic semantics, where the meaning of logical constants is explained in terms of inference rules. In BL one starts with definitional equations characterising logical constants which allows one to generate Gentzen-style sequent introduction rules for this constant. One side of an equation, called formation, gives directly one of the introduction rules; the other one is generated by means of cut from the other side of equation, called implicit reflection (which in fact covers elimination rule(s)). In DR one starts with a definitional system of clauses which directly lead to formation of introduction rules (or rules of definitional closure) and to general elimination rules (rules of definitional reflection). For the sake of comparison it is shown how sequent calculi investigated in BL can be represented in the framework of DR. The analysis based on the notion of complementarity shows that two criteria of adequacy must be satisfied: of cut reduction and of uniqueness. DR establishes a direct duality between formation and reflection rules whereas in BL one obtains reflection rules from the equation covering both formation and elimination rules. Moreover, in BL one needs cut as primitive to deduce reflection rules from formation and elimination rules, whereas in DR the criterion of cut reduction does not presuppose the whole strength of cut.
reviewed by: Andrzej Indrzejczak
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 03A05
zbMATH DE Number: 6145440
zbMATH Keywords: proof-theoretic semantics
zbMATH Keywords: sequent calculus
zbMATH Keywords: definitional reflection
zbMATH Keywords: basic logic
MaRDI profile type: Publication
full work available at URL: j.apal.2012.10.010
OpenAlex ID: W2104615089
DOI: 10.1016/J.APAL.2012.10.010
description: scientific article; zbMATH DE number 6145440