Turlar nazariyasi tarixi - History of type theory

The tip nazariyasi dastlab turli xil rasmiy paradokslardan saqlanish uchun yaratilgan mantiq va tizimlarni qayta yozish. Keyinchalik tip nazariyasi sinfiga ishora qildi rasmiy tizimlar, ularning ba'zilari muqobil bo'lib xizmat qilishi mumkin sodda to'plam nazariyasi barcha matematikaning asosi sifatida.

O'shandan beri rasmiy matematikaga bog'langan Matematikaning printsipi bugungi kunga yordamchi yordamchilar.

1900–1927

Rasselning turlar nazariyasining kelib chiqishi

Uchun maktubda Gottlob Frege (1902), Bertran Rassel paradoksni kashf etganligini e'lon qildi Frege's Begriffsschrift.[1] Frege darhol javob berib, muammoni tan oldi va "darajalar" ning texnik muhokamasida echimini taklif qildi. Frege'dan taklif qilish uchun:

Aytgancha, menga "a predikat o'zi tomonidan aniqlangan "aniq emas. Predikat odatda birinchi darajali funktsiyadir va bu funktsiya ob'ektni argument sifatida talab qiladi va o'zini argument (mavzu) sifatida tuta olmaydi. Shuning uchun men" kontseptsiya oldindan belgilanadi o'z kengaytmasi ".[2]

U bu qanday ishlashi mumkinligini ko'rsatishni davom ettiradi, ammo undan orqaga chekinadiganga o'xshaydi. Sifatida tanilgan narsalarning natijasi sifatida Rassellning paradoksi Frege ham, Rassell ham printerlarda bo'lgan asarlarini tezda o'zgartirishi kerak edi. Rassel unga biriktirilgan B ilovasida Matematika asoslari (1903) turlar haqidagi "taxminiy" nazariyasini topadi. Bu masala Rasselni taxminan besh yil qiynagan.[3]

Willard Quine[4] turlar nazariyasining kelib chiqishi va "ramified" turlar nazariyasining tarixiy sinopsisini taqdim etadi: turlar nazariyasidan voz kechishni o'ylab (1905), Rassel o'z navbatida uchta nazariyani taklif qildi:

  1. zigzag nazariyasi
  2. o'lchov chegarasi nazariyasi,
  3. sinfsiz nazariya (1905-1906) va keyin,
  4. turlar nazariyasini qayta ko'rib chiqish (1908 yil)

Kvinning ta'kidlashicha, Rassellning "ko'rinadigan o'zgaruvchi" tushunchasini joriy etishi quyidagi natijaga erishgan:

"hamma" va "har qanday" o'rtasidagi farq: "hamma" universal kvantlashning chegaralangan ("aniq") o'zgaruvchisi bilan ifodalanadi, u turga qarab o'zgaradi va "har qanday" erkin ("haqiqiy") o'zgaruvchiga ega qaysi turidan qat'iy nazar har qanday aniqlanmagan narsaga sxematik tarzda ishora qiladi.

Quine bu "bog'langan o'zgaruvchi" tushunchasini "turlar nazariyasining ma'lum jihatlaridan tashqari ma'nosiz".[5]

Turlarning 1908 yildagi "kengaygan" nazariyasi

Quine buni tushuntiradi kengaytirilgan nazariya quyidagicha: "Bu shunday nomlangan, chunki funktsiya turi uning argumentlari turlariga ham, undagi (yoki ifodasida) ko'rinadigan o'zgaruvchilar turlariga ham bog'liq, agar ular dalillar ".[5] Stiven Klayn uning 1952 yilda Metamatematikaga kirish tasvirlaydi kengaytirilgan turlar nazariyasi shu tarzda:

