Definitional reflection and basic logic (Q1942043)

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.