نظریه اصل موضوعی منطق گزاره‌ای ۴
منطق و رایانش
درآمد به منطق
دیگر دستگاه‌های بنداشتی، منطق شهودی و جبر لیندنباوم
۱- سرآغاز | ۷- دستگاه لوکاسیویچ |
۲- دستگاه‌های بنداشتی دیگر | ۸- دستگاه‌های صوری تک بنداشتی |
۳- دستگاه صوری L۱ (هیلبرت - آکرمن) | ۹- منطق شهودی (Intuitionistic propositional logic) |
۴- دستگاه صوری L۲ (روسر ۳۹۵۲) | ۱۰- بنداشت‌ها در منطق شهودی گزاره‌ای |
۵- دستگاه صوری L۳ | ۱۱- برخی ویژگی‌ها و قضیه‌های منطق شهودی |
۶- دستگاه صوری L۴ (کلین ۱۹۵۲) | ۱۲- جبر لیندنباوم (Lindenbaum algebra) |
■ سرآغاز
در قسمت پیشین (قسمت سوم: استقلال بنداشت‌ها و منطق‌های چند ارزشی↝) نشان دادیم اصول موضوعه 𝓛 مستقل (A۱ - A۲ - A۳) هستند. سپس با رهنمود و بهره‌گیری از راهکار به کار رفته در اثبات استقلال بنداشت‌ها به منطق‌های چند ارزشی پرداختیم.
در این یادداشت، یعنی قسمت چهارم از نظریه اصل موضوعی منطق گزاره‌ای، به معرفی «دستگاه‌های بنداشتی دیگر منطق گزاره‌ای» از جمله «منطق شهودی» (Intuitionistic propositional logic) می‌پردازیم.
منبع و مرجع اصلی ما در چهار قسمت «نظریه اصل موضوعی منطق گزاره‌ای» متن:
Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015.
است.
■ دستگاه‌های بنداشتی دیگر
اگرچه دستگاه بنداشتی 𝓛 بسیار ساده است، اما بسیاری از دستگاه‌های دیگر نیز هستند که همین کار را انجام دهند. ما می‌توانیم به جای ¬ و ⇒ از هر مجموعه‌ای از رابط‌های منطقی آغازی، تا وقتی این رابط‌ها کفایت تعریف همه رابط‌های تابع-ارزش (تمامیت کارکردی) را داشته باشند، استفاده کنیم. برای نمونه در ادامه جندین دستگاه را مرور خواهیم کرد.
■ دستگاه صوری L۱ (هیلبرت - آکرمن)↧.
Hilbert, D. and W. Ackermann (1950) Principles of Mathematical Logic. Chelsea.
• رابط‌های آغازی در L۱ عبارتند از ∨ و ¬.
• در L۱ از β ⇒ ς به عنوان کوتاه شده ¬β∨ς استفاده می‌شود.
• L۱ دارای چهار طرحواره بنداشتی به قرار زیر است:
۱- β ∨ β ⇒ β;
۲- β ⇒ β ∨ ς;
۳- β ∨ ς ⇒ ς ∨ β;
۴- (ς ⇒ δ) ⇒ (β ∨ ς ⇒ β ∨ δ).
• تنها قاعده استنتاج دستگاه L۱ قیاس استثنایی است.
تمرین (۵۴.۱): نتایج زیر را برای دستگاه L۱ ثابت کنید.
a. β ⇒ ς ⊢L۱ 𝞂 ∨ β ⇒ 𝞂 ∨ ς
b. ⊢L۱ (β ⇒ ς) ⇒ ((𝞂 ⇒ β) ⇒ (𝞂 ⇒ ς))
c. 𝞂 ⇒ β, β ⇒ ς ⊢L۱ 𝞂 ⇒ ς
d. ⊢L۱ β ⇒ β (یعنی, ⊢ L۱ ¬β ∨ β)
e. ⊢L۱ β ∨ ¬β
f. ⊢L۱ β ⇒ ¬¬β
g. ⊢L۱ ¬β ⇒ (β ⇒ ς)
h. ⊢L۱ β ∨ (ς ∨ 𝞂) ⇒ ((ς ∨ (β ∨ 𝞂)) ∨ β)
i. ⊢L۱ (ς ∨ (β ∨ 𝞂)) ∨ β ⇒ ς ∨ (β ∨ 𝞂)
j. ⊢L۱ β ∨ (ς ∨ 𝞂) ⇒ ς ∨ (β ∨ 𝞂)
k. ⊢L۱ (β ⇒ (ς ⇒ 𝞂)) ⇒ (ς ⇒ (β ⇒ 𝞂))
l. ⊢L۱ (𝞂 ⇒ β) ⇒ ((β ⇒ ς) ⇒ (𝞂 ⇒ ς))
m. β ⇒ (ς ⇒ 𝞂), β ⇒ ς ⊢L۱ β ⇒ (β ⇒ 𝞂)
n. β ⇒ (ς ⇒ 𝞂), β ⇒ ς ⊢ L۱ β ⇒ 𝞂
o. (قضیه استنتاج):
اگر Γ, β ⊢L۱ ς آنگاه Γ ⊢L۱ β ⇒ ς.
p. ς ⇒ β, ¬ς ⇒ β ⊢L۱ β
q. ⊢L۱ β اگر و تنها اگر β توتولوژی باشد.
■ دستگاه صوری L۲. (روسر ۳۹۵۲)↧
Rosser, J.B. (1953) Logic for Mathematicians. McGraw-Hill (second edition, Chelsea, 1978).
• ∧ و ¬ رابط‌های آغازی دستگاه L۲ هستند.
• در L۲ از β⇒ς به عنوان کوتاه شده ¬(β∧¬ς) استفاده می‌شود.
• L۲ دارای سه طرحواره بنداشتی به قرار زیر است:
۱- β ∨ β ⇒ β;
۲- β ∧ ς ⇒ β;
۳- (β ⇒ ς) ⇒ (¬(ς ∧ δ) ⇒ ¬(δ ∧ β)).
• تنها قاعده استنتاج دستگاه L۲ قیاس استثنایی است.
تمرین (۵۵.۱): نتایج زیر را برای دستگاه L۲ ثابت کنید.
a. β ⇒ ς, ς ⇒ δ ⊢L۲ ¬(¬δ ∧ β)
b. ⊢L۲ ¬(¬β ∧ β)
c. ⊢L۲ ¬¬β ⇒ β
d. ⊢L۲ ¬(β ∧ ς) ⇒ (ς ⇒ ¬β)
e. ⊢L۲ β ⇒ ¬¬β
f. ⊢L۲ (β ⇒ ς) ⇒ (¬ς ⇒ ¬β)
g. ¬β ⇒ ¬ς ⊢L۲ ς ⇒ β
h. β ⇒ ς ⊢L۲ δ ∧ β ⇒ ς ∧ δ
i. β ⇒ ς, ς ⇒ δ, δ ⇒ Ω ⊢L۲ β ⇒ Ω
j. ⊢L۲ β ⇒ β
k. ⊢L۲ β ∧ ς ⇒ ς ∧ β
l. β ⇒ ς, ς ⇒ δ ⊢L۲ β ⇒ δ
m. β ⇒ ς, δ ⇒ Ω ⊢L۲ β ∧ δ ⇒ ς ∧ Ω
n. ς ⇒ δ ⊢L۲ β ∧ ς ⇒ β ∧ δ
o. ⊢L۲ (β ⇒ (ς ⇒ δ)) ⇒ ((β ∧ ς) ⇒ δ)
p. ⊢L۲ ((β ∧ ς) ⇒ δ) ⇒ (β ⇒ (ς ⇒ δ))
q. β ⇒ ς, β ⇒ (ς ⇒ δ) ⊢L۲ β ⇒ δ
r. ⊢L۲ β ⇒ (ς ⇒ β ∧ ς)
s. ⊢L۲ β ⇒ (ς ⇒ β)
t. (قضیه استنتاج): اگر Γ, β ⊢L۲ ς آنگاه Γ ⊢L۲ β ⇒ ς.
u. ⊢L۲ (¬β ⇒ β) ⇒ β
v. β ⇒ ς, ¬β ⇒ ς ⊢L۲ ς
w. ⊢L۲ β اگر و تنها اگر توتولوژی باشد.
■ دستگاه صوری L۳.
• دستگاه صوری L۳ دقیقاً مانند دستگاه 𝓛 است، با این تفاوت که، L۳ به جای طرحواره‌های بنداشتی A۱ – A۳، دارای سه مورد بنداشت مشخص است، که عبارتند از:
۱- p۱ ⇒ (p۲ ⇒ p۱);
۲- (p۱ ⇒ (p۲ ⇒ p۳)) ⇒ ((p۱ ⇒ p۲) ⇒ (p۱ ⇒ p۳));
۳- (¬p۲ ⇒ ¬p۱) ⇒ ((¬p۲ ⇒ p۱) ⇒ p۲).
• افزون بر قیاس استثنایی، قاعده جایگزینی↝ نیز در L۳ برقرار است. یعنی، می‌توانیم هر فرمولی در L۳ را برای همه موارد رویداد یک حرف گزاره‌ای در یک فرمول داده شده جایگزین کنیم.
تمرین (۵۶.۱): نشان دهید که نظریه L۳ همان قضایای نظریه 𝓛 را دارد.
■ دستگاه صوری L۴. (کلین ۱۹۵۲)↧
Kleene, S.C. (1952) Introduction to Metamathematics. Van Nostrand.
• رابط‌های آغازی در دستگاه صوری L۴ عبارتند از ⇒ و ∧, ∨, ¬.
• تنها قاعده استنتاج دستگاه L۴ قیاس استثنایی است.
• ده طرحواره بنداشتی در L۴ عبارتند از:
۱- β ⇒ (ς ⇒ β);
۲- (β ⇒ (ς ⇒ δ)) ⇒ ((β ⇒ ς ) ⇒ (β ⇒ δ));
۳- β ∧ ς ⇒ β ;
۴- β ∧ ς ⇒ ς;
۵- β ⇒ (ς ⇒ (β ∧ ς ));
۶- β ⇒ (β ∨ ς );
۷- ς ⇒ (β ∨ ς );
۸- (β ⇒ δ) ⇒ ((ς ⇒ δ) ⇒ (β ∨ ς ⇒ δ));
۹- (β ⇒ ς ) ⇒ ((β ⇒ ¬ς ) ⇒ ¬β);
۱۰ ¬¬β ⇒ β.
■ تمرین (۵۷.۱): عبارت‌های زیر را برای دستگاه L۴↝ نتیجه بگیرید.
a. ⊢ L۴ β ⇒ β
b. اگر Γ, β ⊢ L۴ ς آنگاه Γ ⊢ L۴ β ⇒ ς. (قضیه استنتاج)
c. β ⇒ ς, ς ⇒ δ ⊢ L۴ β ⇒ δ
d. ⊢ L۴ (β ⇒ ς) ⇒ (¬ς ⇒ ¬β)
e. β, ¬β ⊢ L۴ ς
f. ⊢ L۴ β ⇒ ¬¬β
g. ⊢ L۴ ¬β ⇒ (β ⇒ ς)
h. ⊢ L۴ β ⇒ (¬ς ⇒ ¬(β ⇒ ς))
i. ⊢ L۴ ¬β ⇒ (¬ς ⇒ ¬(β ∨ ς))
j. ⊢ L۴ (¬ς ⇒ β) ⇒ ((ς ⇒ β) ⇒ β)
k. ⊢ L۴ β اگر و تنها اگر β توتولوژی باشد.
■ دستگاه لوکاسیویچ
[تمرین ۵۸.۱] بنداشت‌های زیر را برای حساب گزاره ای L (از لوکاسیویچ / Lukasiewicz) در نظر بگیرید. L همان فرمول‌های دستگاه 𝓛 را دارد. تنها قاعده استنتاج آن قیاس استثنایی است. طرحواره‌های بنداشتی آن عبارتند از:
a. (¬β ⇒ β) ⇒ β
b. β ⇒ (¬β ⇒ ς)
c. (β ⇒ ς) ⇒ ((ς ⇒ δ) ⇒ (β ⇒ δ)).
ثابت کنید که فرمول β از L در L اثبات شدنی است اگر و فقط اگر β یک توتولوژی باشد.
[راهنمایی: نشان دهید که 𝓛 و L قضایای یکسانی دارند. با این حال، به یاد داشته باشید که هیچ یک از نتایج اثبات شده در مورد 𝓛 به طور خودکار به L منتقل نمی‌شود. به ویژه، قضیه استنتاج تا زمانی که برای L ثابت نشود در دسترس نیست.]
■ دستگاه‌های صوری تک بنداشتی
بنداشتی کردن را برای حساب گزاره‌ای می‌توان طوری انجام داد که فقط یک طرحواره بنداشتی داشته باشد. برای مثال، اگر ¬ و ⇒ رابط‌های آغازی و قیاس استثنایی تنها قاعده استنتاج باشند آنگاه، طرحواره بنداشتی زیر
[(((β⇒ς) ⇒ (¬δ⇒¬β)) ⇒ δ) ⇒ γ] ⇒ [(γ⇒ β) ⇒ (ε⇒β)]
بسنده است☚↧.
Meredith, C.A. (1953) Single axioms for the systems (C,N), (C,O) and (A,N) of the two-valued propositional calculus. J. Comp. Syst., 3, 155–164.
یکی دیگر از پیکر‌بندی‌های تک بنداشتی، از نیکود - ↧ (۱۹۱۷) است، که تنها از رابط نفی اختیاری (↑) استفاده می‌کند. قاعده استنتاج آن چنین است:
Nicod, J.G. (1917) A reduction in the number of primitive propositions of logic. Proc. Camb. Philos. Soc., 19, 32–41.
δ را می‌توان از β ↑ (ς ↑ δ) و β به دست آورد و طرحواره بنداشتی آن عبارت است از:
(β ↑ (ς ↑ δ)) ↑ {[ε ↑ (ε ↑ ε)] ↑ [(γ ↑ ς) ↑ ((β ↑ γ) ↑ (β ↑ γ))]}
اطلاعات بیشتر، از جمله پیشینه تاریخی را می‌توان در چرچ↧ (۱۹۵۶) و در مقاله لوکاسیویچ و تارسکی در تارسکی↧ (۱۹۵۶، IV) یافت.
• Church, A. (1956).Introduction to Mathematical Logic I. Princeton.University Press.
• Tarski, A. (1956) Logic, Semantics, Metamathematics. Oxford University Press (second edition, 1983, J. Corcoran (ed.), Hackett).
■ منطق شهودی (Intuitionistic logic)
[* این بند در متن اصلی↧ تحت عنوان «تمرین 1.60. pg 42» آمده است، در اینجا با اندک افزوده در قالب متن آمده است.*]
Mendelson, Elliott. Introduction to mathematical logic. 6th,ed, CRC Press, Taylor & Francis Group. 2015.
خاستگاه اصلی منطق گزاره‌ای شهودی بنا شده بر اندیشه فیلسوف ریاضیدان هلندی ال.ای.جی برووِر↧ (۱۸۸۱-۱۹۶۶ / L.E.J. Brouwer) است.
*- Brouwer,. L.E.J.. (1976). Collected Works. Vol.. 1,. Philosophy. and. Foundations. of. Mathematics. North-Holland.
بروور بر اساس فلسفه ذهنی که گستراند و تاثیر کانت و شوپنهاور بر آن آشکار بود، ریاضیات را عمدتاً به عنوان فعالیت آزاد اندیشه ورزی ژرف و درونی (در واقع خود تفکر) توصیف می‌کرد. از آنجایی که از دیدگاه برووِر، هیچ عامل تعیین کننده‌ای برای درستی (صدق) ریاضی خارج از فعالیت تفکر وجود ندارد، یک گزاره تنها زمانی درست است که موضوع (گزاره) درستی خود را (با انجام / اجرای سازه ذهنی سازوار) تجربه کرده باشد. به همین ترتیب، یک گزاره تنها زمانی نادرست است که موضوع (گزاره) نادرست بودن خود را (با درک اینکه اجرای سازه ذهنی سازوار امکان پذیر نیست) تجربه کرده باشد. حاصل چنین گرایشمندی ریاضیات شهودی (ریاضیات ساخت‌گرا / سازا / Constructive Mathematics) بود.
منطق شهودی برمبنای چنین شهودگرایی در ریاضیات و کار زدن چنین ریاضیاتی در زبان معرفی و تعبیر می‌شود.↧ پائین‌تر در بند (ب) خواهیم دید که اصل طرد شق وسط در منطق شهودی به عنوان یک اصل برقرار نیست. به عبارت دیگر β∨¬β وقتی ثابت می‌شود که برهانی برای β یا ¬β وجود داشته باشد.
آرند هیتینگ (Arend Heyting) به عنوان شاگرد بروور، نقش بنیادی در تدوین فرمالیسم منطق شهودی داشت.
• Heyting, A. (1956). Intuitionism: An introduction (Studies in logic and the foundations of mathematics) North-Holland, (third revised edition, 1971).
نیز:
• Kleene,.S.C..(1952).Introduction to Metamathematics. Van.Nostrand.
• Troelstra,. A.S. and. D. van. Dalen. (1988) Constructivism in Mathematics, Vols. 1–2. Elsevier
• Dummett, M. (1977) Elements of Intuitionism. Oxford University Press.
• Jaśkowski, S (1936) Recherches sur le système de la logique.intuitioniste. Acta Sci. Ind., Paris, 393, 58–61.
از جمله حوزه‌های کاربردی منطق شهودی علوم کامپیوتر (نظریه توابع بازگشتی - زبان‌های تابعی) است. توضیح آنکه، زبان‌های برنامه نویسی تابعی عموماً بر بنیاد نظریه گونه‌ها (Type theory) هستند که خود مبتنی بر منطق شهودی است. منطق شهودی اجازه می‌دهد گونه‌های با توان گویاگری و انعطاف بیشتر از منطق کلاسیک در اختیار داشت.↧
https://stackoverflow.com/questions/399312/what-is-hindley-milner
■ بنداشت‌ها در منطق شهودی
اگر طرحواره بنداشتی (۱۰) در دستگاه L۴↝ (یعنی، ¬¬β⇒β) با طرحواره (۱۰)′ در زیر جایگزین شود:
¬β ⇒ (β ⇒ ς),
آنگاه سیستم جدید LI، منطق گزاره‌ای شهودی (Intuitionistic propositional logic) نامیده می‌شود. بنابراین، طرحواره‌ها بنداشی LI عبارتند از:
۱- β ⇒ (ς ⇒ β);
۲- (β ⇒ (ς ⇒ δ)) ⇒ ((β ⇒ ς ) ⇒ (β ⇒ δ));
۳- β ∧ ς ⇒ β ;
۴- β ∧ ς ⇒ ς;
۵- β ⇒ (ς ⇒ (β ∧ ς ));
۶- β ⇒ (β ∨ ς );
۷- ς ⇒ (β ∨ ς );
۸- (β ⇒ δ) ⇒ ((ς ⇒ δ) ⇒ (β ∨ ς ⇒ δ));
۹- (β ⇒ ς ) ⇒ ((β ⇒ ¬ς ) ⇒ ¬β);
۱۰ ¬β ⇒ (β ⇒ ς).
■ برخی ویژگی‌ها و قضیه‌های منطق شهودی
تمرین (۶۰.۱):
نتایج زیر را در مورد LI ثابت کنید.
آ.یک منطق چند(n + ۱) ارزشی با رابط‌های زیر در نظر را بگیرید:
¬β مقدار ۰ بگیرد وقتی β مقدار n را بگیرد و در غیر این صورت مقدار آن n باشد.
β ∧ ς حداکثر مقادیر β و ς را بگیرد.
β ∨ ς حداقل مقادیر β و ς را بگیرد.
β ⇒ ς مقدار ۰ بگیرد اگر β مقداری کمتر از ς نداشته باشد و در غیر این صورت همان مقدار ς را بگیرد.
نشان دهید اگر ۰ را به عنوان تنها مقدار گزیده در نظر بگیریم، تمام قضایای LI استثنایی هستند.
ب. A۱ ∨ ¬A۱ و ¬¬A۱ ⇒ A۱ قضیه‌های LI نیستند.
ج. برای هر m فرمول زیر قضیه LI نیست:
(A۱⇔A۲)∨ ... ∨(A۱⇔Am)∨(A۲⇔A۳)∨ ... ∨(A۲⇔Am)∨ ... ∨(Am-۱⇔Am)
د. (گودل، ۱۹۳۳↧) LI برای برای هر منطق چند ارزشی متناهی سازوار نیست.
Gödel,. K.. (1933). Zum. intuitionistischen. Aussagenkalkül;. Zur. intuitionistischen. Arithmetik.und.Zahlentheorie..Ergeb. Math. Koll., 4,.34–38.and.40.(translation. in.Davis,.1965).
ه.
۱- اگر Γ, β ⊢LI ς آنگاه Γ ⊢LI β ⇒ ς. (قضیه استنتاج)
۲- (β ⇒ ς, ς ⇒ δ) ⊢LI β ⇒ δ
۳- ⊢LI β ⇒ ¬¬β
۴- ⊢LI (β ⇒ ς) ⇒ (¬ς ⇒ ¬β)
۵- ⊢LI β ⇒ (¬β ⇒ ς)
۶- ⊢LI ¬¬(¬¬β ⇒ β)
۷- [¬¬(β ⇒ ς), ¬¬β] ⊢LI ¬¬ς
۸- ⊢LI ¬¬¬β ⇒ ¬β
ز. ⊢LI ¬¬β اگر و فقط اگر β یک توتولوژی باشد.
ح. ⊢LI ¬β اگر و فقط اگر ¬β یک توتولوژی باشد.
ط. اگر β فقط شامل رابط‌های ∨ و ¬ باشد آنگاه ⊢LIβ اگر و فقط اگر β یک توتولوژی باشد.
■ جبر لیندنباوم (Lindenbaum algebra)
جبر لیندنباوم (در واقع جبر لیندنباوم تئوری↝ T) که به جبر لیندنباوم-تارسکی (Lindenbaum-Tarski algebra) نیز مشهور است، از جمله انگاره‌ها در منطق ریاضی است. این نام برگرفته از منطق‌دانان آدولف لیندنباوم (Adolf Lindenbaum) و آلفرد تارسکی (Alfred Tarski) است. جبر لیندنباوم برای تئوری↝ T شامل کلاس‌های هم‌ارزی در T (کلاس خارج قسمت T) است
■ تمرین (۶۱.۱)
فرض کنید B و C در رابطه R باشند اگر و فقط اگر ⊢L B ≡ C.
a. نشان دهید که R یک رابطه هم‌ارزی است.
با توجه به کلاس‌های هم‌ارزی [B] و [C]، قرارداد می‌کنیم:
[B] ∪ [C ] = [B ∨ C],
[B] ∩ [C] = [B ∧ C]
و
[] = [¬B].
b. نشان دهید که کلاس‌های هم‌ارزی تحت R یک جبر بول را با توجه به ∩، ∪، و متمم () تشکیل می‌دهند. این جبر که توسط L معین می‌شود، جبر↧ (Lindenbaum) L* [جبر لیندنباوم] نامیده می‌شود.
https://en.wikipedia.org/wiki/Lindenbaum–Tarski_algebra
عنصر 0 درL* کلاس هم‌ارزی است که از همه تناقض‌ها (یعنی نقیض توتولوژی‌ها) تشکیل شده است. عنصر 1 در L* کلاس هم‌ارزی است که از تمام توتولوژی‌ها تشکیل شده است. توجه کنید که ⊢LB≡C اگر و فقط اگر در L* داشته باشیم:
[B] ≤ [C]،
و
⊢L B ⇔ C اگر و فقط اگر [B] = [C] باشد.
c. نشان دهید که یک تابع بولی f (که از متغیرهای 0 و 1 با استفاده از ∪، ∩، و -) ساخته می‌شود برابر است با تابع ثابت 1 در تمام جبرهای بول اگر و فقط اگر داشته باشیم ⊢Lf#، که در آن f# از f با جایگزینی
∪، ∩، −، 0، و 1
به ترتیب برای
∨، ∧، ¬، A۱ ∧ ¬A۱ و A۱ ∨ ¬A۱.
به دست می‌آید.
