معرفي معناشناسي‌هاي مختلف براي منطق شهودي

Introduction of different semantics for intuitionistic logic

منطق شهودي گزاره‌اي منطقي غيركلاسيك است كه از حذف اصل طرد شق ثالث از منطق كلاسيك حاصل مي‌شود. چند معناشناسي مختلف، مانند معناشناسي كريپكي، توپولوژيكي و همسايگي براي منطق شهودي گزاره‌اي وجود دارد كه قضاياي درستي و تماميت براي آنها اثبات شده است. در اين مقاله ابتدا برخي از اين معناشناسي‌ها رابررسي مي‌كنيم، سپس دو معناشناسي همسايگي جديدي را كه يكي از اين معناشناسي‌ها تا حدي پيچيده‌تر از معناشناسي‌هاي همسايگي شناخته شده قبلي مي‌باشد را براي منطق گزاره‌اي شهودي (IPC) معرفي مي‌كنيم. در نهايت قضاياي درستي و تماميت را با روشهاي متفاوتي نسبت به اين دو معناشناسي همسايگي جديد اثبات مي‌كنيم. براي اثبات تماميت يكي از اين معناشناسي‌ها كه NB-همسايگي مي‌ناميم، ابتدا نياز داريم تا دستگاه زيرشهودي WF را كه ضعيف‌تر از دستگاههاي زير شهودي شناخته شده قبلي مانند F مي‌باشد را معرفي ‌كنيم. سپس با استفاده از قصيه تماميت منطق WF نسبت به معناشناسي NB-همسايگي، نشان خواهيم داد كه منطق شهودي IPC نسبت به اين معناشناسي با افزودن برخي ويژگي‌هاي خاص درست و تمام است.

Intuitionistic logic is a non-classical logic obtained by omitting the axiom of excluded middle from classical logic. This logic was created by philosophical motivation towards the foundation of mathematics. There are several semantics for intuitionistic logic (such as Kripke semantics, neighborhood semantics and topological semantics) that are sound and complete. In this paper, we first present two new neighborhood semantics for propositional intuitionistic logic (IPC). Then we establish soundness and completeness of IPC with respect to these new neighborhood semantics. The relation between neighborhood and topological semantics are also investigated. One of these new neighborhood semantics is introduced with a somewhat more complex definition than the usual neighborhood semantics which was introduced before. This semantics is called NB-neighborhood semantics. In order to establish completeness with respect to NB-neighborhood semantics for IPC, first we need to introduce a system WF of subintuitionistic logic, weaker than Corsi's basic subintuitionistic system F.