(فرا) قضیه استنتاج
منطق محمولات و نظریه مدل
درآمد به منطق
منطق محمولات: زبان، تعبیر و مدل (۲)
۱- مقدمه | ۹- قضیه ۲.۴ |
۲- ویژگی‌های تئوری‌های مرتبه اول | ۱۰- قضیه ۲.۵: قضیه استنتاج |
۳- قضیه ۲.۱ | ۱۱- نتیجه ۲.۶: پیامد استنتاج (۱) |
۴- قضیه ۲.۲ | ۱۲- نتیجه ۲.۷: پیامد استنتاج (۲) |
۵- تعریف: سازگاری تئوری | ۱۳- گسترش قضیه‌های ۲.۴ تا ۲.۷ |
۶- نتیجه ۲.۳. سازگاری حساب محمولات مرتبه اول | ۱۴- مثال: کارزدن قضیه استنتاج |
۷- درباره قضیه استنتاج | ۱۵- تمرین |
۸- وابستگی فرمولی |
مگر در مواردی که با نماد "" مشخص شده باشد، محتوای ارائه شده در این یادداشت از مرجع زیر برگرفته و برگردان شده است.
Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015. p. ۶۹-۷۳. ↜
۱- مراد از مجموعه شمارا (Denumerable set) یک مجموعه شمارای نامتناهی است مگر آنکه با صراحت قید شده باشد.
■ مقدمه
`∀x (Man(x)→Mortal(x))`
در یادداشت (منطق محمولات: نظریه‌های مرتبه اول) در باره تئوری‌های مرتبه اول (حساب محمولات)، بنداشت‌های منطقی، بنداشت‌های سره و قواعد استنتاج شرح درخور آمده است. در این یادداشت به ویژگی‌های این دستگاه‌ه و معرفی و اثبات (فرا)قضیه استنتاج برای این دستگاه‌ها می‌پردازیم.
■ ۲.۴ ویژگی‌های تئوری‌های مرتبه اول
همه نتایج در این بخش به یک تئوری مرتبه اول دلخواه K اشاره می‌کند. بجای نوشتن↝ `⊢_K cc"B"`، گاهی اوقات تنها `⊢ cc"B"` را می‌نویسیم، افزون بر این، به تئوری‌های مرتبه اول صرفاً با عنوان تئوری اشاره خواهیم کرد، مگر اینکه چیزی خلاف آن گفته شود.
■ قضیه ۲.۱
هر فرمول `cc"B"` در K که موردی از یک توتولوژی است یک قضیه↝ K است و می‌توان آن را فقط با کارزدن بنداشت‌های (A۱) تا (A۳) و MP ثابت کرد.
اثبات:
فرض کنید فرمول `cc"B"` از توتولوژی `cc"C"` توسط جانشین سازی بدست آمده باشد. بنا بر تمامیت ℒ، برهانی برای `cc"C"` در ℒ وجود دارد. در چنین برهانی، از همان جانشین سازی فرمول‌های K برای حروف محمولی استفاده کنید که در بدست آوردن `cc"B"` از `cc"C"` استفاده شده است. و هر حرف گزاره‌ای در برهان که در `cc"C"` نیست را با فرمول دلخواهی از K جانشین کنید. در این صورت، دنباله حاصل از فرمول‌ها برهان `cc"B"` است، و این برهان فقط از بنداشت‌های (A۱) تا (A۳) و MP استفاده می‌کند.
■ قضیه ۲.۲
هر قضیه↝ یک حساب محمولات مرتبه اول منطقاً معتبر است.
اثبات:
بنداشت‌های (A۱) تا (A۳) بنا به ویژگی (VII) انگاشت صدق↝↝ منطقاً معتبر هستند. (صفحه ۵۸ را ببینید). و بنا بر (X) و (XI) بنداشت‌های ( A۴) و ( A۵) منطقاً معتبر هستند.
بنا بر ویژگی‌های (III) و (VI)، قواعد استنتاج MP و Gen اعتبار منطقی را حفظ می‌کنند، بنابراین، هر قضیه یک حساب محمولات منطقاً معتبر است.
مثال:
فرمول
`(∀x_۲)(∃x_۱)A_۱^۲(x_۱, x_۲)⇒(∃x_۱)(∀x_۲)A_۱^۲(x_۱, x_۲)`
یک قضیه برای هر حساب مرتبه اول نیست، چراکه منطقاً معتبر نیست. (مثال ۵ صفحه ۶۳ را ببینید.)
■ تعریف: سازگاری تئوری
تئوری K سازگار است اگر هیچ فرمول `cc"B"` و نقیض آن `¬cc"B"` هر دو در K قابل اثبات نباشند. یک تئوری ناسازگار است اگر سازگار نباشد.
■ نتیجه ۲.۳: سازگاری حساب محمولات مرتبه اول
هر حساب محمولات مرتبه اول سازگار است. ↜
اثبات:
اگر فرمول `cc"B"` و نقیض آن `¬cc"B"` هر دو قضیه یک حساب محمولات مرتبه اول باشند، از قضیه ۲.۲ داریم هر دو `cc"B"` و نقیض آن `¬cc"B"` منطقاً معتبر خواهند بود، که ممکن نیست.
توجه داشته باشید که در یک تئوری ناسازگار K، هر فرمول ℒ از K در K اثبات شدنی است. در واقع، فرض کنید که فرمول `cc"B"` و `¬cc"B"` هر دو در K اثبات شدنی باشند. از آنجا که فرمول
`cc"B"⇒(¬cc"B" ⇒ cc"C")`
موردی از یک توتولوژی است(↝) از قضیه ۲.۱ می‌دانیم که این فرمول در K اثبات شدنی است. از اینجا با دو بار کاربرد MP خواهیم داشت `⊢cc"C"`.
از این ملاحظه برمی‌آید که، اگر برخی فرمول تئوری K قضیه K نباشد آنگاه K سازگار است.
■ درباره قضیه استنتاج
قضیه استنتاج (قضیه ۱.۹) برای حساب گزاره‌ها را نمی‌توان بدون اصلاح به تئوری‌های مرتبه اول آورد. برای نمونه، برای هر فرمول `cc"B"` داریم
`cc"B"⊢_K(∀x_i)cc"B"`,
اما همیشه چنین نیست که
`⊢_K cc"B"⇒(∀x_i)cc"B"`.
اکنون، دامنه‌ای را در نظر بگیرید که شامل حداقل دو عنصر `c` و `d` باشد. فرض کنید K یک حساب محمولات باشد و `cc"B"` را به قرار `A_۱^۱(x_۱)` بگیرید. `A_۱^۱` را به عنوان یک ویژگی که فقط برای `c` برقرار است تعبیر کنید.
در این صورت `A_۱^۱(x_۱)` با هر دنباله `s=(s_۱, s_۲, …)` که در آن `s_۱ = c` برآورده می‌شود.
اما `(∀x_۱)A_۱^۱(x_۱)` با هیچ دنباله‌‌ای برآورده نمی‌شود. از این رو، فرمول:
`A_۱^۱(x_۱)⇒(∀x_۱)A_۱^۱(x_۱)`
در این تعبیر درست نیست و بنابراین منطقاً معتبر هم نیست. از اینجا، بنا به قضیه ۲.۲، `A_۱^۱(x_۱)⇒(∀x_۱)A_۱^۱(x_۱)` یک قضیه K نیست.
با این حال، ممکن است صورتی اصلاح شده، اما همچنان سودمند، از قضیه استنتاج را بدست آورد.
■ وابستگی فرمولی
فرض کنید `cc"B"` یک فرمول در مجموعه فرمول `Γ` باشد و فرض کنید که یک استنتاج `cc"D"_۱,...,cc"D"_n` از `Γ` به همراه توجیه برای هر مرحله در استنتاج به ما داده شده است. می‌گوییم: `cc"D"_i` در این برهان بستگی به `cc"B"` دارد اگر و تنها اگر:
`cc"D"_i` همان `cc"B"` است و توجیه `cc"D"_i` تعلق آن به `Γ` است، یا
`cc"D"_i` به عنوان یک نتیجه مستقیم کارزدن MP یا Gen به برخی از فرمول‌های قبلی دنباله توجیه می‌شود، جایی که حداقل یکی از این فرمول‌های قبلی به `cc"B"` بستگی دارد.
مثال:
`cc"B", (∀x_۱)cc"B"⇒cc"C"⊢(∀x_۱)cc"C"`
| فرض | `cc"B"` | `(cc"D"_۱)` |
| `(cc"D"_۱)`, Gen | `(∀x_۱)cc"B"` | `(cc"D"_۲)` |
| فرض | `(∀x_۱)cc"B"⇒cc"C"` | `(cc"D"_۳)` |
| `(cc"D"_۲)`, `(cc"D"_۳)`, MP | `cc"C"` | `(cc"D"_۴)` |
| `(cc"D"_۴)`, Gen | `(∀x_۱)cc"C"` | `(cc"D"_۵)` |
در اینجا، `(cc"D"_۱)` و `(cc"D"_۲)` به `cc"B"` بستگی دارند. `(cc"D"_۳)` به `(∀x_۱)cc"B"⇒cc"C"` بستگی دارد. `(cc"D"_۴)` به `cc"B"` و `(∀x_۱)cc"B"⇒cc"C"` بستگی دارد. `(cc"D"_۵)` به `cc"B"` و `(∀x_۱)cc"B"⇒cc"C"` بستگی دارند.
■ قضیه ۲.۴
اگر `cc"C"` به `cc"B"` در استنتاج `Γ,cc"B"⊢cc"C"` بستگی نداشته باشد آنگاه `Γ⊢cc"C"`.
اثبات:
فرض کنید `cc"D"_۱ …، cc"D"_n` استنتاج `cc"C"` از `Γ` و `cc"B"` باشد، که در آن `cc"C"` به `cc"B"` بستگی ندارد. (در این استنتاج `cc"D"_n` همان `cc"C"` است.)
اکنون بنا بر استقرا فرض می‌کنیم این قضیه برای همه استنتاج‌های با طول کمتر از `n` برقرار است.
گر `cc"C"` یک بنداشت باشد یا عضو `Γ` باشد آنگاه `Γ⊢cc"C"`.
اگر `cc"C"` نتجه مستقیم یک یا دو فرمول قبلی توسط MP یا Gen باشد آنگاه، از آنجا که `cc"C"` به `cc"B"` بستگی ندارد، این فرمول‌های قبلی نیز وابستگی ندارند.
بنا بر فرض استقرا، این فرمول‌های قبلی تنها از `Γ` قابل استنتاج هستند.
در نتیجه، `cc"C"` هم چنین است.
■ قضیه ۲.۵: قضیه استنتاج
فرض کنید، در برهانی که نشان دهنده استنتاج `Γ,cc"B"⊢cc"C"` است، هیچ موردی از قاعده Gen (تعمیم) برای فرمولی که به `cc"B"` بستگی دارد و در آن متغیر سوردارشده یک متغیر آزاد در `cc"B"` است، کارزده نشده باشد. در این صورت داریم `Γ⊢cc"B"⇒cc"C"`.
اثبات:
گیریم `cc"D"_۱, …,cc"D"_n` استنتاج `cc"C"` از `Γ` و `cc"B"` باشد، که فرض قضیه را برمی‌آورد. (در این استنتاج `cc"D"_n` همان `cc"C"` است.)
می‌خواهیم با استقرا نشان دهیم که برای هر `i≤ n` داریم `Γ⊢cc"B"⇒cc"D"_i`.
اگر `cc"D"_i` یک بنداشت یا متعلق به `Γ` باشد، از آنجا که↝ `cc"D"_i⇒(cc"B"⇒cc"D"_i)` یک بنداشت است داریم↝ `Γ⊢cc"B"⇒cc"D"_i`.
اگر `cc"D"_i` همان `cc"B"` باشد، پس `Γ⊢cc"B"⇒cc"D"_i`، زیرا، بنا به قضیه ۲.۱، `⊢cc"B"⇒cc"B"`.
اگر `j` و `k` کوچکتر از `i` وجود داشته باشد به قسمی که `cc"D"_k` همان `cc"D"_j⇒cc"D"_i` باشد، آنگاه، با فرض استقرا `Γ ⊢ cc"B" ⇒ cc"D"_j` و `Γ ⊢ cc"B" ⇒ (cc"D"_j ⇒ cc"D"_i )`.
اکنون بنا به بنداشت (A۲) داریم:
`⊢(cc"B"⇒(cc"D"_j⇒cc"D"_i))⇒((cc"B"⇒cc"D"_j)⇒(cc"B"⇒cc"D"_i))`.
بنابراین، با دوبار کارزدن MP داریم `Γ⊢cc"B"⇒cc"D"_i`.
سرانجام، فرض کنید `j` کوچکتر از `i` وجود دارد به قسمی که `cc"D"_i` عبارت باشد از `(∀x_k)cc"D"_j`.
در این صورت، بنا به فرض استقرا، یعنی `Γ⊢ cc"B"⇒cc"D"_j`، و فرض قضیه یا `cc"D"_i` به `cc"B"` بستگی ندارد یا `x_k` یک متغیر آزاد `cc"B"` نیست.
اگر `cc"D"_j` به `cc"B"` بستگی نداشته باشد، بنا به قضیه ۲.۴، `Γ⊢cc"D"_j` و در نتیجه با کار زدن Gen داریم `Γ ⊢ (∀x_k)cc"D"_j`. بنابراین، `Γ⊢cc"D"_i`.
اکنون با بنداشت (A۱) داریم `⊢cc"D"_i⇒(cc"B"⇒cc"D"_i)`.
بنابراین بنا بر MP داریم `Γ⊢cc"B"⇒cc"D"_i`.
از طرف دیگر، اگر `x_k` یک متغیر آزاد `cc"B"` نباشد، با توجه به بنداشت (A۵)،
`⊢(∀x_k)(cc"B"⇒cc"D"_j)⇒(cc"B"⇒(∀x_k)cc"D"_j)`.
از آنجا که `Γ⊢cc"B"⇒cc"D"_j`، از Gen داریم `Γ⊢(∀x_k)(cc"B"⇒cc"D"_j)`. و اکنون از MP داریم `Γ⊢cc"B"⇒(∀x_k)cc"D"_j`. یعنی `Γ⊢cc"B"⇒cc"D"_i`.
این استقرا را کامل می‌کند، و قضیه ما دقیقاً حالت خاص `i=n` است.
فرض قضیه ۲.۵ تا اندازه‌ای دست و پا گیر است. نتایج ضعیف‌تر زیر اغلب مفیدتر هستند.
■ نتیجه ۲.۶: پیامد استنتاج (۱)
اگر در استنتاج `Γ,cc"B"⊢cc"C"` از قاعده تعمیم با متغیرهای سوردارشده که در `cc"B"` آزاد هستند استفاده نشده باشد آنگاه `Γ⊢cc"B"⇒cc"C"`.
به عبارت دیگر، اگر بتوانیم برای `Γ,cc"B"⊢cc"C"` بدون استفاده از قاعده تعمیم بر روی متغیرهای آزاد `cc"B"` برهان بیاوریم، می‌توانیم برای `Γ⊢cc"B"⇒cc"C"` نیز برهان بیاوریم.
■ نتیجه ۲.۷: پیامد استنتاج (۲)
اگر `cc"B"` یک فرمول بسته باشد و داشته باشیم `Γ,cc"B"⊢cc"C"` آنگاه خواهیم داشت `Γ⊢cc"B"⇒cc"C"`.
■ گسترش قضیه‌های ۲.۴ تا ۲.۷
در قضیه‌های ۲.۴ تا ۲.۷ نتیجه افزون زیر را می‌توان از اثبات‌ها بدست آورد.
اثبات جدید `Γ⊢cc"B"⇒cc"C"` (که در قضیه ۲.۴، دیدیم، یعنی `Γ⊢cc"C"`) از قاعده Gen در فرمولی استفاده می‌کند که به برخی فرمول مانند `ε` در `Γ` بستگی دارد. این در صورتی است که در اثبات اصلی `Γ⊢cc"B"⇒cc"C"` قاعده Gen برای همان متغیر سوردار شده و بر روی فرمولی که به `ε` بستگی دارد کار زده شود.
(در اثبات قضیه ۲.۵، باید توجه داشت که `cc"D"_j` به یک مقدمه `ε` از `Γ` در اثبات اصلی بستگی دارد اگر و فقط اگر `cc"B"⇒cc"D"_j` در اثبات جدید به `ε` وابسته باشد.)
این نتیجه‌گیری تکمیلی زمانی مفید خواهد بود که بخواهیم قضیه استنتاج را چندین بار پشت سر هم به یک استنتاج معین اعمال کنیم - برای مثال، برای به دست آوردن
`Γ ⊢ cc"D" ⇒ (cc"B" ⇒ cc"C") `
از
`Γ, cc"D", cc"B" ⊢ cc"C"`.
که از این پس بخش جدایی ناپذیر بیان قضیه‌های ۲.۴ تا ۲.۷ در نظر گرفته خواهند شد.
■ مثال: کارزدن قضیه استنتاج
`⊢(∀x_۱)(∀x_۲)cc"B"⇒(∀x_۲)(∀x_۱)cc"B"`
| فرض | `(∀x_۱)(∀x_۲)cc"B"` | ۱. |
| (A۴) | `(∀x_۱)(∀x_۲)cc"B"⇒(∀x_۲)cc"B"` | ۲. |
| ۱, ۲, MP | `(∀x_۲)cc"B"` | ۳. |
| (A۴) | `(∀x_۲)cc"B"⇒cc"B"` | ۴. |
| ۳, ۴, MP | `cc"B"` | ۵. |
| Gen | `(∀x_۱)cc"B"` | ۶. |
| Gen | `(∀x_۲)(∀x_۱)cc"B"` | ۷. |
بنابراین، از ۱ تا ۷ داریم:
`(∀x_۱)(∀x_۲)cc"B"⊢(∀x_۲)(∀x_۱)cc"B"`
و این در حالی است که در این استنتاج کاربردی از تعمیم وجود ندارد که در آن متغیر سوردار شده یک متغیر آزاد `(∀x_۱)(∀x_۲)cc"B"` باشد. بنابراین، بنابر نتیجه ۲.۷ داریم:
تمرین (۷۳) (۲.۲۷ - ۲.۲۹):
قضیه‌های زیر را بدست آورید.
۲.۲۷:
a. `⊢(∀_x)(cc"B"⇒cc"C")⇒((∀_x)cc"B"⇒(∀_x)cc"C"`
حل:
| فرض | `(∀_x)(cc"B"⇒cc"C")` | ۱. |
| فرض | `(∀x)cc"B"` | ۲. |
| (A۴) | `(∀_x)(cc"B"⇒cc"C")⇒(cc"B"⇒cc"C")` | ۳. |
| ۱, ۳, MP | `cc"B"⇒cc"C"` | ۴. |
| (A۴) | `(∀x)cc"B"⇒cc"B"` | ۵. |
| ۲, ۵, MP | `cc"B"` | ۶. |
| ۴, ۶, MP | `(∀x)cc"C"` | ۷. |
| ۷, Gen | cc"C" | ۸. |
| ۱-۸ | `(∀x)(cc"B"⇒cc"C"),(∀x)cc"B"⊢(∀x)cc"C"` | ۹. |
| ۱-۲, ۲.۶ | `(∀x)(cc"B"⇒cc"C")⊢(∀x)cc"B"⇒(∀x)cc"C"` | ۱۰ |
| ۱, ۱۰, ۲.۶ | `⊢(∀x)(cc"B"⇒cc"C")⇒((∀x)cc"B"⇒(∀x)cc"C")` | ۱۱. |
b. `⊢ (∀x)(cc"B" ⇒ cc"C") ⇒ ((∃x)cc"B" ⇒ (∃x)cc"C"`
c. `⊢(∀x)(cc"B"∧cc"C")⇔((∀x)cc"B"∧(∀x))cc"C"`
d. `⊢(∀y_1)…(∀y_n)cc"B"⇒cc"B"`
e. `¬(∀x)cc"B" ⇒ (∃x) ¬cc"B"`
۲.۲۸:
فرض کنید K یک تئوری مرتبه اول باشد و `K^#` یک تئوری بنداشتی با بنداشت‌های زیر باشد:
a. `(∀y_1)…(∀y_n)cc"B",`
که در آن `cc"B"` (هر) بنداشی از K است و `y_۱,…,y_n(n≥۰)` (هر) متغیر هستند (برای `n=0` هیچ متغیر).
b. `(∀y_۱)…(∀y_n)(cc"B"⇒cc"C")⇒``[(∀y_۱)…(∀y_n)cc"B"⇒``(∀y_۱)…(∀y_n)cc"C"]`
که در آن `cc"B"` و `cc"C"` فرمول و `y_۱ …, y_n` متغیر هستند.
علاوه بر این، تنها قاعده استنتاج `K^#` قیاس استثنایی دارد.
نشان دهید که `K^#` قضایای یکسان با K دارد. بنابراین، به قیمت اضافه کردن بنداشت‌های بیشتر، می‌توان از قاعده تعمیم صرف نظر کرد.
راهنمایی:
فرض کنید `⊢_Kcc"B"`. با استقرا روی تعداد گام‌های برهان `cc"B"` در K نشان دهید که برای هر متغیرهای
`y_۱,…,y_n(n≥۰)`
داریم:
`⊢K^#(∀y_۱)...(∀y_n)cc"B".`