Birlamchi ob'ektlar yoki shaxslar (ya'ni mantiqiy tahlilga berilmagan narsalar) bitta turga (masalan, aytilgan) beriladi 0 turi), shaxslarning xususiyatlari to 1 turi, individual xususiyatlarning xususiyatlari to 2 turi, va boshqalar.; va ushbu mantiqiy turlardan biriga kirmaydigan hech qanday xususiyatlar qabul qilinmaydi (masalan, bu "oldindan taxmin qilinadigan" va "ishonib bo'lmaydigan" xususiyatlarni ... mantiq rangidan tashqarida). Batafsil ma'lumot boshqa ob'ektlar uchun qabul qilingan turlarni munosabatlar va sinflar sifatida tavsiflaydi. Keyin chiqarib tashlash ishonchli bir turdagi doiradagi ta'riflar, 0 turidagi yuqoridagi turlar qo'shimcha ravishda buyurtmalarga bo'linadi. Shunday qilib, 1-toifa uchun biron bir umumiylikni eslatmasdan aniqlangan xususiyatlar tegishli buyurtma 0, va berilgan buyurtma xususiyatlari yig'indisidan foydalangan holda aniqlangan xususiyatlar keyingi yuqori darajaga tegishli. ... Ammo buyruqlarga bo'linish, biz yuqorida keltirilgan tanish bo'lmagan tahlillarni tuzishning iloji yo'q, chunki unda aniq bo'lmagan ta'riflar mavjud. Ushbu natijadan qochish uchun Rassel o'zining postulatini e'lon qildi kamaytirilishi aksiomasi, bu eng past darajadagi buyruqqa tegishli har qanday xususiyatga, 0 tartibli koeffitsientli xususiyat (ya'ni bir xil ob'ektlar egalik qiladi) mavjudligini ta'kidlaydi. Agar faqat aniqlanadigan xususiyatlar mavjud deb hisoblansa, aksioma har birining ma'nosini anglatadi ma'lum bir turdagi impredikativ ta'rif ekvivalent predikativ ta'rifga ega (Kleene 1952: 44-45).

Reduksiya aksiomasi va "matritsa" tushunchasi

