پیش‌درآمد: سفر هیلبرت و منطق مرتبه اول

اوایل قرن بیستم، دیوید هیلبرت—یکی از بزرگ‌ترین ریاضی‌دان‌های وقت—آرزویی بزرگ در سر داشت: این‌که بتواند تمام ریاضیات را تبدیل کند به یک زبان کاملاً رسمی و دقیق از نمادها و قواعدی که از آن‌ها، بدون هیچ حدس و گمانی، همهٔ نتیجه‌های ریاضی را بشود مثل یک دستور کامپیوتری استخراج کرد. هیلبرت می‌خواست زبانی بسازد که هیچ جا برای ابهام یا تفاسیر شخصی نباشد و بشود با روش‌های ساده و کاملاً مطمئن، درستی آن را اثبات کرد.

دستگاهِ صوری (formal system) یعنی یک چارچوب انتزاعی که دو چیز اصلی دارد:
- زبان صوری: مجموعه‌ای از نمادها (حروف، علامت‌ها) و قواعدی که می‌گوید چطور این نمادها را کنار هم بگذاری.

- قواعد استنتاج: دستورالعملی که مشخص می‌کند چطور می‌توانی با استفاده از چند اصل اولیه (axioms)، گزاره‌های جدید تولید کنی.

وقتی با این چارچوب کار می‌کنی، فقط به شکل ظاهری عبارات (syntactic) نگاه می‌کنی—یعنی دنباله‌ای از نمادها—و کاری به «معنی» پشت‌شان نداری، اما در عوض می‌توانی ساختار منطقی و استدلال ریاضی را دقیق ببینی.

هستهٔ کارِ هیلبرت منطق مرتبهٔ اول (first-order logic) بود. این منطق چیزهایی مثل «∀» به‌معنای «برای هر» و «∃» به‌معنای «وجود دارد» را معرفی می‌کند تا بتوانی دربارهٔ عناصر یک مجموعه (مثلاً اعداد یا نقاط) صحبت کنی. فرقش با منطق‌های قوی‌تر این است که فقط می‌توانی دربارهٔ خودِ عناصر کمّی‌سازی (quantify) کنی، نه دربارهٔ «همهٔ خواص» یا توابع. این‌کار باعث می‌شود هم زبان رسمی، قابل فهم و هم تا حدی تصمیم‌پذیر (decidable) باشد. مثلاً می‌نویسیم:

∀x (Prime(x) → ∃y (Prime(y) ∧ y > x))

یعنی «برای هر عدد اول x، عدد اول بزرگ‌تری به نام y وجود دارد.»

سال ۱۹۲۸، هیلبرت و همکارش ویلهم آکرمن پرسیدند: آیا می‌شود یک برنامه یا الگوریتم ساخت که برای هر جمله در منطق مرتبهٔ اول بگوید «در همهٔ شرایط درسته» یا «نیست»؟ اگر جواب مثبت بود، می‌توانستیم همهٔ ریاضیات را با اجرای یک برنامه رایانه‌ای حل کنیم.

اما در ۱۹۳۶، آلونزو چرچ ثابت کرد که چنین الگوریتمی وجود ندارد. او ثابت کرد که این سؤال به مسائل غیرقابل‌حلِ دیگری مثل lambda calculus می‌رسد. تقریباً هم‌زمان، آلن تورینگ با مفهوم «ماشین تورینگ» به همان نتیجه رسید: هیچ روش کامپیوتری‌ای نیست که بتواند همهٔ جملات منطق مرتبهٔ اول را بررسی کند.

این دو کشف، پایهٔ نظریهٔ محاسبات مدرن را گذاشت و نشان داد که برنامهٔ بزرگ هیلبرت—ساختن یک دستگاه کاملاً مکانیزه برای همهٔ ریاضیات—به طور ذاتی محدود است. اما در عوض، فهم عمیقی از ماهیت محاسبه و مرزهای آن به ما داد و مسیر را برای پیدایش علم رایانه هموار کرد.

#بخش1