A formal system of first-order predicate calculus with infinitely long expressions (Q1130508)

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.