A constructive proof of Craig's interpolation lemma for m-valued logic

✍ Scribed by Anita Waselewska

• Publisher: Springer Netherlands
• Year: 1979
• Tongue: English
• Weight: 437 KB
• Volume: 38
• Category: Article
• ISSN: 0039-3215
• DOI: 10.1007/bf00405385

✦ Synopsis

The a]gebraie proof of CrMg's interpolation lemma for m-valued logic was given by Rasiowa in [i]. We present here a constructive proof of this lemma, based on a Gentzen type formMization.

:Let J be the set oi all formulas oi m-valued predicate calculus. We assume that our language does not contain functioi~ constants. Let _~ be the set of all finite sequences of Y. Elements of ff will be denoted by Y, A, S with indices if necessary. When F denotes the sequence A1, As, ... ..., A~, we denote the sequence -]A1, ~A2, ..., "~A, by -IT'. By a Gentzen type formalization of m-vMfied logic we shall understand a relational system G = (F, AK, ~) where AK ~_ .F consists of E~_~ or all sequences Di(A), -]Dj(A) for some 1 <~ i <~j <~ m--i. ~ is the following set of rules of inference: I. Structural rules.