نظریه انواع شهودگرایانه

مقدمه

نظریه انواع شهودگرایانه¹، همون طور که از اسمش پیداست، یک سیستم نوع‌دهی² بر اساس منطق شهودی‌ئه. منطق کمونیستی شهودی³ خیلی خلاصه، با برهان خلف مخالفه و کلا می‌گه «باید مثال نقضت رو بسازی تا مخالفتت رو به حساب بیارم و الا برو پی زندگیت😁». به عبارت دیگه، برهان رو ساختاری می‌خواد و سور وجودی رو جدی می‌گیره؛ وقتی شما می‌گید «وجود دارد فلان چیز که...» یه شهودگرا حتما ازتون می‌پرسه «کجا و با چه ماهیتی وجود داره؟» (خودم معتقدم که «به شما چه مربوط، وقتی می‌گم هست یعنی هست. فضول‌های انقلابی😂»)

نوع‌دهی با اغماض زیاد، فرایندی هست شبیه تعریف کردن نوع برای متغیرها در برنامه‌نویسی، مثل
int a = 3

این مورد رو صرفا برای پیدا کردن شهود گفتم و الا داستان یه چیزی فراتر از اینه (نوع‌ها یه جوری وجود «برهان ساختاری» برای یک گزاره رو تضمین می‌کنن) که جلوتر بهش می‌رسیم.

این سلسله نوشتار تا جای ممکن به صورت خلاصه، حول شهودگرایی، ریشه‌هاش، مدل محاسباتی ساخته‌شده بر پایه‌ش و در نهایت، نظریه انواع شهودگرایانه می‌‌گرده.

پانوشت:
¹ Intuitionistic Type Theory
² Typing
³ Intuitionistic logic

منابع:
• Logic and Structure, D. van Dalen
• Lectures on Curry-Howard Isomorphism, M. H. Sørensen and P. Urzyczyn
• On Brouwer, M. van Atten
• Per-Martin Löf:
- On the Meanings of Logical Constants and the Justifications of the Logical Laws
- Intuitionistic Type Theory

@simplytypedexistence

یه قضیه مهم در آنالیز تابعی
Invariant subspace problem
هست.
منتها این قضیه یه داستان تاریخی داره.
برنشتاین–رابینسون در دهه ۱۹۶۰ در آنالیز غیر استاندارد اون رو اثبات کردند، در همون شماره مجله ای که این قضیه اثبات می شه اثبات هالموس هم از این قضیه ارائه می شه، منتها اثبات با روش های آنالیز کلاسیک بازنویسی می شه.
خیلی ساده بخوایم بگیم در آنالیز غیر استاندارد مفهوم حد رو می ذارند کنار و از اعداد بی نهایت کوچک و بزرگ استفاده می کنند.
بعضی ها می گند این تصمیم شاید تا حدی به خاطر نگاهی بوده که به آنالیز غیر استاندارد وجود داشته(چاپ اثبات آنالیز غیر استاندارد و بعد کلاسیک‌سازی فوری اون، نوعی بی‌اعتمادی یا احتیاط نسبت به NSA رو نشون می‌ده)
عکس هم هالموس هست در جوانی.

#دانستنی های_ به درد_نخور ۴۰
می دونستید که نماد سیگما رو اولین بار فوریه و درسال ۱۸۲۰ به کار برد؟
حرف سیگما به صورت بزرگ، با حدودش که در بالا و پایین نوشته می شه.

از بین اثبات هایی که برای واگرایی سری هارمونیک اومده و تعدادشون هم کم نیست، این یکی از جمع و جورترین ها است. از این خاصیت هم استفاده کرده:
e^x>1 + x
ظاهرا یه ریاضیدان به عنوان حل تمرین اون رو نوشته بوده.

اگر کورت گودل امروز استاد بود:
هر سیستم سازگار و قابل بازنمایی به‌صورت بازگشتی که توانایی بیان حساب ابتدایی را دارد، شامل گزاره‌های تصمیم ناپذیر است.
دانشجو: داداش، این توی امتحان میاد؟

