مقدمه‌ای غیر فرمال بر سیستم‌های فرمال

بیان کردن همه‌ی چیزهای درست¹ کار خیلی سختیه، برای همین فلاسفه و ریاضی‌دان‌ها روش‌های مختلفی رو ارائه دادن که به جای لیست کردن همه چیزهایی که درسته، بشه همه چیزهای درست رو نتیجه گیری کرد. از این بین، کارآمدترین روش روشیه که هیلبرت² توی ربع اول قرن بیستم ارائه داد، به اسم دستگاه صوری یا سیستم‌های فرمال³.

این روش یک سری قوانین پایه و یک سری قانون نتیجه گیری به شما میده و میگه هر چیزی که از این سیستم نتیجه بشه درسته، و عملا با تعداد محدودی گزاره مقدار معمولا نامتناهی گزاره رو بیان می‌کنه. مشابه چیزی که منطق می‌گه، که اگر پیش‌فرض‌های یک اثبات رو بپذیریم و فرایند اثبات درست باشه، نتیجه هم درسته، منتها فرقشون اینه که اثبات در منطق برای یک یا چند گزاره است، درحالی که یک سیستم فرمال هدفش لیست کردن همه گزاره‌های درست هست.

بذارید قبل از این که بیشتر در موردشون حرف بزنیم یک نمونه ساده نشونتون بدم. با اعداد فیبوناچی آشنایی دارید، می‌خوایم یک سیستم فرمال درست کنیم که این دنباله رو لیست کنه، به عبارت دیگه گزاره‌های این سیستم فرمال به ما می‌گن عدد k ام دنباله فیبوناچی چی هست. خب این سیستم چطوری تعریف میشه؟

fib 0 = 0
fib 1 = 1
fib n+1 = fib n + fib n-1

صفرمین عدد فیبوناچی عدد صفر هست و یکمین عدد فیبوناچی عدد یک، بعد از اون عدد n+1م رو با جمع کردن اعداد n و n-1 می‌تونیم به دست بیاریم.

اگر بخوایم یک سیستم فرمال درست کنیم که همه اعداد زوج رو لیست کنه چی‌کار می‌کنیم؟ دو تا قاعده ساده تعریف می‌کنیم، اول این که ۲ زوج هست، و بعد اگر n عدد طبیعی باشه، ۲×n هم زوج هست.

حالا اگر بخوایم سیستمی درست کنیم که همه فرمول‌های منطقی رو قبول کنه چی باید بنویسیم؟

p, q, r, s, t are all P
if x is P, then so is not x.
if x and y are P, then so are (x and y), (x or y) and (x -> y).

که البته میشه تعداد متغییرها رو بیشتر کرد یا به کل الفبا تعمیم داد. حالا با این قواعد چطوری میشه مثلا فرمول (p and not q) -> (r or s) رو بیان کرد؟

اول می‌دونیم که p q r s همه فرمول هستند. با توجه به قاعده دوم، میشه not q رو هم فرمول خطاب کرد. حالا با قاعده سوم، p and not q و r or s هم فرمول به حساب میان. در نهایت، دوباره با قاعده سوم کل ساختار رو تولید می‌کنیم. نکته اینه که توی این ساختار درستی به معنای «فرمول منطقی قابل پارس کردن» هست و مثلا p or or رو فرمول حساب نمی‌کنه. ممکنه جاهای دیگه‌ای باشه که روی فرمول‌های منطقی حرف بزنن اما درستی معنای دیگه‌ای داشته باشه، مثلا «فرمول منطقی‌ای که مقدارش صحیح باشه» که خب قواعد پیچیده‌تری نیاز داره.

---