Ammo keng tarqalgan nazariya qoidalari (og'irlik uchun) Kvinni keltirishi uchun "og'ir" bo'lganligi sababli, Rassel o'zining 1908 y. Matematik mantiq turlar nazariyasiga asoslanib[6] shuningdek, uning taklifini taklif qiladi kamaytirilishi aksiomasi. 1910 yilga kelib Uaytxed va Rassel Matematikaning printsipi a tushunchasi bilan ushbu aksiomani yanada kuchaytiradi matritsa - funktsiyani to'liq kengaytiradigan spetsifikatsiyasi. Uning matritsasidan funktsiyani "umumlashtirish" jarayoni va aksincha olish mumkin edi, ya'ni ikki jarayon orqaga qaytariladi - (i) matritsadan funktsiyaga (ko'rinadigan o'zgaruvchilardan foydalangan holda) umumlashtirish va (ii) ning teskari jarayoni qiymatlarni kurslar bo'yicha turni kamaytirish, ko'rinadigan o'zgaruvchiga argumentlarni almashtirish. Ushbu usul bilan impedikativlikni oldini olish mumkin edi.[7]

Haqiqat jadvallari

1921 yilda, Emil Post ko'rinadigan va haqiqiy o'zgaruvchilar tushunchasini almashtiradigan "haqiqat funktsiyalari" va ularning haqiqat jadvallari nazariyasini ishlab chiqadi. 1921 yildan boshlab uning "Kirish so'zi": "Holbuki, to'liq nazariya [Uaytxed va Rassel (1910, 1912, 1913)] o'z fikrlarini bayon qilishni talab qiladi, bu ikkala shaxsni va taklif funktsiyalari har xil turdagi va natijada turlarning noqulay nazariyasini taqozo etadigan ushbu subtheory faqat haqiqiy o'zgaruvchilardan foydalanadi va bu haqiqiy o'zgaruvchilar mualliflar elementar takliflar deb tanlagan bir xil mavjudotni anglatadi ".[8]

Taxminan bir vaqtning o'zida Lyudvig Vitgenstayn 1922 yilgi ishida shunga o'xshash g'oyalarni ishlab chiqdi Traktatus Logico-Philosophicus:

3.331 Ushbu kuzatuvdan biz Rasselning "Turlar nazariyasi" haqida ko'proq fikr yuritamiz. Rassellning xatosi, uning ramziy qoidalarini tuzishda uning belgilarining ma'nosi haqida gapirishi kerakligi bilan namoyon bo'ladi.

3.332 Hech qanday taklif o'zi haqida hech narsa deya olmaydi, chunki propozitsion belgining o'zida bo'lishi mumkin emas (bu butun "turlar nazariyasi").

3.333 Funktsiya o'z argumenti bo'lolmaydi, chunki funktsional belgi allaqachon o'zining argumentining prototipini o'z ichiga oladi va u o'z ichiga olmaydi ...

Vitgenstayn haqiqat jadvali usulini ham taklif qildi. 4.3-dan 5.101-ga qadar Vitgenstayn cheksiz qabul qiladi Sheffer zarbasi uning asosiy mantiqiy birligi sifatida va keyinchalik ikkita o'zgaruvchining barcha 16 funktsiyasini ro'yxatlaydi (5.101).

Matritsa-haqiqat jadvali tushunchasi 1940-1950 yillarda Tarski asarlarida paydo bo'lgan, masalan. uning 1946 indekslari "Matritsa, qarang: Haqiqat jadvali"[9]

Rassellning shubhalari

Rassell 1920 yilda Matematik falsafaga kirish butun bir bobni "Cheksizlik aksiomasi va mantiqiy turlar" ga bag'ishlaydi, unda u o'z tashvishlarini quyidagicha bayon qiladi: "Endi turlar nazariyasi qat'iyan bizning mavzuimizning tugallangan va ma'lum qismiga tegishli emas: bu nazariyaning aksariyati hanuzgacha maxfiy, chalkash, va tushunarsizdir, ammo zarurat biroz turlar haqidagi ta'limot, ta'limotning aniq shaklidan kamroq shubhali; va cheksizlik aksiomasi bilan bog'liq holda, ba'zi bir bunday ta'limotning zarurligini anglash oson ".[10]

Rassel reduktivlik aksiomasidan voz kechadi: Ning ikkinchi nashrida Matematikaning printsipi (1927) u Vitgensteinning argumentini tan oladi.[11] Kirishning boshida u "hech qanday shubha bo'lishi mumkin emas ... haqiqiy va ko'rinadigan o'zgaruvchilarni ajratishga hojat yo'q ..." deb e'lon qildi.[12] Endi u matritsa tushunchasini to'liq qabul qiladi va "A" ni e'lon qiladi funktsiya matritsada faqat uning qiymatlari orqali paydo bo'lishi mumkin"(ammo izohda demur:" Bu qisqartirish aksiomasining o'rnini egallaydi (etarli darajada emas) "[13]). Bundan tashqari, u yangi (qisqartirilgan, umumlashtirilgan) "matritsa" tushunchasini kiritadi, ya'ni "mantiqiy matritsa ... hech qanday konstantani o'z ichiga olmaydi. Shunday qilib p|q mantiqiy matritsa ".[14] Shunday qilib, Rassel deyarli qisqartirish aksiomasidan voz kechdi,[15] ammo so'nggi xatboshilarida u "bizning hozirgi ibtidoiy takliflarimizdan" u "Dedekindiya munosabatlari va yaxshi tartibli munosabatlar" ni keltirib chiqara olmasligini ta'kidlaydi va agar kamaytirilish aksiomasining o'rnini bosadigan yangi aksioma bo'lsa, "uni topish kerak".[16]

Oddiy turlar nazariyasi

1920-yillarda, Leon Chvistek[17] va Frank P. Ramsey[18] agar kimdir voz kechishga tayyor bo'lsa, buni payqadi ayanchli doira printsipi, "turlarning kengaytirilgan nazariyasi" dagi turlar darajalarining iyerarxiyasi qulashi mumkin.

Natijada cheklangan mantiq oddiy turlar nazariyasi deb ataladi[19] yoki, ehtimol, odatda, oddiy turdagi nazariya.[20] Oddiy tip nazariyasining batafsil formulalari 1920-yillarning oxiri va 30-yillarning boshlarida R. Karnap, F. Ramsey, V.V.O. Kvin va A. Tarski. 1940 yilda Alonzo cherkovi (qayta) uni quyidagicha shakllantirgan oddiygina terilgan lambda hisobi.[21] va 1944 yilda Gödel tomonidan ko'rib chiqilgan. Ushbu o'zgarishlar haqidagi tadqiqot Kollinzda (2012) topilgan.[22]

1940 yillar - hozirgi kunga qadar

Gödel 1944 yil

Kurt Gödel uning 1944 yilda Rassellning matematik mantiqi izohda "oddiy turlar nazariyasi" ga quyidagi ta'rifni berdi:

Oddiy turlar nazariyasi deganda men fikrlash ob'ektlari (yoki boshqa talqinda ramziy ifodalar) turlarga bo'linishini aytadigan ta'limotni nazarda tutayapman, ya'ni: shaxslar, shaxslarning xususiyatlari, shaxslar o'rtasidagi munosabatlar, bunday munosabatlarning xususiyatlari, va boshqalar (kengaytmalar uchun shunga o'xshash iyerarxiya bilan) va ushbu shakldagi jumlalar: " a mulkka ega φ ", " b munosabatlarni o'z ichiga oladi R ga v "va boshqalar ma'nosizdir, agar bo'lsa a, b, c, R, φ bir-biriga mos keladigan turlar emas. Aralashgan turlar (masalan, shaxslarni o'z ichiga olgan sinflar va elementlar sifatida sinflar) va shuning uchun transfinit turlar (masalan, cheklangan turdagi barcha sinflarning klassi) chiqarib tashlanadi. Oddiy turlar nazariyasi, shuningdek, epistemologik paradokslardan saqlanish uchun etarli ekanligi, ularni chuqurroq tahlil qilish orqali ko'rsatiladi. (Qarang Ramsey 1926 va Tarski 1935 yil, p. 399). "Deb nomlangan.[23]

U (1) sodda turlar nazariyasini va (2) aksiomatik to'plamlar nazariyasini "zamonaviy matematikaning kelib chiqishiga yo'l qo'ying va shu bilan birga barcha ma'lum bo'lgan paradokslardan saqlaning" degan xulosaga keldi (Gödel 1944: 126); bundan tashqari, oddiy turlar nazariyasi "birinchi tizimdir Printsipiya [Matematikaning printsipi] tegishli talqinda. . . . [M] har qanday alomatlar juda aniq ko'rsatib turibdi, ammo ibtidoiy tushunchalar yanada tushuntirishga muhtoj "(Gödel 1944: 126).

Kori-Xovard yozishmalari, 1934–1969

The Kori-Xovard yozishmalari dasturlar va formulalar kabi dalillarni talqin qilishdir. 1934 yilda boshlangan g'oya Xaskell Kori va 1969 yilda yakunlangan Uilyam Alvin Xovard. U ko'plab turdagi nazariyalarning "hisoblash komponenti" ni mantiqdagi hosilalar bilan bog'ladi.

Xovard yozgan lambda hisob-kitobi intuitivlikka mos kelishini ko'rsatdi tabiiy chegirma (ya'ni tabiiy chegirma O'rtacha chiqarib tashlangan qonun ). Turlar va mantiq o'rtasidagi bog'liqlik, mavjud mantiq uchun yangi tip nazariyalarni va mavjud tur nazariyalar uchun yangi mantiqlarni topish uchun keyingi izlanishlarga olib keladi.

de Bryuynning AVTOMATI, 1967–2003

Nikolaas Gvert de Bryuyn tip nazariyasini yaratdi Avtomatika dalillarning to'g'riligini tekshiradigan Automath tizimi uchun matematik asos sifatida. Tizim vaqt o'tishi bilan turlar nazariyasi rivojlanib borishi bilan xususiyatlarni ishlab chiqdi va qo'shdi.

Martin-Lyofning intuitivistik tip nazariyasi, 1971–1984

Martin-Lofga mos keladigan tip nazariyasini topdi mantiq tanishtirish orqali qaram turlar deb nomlandi intuitivistik tip nazariyasi yoki Martin-Lyof turi nazariyasi.

Martin-Lof nazariyasi tabiiy sonlar kabi cheksiz ma'lumotlar tuzilishini ifodalash uchun induktiv turlardan foydalanadi.

Barendregtning lambda kubigi, 1991 yil

The lambda kubi yangi tip nazariyasi emas, balki mavjud tur nazariyalarining turkumlanishi edi. Kubning sakkizta burchagi ba'zi mavjud nazariyalarni o'z ichiga olgan oddiygina terilgan lambda hisobi eng past burchakda va qurilishlarning hisob-kitobi eng yuqori qismida.

Adabiyotlar

  1. ^ Rassellning (1902) Fregega xat van Heijenoort 1967: 124-125 da sharh bilan paydo bo'ladi.
  2. ^ Frege (1902) Rasselga xat van Heijenoort 1967 yilda sharh bilan paydo bo'lgan: 126–128.
  3. ^ qarz Kvinning Rasseldan oldingi sharhi (1908) Matematik mantiq turlar nazariyasiga asoslanib van Heijenoortda 1967: 150
  4. ^ qarz tomonidan izoh V. V. O. Quine Rasselldan oldin (1908) Matematik mantiq turlar nazariyasiga asoslanib van Xiyenortda 1967 yilda: 150-153
  5. ^ a b Kvinning Rasseldan oldingi sharhi (1908) Matematik mantiq turlari nazariyasiga asoslanib van Heijenoortda 1967: 151
  6. ^ Rassel (1908) Matematik mantiq turlar nazariyasiga asoslanib van Heijenoort 1967 yilda: 153-182
  7. ^ qarz xususan p. 51 II bobda Mantiqiy turlar nazariyasi va * 12 Turlar iyerarxiyasi va qisqartirilish aksiomasi 162–167 betlar. Uaytxed va Rassel (1910-1913, 1927 yil 2-nashr) Matematikaning printsipi
  8. ^ Xabar (1921) Elementar takliflarning umumiy nazariyasiga kirish van Heijenoort 1967 yilda: 264-283
  9. ^ Tarski 1946 yil, Mantiq va deduktiv fanlari metodologiyasiga kirish, Dover respublikasi 1995 yil
  10. ^ Rassell 1920: 135
  11. ^ qarz "Kirish" 2-nashrga, Rassell 1927: xiv va Qo'shimcha S
  12. ^ qarz "Kirish" 2-nashrga, Rassell 1927: i
  13. ^ qarz "Kirish" 2-nashrga, Rassell 1927: xxix
  14. ^ "|" Vertikal chiziq - Sheffer zarbasi; qarz "Kirish" 2-nashrga, Rassell 1927: xxxi
  15. ^ "Sinflar nazariyasi bir yo'nalishda soddalashtirilgan va boshqa yo'nalishda funktsiyalar faqat ularning qiymatlari orqali va kamaytirilish aksiomasidan voz kechish orqali yuzaga keladi degan taxmin bilan murakkablashadi"; qarz "Kirish" 2-nashrga, Rassell 1927: xxxix
  16. ^ "Kirish" dan ikkinchi nashrga ushbu tirnoqlar, Rassell 1927: xliv – xlv.
  17. ^ L. Chvistek, Antynomje logikiformalnej, Przeglad Filozoficzny 24 (1921) 164–171
  18. ^ F. P. Ramsey, matematikaning asoslari, London Matematik Jamiyati materiallari, 2-seriya 25 (1926) 338-384.
  19. ^ Gödel 1944, 126 va 136-138-betlar, 17-izoh: "Rasselning matematik mantig'i" Kurt Gödel: To'plangan asarlar: II jild nashrlari 1938–1974, Oksford universiteti matbuoti, Nyu-York, NY, ISBN  978-0-19-514721-6(v.2.pbk).
  20. ^ Bu nazariya "sodda" degani emas, demak nazariya shunday deganidir cheklangan: turli xil buyurtmalar turlarini aralashtirishga yo'l qo'yilmaydi: "Aralashgan turlar (masalan, individual elementlarni o'z ichiga olgan sinflar va sinflar kabi elementlar) va shuning uchun transfinit turlar (masalan, cheklangan turdagi barcha sinflarning klassi) chiqarib tashlangan." Gödel 1944, 127-betlar, 17-izoh: "Rasselning matematik mantig'i" paydo bo'lgan Kurt Gödel: To'plangan asarlar: II jild nashrlari 1938–1974, Oksford universiteti matbuoti, Nyu-York, NY, ISBN  978-0-19-514721-6(v.2.pbk).
  21. ^ A. Cherch, turlarning oddiy nazariyasining formulasi, Symbolic Logic 5 jurnali (1940) 56-68.
  22. ^ J. Kollinz, Turlar nazariyasi tarixi: "Principia Mathematica" ning ikkinchi nashridan keyingi o'zgarishlar. LAP Lambert akademik nashriyoti (2012). ISBN  978-3-8473-2963-3, esp. chs. 4-6.
  23. ^ Gödel 1944: 126 izoh 17: "Rassellning matematik mantig'i" paydo bo'ldi Kurt Gödel: To'plangan asarlar: II jild nashrlari 1938–1974, Oksford universiteti matbuoti, Nyu-York, NY, ISBN  978-0-19-514721-6(v.2.pbk).

Manbalar

  • Bertran Rassel (1903), Matematika asoslari: jild. 1, University Press-da Kembrij, Kembrij, Buyuk Britaniya.
  • Bertran Rassel (1920), Matematik falsafaga kirish (ikkinchi nashr), Dover Publishing Inc., Nyu-York, NY, ISBN  0-486-27724-0 (xususan, XIII va XVII boblar).
  • Alfred Tarski (1946), Mantiq va deduktiv fanlari metodologiyasiga kirish, 1995 yilda Dover Publications, Inc tomonidan qayta nashr etilgan, Nyu-York, NY ISBN  0-486-28462-X
  • Jan van Heijenoort (1967, 3-nashr 1976), Frejdan Godelgacha: Matematik mantiqdagi manba kitob, 1879–1931, Garvard universiteti matbuoti, Kembrij, MA, ISBN  0-674-32449-8 (Pbk)
    • Bertran Rassel (1902), Fregega xat van Heijenoort tomonidan yozilgan sharh bilan, 124-125 betlar. Bu erda Rassel Frege asarida "paradoks" kashf etganligini e'lon qiladi.
    • Gottlob Frege (1902), Rasselga xat van Heijenoort tomonidan yozilgan sharh bilan, 126–128 betlar.
    • Bertran Rassel (1908), Matematik mantiq turlar nazariyasiga asoslanib, tomonidan sharh bilan Willard Quine, 150–182 betlar.
    • Emil Post (1921), Elementar takliflarning umumiy nazariyasiga kirish, van Heijenoort tomonidan sharh bilan, 264-283 betlar.
  • Alfred Nort Uaytxed va Bertran Rassel (1910–1913, 1927 yil 2-nashr 1962 yilda qayta nashr etilgan), Mathematica printsipi * 56 gacha, University Press-dagi Kembrij, London Buyuk Britaniya, ISBN yoki AQSh kartalarining katalog raqami yo'q.
  • Lyudvig Vitgenstayn (2009 yilda qayta nashr etilgan), Asosiy asarlar: Tanlangan falsafiy asarlar, HarperCollins, Nyu-York. ISBN  978-0-06-155024-9. Vitgenshteyn (1921 yil ingliz tilida), Traktatus Logico-Philosophicus, 1-82 betlar.

Qo'shimcha o'qish

  • V. Farmer, "Oddiy tip nazariyasining ettita fazilati", Amaliy mantiq jurnali, Jild 6, № 3. (2008 yil sentyabr), 267-286-betlar.