Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization

Archive for Mathematical Logic 60 (7):783-813 (2021)
  Copy   BIBTEX


We extend natural deduction for first-order logic (FOL) by introducing diagrams as components of formal proofs. From the viewpoint of FOL, we regard a diagram as a deductively closed conjunction of certain FOL formulas. On the basis of this observation, we first investigate basic heterogeneous logic (HL) wherein heterogeneous inference rules are defined in the styles of conjunction introduction and elimination rules of FOL. By examining what is a detour in our heterogeneous proofs, we discuss that an elimination-introduction pair of rules constitutes a redex in our HL, which is opposite the usual redex in FOL. In terms of the notion of a redex, we prove the normalization theorem for HL, and we give a characterization of the structure of heterogeneous proofs. Every normal proof in our HL consists of applications of introduction rules followed by applications of elimination rules, which is also opposite the usual form of normal proofs in FOL. Thereafter, we extend the basic HL by extending the heterogeneous rule in the style of general elimination rules to include a wider range of heterogeneous systems.



    Upload a copy of this work     Papers currently archived: 92,261

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Normalization proof for Peano Arithmetic.Annika Siders - 2015 - Archive for Mathematical Logic 54 (7-8):921-940.
A Formalization Of Sambins's Normalization For Gl.Edward Hauesler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
Wittgenstein's ab-Notation: An Iconic Proof Procedure.Timm Lampert - 2017 - History and Philosophy of Logic 38 (3):239-262.
Why does the proof-theory of hybrid logic work so well?Torben Braüner - 2007 - Journal of Applied Non-Classical Logics 17 (4):521-543.
A proof–theoretic study of the correspondence of hybrid logic and classical logic.H. Kushida & M. Okada - 2006 - Journal of Logic, Language and Information 16 (1):35-61.


Added to PP

19 (#803,294)

6 months
11 (#244,932)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
Logic and structure.D. van Dalen - 1980 - New York: Springer Verlag.
Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.

View all 14 references / Add more references