Abstract
We prove three interpolation theorems for typless logics with equality. Typless logics, introduced by Henkin and Tarski, are algebraizable extensions of first-order logic allowing infinitary predicate symbols. Lambda(alpha) (alpha an infinite ordinal) denotes the language of a typless logic with a many variables. As a sample, we shall prove:
THEOREM 1
Let Lambda(alpha) be a language (possibly uncountable). Let psi, phi, be formulas such that
vertical bar=phi ->psi.
Then there exist m <alpha, i epsilon(m)alpha and eta a formula containing only atomic formulas occurring in psi and phi, in short atf (eta)subset of atf(phi)boolean AND(psi), such that
vertical bar=for all nu(i0)...for all nu(im) (1)phi ->eta and vertical bar=eta ->there exists nu(i0)...nu(im) (1)psi
Fm-r denotes the set of all formulas in a language. Now assuming, that everything is countable, we show that there exists two unary connectives, such that if Fm denotes the formulas in this expanded language, then
THEOREM 2
(for all psi,phi epsilon Fm-r)[vertical bar=phi ->psi double right arrow there exists eta epsilon Fm,atf(eta)subset of atf(phi)boolean AND atf(psi)
vertical bar=phi ->eta and vertical bar=eta ->psi].
That is, in the countable case, we can add finitely many connectives to code the quantified variables in Theorem 1. Our last interpolation theorem addresses certain (natural) expansions of Fm-r. We also give counterexamples showing that the scope of our results is the best possible. Our treatmet is algebraic via reducts of polyadic equality algebras. (2000 Mathematics Subject Classification. Primary 03G15. Secondary 03C05, 03C40.).