گویند پل اردوش، ریاضی‌‌دان مشهور مجارستانی، یحتمل تحت تأثیر همکارش آلفرد رنیی که معتاد به قهوه بوده و می‌گفته «ریاضی‌دان ماشینی است که قهوه را به قضیه ریاضی تبدیل می‌کند»، عین چی قهوه می‌خورده. بعد از فوت مادرش دیده قهوه جواب نمی‌ده، رفته سراغ ریتالین و آمفتامین. وسط حال کردنش با سوپرمن بودن، رون گراهام (همکار دیگری) از سر رفاقت می‌گه «داش گلم پل، حالا که هر چی می‌گم آمفتامین نزن، گوش نمی‌دی، بیا شرط ببندیم حداقل یک ماه نخوری مغزت نترکه؛ اگر یک ماه دووم آوردی من بهت ۵۰۰ دلار می‌دم (حساب کنید دهه ۷۰ میلادی چه قدر پول بوده). اگر نه که خود خوشگلت باید سر کیسه رو شل کنی».

اردوش هم با ژست «حالا می‌بینی حسابت رو خالی می‌کنم» می‌ره برای برآورده کردن شرط.

و...

می‌بره! اما به قول خودش (خطاب به گراهام)، «یک ماه ریاضیات عقب می‌افته!»:

شرط ما نشون داد که من معتاد نیستم. ولی این یک ماه هیچ کاری نکردم! صبح از خواب پا می‌شدم عین منگ‌ها زل می‌زدم به کاغذ خالی! عین آدمای معمولی هیچ ایده‌ای نداشتم! تو ریاضیات رو یک ماه عقب انداختی!

بعدم برمی‌گرده به ریتالین و آمفتامین.

فقط اگر امروز زنده بود، بهش می‌گفتم اردوش جان، اینی که گفتی دقیقا سندرم ترک محرکه و شرمنده، شوما معتادی:))

پ.ن: اون زمان محرک تا حدی مثل نقل و نبات بوده و حتی بدون نسخه تجویز می‌شده، تا عوارضش اومد رو و باعث شد فقط به بیش‌فعال‌ها اونم با قسم آیه و هزارتا سند بدن:))

این مثل اینکه قبلا حل شده بود، در یک مقاله در سال ۱۹۸۱. به لحاظ حال گیری:
انسان 1 - هوش مصنوعی 0.

در یه کتاب فارسی خونده بودم به نقل از هایزنبرگ گفته بود: تنها ابزار ریاضی که در مکانیک کوانتوم نیاز دارم ماتریسه(جای دیگه پیدا نکردم، مطمئن نیستم در مورد این جمله)

یه مساله ای که در کتاب های ریاضی وجود داره(منظورم حتی کتاب های درست و حسابی و معتبر هست) اینه که خیلی سمت توضیح یا تفسیر شهودی نمی رند. انگار یه توافق نانوشته وجود داره که اصلا در موردش حرف نزنند. خیلی از کتاب های ریاضی توسط غول های ریاضی نوشته شده و قطعا اونا درک خیلی عمیقی از قضایا دارند و می دونند پشت پرده چه خبره! ولی دریغ از یک کلمه توضیح.
واقعا بخش های خیلی زیادی از ریاضی هست که پشت روابط به ظاهر خشک و دقیق ریاضی می شه توضیحات روان تر و شهودی تری برای درک عمیق تر و بهتر همون مفاهیم(ودر کنارشون) ارائه کرد، ولی این کار رو نمی کنند.
استادها سمتش نمی رند، نویسنده ها در موردش چیزی نمی نویسند، کسی مقاله ای در موردش نمی نویسه و...
خودم همیشه این خلا رو احساس کردم از همون اول که کمی جدی تر ریاضی خوندم، یه بار در دوره ارشد یه کمی جرات کردم و از استاد درس آنالیز حقیقی پرسیدم این تفسیر شهودی اش چی می شه؟ کلیت مساله رو فهمیدم و حتی جزئیات اثبات رو. اما شما شهودی اش رو بگید. استاد فرمودند:
نا نگردی آشنا زین پرده رازی نشنوی!
حالا نمی دونم خودشم نمی دونست یا چی؟

