Hostname: page-component-7b7567c8c-tnzcf Total loading time: 0 Render date: 2026-11-12T04:59:13.043Z Has data issue: false hasContentIssue false

A heterogeneous interpolant

Published online by Cambridge University Press:  22 January 2016

Walter Taylor*
Affiliation:
University of Colorado
Rights & Permissions [Opens in a new window]

Extract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

In this note we exhibit an interpolant for a certain valid implication ╞ φ → ψ, where φ and ψ come from the infinitary language Lω1ω1 . The existence of this interpolant follows from Takeuti’s heterogeneous interpolation theorem [5], but unfortunately the proof in [5] is not explicit enough to allow one to find the interpolant explicitly. Takeuti’s theorem asserts the existence of an interpolant in the class Lω1ω1 of heterogeneous formulas, which admits the rules of formation of Lω1ω1 plus the following additional rule:

Information

Type
Research Article
Copyright
Copyright © Editorial Board of Nagoya Mathematical Journal 1973