Archive for Mathematical Logic:1-31 (forthcoming)

We extend natural deduction for first-order logic 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 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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s00153-020-00759-y
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 58,849
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

A Natural Extension of Natural Deduction.Peter Schroeder-Heister - 1984 - Journal of Symbolic Logic 49 (4):1284-1300.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
A Diagrammatic Inference System with Euler Circles.Koji Mineshima, Mitsuhiro Okada & Ryo Takemura - 2012 - Journal of Logic, Language and Information 21 (3):365-391.

View all 6 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

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 index

Total views
7 ( #1,015,951 of 2,426,098 )

Recent downloads (6 months)
7 ( #102,183 of 2,426,098 )

How can I increase my downloads?


My notes