مجتبی مجتهدی،  دانشکده ی ریاضی، آمار و علوم کامپیوتر، پردیس علوم، دانشگاه تهران

برای عملگر وجهی در منطق موجهات، تعابیر گوناگونی در نظر گرفته می شود. ضرورت ، باور، زمان و اثبات پذیری و...به معنای دقیق تر ، \(\Box A\)   به این صورت تعبیر می شود : ضرورتا \(A\) درست است، شخص الف \(A\) را می داند ، شخص الف به \(A\) باور دارد، \(A\) در همه زمان های آینده برقرار است و \(A\) قابل اثبات است و....ازبین تمامی این تعابیر، تنها اثبات پذیری در یک دستگاه مشخص ریاضی است که به زبان دقیق تر و غیر مبهم بیان شده است.

به طور مشخص، اولین بار منطق اثبات پذیری در سال 1933 توسط Kurt Godel در پی یافتن یک تعبیر کلاسیک برای منطق شهود گرایی \({\sf IPC}\) معرفی شد.هم چنین پس از اثبات قضایای ناتمامیت (1931) این مساله طبیعی مطرح شد «آیا می توان در منطق موجهات گزاره ای ، مفهوم اثبات پذیری در ریاضیات کلاسیک را به نحو صحیح و کاملی استخراج کرد؟» پس از تلاشهای بسیار، نهایتا Robert Solovay در سال 1976 توانست نشان دهد که نظریه  \({\sf GL}:={\sf K4}+\Box(\Box A\to A)\to\Box A\)  به خوبی مفهوم اثبات پذیری در ریاضیات کلاسیک را استخراج می کند.

در ادامه کارهای وی   مسائل زیادی در حوزه منطق اثبات پذیری مطرح شده کا غالبا همان مساله مشابه برای ریاضات ضعیف تر (کلاسیک و غیرکلاسیک) است. دراین بین مساله یافتن منطق موجهاتی که مفهوم اثبات پذیری در حساب ساختی    \({\sf HA}\)  را استخراج کند مساله است که مورد توجه ماست .این مساله از سال 1981 توسط   Albert Visser مطرح شده است . هرچند که نخسین نتایج در این قلمرو به کارهای  John Myhill   (1973 ) Harvay Friedman   (1973)  Danil Leivant  (1975) بر می گردد. 

مکان: تهران ، خیابان ولی عصر ، خیابان نوفل لوشاتو ، خیابان آراکلیان ، شمارة 4

 موسسه‌ی پژوهشى حکمت و فلسفه ایران

زمان: چهارشنبه، 27 آبان 1394 ، ساعت 4:30 بعد از ظهر

با همکاري موسسة پژوهشى حكمت و فلسفه ايران