منطق محمولات و نظریه مدل: پیشنیازهای فراقضیه تمامیت
منطق و فرامنطق
درآمد به منطق
منطق محمولات: پیشنیازهای فراقضیه تمامیت
۱- مقدمه | ۱۱- دو تعریف: تئوری تمام و گسترش یک تئوری |
۲- فرا-قضیههای تمامیت | ۱۲- تعریف: تئوری بازگشتی (Recursive theory) |
۳- تعریف: یکجوری (similarity) | ۱۳- قضیه ۲.۱۴ (لم لیندنباوم - Lindenbaum’s Lemma) اگر K یک تئوری سازگار باشد، آنگاه یک گسترش تمام و سازگار برای K وجود دارد. |
۴- لم. ۲.۱۱ | ۱۴- تمرین |
۵- تمرین | ۱۵- چند تعریف: ۱- ترم بسته، ۲- تئوری سپربلا (بلاگردان) |
۶- لم. ۲.۱۲ | ۱۶- لم ۲.۱۵ |
۷- نتیجه مهم | ۱۷- لم ۲.۱۶ |
۸- لم ۲.۱۳ مجموعه عبارتهای یک زبان `cc"L"` شمارا است. | ۱۸- قضیه ۲.۱۷. هر تئوری سازگار K دارای یک مدل شمارا است. |
۹- برشمارش قضیههای تئوری | ۱۹- قضیه ۲.۱۸ هر فرمول منطقاً معتبر `cc"B"` از یک تئوری K قضیه K است. |
۱۰- تصمیمناپذیری قضیههای تئوری مرتبه اول |
مگر در مواردی که با نماد "
" مشخص شده باشد، محتوای ارائه شده در این یادداشت از مرجع زیر برگرفته و برگردان شده است.
Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015. p. ۸۲-۸۹. ↜
۱- مراد از مجموعه شمارا (Denumerable set) یک مجموعهای شمارای نامتناهی است مگر آنکه با صراحت قید شده بشد.
■ مقدمه
در ادامه قسمت قبل، یعنی «منطق محمولات: برخی ویژگیهای تئوریهای مرتبه اول»، این قسمت، ژرفتر به منطق مرتبه اول (FOL) میپرادزد و بر ارائه قضایا و لمهایی متمرکز میشود که پیش نیازهای ضروری برای درک قضیه تمامیت هستند. این نتایج بنیادی نقش مهمی در ایجاد زمینه برای اثبات تمامیت ایفا میکنند که تمرکز اصلی قسمت بعدی خواهد بود. با تکیه بر مفاهیم و نتایج معرفی شده در اینجا، اثبات قضیه تمامیت (در منطق مرتبه اول) را در قسمت بعدی نشان خواهیم داد.
■ فرا-قضیههای تمامیت
میخواهیم نشان دهیم که قضیههای یک حساب محمولات مرتبه K دقیقاً مانند فرمولهای منطقاً معتبر K است. نیمی از این نتیجه در اثبات قضیه ۲.۲ انجام شد [قضیه ۲.۲: هر قضیه یک حساب محمولات مرتبه اول منطقاً معتبر است]. نیمی دیگر[↝] از یک قضیه بسیار کلیتر که بعداً خواهیم دید (قسمت بعدی)، نتیجه میشود. اما، پیشتر باید چند لم مقدماتی را اثبات کنیم.
■ تعریف: یکجوری (similarity)
اگر `x_i` و `x_j` متمایز باشند، آنگاه گوییم: `cc"B"(x_i)` و `cc"B"(x_j)` یکجور هستند اگر و فقط اگر `x_j` برای `x_i` در `cc"B"(x_i)` آزاد↝ باشد و `cc"B"(x_i)` دارای رویداد آزاد `x_j` نداشته باشد. در اینجا چنین فرض شده که `cc"B"(x_j)` از `cc"B"(x_i)` با جایگزینی `x_j` به جای تمام رویدادهای آزاد `x_i` بدست آمده باشد.
آشکار است که، اگر `cc"B"(x_i)` و `cc"B"(x_j)` یکجور باشند، آنگاه `x_i` برای `x_j` در `cc"B"(x_j)` آزاد است و `cc"B"(x_j)` هیچ رویداد آزاد `x_i` ندارد. بنابراین، اگر `cc"B"(x_i)` و `cc"B"(x_j)` یکجور باشند، `cc"B"(x_j)` و `cc"B"(x_i)` یکجور هستند.
به طور شهودی، `cc"B"(x_i)` و `cc"B"(x_j)` یکجور هستند اگر و فقط اگر `cc"B"(x_i)` و `cc"B"(x_j)` یکسان باشند با این تفاوت که `cc"B"(x_i)` دقیقاً در جاهایی که `cc"B"(x_j)` دارای رویداددهای آزاد `x_j` است، رویدادهای آزاد `x_i` دارد.
مثال:
`(∀x_۳ )[A_۱^۲(x_۱,x_۳)∨ A_۱^۱(x_۱)] `
و
`(∀x_۳ )[A_۱^۲(x_۲,x_۳)∨ A_۱^۱(x_۲)] `
یکجور هستند.
■ لم. ۲.۱۱
اگر `cc"B"(x_i)` و `cc"B"(x_j)` یکجور باشند، آنگاه
`⊢(∀x_i)cc"B"(x_i)⇔(∀x_j)cc"B"(x_j)`.
برهان:
از (A۴) داریم: `⊢(∀x_i)cc"B"(x_i)⇒cc"B"(x_j)`.
اکنون از Gen: `⊢(∀xj)((∀x_i)cc"B"(x_i)⇒cc"B"(x_j))`،
و بنابراین، بنا به بنداشت (A۵) و MP: `⊢(∀x_i)cc"B"(x_i)⇒(∀x_j)cc"B"(x_j)`.
به طور مشابه، `⊢(∀x_j)cc"B"(x_j)⇒(∀x_i)cc"B"(x_i)`.
بنابراین، با وضع دو شرطی، `⊢(∀x_i)cc"B"(x_i)⇔(∀x_j)cc"B"(x_j)`.
■ تمرین
۲.۴۷ اگر `cc"B"(x_i)` و `cc"B"(x_j)` یکجور باشند، نشان دهید: `⊢(∃x_i)cc"B"(x_i)⇔(∃x_j)cc"B"(x_j)`.
۲.۴۸ تغییر متغیرهای پابند: اگر `cc"B"(x)` با `cc"B"(y)` یکجور باشد، `(∀x)cc"B"(x)` زیرفرمول `cc"C"` باشد و `cc"C"^′` نتیجه جایگزینی یک یا بیشتر رویداد `(∀x)cc"B"(x)` در `cc"C"` با `(∀y)cc"B"(y)` باشد، آنگاه نشان دهید: `⊢cc"C"⇔cc"C"′`..
■ لم. ۲.۱۲
اگر فرمول بسته `¬cc"B"` در یک تئوری K در K قابل اثبات نباشد، و اگر K' تئوریای باشد که با افزودن `cc"B"` به عنوان یک بنداشت جدید از K به دست آمده باشد، آنگاه K' سازگار است.
برهان:
`K'` را ناسازگار فرض میکنیم.
بنابراین، برای برخی از فرمول `cc"C"` داریم `⊢_{K^′} cc"C"` و `⊢_{K^′}¬cc"C"`.
اکنون بنا بر قضیه ۲.۱: `⊢_{K^′}cc"C"⇒(¬cc"C"⇒¬cc"B")`.
بنابراین، با دو کاربرد MP داریم: `⊢_{K^′}¬cc"B"`.
اکنون، هر استفاده از `cc"B"` به عنوان یک بنداشت در یک برهان `K'` را میتوان به عنوان یک فرض در برهان در `K` در نظر گرفت. بنابراین، `cc"B" ⊢_K¬cc"B"`.
از آنجا که `cc"B"` بسته است از نتیجه ۲.۷ داریم: `⊢_K cc"B"⇒¬cc"B"`.
اما از قضیه ۲.۱ داریم: `⊢_K (cc"B"⇒¬cc"B")⇒¬cc"B"`. و از اینجا، توسط MP داریم: `⊢_K¬cc"B"`، که این خلاف فرض ما است.
■ نتیجه مهم
اگر فرمول بسته `cc"B"` یک تئوری K در K قابل اثبات نباشد، و اگر K' تئوریای باشد که با افزودن `¬cc"B"` به عنوان یک بنداشت جدید از K به دست میآید، آنگاه K' سازگار است.
■ لم ۲.۱۳ مجموعه عبارتهای یک زبان `cc"L"` شمارا است.
[از این رو، این امر در مورد مجموعه ترمها، مجموعه فرمولها و مجموعه فرمولهای بسته نیز درست است.]
برهان:
[
شمار گذاری گودل را ببینید.]
ابتدا عدد صحیح مثبت متمایز `g(u)` را به هر نماد `u` به صورت زیر اختصاص دهید:
`g(()=3, g())=5, g(,) = 7, g(¬) = 9,`` g(⇒) = 11, g(∀) = 13,`` g(x_k) = 13 + 8k, ``g(a_k) = 7+8k, g(f_k^n)= 1+8(2^n3^k) , `` g(A_k^n)=3+8(2^n3^k)`.
سپس، به عبارتی مانند `u_0u_1...u_r` عدد `2^{g(u_0)}...p^{g(u_r)}` را نظیر کنید، که در آن `p_j` عبارت باشد از `j`امین عدد اول، که از `p_0=2` شروع شده باشد. (برای نمونه عدد نظیر شده به `A_1^1(x_2)` عبارت خواهد بود از `2^51 3^3 5^29 7^5`).
اکنون میتوانیم همه عبارتها را به ترتیب اعداد نظیرشده به آنها برشماریم. بنابراین، مجموعه عبارتها شمارا است.
■ برشمارش قضیههای تئوری
فرض کنید میتوانیم به بطور کارآمد بگوییم که آیا هر نماد مفروض نمادی از `cc"L"` است یا نه. در این صورت، برشمارش میتواند به طور کارآمد انجام شود، و علاوه بر این، میتوانیم به طور کارآمد تصمیم بگیریم که آیا هر عدد داده شده، عدد نظیر شدهای به یک عبارت `cc"L"` است یا نه. همین نیز برای ترمها، فرمولها و فرمولهای بسته نیز برقرار است.
فرض کنید تئوری K در زبان `cc"L"` بنداشی باشد. در این صورت، یعنی اگر بتوانیم به طور کارآمد تصمیم بگیریم که آیا هر فرمول داده شده یک بنداشت K است، آنگاه میتوانیم قضایای K را به طور کارآمد برشماریم. برای اینکار:
۱- با فهرستی که حاوی اولین بنداشت K از برشمارش مشخص شده است شروع کنید.
۲- در مرحله بعد، همه نتیجههای مستقیم دست آمده از بنداشتها توسط قاعده قیاس استثنایی (MP) و قاعده تعمیم (Gen) را به این فهرست اضافه کنید، که در آن Gen تنها یک بار و منحصراً با `x_1` به عنوان متغیر سوردار شده اعمال شده است.
۳- بنداشت دوم را به این فهرست جدید اضافه کنید. سپس همه نتیجههای مستقیم جدید فرمولهای موجود در این فهرست افزوده شده را با کارزدن MP و Gen بنویسید، که در آن Gen تنها یک بار با `x_1` و `x_2` به عنوان متغیر سوردار شده اعمال شده است.
۴- اگر در مرحله `k`ام، بنداشت `k`ام را افزوده و MP و Gen را به فرمول موجود در فهرست جدید بکار ببریم (در صورتی که Gen فقط یک بار برای هر یک از متغیرهای `x_1, ..., x_k` کار زده شود)، آنگاه سرانجام به این روش همه قضایای K را بدست خواهیم آورد.
■ تصمیمناپذیری قضیههای تئوری مرتبه اول
با این حال، در تقابل با موردهای عبارات، ترمها، فرمولها و فرمولهای بسته [ خوانش یکتای فرمول]، میتوان نشان داد که تئوریهای بنداشتی K وجود دارند که نمیتوانیم از قبل بگوییم آیا هر فرمول داده شدهای از K در نهایت در فهرست قضایا ظاهر میشود یا نه. [
به عبارت دیگر، قضیه بودن یک فرمول در تئوریهای مرتبه اول تصمیمپذیر ↝ ↝ نیست - و در واقع نیمی-تصمیمپذیر است. به عبارت دیگر، اگر فرمول دادهشده قضیه K نباشد برشمارش میتواند نامحدود ادامه یابد و پاسخ آری یا نه دریافت نکنیم.]
■ دو تعریف: تئوری تمام و گسترش یک تئوری
■ تعریف: تئوری بازگشتی (Recursive theory)
یک تئوری منطق مرتبه اول (FOL) بازگشتی است اگر و تنها اگر مجموعه بنداشتهای آن یک مجموعه بازگشتی باشد، به این معنی که یک روش کارآمد برای تصمیمگیری وجود دارد که آیا هر عبارت داده شده به مجموعه بنداشتها تعلق دارد یا خیر. بنابراین یک تئوری مرتبه اول با تعداد متناهی بنداشت بازگشتی است.
■ قضیه ۲.۱۴ (لم لیندنباوم - Lindenbaum’s Lemma) اگر K یک تئوری سازگار باشد، آنگاه یک گسترش تمام و سازگار برای K وجود دارد.
برهان:
فرض کنید `cc"B"_1, cc"B"_2,…` یک برشمارش از تمام فرمولهای بسته تئوری K توسط لم ۲.۱۳ باشد.
دنباله `\text{J}_0,\text{J}_1, \text{J}_2,…` از تئوریها را به روش زیر تعریف کنید:
`\text{J}_0` تئوری K باشد. نیز، فرض کنید `\text{J}_n` برای `n≥0` تعریف شده باشد.
اگر چنین نیست که `⊢_{\text{J}_n}¬cc"B"_{n+1}`، آنگاه `\text{J}_{n+1}` را دست آمده از `\text{J}_n` با افزودن `cc"B"_{n+1}` بهعنوان یک بنداشت اضافی بگیرید.
از طرف دیگر، اگر `⊢_{\text{J}_n}¬cc"B"_{n+1}`، آنگاه `\text{J}_{n+1}=\text{J}_n` را بگیرید.
`\text{J}` را تئوریای بگیرید که تمام بنداشتهای همه تئوریهای `\text{J}_i s` را به عنوان بنداشت داشته باشد.
آشکار است که `\text{J}_{i+1}` گسترش `\text{J}_i` است و `\text{J}` یک گسترش از همه `\text{J}_i s`ها، از جمله `\text{J}_0 = K` است.
برای نشان دادن اینکه `\text{J}` سازگار است، کافی است ثابت کنیم که هر `\text{J}_i` سازگار است چرا که اثبات یک تناقض در `\text{J}`، که فقط شامل تعداد محدودی از بنداشت است، در واقع، اثبات یک تناقض در برخی `\text{J}_i` است.
سازگاری `\text{J}_is` را با استقرا اثبات میکنیم. بنابر فرض، `\text{J}_0=`K سازگار است. فرض میکنیم `\text{J}_i` سازگار است. اکنون میگوییم:
اگر `\text{J}_{i+1}=\text{J}_i`، آنگاه `\text{J}_{i+1}` سازگار است.
اگر `\text{J}_i≠\text{J}_{i+1}`، پس، بنا بر تعریف تئوری `\text{J}_{i+1}` فرمول `¬cc"B"_{i+1}` در `\text{J}_i` قابل اثبات نیست. بنابراین، بنابر لم ۲.۱۲، `\text{J}_{i+1}` نیز سازگار است.
بنابراین، ثابت کردیم که همه `\text{J}_is`ها سازگار هستند و بنابراین: `\text{J}` سازگار است.
برای اثبات تمام بودن `\text{J}` فرض کنید `cc"C"` هر فرمول بستهای در K باشد. پس برای برخی `j≥0` داریم `cc"C"=cc"B"_{j+1}`.
اکنون، یا `⊢\text{J}_j¬cc"B"_{j+1}` یا `⊢_{\text{J}_{j+1}}cc"B"_{j+1}`، زیرا اگر اینگونه نباشد که `⊢_{\text{J}_j}¬cc"B"_{j+1}`، آنگاه `cc"B"_{j+1}` به عنوان یک بنداشت به `\text{J}_{j+1}` اضافه میشود.
بنابراین، یا `⊢_\text{J} ¬cc"B"_{j+1}` یا `⊢_Jcc"B"_{j+1}`. بنابراین، `\text{J}` تمام است.
توجه داشته باشید که حتی اگر بتوان به طور کارآمد تصمیم گرفت که آیا هر فرمولی در K یک بنداشت است یا نه، ممکن است نتوان این کار را با بنداشتهای `\text{J}` (یا حتی با برشمارش کارآمد) انجام داد. یعنی `\text{J}` ممکن است بنداشتی نباشد حتی اگر K بنداشتی باشد. این به دلیل امکان عدم امکان تشخیص در هر مرحله است که آیا `¬cc"B"_{n+1}` در `\text{J}_n` قابل اثبات است یا نه.
■ تمرین
۲.۴۹ نشان دهید نظریه K تمام است اگر و فقط اگر، برای هر فرمول بسته `cc"B"` و `cc"C"` در K، اگر `⊢_Kcc"B"∨cc"C"`، آنگاه `⊢_Kcc"B"` یا `⊢_Kcc"C"`.
حل:
K را تمام و `ccB` و `ccC` را فرمولهای بسته K بگیرید، به قسمی که `⊢_KccB∨ccC`.
فرض کنید چنین نیست که `⊢_KccB`. اکنون بنا به تمامیت داریم `⊢_K ¬ccB`. از این رو، توسط توتولوژی `¬A⇒((A∨ B)⇒B)` داریم `⊢_Kcc"B"`.
برعکس، فرض کنید K کامل نیست. پس یک جمله `cc"B"` در K هست که چنین نیست که `⊢_Kcc"B"` و چنین نیست که `⊢_K¬cc"B"`. اما، `⊢_K B∨¬B`.
۲.۵۰ ثابت کنید که هر نظریه تصمیمپذیر سازگار دارای یک گسترش سازگار، تصمیمپذیر و تمام است.
حل:
رجوع کنید به:
Tarski, A., A. Mostowski, and R. Robinson (1953) Undecidable Theories. North-Holland. Tarski, A. and R.L. Vaught (1957) Arithmetical extensions of relational systems. Comp. Math., 18, 81–102.
■ چند تعریف: ۱- ترم بسته، ۲- تئوری سپربلا
یک تئوری K یک تئوری سپربلا (تئوری بز سپربلا ↝ / تئوری بلاگردان) است (scapegoat theory)* اگر برای هر فرمول `cc"B(x)` که `x` را به عنوان تنها متغیر آزاد خود دارد، یک ترم بسته `t` وجود داشته باشد به قسمی که:
`⊢_K (∃x)¬cc"B"(x)⇒¬cc"B"(t)`.
*- اگر یک تئوری سپریلا فرض کند که ویژگی B حداقل برای یک شی ناکام است، باید یک نام (یعنی یک ترم بسته سازوار `t`) برای یک شی خاص وجود داشته باشد که B به طور اثباتپذیر برای آن ناموفق باشد. بنابراین، `t` نقش یک بزغاله (goat) را به معنای معمول آن را بازی میکند. بسیاری از تئوریها فاقد منابع زبانی (ثابتهای انفرادی و حروف تابعی) برای تئوریهای سپریلا هستند، اما مفهوم تئوری سپریلا برای اثبات برخی ویژگیهای ژرف تئوریهای مرتبه اول بسیار مفید خواهد بود.

