مقدمات نظریه برهان (دستگاه صوری استنتاج)
منطق و فرامنطق
درآمد به منطق
بر آن بودم تا فرمالیسمی بنا کنم هر چه بیشتر نزدیک به استدلال، آنگونه که هست. این بود که حساب استنتاج طبیعی به وجود آمد. __گرهارد گنتزن
Gerhard Gentzen, "Investigations into Logical Deduction", American Philosophical Quarterly, Vol. 1, No. 4 (Oct., 1964), pp. 288-306
۴. دستگاه صوری استنتاج
≡
۱- مقدمه: دستگاه صوری و برهان | ۷- ناسازگاری |
۲- یادآوری نه قاعده استنتاج | ۸- انفجار استنتاج / اصل سرریزی |
۳- استنتاج و برهان |
۹- منطق‌های پاراسازگار (Paraconsistent logics) |
۴- ویژگی این‌همانی | ۱۰- قاعده برهان شرطی |
۵- هم‌ارزی نحوی | ۱۱- قضیه در دستگاه صوری (استنتاجی) |
۶- قاعده جایگزینی نحوی |
■ مقدمه: دستگاه صوری و برهان
موضوع این یادداشت درآمدی کوتاه بر نظریه برهان (منطق گزاره‌ای) و در واقع مرور و جمع بندی قسمت‌های یک تا هشت فصل دهم (روش‌های استنتاج) «کتاب درآمد به منطق» است. در یادداست صورت و معنا در منطق گزاره‌ای رویکرد ما برای گسترش منطق گزاره‌ای بر مبنای مدل (Model Theoritic) بود. کلید واژه‌ها در آنجا عبارت بودند از زبان صوری، تعبیر، مدل و استنتاج سمانتیکی. برای مثال در مثال‌های ۱، ۲ و ۳ به ترتیب نشان دادیم:
مثال.۱- (p ⊃ q) ⊩ (~q ⊃ ~p) یک استنتاج معتبر سمانتیکی معتبر است.
مثال.۲- p ⊃ (q ⊃ r) ⊩ p ⊃ (q ⊃ r) یک استنتاج سمانتیکی نامعتبر است.
مثال.۳- ((p • q) ⊃ r)) ⊩ ((p ⊃ r) ∨ (q ⊃ r)) یک استنتاج سمانتیکی معتبر است.
روند اثبات در مثال‌های بالا بدین قرار بود که، نشان دهیم هر تعبیر که برای مقدمات مدل است برای نتیجه نیز مدل است و برای خلاف آن بدین قرار بود که، نشان دهیم دست‌کم یک تعبیر وجود دارد که برای مقدمات مدل است ولی برای نتیجه مدل نیست (مثال ۲). ازاین‌جهت، این‌گونه روند گسترش به نظریه مدل [نیز نظریه مبتنی بر مدل (Model-theoretic) یا معناشناختی مبتنی بر مدل / Model-theoretic semantics] نامیده می‌شود.
نظریه برهان (Proof Theory)
در نظریه برهان کوشش بر آن است تا برای مثال دست‌آوری ((p⊃r)∨(q⊃r)) را از (p•q)⊃r نه در یک روند تعبیری، بلکه در یک روند نحوی (اشتقاق نحوی / Syntactic derivation) انجام شود. این روند به نظریه برهان (برهان شناختی / نظریه مبتنی بر برهان / معناشناختی مبتنی بر نظریه برهان] موسوم است. درواقع:
در نظریه برهان، فرض بنیادی بر این استوار است که انگاره اصلی، از این جهت که چه معنایی به عبارت‌های زبان نظیر می‌شود، به‌جای تعبیر، برهان است. به عبارت دیگر، در این روند برهان صوری اعتبار بجای تعبیر می‌نشیند.
بنابراین، تا پایان این قسمت آنچه تاکنون در باره تعبیر، گفته‌ایم اعم از مقدار معنایی، مدل و جدول ارزش، موقتاً به کنار نهاده و آنچه ابتدا در پیش روی خود می‌گذاریم، زبان صوری و فرمول خواهند بود.
برای تاکید یادآور می‌شویم آن چه در این قسمت می‌آید مرور فصل دهم «کتاب درآمد به منطق» است — قسمت ۷، دستگاه استنتاجی، حساب گزاره‌ها - ۱۹ قاعده استنتاج — که بر پایه زبان صوری LC گسترش یافته است.
■ یادآوری نه قاعده استنتاج
فرض کنید ℱ مجموعه فرمول‌های LC باشد. یک قاعده استنتاج نحوی [یا فقط قاعده استنتاج] در یک دستگاه نحوی، یک رابطه به صراحت تعریف‌شده بین فرمول‌ها، یعنی ℱ، و مجموعه‌های فرمول، یعنی مجموعه توانی ℱ، است، به قسمی که، بتوان تصمیم گرفت آیا هر فرمول در این رابطه با هر مجموعه فرمول دلخواه است یا نه؟ بنابراین هر قاعده استنتاج یک رابطه تصمیم پذیر است.
برای یادآوری، در جدول ۱ در زیر نه قاعده استنتاج آمده است:
| ۹ قاعده استنتاج نحوی | |||
| ~β, α ⊃ β —————R۲ ~α | ۲. | α , α ⊃ β ———————R۱ β | ۱. |
| (α ∨ β ) , ~α ———————R۴ β | ۴. | (α ⊃ β), (β ⊃ γ) —————————R۳ α ⊃ γ | ۳. |
| α ⊃ β ———————R۶ α ⊃ (α • β) | ۶. | (α ⊃ β) • (γ ⊃ λ), (α ∨ γ ) —————————————R۵ β∨λ | ۵. |
| α, β ———R۸ α • β | ۸. | α • β ———R۷ α | ۷. |
| α ————R۹ α ∨ β | ۹. | ||
■ گرهارد گنتسن - Gerhard Gentzen
گرهارد گنتسن (Gerhard Gentzen - ۱۹۴۵-۱۹۰۹) ریاضیدان و منطقی آلمانی در برگن (شهری واقع در جزیره روگن آلمان) پا به دنیا گشود. پدر وی که یک حقوق‌دان بود در جنگ جهانی اول کشته شد. وی در ۱۹۲۸ تحصیلات متوسطه را به پایان برد و از همان موقع توان استثنایی وی در ریاضیات آشکار گردید. تحصیل ریاضیات را از سال ۱۹۲۸ به ترتیب در دانشگاه‌های گریفزوالد(Greifswald) گوتینگن، برلین و مونیخ ادامه داد. سرانجام در ۱۹۳۳ از دانشگاه گوتینگن دکتری خود را دریافت کرد. پس از مدتی استراحت برای بازیابی سلامت به‌عنوان دستیار هیلبرت در دانشگاه کوتینگتن به کار ادامه داد. گنتزن به‌ویژه همکار اصلی هیلبرت در برنامه اصل موضوعی کردن ریاضیات بود. ازجمله کارهای وی معرفی دستگاه‌های استنتاج طبیعی (Natural deduction systems) و دستگاه حساب دنبالک‌ها (Sequent calculus systems) است.
گنتزن در زمان جنگ دوم به‌عنوان مدرس در مؤسسه ریاضی دانشگاه آلمانی پراگ در چک مشغول کار شد ودر روزهای پایانی جنگ در اعتراض مردم پراگ به اشغال، همراه با سایر اعضای آلمانی دانشگاه دستگیر و ۴ روز بعد از دستگیری و آمدن روس‌ها به آنان تحویل شد. وی که سابقه حمایت از نازی‌ها را داشت تحت شرایط بدی در بازداشت روس‌ها باقی ماند و سه ماه بعد به علت سوءتغذیه درگذشت. — برگرفته از: http://www-history.mcs.st-andrews.ac.uk/Biographies/Gentzen.html دو مقاله از گنتسن: |
■ استنتاج و برهان
گیریم S={α۱, α۲, . . ., αn}⊂ℱ یک مجموعه فرمول باشد. گوییم فرمول β در دستگاه از S دست آوردنی [همچنین:β نتیجه استنتاجی S، یا β نتیجه برهانی S، یا β نتیجه نحوی S در دستگاه است] و نوشته:
(آ'): S ⊢β
اگر و فقط اگر دنباله متناهی فرمول‌های:
(ب'): <β۱, β۲, . . ., βm>
وجود دارد، به قسمی که:
۱- هر عضو این دنباله متعلق به S
یا در رابطه با یکی از
قواعد استنتاج و زیرمجموعه‌ای از عناصر قبلی دنباله باشد؛
و بعلاوه
۲-
βm همان β باشد.
می‌توان در S ⊢ β به‌جای S اعضای آن را فهرست کرد و نوشت:
α۱, α۲, . . ., αn ⊢β
به (آ') در بالا یک استنتاج معتبر نحوی [یا فقط استنتاج] و به دنباله:
β۱, β۲, . . .,βm
یک برهان در دستگاه گفته می‌شود. بعلاوه به مجموعه S مقدمان استنتاج می‌گویند.
بنابراین:
یک برهان در دستگاه یک دنباله β۱, β۲, . . .,βm فرمول (در دستگاه ) است به قسمی که برای هر i، یا βi یک مقدمه است یا βi نتیجه برخی از فرمول‌های قبلی در دنباله است که به موجب یکی از قواعد استنتاج در دستگاه نتیجه شده است.
وقتی نام دستگاه استنتاجی مورد بحث از زمینه مشخص است، (آ') را به‌صورت زیر می‌نویسند:
S ⊢ β
نماد '⊢' یک نماد فرازبانی (موسوم به Turnstile / گردان در) است و S⊢β طبق تعریف برابر با دنباله (ب') آنگونه که گفته شد است.
مراد از S, α ⊢ β استنتاج S ∪ {α} ⊢ β است.
■ ویژگی این‌همانی
α ⊢ α یک استنتاج معتبر نحوی است.
اثبات:
در دنباله تک عنصری <α۱=α> آخرین عنصر، یعنی α، یک مقدمه α⊢α است. بنابراین طبق تعریف، دنباله <α> یک برهان α⊢α است. این خاصیت که نتیجه مستقیم تعریف برهان در است را خاصیت این‌همانی می‌نامیم.
■ هم‌ارزی نحوی
صورت‌های گزاره‌ای α و β را هم‌ارزی نحوی گوییم اگر و تنها اگر α⊢β و β⊢α. در این صورت می‌نویسیم α⊢⊣β.
به‌آسانی می‌توان نشان داد هم‌ارزی نحوی یک رابطه هم‌ارزی در مجموعه فرمول‌ها است.
■ قاعده جایگزینی نحوی
اکنون قاعده جایگزینی نحوی را معرفی می‌کنیم؛ قاعده‌ای که طبق آن مجازیم از هر فرمول، فرمول حاصل از جایگزینی هر مؤلفه دلخواه آن را با هر عبارت به گونه نحوی هم‌ارز با آن مؤلفه، دست آوریم. [ب قاعده جایگزینی در کتاب مقایسه نمایید.] برای قاعده جایگزینی نحوی ۱۰ مورد کاربرد به‌عنوان هم‌ارزی‌های مقدماتی نحوی به شرح جدول زیر معرفی می‌کنیم.
| هم‌ارزی‌های نحوی مقدماتی — کاربرد قاعده جایگزینی نحوی | |||
|
(α∨β) ⊢⊣ (β∨α) (α•β) ⊢⊣ (β • α) |
۱۱. | ~(α•β) ⊢⊣ (~α∨~β) ~(α∨β) ⊢⊣ (~α • ~β) |
۱۰. |
|
[α•(β∨γ)] ⊢⊣
[(α•β)∨(α•γ)] [α∨(β•γ)] ⊢⊣ [(α∨β)•(α∨γ)] |
۱۳. |
[(α•β)•γ] ⊢⊣
[α•(β•γ)] [(α∨β)∨γ] ⊢⊣ [α∨(β∨γ)] |
۱۲. |
| α ⊃ β ⊢⊣ ~β ⊃ ~α | ۱۵. | α ⊢⊣ ~~α | ۱۴. |
| (α
≡ β ) ⊢⊣
[(α•β)∨(~α
• ~β)] (α ≡ β) ⊢⊣ [(α⊃β)∨(α⊃β)] |
۱۷. | (α ⊃β) ⊢⊣ (~β ∨α) | ۱۶. |
|
α ⊢⊣ (α∨α ) α ⊢⊣ (α • α) |
۱۹. | [(α • β)⊃ γ] ⊢⊣ [α ⊃ (β ⊃γ)] | ۱۸. |
| جدول ۲. ۱۰ مورد کاربرد قاعده جایگزینی | |||
■ اثبات اعتبار یک استنتاج نحوی، به‌وسیله برهان است.
مثال: نشان می‌دهیم رابطه:
((p • q) ⊃ r)) ⊢ ((p ⊃ r)∨(q ⊃ r))
یک استنتاج معتبر نحوی است.
| مقدمه | (p • q) ⊃ r | ۱. |
| ۱ و هم‌ارزی ۱۶ | ~(p • q) ∨ r | ۲. |
| ۲ و هم‌ارزی ۱۰ | (~p ∨ ~q) ∨ r | ۳. |
| ۳ و هم‌ارزی ۱۳ | (~p ∨ r) ∨(~q ∨ r) | ۴. |
| ۴ و هم‌ارزی ۱۶ | (p ⊃ r) ∨ (q ⊃ r) | ۵. |
■ ناسازگاری
گوییم دستگاه یک دستگاه صوری ناسازگار است اگر و فقط اگر در آن فرمول β وجود داشته باشد، به قسمی که β از {~β} دست آمدنی است، یعنی داشته باشیم:
{~β} ⊢ β.
در غیر این صورت دستگاه را دستگاه صوری سازگار گوییم.
■ انفجار استنتاج / اصل سرریزی
گیریم دستگاه ناسازگار باشد. در این صورت فرمول β هست که از ~β دست آمدنی است. اما بنا بر R۹ و R۳ فرمول β∨x که در آن x فرمول دلخواه است نیز از ~β دست آمدنی است. اما از β∨x و ~β و قاعده R۴ می‌توان x را به دست آورد.
بنابراین، اگر دستگاه ناسازگار باشد آنگاه هر فرمولی دست آمدنی است. این که از یک تناقض هر گزاره‌ای قابل استنتاج است به انفجار استنتاجی (اصل انفجار / اصل سرریز / Ex Falso Quodlibet) موسوم است. آشکار است که چنین دستگاه استنتاجی در منطق کلاسیک (سه قانون اندیشه) دارای هیچ دیدگاه وجودی نیست و خانه از پای‌بست ویران است.
نشان دادن سازگاری دستگاه را در بند سازگاری در بحث منطق و فرامنطق خواهیم دید.
■ منطق‌های پاراسازگار (Paraconsistent logics)
جهان سازگار است یا سازگار نیست؟! حداقل گاهی و جایی ناسازگار می‌نماید↧. پرسشی که از ۱۹۷۰ توسط ریاضیدانان و فیلسوفان، نیوتون دا کاستا (Newton da Costa) گراهام پریست (Graham Priest)، به‌طور نظام‌مند و جدی پی گرفته شد و دست آوُرد آن منطق‌های موسوم به منطق‌های فراسازگار (Paraconsistent logics) بود. این منطق‌ها پذیرای ناسازگاری بگونه ویژه‌ای هستند. در این منطق‌ها ناسازگاری اداره می‌شود. به عبارت دیگر، به شیوه خاص از میان ناسازگاری (یا از کنار آن / para ) گذر می‌شود.
This paradoxical life.
When logic fails to make sense of a world noisy with inconsistency, paraconsistent logics hold out (im)possible solutions (2021).
"https://aeon.co/essays/paraconsistent-logics-find-structure-in-our-inconsistent-world"
در گونه‌ای دستگاه منطقی فراسازگار موسوم به منطق گفتمانی (Discussive Logic) تعبیر درستی/نادرستی به کجا یا چه هنگام بر می‌گردد. فرض کنید شخص (آ) مدعی گزاره A و شخص (ب) مدعی گزاره A~ است. در این حالت می‌توان گفت گزاره A در یک تعبیر و در جهان ممکن w۱ درست است و گزاره A~ در جهان ممکن w۲ درست است. در این دستگاه آنچه در کل درست است حاصل تمام ادعاهایی است که در جهان‌های ممکن (ادعا کنندگان) ادعا شده است. بنابراین A و A~ هر دو در این تعبیر از دستگاه منطق گفتمان درست هستند. در این دستگاه اگر گزاره x در هیچ جهان ممکن درست نباشد آنگاه نادرست برآوُرد می‌گردد و چنین نیست که انفجار استنتاج روی دهد.
گونه دیگری دستگاه منطقی پاراسازگار، دستگاه‌های نا-پیوستی (Non-Adjunctive Systems) نامیده می‌شوند. از جمله اینکه قاعده پیوست در این دستگاه‌ها معتبر نیست و در واقع داریم:
{A, B} ⊭ A • B.
گرچه در دستگاه منطقی ناپیوستی هنوز انفجار استنتاج میسر است اما نبود قاعده پیوست مانع آن می‌شود.
■ قاعده برهان شرطی
قاعده برهان شرطی، به‌عنوان یک قاعده استنتاج، اجازه می‌دهد تا استنتاج با شمای ⊢α⊃β را از استنتاج معتبر نحوی با شمای α⊢β نتیجه گرفت. به عبارت دیگر:
(α ⊢ β) ⇒ (⊢ α ⊃ β).
از اینجا به بعد از دستگاه به شمول قاعده برهان شرطی با C.P یاد می‌کنیم.
■ قضیه در دستگاه صوری (استنتاجی)
به فرمول α در یک دستگاه استنتاجی یک قضیه گوییم (نیز α را در این دستگاه اثبات شدنی گوییم)، اگر α بدون هیچ مقدمه در این دستگاه دست آوردنی باشد. به‌عبارت‌دیگر، اگر α در آن دستگاه استنتاجی نتیجه نحوی یک استنتاج با مجموعه مقدمات تهی باشد. قضیه بودن α را در دستگاه‌های استنتاجی به‌صورت {}⊢α نشان می‌دهند. همان‌طور که مشاهده می‌شود مقدمات این استنتاج یک مجموعه تهی است.
ازآنجاکه یک و فقط یک مجموعه تهی وجود دارد، برای قضیه بودن فرمول α به نوشتن:
⊢ α
بسنده می‌گردد. فرمول α را در یک دستگاه استنتاجی اثبات نشدنی گوییم اگر α بدون مقدمه در این دستگاه دست آمدنی نباشد. مثال‌هایی از قضیه را می‌توان در اینجا ببینید.
■ ■ ■ ■ ■ ■ ■ ■
