A formal system of first-order predicate calculus with infinitely long expressions
type: Item
instance of: scholarly article
title: A formal system of first-order predicate calculus with infinitely long expressions
zbMATH Open document ID: 0108.00203
author: Shôji Maehara
author: Gaisi Takeuti
published in: Journal of the Mathematical Society of Japan
publication date: 1962-01-01T00:00:00Z
review text: For any fixed strongly inaccessible number \(\Omega_0\) the authors consider a language whose notion of well-formed formula is defined roughly as follows: (i) Prime formulas are predicate symbols followed by a well-ordered sequence of terms whose order-type is less than \(\Omega_0\). (ii) If \(A\), \(A_\lambda\) are formulas for all \(\lambda< \alpha <\Omega_0\) then \(\dashv A\) and \(\bigvee_{\lambda< \alpha}A_\lambda\) are formulas. (iii) If \(A(a_0, a_1, \ldots)\) is a formula containing the well-ordered sequence (of type \(< \Omega_0\)) \(a_0, a_1, \ldots\) of distinct free variables then \((\exists\) \(x_0, x_1,\ldots)\) \(A(x_0, x_1,\ldots)\) is a formula where \(x_0, x_1,\ldots\) is a sequence of distinct bound variables. A Gentzen-type set of rules of proof is then proposed and proven semantically complete by adapting Schütte's method [\textit{K. Schütte}, Arch. Math. Logik Grundlagenforsch. 2, 55--67 (1956; Zbl 0071.00802)] for a proof of the corresponding result for first order predicate logic. This proof also gives a Löwenheim-Skolem-type theorem. The authors prove furthermore the cut-elimination theorem and Craig's interpolation theorem for their system.
Mathematics Subject Classification ID: 03B10
zbMATH DE Number: 3176037
zbMATH Keywords: first-order predicate calculus
zbMATH Keywords: infinitely long expressions
zbMATH Keywords: Gentzen-type set of rules of proof
zbMATH Keywords: semantic completeness
zbMATH Keywords: Schütte's method
zbMATH Keywords: Löwenheim-Skolem-type theorem
zbMATH Keywords: cut-elimination theorem
zbMATH Keywords: Craig's interpolation theorem
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.2969/jmsj/01340357
OpenAlex ID: W2018651033
DOI: 10.2969/JMSJ/01340357
description: scientific article; zbMATH DE number 3176037