بسط پایستار تئوری، برهانِ ساختی (سازنده) و منطق شهودی
منطق محمولات و نظریه مدل
درآمد به منطق و رایانش
منطق
محمولات: بسط پایستار تئوری، برهانِ ساختی (سازنده) و منطق شهودی
۱- مقدمه | ۷- بی‌نیازی به حرف تابعی و ثابت انفرادی در تئوری‌های با تساوی |
۲- ۲.۹ تعریف حروف تابعی و ثابت‌های انفرادی جدید | ۸- مثال برای حذف حروف تابعی |
۳- قضیه (۲.۲۸). بسط پایستار (Conservative) تئوری | ۹- برهان ساختی و برهان غیرساختی |
۴- تمرین (۲.۸۳ - ۲.۸۳) | ۱۰- براوئر (L.E.J. Brouwer - 1881 - 1966) و منطق شهودی |
۵- تبدیل آزاد-`(f_1, ..., f_m)` | ۱۱- وصف معین |
۶- مثال از نظریه‌های گروه و میدان |
مگر در مواردی که با نماد "" مشخص شده باشد، محتوای ارائه شده در این یادداشت از مرجع زیر برگرفته و برگردان شده است.
Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015. p. 103-105.
۱- مراد از مجموعه شمارا (Denumerable Set) یک مجموعه مدل نرمال شمارای نامتناهی است مگر آنکه با صراحت قید شده باشد.
■ مقدمه
این قسمت در ادامه قسمت قبل (منطق محمولات: تساوی، وجود یکتا، وصف معین و انقباض مدل) بر توانایی دستگاه‌های صوری در حذف حروف تابعی / ثابت‌های انفرادی در تئوری‌های با تساوی (برای مثال: نظریه‌های گروه/میدان) بدون از دست دادن توان گویایی تأکید دارد. همچنین منطق کلاسیک را با شهودگرایی براوئر (L.E.J. Brouwer) مقایسه می‌کند، که در آن اصل طرد شق وسط پذیرفته نیست و برهان‌های ساختی در اولویت قرار دارند.*
* در بخش‌هایی از منطق شهودی در این قسمت، از AI برای بازبینی تا حد امکان به منظور وضوح و انسجام مفهومی استفاده شده است.
■ ۲.۹ تعریف حروف تابعی و ثابت‌های انفرادی جدید
در ریاضیات، هنگامی که برای هر `y_1, ..., y_n`، وجود یک شی منحصر به فرد `u` را ثابت کردیم که دارای ویژگی `cc"B"(u, y_1, ..., y_n)` است، اغلب حرف تابعی جدید `f(y_1, ..., y_n)` را معرفی می‌کنیم به قسمی که `cc"B"(f(y_1, ..., y_n), y_1, ..., y_n)` برای همه `y_1, ..., y_n` برقرار باشد. در مواردی که ما وجود یک شی منحصر به فرد `u` را ثابت کرده‌ایم که فرمول `cc"B"(u)` را برمی‌آورد و `cc"B"(u)` شامل `u` به عنوان تنها متغیر آزاد آن است، آنگاه یک ثابت انفرادی جدید `b` را معرفی می‌کنیم طوری که `cc"B"(b)` برقرار باشد. به طور کلی پذیرفته است که چنین تعاریف، اگرچه راحت هستند، اما هیچ چیز واقعا جدیدی به این تئوری نمی‌افزایند. این را می‌توان به روش زیر دقیق کرد.
■ قضیه
(۲.۲۸).
بسط پایستار (Conservative)
تئوری
[
این قضیه تأکید می‌کند که چگونه دستگاه‌های صوری می‌توانند به طور پایستار نظریه‌ها را با نمادهای قابل تعریف گسترش دهند و در عین حال انسجام نحوی و معنایی را حفظ کنند.]
• `\text{K}` را یک نظریه با تساوی بگیرید.
• فرض کنید `⊢_K (∃_1u)cc"B"(u, y_1, ..., y_n)`.
• نیز `K^#` را یک تئوری با تساوی بگیرید که با افزودن یک حرف تابعی جدید `f` با `n` آرگومان به `\text{K}` و بنداشت سره *`cc"B"(f(y_1, . . ., y_n), y_1, . . ., y_n)`، و همچنین تمام موردهای بنداشت‌های (A۱) - (A۷) که شامل `f` می‌شود، بدست آمده است.
* بهتر است این بنداشت را به صورت `(AAu)(u=f(y_1,…,yn)=>``cc"B"(u,y_1,…,y_n))` بگیریم، چرا که `f(y_1,…,y_n)` ممکن است برای `u` در `cc"B"(u,y_1,…,y_n)` آزاد نباشد.
در این صورت، یک تبدیل کارآمد وجود دارد که هر فرمول `cc"C"` از `K^#` را به یک فرمول `cc"C"^#` می‌نگارد، به قسمی که:
-
اگر `f` در `cc"C"` روی ندهد آنگاه `cc"C"^#` همان `cc"C"` است.
-
`(¬cc"C")^#` عبارت از `¬(cc"C"^#)` است.
-
`(cc"C" ⇒ cc"D")^#` عبارت از `cc"C"^# ⇒ cc"D"^#` است.
-
`((AAx)cc"C")^#` عبارت از `(AAx)(cc"C"^#)` است.
-
`⊢_{K^#}(cc"C"lArr cc"C"^ #)`
-
اگر `⊢_{K^#}cc"C"^#` آنگاه `⊢_Kcc"C"`.
اثبات:
مراد ما از یک f -ترم ساده عبارت از `f(t_1, ..., t_n)` است که در آن `t_1, ..., t_n` ترم‌هایی هستند که حاوی `f` نیستند.
گیریم فرمول اتمی ` cc"C"` در `K^#` داده شده باشد. `cc"C"^***` را نتیجه جایگزینی سمت چپ‌ترین رویداد یک ترم ساده `f(t_1, ..., t_n)` در ` cc"C"` با اولین متغیری، بفرض `v`، که نه در `cc"C"` یا `cc"B"` باشد، بگیرید.
فرمول `(EEv)(cc"B"(v, t_1, ..., t_n) ∧ cc"C"^***)` ر f-تبدیل ( f-دگرسانگر) فرمول `cc"C"` بنامید.
اگر `cc"C"` حاوی `f` نیست، خود ` cc"C"` را `f`-تبدیل بگیرید.
واضح است که داریم:
`⊢_{K^#}(EEv)(cc"B"(v, t_1, ..., t_n) ∧ cc"C"^***)⇐cc"C"`.
(در اینجا، از `⊢_K(EE_1u)cc"B"(u, y_1, ..., y_n)` و بنداشت `cc"B"(f(y_1, ..., y_n), y_1, ..., y_n)` در `K^#` استفاده کرده‌ایم.)
از آنجا که `f`-تبدیل `cc"C"^′` از `cc"C"` شامل یک `f` کمتر از `cc"C"` و `⊢_{K^#}cc"C"′⇔cc"C"` است، اگر `f`-تبدیل‌های پی در پی را در نظر بگیریم ، در نهایت فرمول `cc"C"^#` را بدست می‌آوریم که حاوی `f` نیست و به این ترتیب `⊢_{K^#}cc"C"^#⇔cc"C"`.
`cc"C"^#` را تبدیل f-less فرمول `cc"C"` بنامید.
با برگردان `(¬cc"D")^#` به `¬(cc"D"^#)`، `(cc"D"⇒cc"E")^#` به `cc"D"^#⇒cc"E"^#`، و `((AAx)cc"D")^#` به `(AAx)cc"D"^#` تعریف را به همه فرمول‌های `K^#` گسترش دهید.
در این صورت ویژگی‌های (a)–(e) قضیه ۲.۲۸ آشکار هستند.
برای اثبات ویژگی (f)، کافی است با ویژگی (e) نشان دهیم اگر `cc"C"` حاوی `f` و `⊢_{K^#}cc"C"` نباشد، آنگاه `⊢_K C`.
می‌توان فرض کرد که `cc"C"` یک فرمول بسته است، زیرا یک فرمول و بستار آن از یکدیگر قابل دست آوردن هستند.
فرض کنید `\text{M}` مدلی از `\text{K}` باشد. نیز `\text{M}_1` را یک مدل نرمال بگیرید که با هم‌فشردن `\text{M}` به دست می‌آید. می‌دانیم (↝) که یک فرمول برای `\text{M}` درست است اگر و فقط اگر برای `\text{M}_1` درست باشد.
از آنجا که `|--_K(EE_1u)cc"B" (u, y_1, ..., y_n)`، بنابراین، برای هر `b_1, ..., b_n` در دامنه `\text{M}_1`، یک `c` یکتا در دامنه `\text{M}_1` وجود دارد به طوری که `|==_{\text{M}_1} cc"B" [ c, b_1 , , ... b_n ]`.
اگر `f_1(b_1, ..., b_n)` را به عنوان `c` تعریف کنیم، با در نظر گرفتن `f_1` به عنوان تعبیر حرف تابعی `f`، آنگاه از `text{M}_1` مدل `M^#` از `K^#` را بدست خواهیم آورد.
چون بنداشت‌های منطقی `\text{K}^#` (از جمله بنداشت‌های تساوی `\text{K}^#`) در هر تعیبر نرمال برقرار است، بنداشت `cc"B"(f(y_1, ..., y_n), y_1, ..., y_n)` نیز به موجب تعریف `f_1` در `\text{M}^#` برقرار است.
از آنجایی که سایر بنداشت‌های سره `\text{K}^#` حاوی `f` نیستند و نیز از آنجا که برای `\text{M}_1` درست هستند، برای `\text{M}^#` نیز درست هستند.
اما `|--_{K^#}cc"C"`. بنابراین، `cc"C"` برای `text{M}^#` درست است، اما از آنجا که `cc"C"` حاوی `f` نیست، `cc"C"` برای `text{M}_1` و از این رو برای `text{M}` نیز درست است.
بنابراین، `cc"C"` برای هر مدل `\text{K}` درست است. از اینجا، و نتیجه ۲.۲۰(a) ، داریم `|--_K cc"C"`.
(در حالتی که `|--_K (EE_1u)cc"B"(u)` و `cc"B"(u)` فقط شامل `u` به عنوان یک متغیر آزاد هستند، `K^#` را با اضافه کردن یک ثابت انفرادی جدید `b` و بنداشت `cc"B"(b)` تشکیل می‌دهیم. در این صورت به قیاس از همین قضیه (۲.۲۸) عملاً از برهانی که ارائه شد نتیجه گرفته می‌شود.)
■ تمرین (۲.۸۳ - ۲.۸۳)
۲.۸۳- تبدیل f-less فرمول‌های زیر را بیابید.
a. `(AAx)(EEy)` `(A_1^3(x,y, f(x, y_1,...., y_n))=>``f(y,x , ..., x)=x)`
b. `A_1^1(f(y_1, ..., y_{n-1}, f(y_1, ..., y_n))) ``^^ ``(exists x) A_1^2(x, f(y_1, ..., y_n))`
حل a:
`(forall x)(exists y)(exists z)``(cc"B"(z, x, y, ..., y) ^^ A_i^3(x, y, z)) =>`` (exists z)(cc"B"(z, y, x, ..., z) ^^ z = x)`
■ تبدیل آزاد-`(f_1, ..., f_m)`
توجه کنید که قضیه ۲.۲۸ زمانی نیز اعمال می‌شود که چندین نماد جدید `f_1, ..., f_m` را معرفی کرده باشیم چراکه می‌توان فرض کرد هر `f_i` را به تئوری‌ای که قبلا با افزودن `f_1, ..., f_{i−1}` به دست آمده است، اضافه کرده‌ایم. که در این صورت کاربردهای پی در پی قضیه ۲.۲۸ ضروری است.
فرمول `cc"C"^#` دست آمده از `\text{K}` را می‌توان به عنوان یک تبدیل آزاد-`(f_1, ..., f_m)` [free-`(f_1, ..., f_m)` transform] از `cc"C"` به زبان `\text{K}` در نظر گرفت.
■ مثال از نظریه‌های گروه و میدان
۱.
در تئوری مقدماتی گروه‌ها `\text{G}`، می‌توان `(EE_۱y)x + y = ۰` را ثابت کرد. سپس یک حرف تابعی جدید `f` یک آرگومانی `f(t)` را معرفی که با `(−t)` نمایانده شود، و به آن بنداشت جدید `x + (−x) = ۰` نیز اضافه شده باشد. بنا به قضیه ۲.۲۸، اکنون نمی‌توان هیچ فرمول `\text{G}` را که قبلاً نمی‌توانستیم اثبات کنیم، اکنون نیز اثبات کنیم. بنابراین، تعریف `(-t)` هیچ توان جدیدی به نظریه اصلی اضافه نمی‌افزاید.
۲.
در تئوری مقدماتی میدان `\text{F}`، می‌توان
`(EE_۱y)((x ≠ ۰ ^^ x * y = ۱) vv (x = ۰ ^^ y = ۰))`
را ثابت کرد. سپس یک حرف تابعی جدید `g` یک آرگومانی `g(t)` را معرفی که با `t^{−۱}` نمایانده شود، و به آن بنداشت
`(x != ۰ ^^ x * x^{−۱} = ۱) vv (x = ۰ ^^ x^{−۱} = ۰)`
نیز اضافه شده باشد. از این می‌توان `x ≠ ۰ => x * x^{−۱} = ۱` را ثابت کرد.
■ بی‌نیازی به حرف تابعی و ثابت انفرادی در تئوری‌های با تساوی
از صورت و اثبات قضیه ۲.۲۸ می‌توان دریافت که در تئوری‌های با تساوی، فقط به حروف محمولی نیاز است. حروف تابعی و ثابت‌های انفرادی قابل صرف نظر هستند.
اگر `f_j^n` یک حرف تابعی باشد، آنگاه اگر بنداشت `(EE_1u)A_k^{n+1}(x, y_1,...,y_n)` را بیافزاییم، می‌توانیم آن (`f_j^n`) را با حرف محمولی جدید `A_k^{n+1}` جایگزین کنیم.
یک ثابت انفرادی با یک حرف محمولی جدید `A_k^1` جایگزین خواهد شد اگر بنداشت `(EE_1u)A_1^k(u)` را نیز بیافزاییم.
نهاده وجودی در تئوری‌های مرتبه-اول را ببینید.
■ مثال برای حذف حروف تابعی
در تئوری مقدماتی گروه‌ها `\text{G}`، اگر بنداشت‌های `(AAx_1)(AAx_2)(EE_1 x_3)A_1^3(x_1,x_2,x_3)` و `(EE_1 x_1)A_1^1(x_1)` را بیافزاییم، و نیز بنداشت‌های (a) ،(b) ،(c) و (g) [در گروه‌ها] را با موردهایی که در زیر آمده‌اند جایگزین کنیم، آنگاه می‌توانیم `+` و `0` را با حرف‌های محمولی `A_1^3` و `A_1^1` جایگزین کنیم:
a'.
`A_1^3(x_2, x_3, w) ^^`` A_1^3(x_1, u, v) ^^`` A_1^3(x_1, x_2, w) ^^ A_1^3(w, x_3, y) => ``v = y`
b'.
`A_1^1(y) ^^ A_1^3(x, y, z) => z = x`
c'.
`(exists y)(forall w)(forall v)(A_1^1(w) ^^ ``A_1^3(x, y, v) => v = u)`
g'.
`[x_1 = x_2 ^^ A_1^3(x_1, y, z) ^^ ``A_1^3(x_2, y, u) ^^ A_1^3(y, x_1, v) ^^ A_1^3(y, x_2, w)] => ``z = u ^^ v = w`
توجه داشته باشید که اثبات قضیه ۲.۲۸ بسیار غیرساختی است، زیرا از مفاهیم معنایی (مدل، صدق) استفاده می‌کند و بر مبنای نتیجه ۲.۲۰(a) است که به روشی غیرساختی ثابت شده است. برهان نحوی ساختی برای قضیه ۲.۲۸ ارائه شده است که می‌توانید در
Kleene, S.C. (1952) Introduction to Metamathematics. Van Nostrand. § 74,
آن را ببینید. اما باید به طور کلی گفت که این برهان‌ها بسیار پیچیده هستند.
⦿ برهان
ساختی و برهان غیرساختی■ برهان ساختی و برهان غیرساختی
برهان ساختی: وجود و ساخت
یک برهان ساختی وجود شی‌ای (شی‌ای ریاضی، منطقی یا مجرد) را با ارائه صریح خود آن شی یا با ارائه روشی (الگوریتم) برای ایجاد آن، ثابت می‌کند. برای مثال فرض کنید می‌خواهیم ثابت کنیم عدد زوج اول وجود دارد. می‌گوییم ۲ یک عدد طبیعی است که هم زوج است و هم اول است (ارائه صریح خود شی). یا می‌خوهیم ثابت کنیم که برای هر دو عدد صحیح مثبت بزرگترین مقسوم علیه مشترک وجود دارد. در اثبات الگوریتم اقلیدس را ارایه می‌کنیم.
اثبات ناگویایی ریشه دوم عدد ۲ را می‌توان در اینجا دید. آیا این برهان یک برهان ساختی است؟ توجه داریم که این برهان وجود ریشه دوم عدد ۲ را ثابت نمیکند تا برای یافتن آن یک الگوریتم ارائه دهد. این برهان نشان می‌دهد به فرض وجود ریشه دوم عدد ۲ آنگاه `sqrt ۲` گویا نیست. به عبارت دیگر، عدد گویایی وجود ندارد که ریشه دوم عدد ۲ باشد. از این جهت، برهان ناگویایی ریشه دوم عدد ۲ یک برهان ساختی است.
اکنون می‌توان گفت برهان‌هایی که برای اثبات عدم وجود شی‌ای آورده می‌شوند، اگر در آنها فقط از روش‌های آنچه منطق شهودی نام دارد استفاده شده باشند، ساختی خواهند بود. در واقع در برهان ساختی بجای نشان دادن `¬(EEx)A(x)` به شیوه ساختی نشان می‌دهند که `(AAx)¬P(x)` اثبات می‌شود. برای مثال برای ثابت کردن اینکه عدد اول زوج بزرگتر از ۲ وجود ندارد باید نشان داد همه اعداد زوج بزرگتر از ۲ عدد اول نیستند.
برهان غیرساختی: وجود بدون ساخت
یک برهان در منطق به دنبال اثبات درستی یک گزاره است. همان‌طور که گفته شد برهان‌های ساختی با ارائه صریح شی مورد نظر یا ارائه یک الگوریتم برای ایجاد آن بدان دست می‌یابند. با این حال، دسته دیگری از برهان وجود دارد که به عنوان برهان غیرساختی شناخته می‌شوند. این برهان‌ها وجود یک شی را بدون لزوم یافتن یا ساختن صریح آن ثابت می‌کنند.
برهان‌های غیرساختی بیشتر بر اصول منطقی بنیادینی تکیه می‌کنند که امکان می‌دهند وجود را به طور غیرمستقیم استنتاج کنیم. یک ابزار متداول اصل طرد شق وسط است. تکنیک دیگری که برای اثبات وجود استفاده می‌شود برهان غیرمستقیم است. یعنی، نشان دادن اینکه فرض عدم وجود یک شی منجر به امتناع منطقی (تناقض یا ناسازگاری) می‌شود. سپس بنا بر این نتیجه، گفته می‌شود که شی باید وجود داشته باشد. (این دومی اغلب به طور ضمنی بر اصل طرد شق وسط یا اصولی متکی است که در منطق‌های ساختی پذیرفته نشده‌اند).
برای مثال می‌خواهیم نشان دهیم اعداد ناگویای `a` و `b` وجود دارند بقسمی که `a^b` یک عدد گویا است.
`sqrt ۲^{sqrt ۲}` را در نظر می‌گیریم.
می‌گوییم: `sqrt ۲^{sqrt ۲}` گویا است یا گویا نیست و از این دو نیز خارج نیست.
اگر گویا است که (از اینکه می‌دانیم `sqrt ۲` گویا نیست) نشان داده‌‌ایم:
`a=sqrt ۲` و `b=sqrt ۲`.
اگر گویا نیست فرض می‌کنیم:
`a = sqrt ۲^{sqrt ۲}` و `b = sqrt ۲`.
بنابراین:
`a^b = (sqrt ۲^{sqrt ۲})^sqrt ۲ =`` sqrt ۲^{(sqrt ۲ * sqrt ۲)} =`` (sqrt ۲)^۲=۲`
که گویا است.
پس، ما ثابت کرده‌ایم که زوج `(a, b)` باید وجود داشته باشد زیرا یکی از این دو مورد طبق LEM باید درست باشد.
اما، این برهان به ما نمی‌گوید که کدام مورد درست است (آیا `sqrt ۲^{sqrt ۲}` گویا است یا نه؟). بنابراین ما `(a, b)` مشخصی را در همه موارد نیافته‌ایم.
این تکیه بر اصولی مانند LEM برای تضمین وجود بدون ارائه مورد مشخص یا روش ساخت، مشخصه تعیین کننده برهان‌های غیرساختی است. در حالی که این اصول کاملا معتبر هستند و به طور گسترده در ریاضیات کلاسیک استفاده می‌شوند، اما در چارچوب‌های ریاضیات ساختی (مانند شهودگرایی)، که نیاز به شواهد صریح برای وجود دارند، متفاوت دیده می‌شوند.
⦿
براوئر 
برگردان فارسی واژگان «ذهن آفریننده» برای «Creative Subject» و «دوئیت» برای «Towity» و برخی دیگر از اینجا برگرفته شده است.
■ براوئر (L.E.J. Brouwer - 1881 - 1966) و منطق شهودی⇖
براوئر (Luitzen Egbertus Jan Brouwer - 1881 - 1966) یک ریاضیدان و فیلسوف هلندی پیشگام بود. او در ۲۷ فوریه ۱۸۸۱ در اوورشی (Overschie) در هلند پا به دنیا گشود. در دانشگاه آمستردام تحصیل کرد و در سال ۱۹۰۷ دکترای خود را با پایان‌نامه تحت عنوان "Over de grondslagen der wiskunde / در مبانی ریاضی↝" دریافت کرد. حرفه آکادمیک براوئر اساساً در دانشگاه آمستردام متمرکز بود، جایی که او از سال ۱۹۱۲ تا زمان بازنشستگی خود در سال ۱۹۵۱ به عنوان استاد در آنجا به تدریس و پژوهش پرداخت.
سهم او در ریاضیات شامل نتایج اساسی در توپولوژی است، ازجمله قضیه مشهور به نقطه برجای براوئر (Brouwer’s Fixed Point Theorem)، که می‌گوید هر تابع پیوسته از یک زیرمجموعه فشرده و محدب از فضای اقلیدسی به خود حداقل یک نقطه ثابت دارد. به عبارت دیگر:
گیریم `D` یک دیسک بسته `[D = {p ∈ RR^۲: ||p|| ≤۱}]` در `RR^۲` باشد (یا، یک گوی بسته در `RR^۳` باشد). و نیز `f` یک تابع پیوسته از `D` در `D` باشد. در این صورت `x in D` وجود دارد، بقسمی که: `f(x)=x` [قضیه نقطه ثابت را در اینجا و اینجا (قضیه بازگشت) ببینید.]
فراتر از این دستاوردهای ریاضی، براوئر بنیانگذار منطق شهودی است، رویکردی فلسفی به ریاضیات که بر ساخت ذهنی بیش از دستکاری نمادین صوری تأکید دارد. شهودگرایی دیدگاه‌های فرمالیستی (صورت گرایی - Formalism) مسلط زمان خود را به چالش کشید، به‌ویژه او را در تقابل فکری با چهره‌هایی مانند دیوید هیلبرت، [دستگاه هیلبرت] قرار داد که از فرمالیسم و اصل طرد شق وسط دفاع می‌کرند. رد این قانون منطق کلاسیک برای مجموعه‌های نامتناهی منجر به بحث‌های شدید در مورد ماهیت و مبانی ریاضیات شد. این بحث‌های بین مکاتب فکری مختلف (شهودگرایی، فرمالیسم، منطق‌گرایی) و فلسفه ریاضیات و منطق را برای دهه‌ها شکل داد. [ ↜ از براوئر تا هیلبرت - ↜ از فرگه تا گودل - ↜ مناقشه فرگه-هیلبرت]
براوئر علاوه بر نوآوری‌های ریاضی خود، تحت تأثیر و مشارکت پروژه (Significs) در هلند قرار گرفت، که زبان، معنا و منطق را مورد بررسی قرار می‌داد. این دیدگاه‌های فلسفی او را در مورد شهود و یقین در ریاضیات تقویت کرد.
سال‌های بعدی براوئر بیشتر انزوا گزید، که تا اندازه‌ای ناشی از ماهیت بحث‌برانگیز ایده‌های او و سرسختی او در دفاع از آن بود. با وجود این، میراث او از طریق کار پیروانی مانند آرند هیتینگ و توسعه تفسیر براوئر-هیتینگ-کلموگروف در منطق شهودی ماندگار شد. وی همچنین به عضویت مؤسسات معتبر زمان، آکادمی سلطنتی هنر و علوم هلند، انجمن سلطنتی لندن، آکادمی علوم گوتینگن و آکادمی علوم برلین درآمد. براوئر در ۲ دسامبر ۱۹۶۶ در بلاریکوم هلند درگذشت. کارهای پیشگامانه او همچنان بر ریاضیات مدرن، منطق ساختی و فلسفه ریاضیات تأثیر گذار است.
در اینجا فهرستی اولویت‌بندی شده از برخی واژگان کلیدی در منطق / ریاضیات شهودی، همراه باشرح کوتاه، آمده است که بر اساس استقلال مفهومی (کمترین وابستگی) مرتب شده‌اند:
| ۱. |
ذهنِ آفریننده Creative Subject یک ریاضیدان مفهومی (عامل معرفتی - ذهن آفریننده) است که کنش زمان‌مند او صدق (حقیقت) ریاضی را تعیین می‌کند. (برای مثال، یک گزاره زمانی درست است که سوژه آفریننده آن را ثابت کند). بنابراین، ریاضیات فقط مجموعه‌ای از حقایق ابدی نیست که در انتظار کشف شدن باشند - بلکه یک کنش آفرینشی-ذهنی است. ریاضیات یک روند پیشرونده است که در ذهن ریاضیدان شکوفا می‌شود. هیچ شی ریاضی به طور مستقل «در بیرون» وجود ندارد. در عوض، وجود ریاضی عمیقاً شخصی و ساختی است. در اینجا است که «ذهن آفریننده» به میدان می‌آید - نه همچون یک دانای کل، بلکه همچون یک ریاضیدان مفهومی و همیشه در حال آفرینش. این عامل معرفتی صرفاً حقایق را کشف نمیکند، آنها را به طور پویا می‌سازد، یک گام ذهنی دقیق در هر لحضه زمان. هر هستی‌مند ریاضی، هستی خود را مدیون یک کنش صریح ساختن به واسطه این عامل معرفتی است و اگر آن را نساخته باشد، آنی در کار نیست. این عامل معرفتی (ذهن آفریننده) آغازگر و پیشرونده از اکنون است. و لذا هر برهان (الگوریتم) و هر تعریف یک کنش زنده و یک شکفتن در اکنون است. شکفتنی که توان شهود ریاضی و آفرینندگی انسانی آن را محدود می‌کند. بنابراین می‌توان از سه گانه زیر را به عنوان سه وپژگی مبنایی ذهن آفریننده سخن گفت: ۱. کنش‌های زمان‌مند: حقیقت در زمان و با گام‌های ذهن پدیدار می‌شود. ۲. آزادی رادیکال: شناسا پابند قوانین از پیش موجود نیست و این موجد ضرورت منطقی است. [ضرورت منطقی از پیش مقدر نیست: از خودِ کنشِ ساخت برمی‌خیزد.] ۳. ضد واقع‌گرایی: اشیا (مثل اعداد) فقط همچون ساخت‌های ذهنی هستند و نه چون مطلق‌های افلاطونی↜. 
(AI generated image. Personal communication.) در اینجا است که برای آموزنده منطق و به ویژه علوم کامپیوتر، ارتباط با موضع خلاقانه براوئر یک تغییر دهنده بازی است. این پیوند، شهود و صورت را به هم می‌پیونداند. ما را وامیدارد نه تنها در مورد آنچه که هست، بلکه در مورد آنچه می‌توان ساخت، بیاندیشیم. اکنون و در این زمانه این رویکرد بیش از هر زمان دیگری مرتبط به نظر می‌رسد: واقعیت چیزی است که است که می‌توان آن را با گام‌های ساختی واقعی کرد. داستان این نیست که چگونه چیزی را می‌توان به وجود آورد. داستان این است که چگونه بطور ساختی آن را توصیف کنیم. به عبارت دیگر، واقعیت یافتنی نیست، ساختنی است. |
||||||
| ۲. |
شهود ریاضی Mathematical Intuition ریاضیات از شهود آغازین ذهن از زمان ناشی می‌شود و اشیا را از طریق کنش ذهنی (نه بنداشت‌ها یا زبان) می‌سازد (تقدم بستر فلسفی بر دستگاه‌های صوری). در این دیدگاه، شهود به آگاهی اولیه و پیشازبانی از جریان زمان اشاره دارد - آگاهی از یک لحظه (دوئیت / Twoity)، که خود به دو لحظه مجزا، آنگونه که پائین‌تر خواهیم (⤓) دید، تقسیم می‌شود. براوئر این را شهود آغازین (Ur-intuition) زمان نامید. این شهود زمانی، بنیادی است که همه ریاضیات باید بر آن بنا شود. این منبعِ درک ما از توالی‌های بنیادین است. این شهود، بنیادی‌تر از زبان یا منطق صوری در نظر گرفته می‌شود. منطق و زبان همچون ابزارهایی برای توصیف یا ارتباط این ساخت‌های ذهنی پس از درک شهودی آنها در نظر گرفته می‌شوند، نه مبنایی برای وجود یا حقیقت آنها. بنابراین، در دیدگاه شهودی، شهود منبع و کنش بنیادی ذهن آفریننده است که ریاضی از آن سرچشمه می‌گیرد و به طور خاص، دریافت مبنایی ذهن از توالی زمانی است. |
||||||
| ۳. |
برهانِ ساختی Constructive proof اشیا (صدق) می‌باید بطور صریح ساخته شوند، نه اینکه صرفا فرض شود وجود دارند. برهان‌ها نیازمند به الگوریتم یا خلق ذهنی موجودیت (هست‌مندی) هستند. این اصل بنیادین می‌گوید ریاضیات «اساسا یک فعالیت ذهن بدون زبان» است که ریشه در درک زمان دارد — که در آن "شهود نخستینی" یک مفهوم بنیادی است. ارجاع آن به درک درونی انسان (آگاهی / Awareness) از زمان به عنوان پایه‌ای برای تمام تفکر ریاضی است. "شهود نخستینی / ur-intuition" ناشی از فروپاشی یک لحظه در (حافظه) به دو بخش مجزا است - یکی پس گرد در زمانه (حافظه) و دیگری برایش (Emergence) آن. این "دوئیت / Twoity" به صورت محض از همه این دوگانه‌ها انتزاع می‌شود و پایه‌ای برای ساختن اعداد طبیعی و اشیا ریاضی بیشتر را تشکیل می‌دهد. برای مثال:
دوئیت (Two-ity). (AI generated image. Personal communication.) بنابراین، دوئیت یک ساخت ذهنی، شهودی و بنیادی است که زیربنای پیدایش اعداد طبیعی در شهودگرایی براوئر است. این کنشِ نخستینیِ تقسیم جریان پیوسته زمان به دو بخش متمایز - یک "قبل" و یک "بعد" - ایجاد یک همزادی بنیادی است که از آن می‌توان دنباله اعداد طبیعی را تولید کرد. و از اینجا، دوئیت را می‌توان توانایی درونی در درک زمان و توالی، یک نخستینی که با آن ساختن ریاضی آغاز می‌شود، انگاشت. در مبانی شهودی براوئر، صفر یا بهتر بگوییم «صفر» به عنوان یک عدد طبیعی، برآمده از دوئیت نیست و بنابراین اعداد طبیعی از یک شروع می‌شوند. صفر صرفاً یک نماد صوری است (ثابت انفرادی که تعبیر آن خودش است / ثابت انفرادی پایه). |
||||||
| ۴. |
طردِ اصل طرد شق وسط Law of Excluded Middle (LEM) Rejection شهودگرایی اصل طرد شق وسط [«`P vee not P`»، که می‌گوید یک گزاره درست است و یا نقیض آن درست است] را نمی‌پذیرد و آن را به گزاره‌های تصمیم‌پذیر محدود می‌کند. |
||||||
| ۵. |
توالی‌های (دنباله‌های) انتخاب آزاد Free Choice Sequences دنباله‌های انتخاب آزاد دنباله‌هایی بیپایان پیشرونده هستند (مثلاً اعداد) که در آن مقادیر بعدی از پیش تعیین نشده هستند. به عبارت دیگر، توالی‌های بالقوه نامتناهی که گام به گام توسط ذهن آفریننده (فاعل شناسا) آفریده می‌شوند. |
||||||
| ۶. |
تعبیر BHK (براوئر-هیتینگ-کلموگروف - Brouwer-Heyting-Kolmogorov) تعبیر رابط‌های منطقی از طریق شرط اثبات به قرار زیر است: `A∧B`: اثبات `A` و اثبات `B`. `A∨B`: اثبات `A` یا اثبات `B`. `¬A`: ساختی که هر گونه اثبات `A` را به پوچی صوری (`_|_`) تبدیل می‌کند. به عبارت دیگر، نقض شهودی ابطال ساختی است و نه اشاره به مقدار ارزش. |
||||||
| ۷. |
بی‌نهایتِ بالقوه Potential Infinity بی‌نهایت یک روند پیشرونده (برای مثال، اعداد طبیعی به عنوان بیپایان) است و این در رد مجموعه‌های بی‌نهایت «تمام» (مثلاً بی نهایت واقعی کانتور) است. |
||||||
| ۸. |
پیوستار همچون نخستینی Continuum as Primitive پیوستار شهودی (برای مثال اعداد حقیقی) از نقاط تشکیل نشده است، بلکه یک واسطِ شدنِ آزاد (medium of free becoming) است که به موجودیت‌های گسسته تحویل ناپذیر است. اصطلاح "واسطِ شدنِ آزاد" انگاشتی از پیوستار را به عنوان موجودیت پویا و ناتمام که توسط توالی‌های انتخاب آزاد و اعمال ذهنی شکل می‌گیرد، توصیف می‌کند. برای مثال عدد حقیقی `r` (به فرض `pi`=۳/۱۴۱۵ ...) در ریاضیات کلاسیک یک شی تمام است. ولی در ریاضیات ساختی`r` یک روند است، که در هر لحظه، ریاضیدان بطور مختار رقم بعدی را برمی‌گزیند و `r` همیشه ناتمام می‌ماند. `r` یک «شی» نیست، بلکه راهی برای کنش در پیوستار است. بنابراین در دیدگاه شهودی پیوستار اعداد حقیقی واسط بنیادی و اولیه است که در آن نقاط به صورت پویا از طریق توالی انتخاب‌ها ساخته می‌شوند. این پیوستار از نقاط از پیش ساخته شده تشکیل نشده است. |
||||||
| ۹. |
تعبیر برهان Proof Interpretation گزاره‌های منطقی با برهان همچون ساخت اعتبار سنجی می‌شوند، نه مقادیر ارزش. برای مثال، وجود `x` به قسمی که `P(x)` نیازمند به برنمایاندن چنین `x`ای است. |
||||||
| ۱۰. |
نقض همچون اثبات ناپذیری Negation as Non-Provability `¬A` به معنای "هیچ برهان مبنی بر `A` نمی‌تواند وجود داشته باشد (چنین نیست که «`A` نادرست است») است. عدم وجود ساخت برای نقض کافی است، که این بازتعریف نقیض کلاسیک است. |
||||||
| ۱۱. |
تصمیم پذیری در مقابل تصمیم ناپذیری Decidability and Undcidability فقط محمولات تصمیم‌پذیر (برای هر `x`, `P(x)` یا `¬P(x)`) در کاربرد LEM مجوز دارند. (برای مثال، مسئله وقف ماشین تورینگ LEM کلاسیک را نمی‌پذیرد.). فرض کنید `H(M, I)` گزاره "ماشین تورینگ `M` با ورودی `I` متوقف می‌شود" باشد. اما، هیچ الگوریتمی وجود ندارد که برای هر ماشین تورینگ دلخواه `M` و هر ورودی `I` برای آن تصمیم بگیرد که آیا `H(M, I)` درست است یا `H(M, I)` نادرست است (یعنی `M` برای همیشه متوقف می شود یا اجرا می شود). بنا به LEM (کلاسیک) داریم `H(M, I) vee ¬H(M, I)` اگر LME (کلاسیک) بطور کلی در منطق شهودی معتبر بود، به وجود یک الگوریتم برای مسئله توقف دلالت می‌کرد. یعنی: برای هر `M` و `I`، می‌توانیم به طور ساختی تعیین کنیم که آیا `H(M, I)` برقرار است یا `¬H(M, I)`. برقرار است. و از آنجایی که می‌دانیم چنین الگوریتم بطور کلی وجود ندارد، شهودگرایی نمی‌تواند LEM را به عنوان یک اصل معتبر جهانی بپذیرد. مانند این را می‌توان در باره حدس‌های ریاضی مانند حدس گلدباخ نیز گفت. اما توجه داریم که این رد به این دلیل نیست که حدس گلدباخ تصمیم‌ناپذیر است (مانند مسئله توقف)، بلکه صرفاً به این دلیل است که نه حدس (صحت آن) و نه نفی آن به طور ساختی اثبات نشده است. شهودگرایی پیش از پذیرش گزاره‌ای مانند `P vee ¬P` در پی چنین ساختی است. |
||||||
| .۱۲ |
غیبت مقادیر ارزش Absence of Truth Values گزاره‌ها فاقد ارزش‌های صدق از پیش تعریف شده هستند. صدق گره خورده به برهان است. به عبارت دیگر درستی یک گزاره، وجود یک ساخت (برهان ساختی) موفق است و نادرستی یک گزاره، به معنای داشتن یک برهان ساختی است که درستی گزاره منجر به تناقض می‌شود. بنابراین گزاره‌هایی که هیچ یک را برای آنها نداریم، نامعین باقی می‌مانند. این، اینکه در منطق کلاسیک هر گزاره باید درست باشد یا نادرست باشد را رد می‌کنند، یعنی، گزاره‌های اثبات نشده نه درست هستند و نه نادرست هستند. |
||||||
| .۱۳ |
قانون‌سانی و انواع Spreads - Species قانون‌سا‌ن‌ها (Spreads) قواعدی برای تولید اشیا (به عنوان مثال، دنباله‌ها) هستند و انواع (Species) ویژگی‌های اشیای ساخته‌شده هستند. و از این جهت، «انواع» در شهودگرایی، همتای مجموعه‌های کلاسیک هستند، اما ماهیتشان اساساً متفاوت است. آنها بگونه‌ای مجموعه‌های شهودی از موجودیت‌های ریاضی ساختی (ساخته‌شده) قبلی هستند که یک ویژگی خاص را به اشتراک می‌گذارند. آنها با یک ویژگی یا روش ساختی تعریف می‌شوند و نه صرفاً با عضویت — حال آن که در منطق کلاسیک این‌همانی (Identity) گسترشی و صرفاً مبتنی بر عضویت است (اصل موضوع گسترش را ببینید). این ویژگی می‌باید پیرو این‌همانی مفهومیتی↝ - ↝ - ↝ باشد - یعنی دو نوع با اعضای یکسان اما به گونه متفاوت تعریف شده لزوماً یکسان نیستند. انواع «وجهی از خودگشایی شهود نخستینی ریاضیات_ On Brouwer.» هستند. یک نوع با ویژگی `P` ساخته می‌شود به قسمی که: • این ویژگی بر موجودیت‌های ریاضی پیش ساخته کار زدنی است. بنابراین، انواع می‌توانند انواع دیگری را به عنوان عنصر داشته باشند و انواع مرتبه بالاتر را به وجود آورند. • اگر موجودیت `P` ،`x` را بربیاورد، `x` عنصری از نوع است. • ویژگی باید با تساوی سازگار باشد (یعنی اگر `x` مساوی `y` باشد و `x` در نوع باشد، `y` نیز در نوع است). • انواع دارای مفهومیت - ↝ - ↝ - ↝ - هستند: نحوه مشخص شدن ویژگی بر چیستی (Identity) نوع تأثیر می‌گذارد. مثال: • دنباله‌های انتخاب را در نظر بگیرید. • نوع `S` می‌تواند تمام دنباله‌های انتخابی باشد که ویژگی `Q` را برمی‌آورد (مثلاً توالی‌های محدود شده توسط برخی معیارهای ساختی). • این نوع دربردار اشیای نامتناهی است اما عضویت در آن بناشده بر روند ساختی ایجاد این توالی‌ها است. یک قانون‌سا‌ن یک قاعده (یا "قانون") خاص و ریاضی تعریف شده است. این قانون می‌گوید که چگونه می‌توان دنباله‌های بالقوه نامتناهی را از اشیا ساخت (مانند اعداد، که از دوئیت برآمده‌اند). این قانون گام به گام تعیین می‌کند که کدام آغاز متناهی دنباله‌ها مجاز (Admissible) است. بنابراین، یک قانون‌سا‌ن قاعده یا قانونی است که نحوه تولید دنباله‌های بالقوه نامتناهی از اشیا را تعیین می‌کند و به عنوان یک "گردایه" ساختی و پیشرونده از این توالی‌های بالقوه عمل می‌کند. برای مثال، یک درخت ↝ را در نظر بگیرید که در طول زمان رشد می‌کند: |
||||||
| .۱۴ |
زمانی بودگیِ شدنِ ریاضی Temporal Becoming of Mathematics صدق ریاضی زمان‌مند است: برهان‌ها یا ساخت‌های جدید می‌توانند اعتبار (ساختی) گزاره‌ها را تغییر دهند (برای نمونه، پیشروندگی ذهن آفریننده). |
||||||
مراجع:
1. Van Atten, Mark. On Brouwer. Belmont, CA: Wadsworth/Thomson Learning, 2004.
این اثر به فارسی با عنوان زیر ترجمه شده است (مترجم خود از ریاضیدانان و منطق دانان برجسته حاضر است.):
فلسفه براوئر، مارک فان آتن، محمد اردشیر (مترجم)، ناشر: هرمس، ۱۳۸۷.
2. Sørensen, Morten Heine, and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
3. Van Atten, Mark, Luitzen Egbertus Jan Brouwer, The Stanford Encyclopedia of Philosophy.
4. Moschovakis, Joan, Intuitionism and Proof Theory, The Stanford Encyclopedia of Philosophy. 2024.
5. A. Heyting, L. E. J. Brouwer Collected Works (1), North-Holland Publishing Company, 1975.
6. Hans Freudenthal, L. E. J. Brouwer Collected Works (2), North-Holland Publishing Company, 1976.
7. Rex Page and Ruben Gamboa. Essential Logic for Computer Science, MIT press, 2019.
8. Weir, Alan, The Curry-Howard Correspondence - Formalism in the Philosophy of Mathematics, The Stanford Encyclopedia of Philosophy, 2025.
9. Bridges, Douglas, Erik Palmgren, and Hajime Ishihara Constructive Mathematics, The Stanford Encyclopedia of Philosophy, 2022.
■ وصف معین
عبارت‌های وصفی از نوع «`u` به قسمی که `cc"B" (u, y_۱, ...، y_n)`» در زبان معمولی و ریاضیات بسیار رایج است.
چنین عباراتی را وصف معین -
↝ می‌نامند. ما
"`ιu(cc"B" (u, y_1, ..., y_n))`" را
دلالت کننده به شی یکتای `u` می‌گیریم به قسمی که
`cc"B" (u, y_۱, ..., y_n)`، اگر چنین شی یکتایی
وجود داشته باشد. [ ι: Iota (/aɪˈoʊtə/]
اگر چنین شیئِ یکتایی وجود نداشته باشد، می‌توانیم "`ι"u(cc"B" (u, y_1, ..., y_n))`" را کوتاه شده یک شی ثابت بگیریم، یا آن را بدون معنی بدانیم. (برای مثال، ممکن است بگوییم که عبارت‌های "پادشاه کنونی فرانسه" و "کوچکترین عدد صحیح" بی‌معنی هستند یا ممکن است دلخواهانه قرارداد کنیم که آنها دلالت بر ۰ دارند.)
روش‌های مختلفی برای گنجاندن این ι-termها در تئوری‌های صوری وجود دارد، اما از آنجا که در بیشتر موارد نتایج یکسانی با استفاده از حروف تابعی جدید یا ثابت‌های انفرادی مانند بالا حاصل می‌شود، و از آنجا که همه آنها به قضایای مشابه قضیه ۲.۲۸ منجر می‌شوند، در اینجا بیشتر در درباره آنها بحث نخواهیم کرد. برای جزئیات بیشتر موردهای زیر را ببینید:
1- Hilbert, D. and P. Bernays (1934, 1939) Grundlagen der Mathematik, Vol. I (1934), Vol. II (1939). Springer (second edition, 1968, 1970).
2. Rosser, J.B. (1939) An informal exposition of proofs of Gödel’s theorem and Church’s theorem. JSL, 53–60 (reprinted in Davis, 1965).
