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