منطق اثبات‌پذیری گودل–لوب (GL) منطقی موجهاتی است که از یک سو نسبت به قاب‌های کریپکی متعدیِ معکوس‌خوش‌بنیاد کامل است و از سوی دیگر، بنا بر قضیهٔ سولووی، دقیقاً اصولی را دربارهٔ اثبات‌پذیری در PA به دست می‌دهد که خودِ PA آن‌ها را ثابت می‌کند. در این سخنرانی به این پرسش می‌پردازیم که همتای نامتناهیِ GL چیست، یعنی وقتی زبان موجهاتی را با عطف و فصل‌های شمارای نامتناهی غنی کنیم. نشان می‌دهیم که برخلاف حالت متناهی، حساب‌های رشته‌ای معمول در این‌جا کارساز نیستند و به‌جای آن یک حساب رشته‌ایِ تودرتو با اثبات‌های ناخوش‌بنیاد معرفی می‌کنیم که در آن هر شاخهٔ نامتناهیِ اثبات باید شامل بی‌نهایت کاربرد تودرتو از قاعدهٔ ☐ باشد. نتیجهٔ اصلی این است که این حساب نسبت به مدل‌های کریپکیِ متعدیِ معکوس‌خوش‌بنیاد صحیح و کامل است و قاعدهٔ برش در آن حذف‌پذیر است؛ در حالی که کامل‌بودنِ کریپکیِ دستگاه هیلبرتیِ متناظر همچنان پرسشی باز می‌ماند.

در نهایت اشاره‌ای به تعبیر اثبات‌پذیری در نظریه‌ی مجموعه‌های کریپکی-پلاتک KP خواهیم کرد: نشان می‌دهیم که منطق اثبات‌پذیری برای گسترش مناسبی از KP زیرمنطقی از حساب رشته‌ای معرفی شده است.

هدف از این کارگاه فراهم آوردن محیطی علمی و دوستانه برای یادگیری، پرسش، بحث و تبادل نظر دربارهٔ موضوعاتی در منطق ریاضی و نظریهٔ مدل است که معمولاً در یک درس معمول منطق ریاضی امکان پرداختن جامع و کافی به همهٔ آن‌ها پیش نمی‌آید. دامنهٔ موضوعی کارگاه متنوع است: ارتباط نظریهٔ مدل و دسته‌بندی گروه‌های متناهی، فیلترها، فراضرب‌ها، آنالیز نااستاندارد، فشردگی، مدل‌های نااستاندارد حساب و بازی‌های اِرِنفویشت-فِراسه، و همچنین موضوعاتی از منطق جهت (موجهات) از جمله شبیه‌سازی دوسویی از دیدگاه نظریهٔ بازی‌ها و کاربردهای منطق جهت در تأیید برنامه‌ها.

همهٔ سخنرانی‌ها برای دانشجویان کارشناسی مناسب و قابل دنبال کردن تنظیم شده‌اند. آشنایی با منطق ریاضی و مباحثی از منطق جهت به دنبال کردن بهتر مباحث کمک می‌کند.

این کارگاه بر پیوند میان پژوهش‌های فلسفیِ معاصر دربارهٔ ریاضیاتِ تولیدشده به‌وسیلهٔ هوش مصنوعی و آثار متأخر ترنس تائو استوار است؛ آثاری که در آن‌ها تائو و فلاسفه عمل ریاضی، از خلال نوشته‌ها، سخنرانی‌ها و گفت‌وگوهای اخیر خود، نه‌تنها توانایی‌های فنی سامانه‌های هوش مصنوعی در تولید، صوری سازی و بررسی اثبات‌های ریاضی را تحلیل می‌کند، بلکه پرسش‌های بنیادی‌تری دربارهٔ هدف، ارزش و آیندهٔ فعالیت ریاضی مطرح می‌سازد. از این منظر، مقالات و مباحث این کارگاه به‌عنوان بسط، تفسیر و گفت‌وگویی انتقادی با دیدگاه‌های متأخر تائو خوانده می‌شوند: از تمایز میان درستی صوری و فهم ریاضی، و از نگرانی دربارهٔ انباشت «بدهی فنی» ناشی از تولید انبوه نتایج، تا بررسی دشواری ذاتی مسائل ریاضی، نقش توضیح و شهود، و ضرورت بازاندیشی در نهادهای علمی و معیارهای ارزیابی ریاضیات. بنابراین، هدف کارگاه شکل‌دادن به بحثی منسجم پیرامون تصویری است که در آثار متأخر پژوهشگران این حوزه، از گذار ریاضیات به عصر هوش مصنوعی ارائه می‌دهند؛ تصویری که در آن مسئلهٔ اصلی دیگر فقط این نیست که آیا ماشین می‌تواند قضیه‌ای را اثبات کند، بلکه این است که جامعهٔ ریاضی چگونه می‌تواند نتایج ماشینی را بفهمد، ارزش‌گذاری کند، در ساختار دانش جای دهد و همچنان نقش فهم انسانی را در پیشرفت ریاضیات حفظ کند.

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