البته می دونم که هر کس باید با تلاش و سخت کوشی و تمرین زیاد و مطالعه عمیق و ... به درک از مفاهیم ریاضی برسه، ولی کلیت این ماجرا به نظرم کمی مشکوکه!

به یمن اینترنت و سایت های پرسش و پاسخ تا حدی این خلا جبران شده و الان هم تا حدی هوش مصنوعی کمک کننده است، ولی انتظارمون چیز دیگه ای بود.

طرف این رابطه رو دیده، نوشته:
واوووووو... پی خیلی عدد خاصیه!
اگر اون موقع که استاد داشت بسط مک لورن رو درس می داد حواست رو جمع می کردی، این طور اظهار نظر نمی کردی.
صد تا رابطه مثل این می شه نوشت.

باعث قهقه شاید نشه، ولی ریاضی دوست(دان) پسنده!
شوخی با ندانسته های بزرگ.

فرمال متد با اغماض زیاد، یکی از کاربردهای منطق تو علوم کامپیوتره. منطق ریاضی رو بشین از کتاب فان‌دالن یا دکتر اردشیر بخون ببین خوشت میاد یا نه. نظریه زبان‌ها و ماشین‌ها رو هم خوب یاد بگیر، بعدش فکر کن به بقیه‌ش.

بعد این که دانشگاه معمولی و دسته‌ی بیل. داری چیزی رو که دوست داری می‌خونی و همین برای ادامه کافیه.

من رشته‌م ریاضی نبوده، نمی‌تونم مسیر دقیقی بدم. ولی جبر و lattice theory توی کار من دید خوبی به آدم می‌ده.

خیلی مسیر رو تا ته نبین، الکی سنگ بزرگ برمی‌داری دل‌سرد می‌شی. ریاضی خواستی بخونی یه کم حساب دیفرانسیل و انتگرال بخون، بعدشم برو سراغ جبر مجرد و یه کم آنالیز ریاضی و نظریه اعداد ببین. وقتی شروع می‌کنی چیز یاد گرفتن، دیدت عوض می‌شه. دیگه آدم قبلی نیستی. بعدا می‌فهمی چیکار باید بکنی.

آقای
Ken Ono
که یه نامبر تئوریست درجه یک هم هست، تصمیم گرفته بعد از سال ها فعالیت در دانشگاه، قید دنیای آکادمیک رو بزنه و بره تو استارتاپی که شاگرد ۲۴ ساله اش راه انداخته کار کنه.
این خانم هم استارتاپش حسابی سروصدا کرده و مساله های معروف اردوش رو حل کرده.
استاد می گه نسبت به هوش مصنوعی نگاه مثبتی نداشته و فکر می کرده هیاهو باشه، بعد دیده قضیه جدیه. گفته اگر بخواد خیلی بروز باشه مجبوره بره سمت هوش مصنوعی. تصمیم گرفته راه جدیدی رو انتخاب کنه، راه متفاوتی برای انجام ریاضی.
این شرکت
لینک مربوط