از ویژگیهای تعیینکننده این تئوری (سپربلا) این است که اگر گزارهای در مورد یک فرد نامشخص بیان شود - در مورد `x`ای ناشناس - این تئوری تضمین میکند که میتوانیم یک مورد مشخص و یافتنی پیدا کنیم که "نقش سپر بلا را بر عهده بگیرد".
فرض کنید در دستگاه K هستیم و `cc"B"(x)` را داریم. این `cc"B"(x)` مانند یک ویژگی یا شرحی بر `x` است، که در آن `x` فقط یک جایبان برای چیزهایی (که معلوم نیست چه هستند) است که ما در مورد آن صحبت میکنیم.
در اینجا نقش سپربلا به میان میآید، یعنی وقتی که این تئوری میگوید:
اگر چنین است که هیچ `x`ای `cc"B"(x)` را برنمیآورد، به عبارت دیگر، `(∃x)¬cc"B"(x))`، آنگاه میتوانم یک «مورد» خاص را نام ببرم که در آن `cc"B"(t)` قطعاً نادرست است.
دنباله نمادهای صوری `(∃x)¬cc"B"(x)⇒¬cc"B"(t)` فقط میگویند: اگر نظریه K ثابت کند که "برخی `x` وجود دارد که `cc"B"(x)` نادرست است،" آنگاه نظریه همچنین میتواند به صراحت یک شی خاص `t` را بیابد کند به قسمی که `cc"B"(t)` برای آن نادرست است. این ساختار تضمین میکند که همیشه میتوانیم یک نمونه خاص را تعیین کنیم، نه اینکه فقط در مورد احتمال حرف بزنیم.
در واقع، `⊢_K (∃x)¬cc"B"(x)⇒¬cc"B"(t)` یر آن است تا با یک سور وجودی رفتار یک سور عمومی را داشته باشد [`⊢_K cc"B"(t) ⇒ (∀x)cc"B"(x)`]. تمرین ۲.۶۳.ج نشان میدهد یک تئوری مرتبه اول یک تئوری سپربلا نیست.
■ لم ۲.۱۵
هر تئوری سازگار K یک گسترش سازگار K' دارد، به قسمی که K' یک تئوری سپربلا است و K' دارای بسیار ترم بسته شمارا است.
برهان:
به نمادهای K مجموعه شمارا `{b_1، b_2، …}` از ثابتهای انفردی جدید اضافه کنید. این تئوری جدید را `\text{K}_0` بنامید. بنداشتهای آن بنداشتهای K به اضافه آن دسته از بنداشتهای منطقی است که نمادهای K و ثابتهای انفرادی جدید را شامل میشود. `\text{K}_0` سازگار است. زیرا، اگر نباشد، در `\text{K}_0` یک برهان برای فرمولی مانند `cc"B"∧¬cc"B"` وجود دارد. هر `b_i` را که در این برهان ظاهر شده است با متغیری جایگزین کنید که در برهان ظاهر نشده است. با این کار، یعنی جایگزینی، بنداشتها هنوز بنداشت باقی میماند و صحت کاربرد قواعد استنتاج حفظ میشود. فرمول نهایی در برهان هنوز یک تناقض است، اما اکنون برهان شامل هیچ یک از `b_i`ها نمیشود و بنابراین یک برهان در K است. این با سازگاری K در تناقض است. بنابراین، `\text{K}_0` سازگار است.
بنابر لم ۲.۱۳، دنباله `F_1(x_{i_1}), F_2(x_{i_2}), ...,F_k(x_{i_k})` را برشمارشی از تمام فرمولهای `\text{K}_0` بگیرید به قسمی که دارای یک متغیر آزاد باشند.
دنباله `b_{j_1}, b_{j_2}, …` را از ثابتهای انفرادی جدید را انتخاب کنید به قسمی که هر `b_{j_k}` در هیچ یک از فرمولهای `F_1(x_{i_1}), ...,F_k(x_{i_k})` نباشد و به گونهای باشد که `b_{j_k}` با هر یک از `b_{j_1}, ..., b_{j_{k-1}}` متفاوت باشد.
اکنون، فرمول زیر را در نظر بگیرید:
`(S_k)` `(∃x_{i_k})¬F_k (x_{i_k}) ⇒ ¬F_k (b_{j_k} )`
فرض کنید `\text{K}_n` تئوریای باشد که با افزودن `(S_1),..., (S_n)` به بنداشتهای `\text{K}_0`، و `\text{K}_∞` با افزودن همه `(S_i)`ها به عنوان بنداشتها به `\text{K}_0` بهدست میآید.
هر برهانی در `\text{K}_∞` فقط شامل تعداد محدودی از `(S_i)` است و بنابراین، در برخی `\text{K}_n` نیز اثباتپذیر خواهد بود.
بنابراین، اگر همه `\text{K}_n`ها سازگار باشند، `\text{K}_∞` نیز سازگار است.
برای نشان دادن اینکه همه `\text{K}_n`ها سازگار هستند، با استقرا ادامه میدهیم. میدانیم که `\text{K}_0` سازگار است. فرض کنید `\text{K}_{n-1}` سازگار است ولی `\text{K}_n` ناسازگار است `(n≥1)`.
اما میدانیم، هر فرمولی در `\text{K}_n` قابل اثبات است [بنا به توتولوژی `¬A⇒(A⇒B)`، قضیه ۲.۱ و MP]. به ویژه `⊢_{K_n}¬(S_n)`. بنابراین، `(S_n) ⊢_{K_{n−1}}¬(S_n)`.
از آنجا که `(S_n)` بسته است، از نتیجه ۲.۷ داریم: `⊢_{K_{n−1}}(S_n)⇒¬(S_n)` داریم.
اما، از توتولوژی `(A⇒¬A)⇒¬A`، قضیه ۲.۱ و MP داریم: `⊢_{K_{n−1}}¬(S_n)`، و این یعنی: `⊢_{K_{n−1}}¬[(∃x_{i_n} )¬F_n(x_{i_n})⇒¬F_n(b_{j_n})]`.
اکنون، با حذف شرطی، `⊢_{K_{n−1}}(∃x_{i_n})¬F_n(x_{i_n})` و `⊢_{K_{n−1}}¬¬F_n(b_{j_n})` را بدست میآوریم و سپس با حذف نقیض، `⊢_{K_{n−1}}F_n(b_{j_n})` را.
از دومی و این واقعیت که `b_{j_n}` در `(S_0)، …، (S_{n−1})` رخ نمیدهد، نتیجه میگیریم `⊢_{K_{n−1}}F_n(x_r)`، که در آن `x_r` متغیری است که در اثبات `F_n(b_{j_n})` وجود ندارد.
(صرفا با جایگزینی تمام رویدادهای `b_{j_n}` با `x_r` در برهان) با Gen (تعمیم)، `⊢_{K_{n−1}} (∀x_r )F_n(x_r )`، و سپس، توسط لم ۲.۱۱ و حذف دو شرطی: `⊢_{K_{n−1}}(∀x_{i_{n}})F_n(x_{i_{n}})`. (با توجه به این که `F_n(x_r)` و `F_n(x_{i_n})` یکجور هستند.)
اما، ما `⊢_{K_{n−1}}(∃x_{i_n} )¬F_n(x_{i_n})`را داریم که کوتاهشده `⊢_{K_{n−1}}¬(∀x_{i_n})¬¬F_n(x_{i_n)}` است.
اکنون، بنا بر قضیه جایگزینی، `⊢_{K_{n−1}}¬(∀x_{i_n})F_n(x_{i_n})`. که این در تناقض با این فرض است که `K_{n−1}` سازگار است. از این رو، `K_n` نیز باید سازگار باشد. بنابراین `K_∞` سازگار است، گسترش K است و آشکارا یک تئوری سپربلا است.
■ لم ۲.۱۶
گیریم `\text{J}` یک تئوری تمام و سازگار باشد. در این صورت `\text{J}` دارای یک مدل `M` است به قسمی که دامنه آن مجموعه `D` از ترمهای بسته `\text{J}` است.
برهان:
تعبیر هر ثابت انفرادی `a_i` در `\text{J}` را `(a_i)^M = a_i` بگیرید. تعبیر هر حرف تابعی `f_k^n` در `\text{J}` و هر ترم بسته `t , …, t` در `\text{J}` را از قرار `(f_k^n)^M(t, ..., t ) = f_k^n(t , ..., t )` بگیرید. (توجه کنید که `f_k^n(t_1، ...، t_n)` یک ترم بسته است. بنابراین، `(f_k^n)^M` یک عمل `n`-گانه روی `D` است.)
برای هر حرف محمولی `A_k^n` در `\text{J}`، فرض کنید `(A_k^n)^M` از تمام `n`-گانههای `〈t_1, …, t_n〉 ` از ترمهای بسته `t , …, t` در `\text{J}` تشکیل شده باشد به قسمی که `⊢_J A_k^n(t, ..., t)`. اکنون کافی است نشان دهیم که برای هر فرمول بسته `cc"C"` در `\text{J}`:
(⧠) `⊩_M cc"C"` اگر و تنها اگر `⊢_J cc"C"`
(اگر این ثابت شده و `cc"B"` یکی از بندشتهای `\text{J}` بود، `cc"C"` را بستار `cc"B"` بگیرید. از Gen داریم `⊢_J cc"C"`. از (⧠) داریم `⊧_M cc"C"`. توسط (VI) درصفحه ۵۸: `⊧_M cc"B"`. بنابراین، `M` مدلی از `\text{J}` خواهد بود.)
(⧠) را به روش استقرا روی تعداد `r` رابطها و سورها در `cc"C"` اثبات میکنیم. فرض کنید که (⧠) برای همه فرمولهای بسته با رابطها و سورهای کمتر از `r` برقرار است.
حالت ۱. `cc"C"` یک فرمول اتمی بسته `A_k^n(t _1, ..., t_n)` است. پس (□) یک نتیجه مستقیم از تعریف `(A_k^n)^M` است.
حالت ۲. `cc"C"` به قرار `¬cc"D"` است. اگر `cc"C"` برای تعبیر `M` درست است، پس `cc"D"` برای `M` نادرست است و بنابراین، بر اساس فرض استقرا، چنین نیست که `⊢_J cc"D"`. از آنجا که `\text{J}` تمام است و `cc"D"` بسته است، `⊢_J ¬cc"D"`— یعنی `⊢_J cc"C"`. برعکس، اگر `cc"C"` برای `M` درست نیست، `cc"D"` برای `M` درست است. بنابراین، `⊢_J cc"D"`. از آنجایی که `\text{J}` سازگار است، چنین نیست که:`⊢_J ¬cc"D"`، یعنی چنین نیست که: `⊢_J cc"C"`.
حالت ۳.
`cc"C"` به قرار `cc"D"⇒cc"E"` است. از آنجا که `cc"C"` بسته است، `cc"D"` و `cc"E"` نیز بسته هستند. اگر `cc"C"` برای `M` نادرست باشد، `cc"D"` درست و `cc"E"` نادرست است.
از این رو، با فرض استقرا داریم `⊢_J cc"D"`، و نیز داریم `\text{not-}(⊢_J cc"E")`. از تمام بودن `\text{J}` داریم `⊢_J ¬cc"E"`. بنابراین، با موردی از توتولوژی `cc"D"⇒(¬cc"E"⇒¬(cc"D"⇒cc"E"))` و دو کاربرد (MP) داریم: `⊢_J¬(cc"D"⇒cc"E")`. که این یعنی `⊢_J ¬cc"C"`. و بنابراین، با سازگاری `\text{J}` میرسیم به: `\text{not-}(⊢_J cc"C")`.
برعکس، اگر چنین نیست که `⊢_J cc"C"`، پس با تمامیت `\text{J}` داریم `⊢_J ¬cc"C"`، یعنی `⊢J¬(cc"D"⇒cc"E")`.
با حذف شرطی: `⊢_J cc"D"` و `⊢_J ¬cc"E"`. بنابراین، توسط (⧠) برای `cc"D"` چنین داریم که `cc"D"` برای `M` درست است.
از سازگاری `\text{J}` داریم: `\text{not-}⊢_J cc"E"`. بنابراین، از (⧠) برای `cc"E"` داریم که `cc"E"` برای `M` نادرست است.
بنابراین ، از آنجا که `cc"D"` برای `M` درست است و `cc"E"` برای `M` نادرست است، پس `cc"C"` برای `M` نادرست است.
حالت ۴.: `cc"C"` عبارت است از `(∀x_m)cc"D"`.
حالت ۴.آ. فرمول `cc"D"` یک فرمول بسته است.
از فرض استقرا : `⊧_M cc"D"` اگر و فقط اگر `⊢_J cc"D"`.
از تمرین ۲.۳۲.a داریم: `\( \vdash_{J} cc"D" \iff (\forall x_{m}) cc"D" \)`.
بنابراین، با حذف دو شرطی: `⊢_J cc"D"` اگر و فقط اگر `⊢_J (∀x_m)cc"D"`.
علاوه بر این، از ویژگی (VI) در صفحه ۵۸، `⊧_M cc"D"` اگر و فقط اگر `⊧_M(∀x_m)cc"D"`.
از این رو، `⊧_M cc"C"` اگر و فقط اگر `⊢_J cc"C"`.
حالت ۴.ب. فرمول `cc"D"` یک فرمول بسته نیست. از آنجا که `cc"C"` بسته است، `cc"D"` متغیر `x_m` را به عنوان تنها متغیر آزاد خود دارد، بفرض `cc"D"` به قرار `F(x_m)` است. پس `cc"C"` ازقرار `(∀x_m)F(x_m)` است.
فرض کنید `⊧_M cc"C"` و `\text{not-}⊢_J cc"C"`.
از تمامیت `\text{J}` داریم `⊢_J ¬cc"C"`، یعنی `⊢_J ¬(∀x_m)F(x_m)`.
از تمرین ۲.۳۳.a و حذف دو شرطی خواهیم داشت، `⊢_J(∃x_m) ¬F(x_m)`. از آنجا که `\text{J}` یک تئوری سپربلا است، برای برخی از ترمهای بسته `t` در `\text{J}` داریم `⊢J ¬F(t)`.
اما `⊧_M cc"C"`، یعنی `⊧_M(∀x_m)F(x_m)`. از آنجا که بنا ویژگی X در صفحه ۵۹ `(∀x_m)F(x_m)⇒F(t)` برای `M` برقرار است، پس، `⊧_M F(t)`.
از این رو، توسط (□) برای `F(t)` داریم `⊢_JF(t)`. این خلاف سازگاری `\text{J}` است. بنابراین، اگر `⊧_M cc"C"`، پس `⊢_J cc"C"`.
فرض کنید `⊢_J cc"C"` و `\text{not-}⊧_M cc"C"`. و از اینجا:
(#) `⊢_J (∀x_m)F(x_m)`
و
(##) `\text{not-}⊢_M(∀x_m )F(x_m)`.
بنا به (##)، دنبالهای از عناصر دامنه `D` هست که `(∀x_m)F(x_m)` را برنمیآورد.
از این رو، برخی از دنباله، به فرض `s`، `F(x_m)` را برنمیآورد.
`t` را مولفه `i`ام `s` میگیریم.
توجه داشته باشید که برای همه ترمهای بسته `u` در تئوری `\text{J}` داریم `s^**(u)=u` (بنا به تعریف `(a_i)^M` و `(f_k^n)^M`).
همچنین توجه داشته باشید که `F(t)` رابطها و سورهای کمتری نسبت به `cc"C"` دارد و بنابراین، فرض استقرا در مورد `F(t)` کارزدنی شدنی است ، یعنی (□) برای `F(t)` برقرار است.
از این رو، توسط لم a.۲ در صفحه ۶۰، `F(t)` توسط `s` برآورده نمیشود.
بنابراین، `F(t)` برای `M` نادرست است.
اما، از (#) و قاعده A۴ داریم: `⊢_J F(t)`. و از اینجا، از (⧠) برای `F(t)` داریم `⊧_M F(t)`.
این تناقض نشان می دهد که اگر `⊢_J cc"C"`، آنگاه `⊧_M cc"C"`.
■ مدل شمارا و قضیه بنیادی نظریه تسویر
اکنون میتوانیم قضیه بنیادی نظریه تسویر (کمیسازی) را ثابت کنیم. پیشتر بگوییم، مراد ما از یک مدل شمارا مدلی↝ است که در آن دامنه↝ شمارا باشد.
■ قضیه ۲.۱۷. هر تئوری سازگار K دارای یک مدل شمارا است.
[
به عبارت دیگر (عکس نقیض): اگر K دارای مدل قابل شمارا
نباشد، آنگاهK یک تئوری سازگار نیست.]
برهان:*
اثبات ارائه شده در اینجا اساسا مربوط Henkin (1949) است، همانطور که توسط Hasenjaeger (1953) ساده شده است. نتیجه در ابتدا توسط گودل (1930) ثابت شد. شواهد دیگر توسط Rasiowa و Sikorski (1951، 1952) و Beth (1951) به ترتیب با استفاده از روشهای جبری (بولی) و توپولوژیکی منتشر شده است. با این حال، شواهد دیگری را می توان در Hintikka (1955a,b) و در Beth (1959) یافت.
• Henkin, L. (1949) The completeness of the first-order functional calculus. JSL, 14, 159–166.
• Hasenjaeger, G. (1953) Eine Bemerkung zu Henkin’s Beweis für die Vollständigkeitdes Prädikatenkalküls der ersten Stufe. JSL, 18, 42–48.
• Gödel, K. (1930) Die Vollständigkeit der Axiome des logischen Funktionenkalküls, Monatsh. Math. Phys., 37, 349–360 (English translation in Van Heijenoort, 1967, 582–591).
• Beth, E. (1951) A topological proof of the theorem of Löwenheim–Skolem–Gödel. Indag. Math., 13, 436–444
• Sikorski, R. (1960) Boolean Algebra. Springer (third edition, 1969).
• Hintikka, J. (1955a) Form and content in quantification theory. Acta Philos. Fennica, 11–55.
• Beth, E. (1959) The Foundations of Mathematics. North-Holland.
از لم ۲.۱۵ میدانیم K دارای یک گسترش سازگار K′ است، به قسمی که K′ یک تئوری سپربلا باشد و ترمهای بسته بسیار داشته باشد. بنا بر لم نباوم، K′ دارای یک گسترش سازگار و تمام `\text{J}` است که نمادهای یکسان K′ را دارد. از این رو، `\text{J}` نیز یک تئوری سپربلا است. بنا به لم ۲.۱۶ تئوری `\text{J}` دارای یک مدل `M` است که دامنه آن مجموعه شمارای ترمهای بسته `\text{J}` است. از آنجا که `\text{J}` گسترش K است، `M` یک مدل شمارا از K است.
■ قضیه ۲.۱۸ هر فرمول منطقاً معتبر `cc"B"` از یک تئوری K قضیه K است.
ما باید فقط فرمول بسته `cc"B"` را در نظر بگیریم، زیرا یک فرمول `cc"D"` منطقاً معتبر است اگر و تنها اگر بستار آن منطقاً معتبر باشد. `cc"D"` در K اثبات شدنی است اگر و تنها اگر بستار آن در K اثبات شدنی باشد. بنابراین، `cc"B"` را یک فرمول بسته منطقا معتبر در K میگیریم. فرض کنید `\text{not-}⊢_K cc"B"`.
از لم ۲.۱۲ میدانیم، اگر `¬cc"B"` را به عنوان یک بنداشت جدید به K بیافزاییم، تئوری جدید K′ سازگار است.
از این رو، از قضیه ۲.۱۷ داریم، K′ یک مدل↝ M دارد.
از آنجا که `¬cc"B"` بنداشت K′ است، `¬cc"B"` برای M درست است.
اما، از آنجایی که `cc"B"` منطقا معتبر است، `cc"B"` برای M درست است.
از این رو، `cc"B"` برای M هم درست و هم نادرست است، که غیرممکن است (از (II) در صفحه ۵۷).
بنابراین، `cc"B"` باید قضیه K باشد.