A general method of axiomatizing fragments
type: Item
instance of: scholarly article
title: A general method of axiomatizing fragments
zbMATH Open document ID: 0737.03002
author: Tadahiro Uesu
published in: Journal of the Mathematical Society of Japan
publication date: 1992-06-25T00:00:00Z
review text: The author presents a general method for axiomatizing fragments of first- order theories. The paper is obviously the contribution [U2 ] announced by the author in Lect. Notes Math. 1104, 453-475 (1984; Zbl 0574.03049). The method is so to speak the proof-theoretic counterpart of the model- theoretic procedure of \textit{C. Smorynski} in J. Symb. Logic 42, 530-544 (1977; Zbl 0381.03046). The fragment to be axiomatized is characterized by some property which is expressed by a sequence of so-called approximations of a certain type. \textit{N. Motohashi} introduced this procedure in Fundam. Math. 120, 127-142 (1984; Zbl 0582.03004) to express uniqueness by existence. An approximation is a function which associates a formula to any sequent of a certain type. The central concept of the paper under review is that of inference forms. These are figures for inference rules such that the axioms of a theory can be gained from them. A cut-elimination theorem for theories formalized by such inference forms is given. First, the new concept is applied to get and partly regain some concrete axiomatization results, and finally two general axiomatization theorems are proven for intuitionistic and classical theories with equality.
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F03
zbMATH DE Number: 13436
zbMATH Keywords: axiomatization of fragments of first-order theories
zbMATH Keywords: inference forms
zbMATH Keywords: cut-elimination
zbMATH Keywords: intuitionistic and classical theories with equality
reviewed by: Helmut Pfeiffer
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.2969/jmsj/04320413
OpenAlex ID: W2066038333
DOI: 10.2969/JMSJ/04320413
Recommended article: Axiomatizing a fragment of PAFAS
Recommended article: A constructive consistency proof of a fragment of set theory
Recommended article: Q3476809
Recommended article: A decidable fragment of predicate calculus
Recommended article: Closed Fragments of Provability Logics of Constructive Theories
Recommended article: Axiomatizing schemes and their behaviors
Recommended article: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
Recommended article: Fragments of First-Order Logic
Recommended article: Algebraic Characterizations for Universal Fragments of Logic
Recommended article: Q3172386
description: scientific article; zbMATH DE number 13436