Pairing Without Conventional Restraints

✍ Scribed by Henk Barendregt

• Publisher: John Wiley and Sons
• Year: 1974
• Tongue: English
• Weight: 886 KB
• Volume: 20
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19740201902

✦ Synopsis

PAIRING WITHOUT CONVENTIONAL RESTRAINTS by HENK BARENDREGT in Utrecht (Netherlands) 1) Dedicated to Kathleen McLaughlin 8 0. Introduction A w i r i n g (in some formal system) is a triple of terms D, D1, D2 such that D1 (Dab) = a and D2(Dab) = b are provable in that system. A surjective pairing has the additional condition D(Dla) (D2a) = a .

As formal systems we consider the type free A-calculus, the typed A-calculus and the various versions of intuitionistic arithmetic of all finite types, HA", all systems with or without extensionality. Also the combinatory formulation of those systems is treated. The results are 1. There is a pairing for all type free systems (1.13, CHURCH, BERNAYS). 2. There is a pairing for all typed systems containing (weak) extensionality (2.10, 3. For the typed systems without extensionality there is in general no pairing (3.16). 1. There is no surjective pairing (at all) for any of the systems considered, except Furthermore a characterization is given of the types cr, z for which pairing is possible in the typed systems without extensionality (3.16).