Amir Hossein Akbar Tabatabai
Utrecht University
In 1933, Gödel introduced a provability interpretation for intuitionistic propositional logic, \(\mathbf{IPC}\), to establish a formalization for the BHK interpretation, reading intuitionistic constructions as the usual classical proofs [1]. However, instead of using any concrete notion of a proof, he used the modal system \(\mathbf{S4}\), as a formalization for the intuitive concept of provability and then translated \(\mathbf{IPC}\) into \(\mathbf{S4}\) in a sound and complete manner. His work then suggested the problem to find the missing concrete provability interpretation of the modal logic \(\mathbf{S4}\) to complete his formalization of the BHK interpretation via classical proofs.
In this talk, we will develop a framework for such provability interpretations. We will first generalize Solovay's seminal provability interpretation of the modal logic \(\mathbf{GL}\) to capture other modal logics such as \(\mathbf{K4}\), \(\mathbf{KD4}\) and \(\mathbf{S4}\). The main idea is introducing a hierarchy of arithmetical theories to represent the informal hierarchy of meta-theories of the discourse and then interpreting the nested modalities in the language as the provability predicates of the different layers of this hierarchy. Later, we will combine this provability interpretation with Gödel's translation to propose a classical formalization for the BHK interpretation. The formalization suggests that the BHK interpretation is nothing but a plural name for different provability interpretations for different propositional logics based on different ontological commitments that we believe in. They include intuitionistic logic, minimal logic and Visser-Ruitenburg's basic logic. Finally, as a negative result, we will first show that there is no provability interpretation for any extension of the logic \(\mathbf{KD45}\), and as expected, there is no BHK interpretation for the classical propositional logic.
[1] K. Gödel, Eine Interpretation des Intuitionistichen Aussagenkalküls, Ergebnisse Math Colloq., vol. 4 (1933), pp. 39-40.
محمّدصالح زارع‌پور
دانشگاه لودویگ ماکسیمیلیان مونیخ
در سنت اسلامی راه‌حل‌های متفاوتی برای پارادوکس دروغگو ارائه شده است. بر اساس برخی از این راه‌حل‌ها جمله‌های دروغگو بدون هیچ تناقضی کاذب هستند و هر استدلالی که صدق و کذب توأمان این جمله‌ها را نتیجه دهد مغالطه‌آمیز است. در سنت اسلامی، بیشتر کسانی که از چنین راه‌حل‌هایی دفاع کرده‌اند، از راه‌حل اثیر الدین ابهری (597-663 ه.ق) الهام گرفته‌اند. در این سخنرانی راه‌حل ابهری را معرفی و بررسی می‌کنم و نشان می‌دهم که این راه‌حل به‌طور ضمنی متکی بر دیدگاهی به‌خصوص درباره‌ی شرایط صدق گزاره‌ها است؛ دیدگاهی که خود ابهری به صراحت آن را ذکر نکرده است اما در آثار برخی فیلسوفان بعد از او مورد بررسی و دفاع قرار گرفته است.
سید نصراللّه موسویان
پژوهشگاه دانش‌های بنیادی
توضیح و تفسیر دیدگاه ابن‌سینا در باب «معنی» به مسائل مناقشه‌برانگیزی در تاریخ منطق و فلسفه می‌انجامد. در این سخنرانی سعی خواهم کرد دیدگاه ابن‌سینا درباب «معنی» را از منظری «معناشناسانه» مورد بررسی قرار دهم و نشان دهم «معانی»، نزد ابن‌سینا، با ویژگی‌های «معناشناسانه»، در زبان ما، معرفی می‌شوند. اول، پس از معرفی کوتاه یکی از مناقشات مهم در این زمینه، به بررسی بعضی کاربردهای فنی «معنی» در متون منطقی ابن‌سینا می‌پردازم و سعی می‌کنم رابطه آن را با اصطلاحات کلیدی دیگری، نظیر «دلالت»، «ترکیب» و «تعریف» وارسی کنم. سپس، به اختصار، «معانی» را در ظرف و زمینه معرفت‌شناسی ابن‌سینا مطالعه می‌کنم. در مرحله سوم، تلاش می‌کنم تا نشان دهم چگونه دیدگاه «معناشناسانه»ای که معرفی کرده‌ام می‌تواند درک منسجم‌تری از فلسفه و منطق ابن‌سینا فراهم آورد و راه متفاوتی برای پیوند دادن مطالعات تاریخ منطق و منطق‌های جدید بگشاید.
Stefan Hetzl
Vienna University of Technology
A formula equation is a formula in first-order logic with unknowns representing predicates. Solving a formula equation consists of finding first-order instances of these unknowns that result in a valid formula. In the first part of this talk I will give a general overview of formula equations, linking them, in particular, to applications in automated theorem proving. In the second part I will present joint work with Sebastian Zivota showing that solvability of affine formula equations is decidable, thus generalising previous results about loop invariant generation.