پیش‌نیازهای فراقضیه تمامیت

■ مقدمه

در ادامه قسمت قبل، یعنی «منطق محمولات: برخی ویژگی‌های تئوری‌های مرتبه اول»، این  قسمت، ژرف‌تر به منطق مرتبه اول (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` دارد.

■ لم. ۲.۱۱

اگر `cc"B"(x_i)` و `cc"B"(x_j)` یکجور باشند، آنگاه

`⊢(∀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' سازگار است.

■ نتیجه مهم

■ لم ۲.۱۳ مجموعه عبارت‌های یک زبان `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`).

اکنون می‌توانیم همه عبارت‌ها را به ترتیب اعداد نظیرشده به آنها برشماریم. بنابراین، مجموعه عبارت‌ها شمارا است.

■ چند تعریف: ۱- ترم بسته، ۲- تئوری سپربلا

1. یک ترم بسته یک ترم بدون متغیر است.

2. یک تئوری K یک تئوری سپربلا (تئوری بز سپربلا ↝ / تئوری بلاگردان) است (scapegoat theory)^* اگر برای هر فرمول `cc"B(x)` که `x` را به عنوان تنها متغیر آزاد خود دارد، یک ترم بسته `t` وجود داشته باشد به قسمی که:

`⊢_K (∃x)¬cc"B"(x)⇒¬cc"B"(t)`.

از ویژگی‌های تعیین‌کننده این تئوری (سپربلا) این است که اگر گزاره‌ای در مورد یک فرد نامشخص بیان شود - در مورد `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}`:

(اگر این ثابت شده و `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` برقرار است.

■ قضیه ۲.۱۷. هر تئوری سازگار K دارای یک مدل شمارا است.

[ به عبارت دیگر (عکس نقیض): اگر K دارای مدل قابل شمارا نباشد، آنگاهK یک تئوری سازگار نیست.]

برهان:^*

از لم ۲.۱۵ می‌دانیم 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 باشد.