آقای
Greg Egan
نویسنده ساینس فیکشن و ریاضیدان هستند.
در زمینه
Hard science fiction
می نویسند(در اینجا بیشتر جنبه های علمی و اصول منطقی، فنی و مهندسی در داستان مهم هست تا مسائل مربوط به خط روایی داستان و شخصیت پردازی و... چهره شاخص در این زمینه آرتور کلارک هست)
خود آقای Greg Egan بیشتر در زمینه ریاضیات و مکانیک کوانتوم می نویسه داستان هاش رو.
در ریاضی هم کارهایی کرده مثل
Egan conjecture
روحیات خاصی داره: در مجامع مربوط به کارش حضور نداره، کتاب هاش رو امضا نمی کنه و هیچ جا عکسی ازش نیست!
سوالاتی که در داستان هاش تکرار می شه:
من کیه؟ بدن من یا مغز من یا اطلاعات من؟
اگر یه کپی از من به وجود بیاد کدوم واقعی تره؟
توی یکی از داستان هاش یکی از شخصیت ها معتقد هست که جهان رو باید براساس یه سری axiom بازسازی کنیم.
به امید ترجمه آثارش، که تعدادشون کم هم نیست.
https://www.gregegan.net/

طرف شغلش چیه؟
mathematics book editor
توی Springer.
در دوره ای که همه می خواند دیتا ساینتیست و تحلیل گر فلان و... بشند، این به نظرم کار فوق العاده ای باید باشه(کارش پاره وقت و... نیست)

این کتاب هم کتاب خوبیه که بیانش البته مقدماتی هست و حتی به کار دبیرستانی ها هم میاد.
https://www.goodreads.com/list/show/163609.Best_of_Springer_Mathematics

آقای
Laurent Simons
هستند، متولد سال ۲۰۰۹.
در سن ۴ سالگی مدرسه رو شروع کرد، ۸ سالگی دیپلم گرفت، ۱۱ سالگی لیسانس، ۱۲ سالگی فوق لیسانس و در ۱۵ سالگی دکتری در فیزیک کوانتوم(تازه دفاع کرده)
معروفه به انیشتین کوچولو.
https://www.sciencealert.com/belgiums-little-einstein-earns-phd-in-quantum-physics-at-age-15

حقیقتا دلیل خنده رو متوجه نمی شم. چند دهه دکتر حسابی ها رو بهتون قالب کردند خنده تون نگرفت، به این می خندید؟

Évariste Galois (1811–1832)–
Age 20

Niels Henrik Abel (1802–1829)–
Age 26

Gotthold Eisenstein (1823–1852)– Age 29

Srinivasa Ramanujan (1887–1920)
–Age 32

William Clifford (1845–1879)– 
Age 33

Blaise Pascal (1623–1662)–
Age 39

Bernhard Riemann (1826 – 1866)– Age 39

Maryam Mirzakhani (1977–2017)–
Age 40

دوستان می گند جناب
Ken Ono
و نه Oho قبلا هم خبرساز شده‌.
از ریاضی و فیزیک کمک گرفتند تا عملکرد شناگرها رو بهبود بدند اونم در حد صدم ثانیه ها.
یه دانشجویی در ریاضی کاربردی و فیزیک داشته به اسم
Andrew Wilson
که عضو تیم شنای دانشگاه هم بوده، با هم کار مشترکی رو شروع می کنند و با تیم شنای زنان آمریکا همکاری می کنند.
ریاضی(به طور خاص جبر خطی)، فیزیک(به طور خاص فیزیک کلاسیک و قوانین نیوتن) و تحلیل روی داده ها کمک کرد تا چند تا شناگر بتونند رکوردها رو جابه جا کنند.
حتی توی جزئیات حرکات شناگرها هم نظر می دند براساس تحلیل ها، بعد از شیرجه چی کار کنی؟ کی نفس بگیری؟ دستات رو چطور بچرخونی؟ زاویه بدنت چی باشه؟ در فلان نقطه مسیر چه حرکتی بکنی و چیزهای دیگه.
در واقع این روش بهینه اشتباهاتی که حتی توسط دوربین ها ثبت نمی شه و غیرقابل دیدن هست رو بهبود می ده.
عکس بالا یعنی خانم
Kate Douglass
کسی بوده که بیشترین بهره رو از این روش برده.
https://www.quantamagazine.org/how-americas-fastest-swimmers-use-math-to-win-gold-20240710/