Generalized definitional reflection and the inversion principle

DOI10.1007/S11787-007-0018-7MaRDI QIDQ2470764zbMATH OpenOpenAlexFDO

Authors Peter Schroeder-Heister

Publication date 15 February 2008

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-007-0018-7

zbMATH Keywords

definitional reflectioninversion principleproof-theoretic semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Structure of proofs (03F07)

Review text

In this paper, definitional reflection -- a principle proposed by Hallnäs and the author in a series of other papers -- is related to the inversion principle -- as introduced by Lorenzen, corrected by Hermes, and later adopted by Prawitz for his programme of general proof theory. It is shown that ``both, definitional reflection and the inversion principle are consequences of generalized definitional reflection, a generalization of the definitional reflection in the presence of variables. However, ``both are strictly weaker than generalized definitional reflection, but neither of them entails the other one. To obtain generalized definitional reflection from simple definitional reflection, an \(\omega\)-principle is considered. The question remains whether there is a similar principle for the inversion principle.

Recommendations

• INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
• scientific article; zbMATH DE number 1231672
• Definitional reflection and basic logic
• scientific article; zbMATH DE number 1523032
• The principle of reflection via nested sequents
• Realizability interpretation of generalized inductive definitions
• scientific article; zbMATH DE number 1396736
• Logics with definitional reflection rules
• Definability and invariance

Cited in

(15)

• The explosion calculus
• Speech acts, categoricity, and the meanings of logical connectives
• Steps towards a proof-theoretical semantics
• HARMONISING HARMONY
• On Inversion Principles
• INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES
• Inversion principles and introduction rules
• General-elimination harmony and higher-level rules
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus
• General-elimination stability
• CATEGORICAL HARMONY AND PATH INDUCTION
• a-logic with arrows
• Proof-theoretic semantics: an autobiographical survey
• When rules define logical operators: rules as second-order definitions
• Whence admissibility constraints? From inferentialism to tolerance

This page was built for publication: Generalized definitional reflection and the inversion principle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2470764)