منطق محمولات: (فرا) قضیه استنتاج

منطق و فرامنطق

درآمد به منطق


روند منطق محمولات: زبان، تعبیر و مدل (۲)

۱- مقدمه

۹- قضیه ۲.۴

۲- ویژگی‌های تئوری‌های مرتبه اول

۱۰- قضیه ۲.۵: قضیه استنتاج

۳- قضیه ۲.۱

۱۱- نتیجه ۲.۶: پیامد استنتاج (۱)

۴- قضیه ۲.۲

۱۲- نتیجه ۲.۷: پیامد استنتاج (۲)

۵- تعریف: سازگاری تئوری

۱۳- گسترش قضیه‌های ۲.۴ تا ۲.۷

۶- نتیجه ۲.۳. سازگاری حساب محمولات مرتبه اول

۱۴- مثال: کارزدن قضیه استنتاج

۷- درباره قضیه استنتاج

۱۵- تمرین

۸- وابستگی فرمولی

توجه: مگر در مواردی که با نماد "توجه:" مشخص شده باشد، محتوای ارائه شده در این یادداشت از مرجع زیر برگرفته و برگردان شده است.

Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015. p. ۶۹-۷۳.


عضو- عضویت و نظریه مجموعه ها (۱) -  (ریاضیات)

توجه: ■ مقدمه

`∀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) بنداشت‌های () و () منطقاً معتبر هستند.

بنا بر ویژگی‌های (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"` دارد اگر و تنها اگر:

  1. `cc"D"_i` همان `cc"B"` است و توجیه `cc"D"_i` تعلق آن به `Γ` است، یا

  2. `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 )`.

اکنون بنا به بنداشت () داریم:

`⊢(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`.

اکنون با بنداشت () داریم `⊢cc"D"_i⇒(cc"B"⇒cc"D"_i)`.

بنابراین بنا بر MP داریم `Γ⊢cc"B"⇒cc"D"_i`.


از طرف دیگر، اگر `x_k` یک متغیر آزاد `cc"B"` نباشد، با توجه به بنداشت (

`⊢(∀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".`

۲.۲۹:

گسترش قضیه‌های ۲.۴ تا ۲.۷ در بالا را اثبات کنید.


توجه: