منطق محمولات: دست آوری قواعد بیشتر
منطق و فرامنطق
درآمد به منطق
منطق محمولات: دست آوری قواعد بیشتر
۱- مقدمه | ۸- قضیه ۲.۹ |
۲- فراقضیه‌های و قواعد بیشتر | ۹- تمرین |
۳- قاعده ویژه‌ساز A۴ | ۱۰- قاعده C (گزینش) |
۴- قاعده وجودی E۴ | ۱۱- قضیه ۲.۱۰ |
۵- برخی قواعد دست آوردنی | ۱۲- مثال |
۶- تمرین | ۱۳- خلاصه |
۷- لم ۲.۸ | ۱۴- تمرین |
مگر در مواردی که با نماد "" مشخص شده باشد، محتوای ارائه شده در این یادداشت از مرجع زیر برگرفته و برگردان شده است.
Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015. p. ۷۵-۸۲. ↜
■ مقدمه
در یادداشت (منطق محمولات: نظریه‌های مرتبه اول) به توضیح مفصل از تئوری‌های مرتبه اول (حساب محمولات)، ارائه گردید. نیز، در یادداشت منطق محمولات: (فرا) قضیه استنتاج (فرا)قضیه استنتاج برای این دستگاه‌ها معرفی و برهان آن ارائه شد.
این یادداشت سه قاعده دست-آوردنی (قاعده تجرید - قاعده وجودی - قاعده C) را برای تئوری‌های مرتبه اول معرفی و اثبات می‌کند. با کمک این سه قاعده و ابزارهای معرفی شده قبلی در قسمت‌های بعد به معرفی و اثبات فراقضیه تمامیت در تئوری‌های مرتبه اول خواهیم پرداخت.
■ ۲.۵ فراقضیه‌های و قواعد دست-آوردنی بیشتر
به منظور آسانی کار با تئوری‌های ویژه در ادامه، تکنیک‌های مختلفی را برای ساختن برهان‌ها معرفی خواهیم کرد. در این بخش، فرض بر این است که ما با یک تئوری دلخواه K سر و کار داریم.
اغلب در روند برهان آوری نیاز داریم `cc"B"(t)` را از `(∀x)cc"B"(x)` بدست آوریم، جایی که `t`↝ یک ترم آزاد برای `x` در `cc"B"(x)` است. این کار را می‌توان توسط قاعده دست-آوردنی زیر میسر ساخت.
■ ۲.۵.۱ قاعده ویژه‌ساز A۴
[نیز نامیده به قاعده A۴ - و نیز قاعده تجرید A۴]
اگر `t` برای `x` در `cc"B"(x)` آزاد↝ باشد آنگاه:
`(∀x)cc"B"(x)``⊢``cc"B"(t)` *
[*- از نگاه دقیق، `(∀x)cc"B"(x)⊢cc"B"(t)` یک واقعیت را در مورد دست-آوری می‌گوید. می‌گوید قاعده تجرید A۴ را باید به این معنا در نظر گرفت که، اگر `(∀x)cc"B"(x)` به عنوان مرحله‌ای در برهان رخ دهد، می‌توان `cc"B"(t)` را به عنوان مرحله بعدی در برهان نوشت (اگر `t` برای `x` در `cc"B"(x)` آزاد باشد). در این مورد و اغلب در موارد دیگر، قاعده دست آمده را به عنوان نتیجه متناظر که آن را موجه می‌کند بیان می‌کنیم.) (( به عبارت دیگر، یک قاعده دست‌آمده را با اشاره به نحوه دست آوری آن موجه می‌کنیم)).]
برهان:
از `(∀x)cc"B"(x)` و مورد `(∀x)cc"B"(x)⇒cc"B"(t)` از بنداشت (A۴)، `cc"B"(t)` را با قیاس استثنایی بدست می‌آوریم.
قاعده تجرید
از آنجا که `x` برای `x` در `cc"B"(x)` آزاد است↝، یک مورد خاص از قاعده A۴ عبارت است از:
`(∀x)cc"B"⊢cc"B"`
■ قاعده دست آوردنی بسیار مفید دیگری وجود دارد که در اصل، عکس متقارن (contrapositive) قاعده A۴ است. [: یعنی، A۴ یک مورد خاص را از یک ادعای کلی استخراج می‌کند، در حالی که E۴ (قاعده مورد اشاره در ادامه) این روند را وارون می‌کند و یک ادعای وجودی عام را از یک مورد خاص استخراج می‌کند.]
■ قاعده وجودی E۴ (تخصيص وجودی را ببینید)
فرض کنید `t` ترمی باشد که برای `x` در فرمول `cc"B"(x,t)` آزاد↝ است، و نیز `cc"B"(t,t)` از `cc"B"(x,t)` با جایگزینی تمام رویدادهای آزاد `x` با `t` حاصل شده باشد. [`cc"B"(x,t)` ممکن است شامل رویداد `t` باشد یا نباشد.] در این صورت:
`cc"B"(t,t)⊢(∃x)cc"B"(x,t)`
برهان:
کافی است نشان دهیم `⊢cc"B"(t,t)⇒(∃x)cc"B"(x,t)`.
از بنداشت A۴ داریم:
`⊢(∀x)¬cc"B"(x,t)⇒¬cc"B"(t, t)`
بنابراین، از توتولوژی `(cc"A" ⇒ ¬cc"B") ⇒ (cc"B" ⇒ ¬cc"A")` و MP داریم:
`⊢cc"B"(t,t)⇒¬(∀x)¬cc"B"(x,t)`
یک مورد خاص از این قاعده، وقتی `t` برای `x` در `cc"B"(x)` آزاد است، عبارت است از:
`cc"B"(t)⊢(∃x)cc"B"(x)`.↝
به ویژه، وقتی `t` خود `x` باشد داریم:
`cc"B"(x)⊢(∃x)cc"B"(x)`.
■ مثال
■ برخی قواعد دست آوردنی
قواعد دست آوردنی زیر بسیار زیاد سودمند هستند.
| اثبات با خلف: اگر برهانی برای `Γ,¬cc"B"⊢cc"C"∧¬cc"C"` شامل هیچ کاربرد Gen با استفاده از یک متغیر آزاد در `cc"B"` نباشد آنگاه `Γ⊢cc"B"`. (به همین صورت، `Γ⊢¬cc"B"` از `Γ،cc"B"⊢cc"C"∧¬cc"C"` به دست می‌آید.) | حذف نقیض وضع نقیض | a. `¬¬cc"B"⊢cc"B"`, b. `cc"B"⊢¬¬cc"B"` | ۱. |
| حذف عطفی | `cc"B"∧cc"C"⊢cc"B"` | ۲. | |
| `cc"B"∧cc"C"⊢cc"C"` | ۳. | ||
| `¬(cc"B"∧cc"C")⊢¬cc"B"∨¬cc"C"` | ۴. | ||
| وضع عطفی | `cc"B",cc"C"⊢cc"B"∧cc"C"` | ۵. | |
| حذف شرطی | `cc"B"∨cc"C",¬cc"B"⊢cc"C"` | ۶. | |
| `cc"B"∨cc"C",¬cc"C"⊢cc"B"` | ۷. | ||
| `¬(cc"B"∨cc"C")⊢¬cc"B"∧¬cc"C"` | ۸. | ||
| `cc"B"⇒cc"D",cc"C"⇒cc"D",cc"B"∨cc"C"⊢cc"D"` | ۹. | ||
| وضع فصلی | `cc"B"⊢cc"B"∨cc"C"` | ۱۰. | |
| `cc"C"⊢cc"B"∨cc"C"` | ۱۱. | ||
| حذف شرطی | `cc"B"⇒cc"C",¬cc"C"⊢¬cc"B"` | ۱۲. | |
| `cc"B"⇒¬cc"C",cc"C"⊢¬cc"B"` | ۱۳. | ||
| `¬cc"B"⇒cc"C",¬cc"C"⊢cc"B"` | ۱۴. | ||
| `¬cc"B"⇒¬cc"C",cc"C"⊢cc"B"` | ۱۵. | ||
| `¬(cc"B"⇒cc"C")⊢cc"B"` | ۱۶. | ||
| `¬(cc"B"⇒cc"C")⊢¬cc"C"` | ۱۷. | ||
| وضع شرطی | `cc"B",¬cc"C"⊢¬(cc"B"⇒cc"C")` | ۱۸. | |
| عکس نقیض شرطی | `cc"B"⇒cc"C"⊢¬cc"C"⇒¬cc"B"` | ۱۹. | |
| `¬cc"C"⇒¬cc"B"⊢cc"B"⇒cc"C"` | ۲۰. | ||
| حذف دو شرطی | `cc"B"⇔cc"C",cc"B"⊢cc"C"` `cc"B"⇔cc"C",¬cc"B"⊢¬cc"C"` | ۲۱. | |
| `cc"B"⇔cc"C",cc"C"⊢cc"B",` `cc"B"⇔cc"C",¬cc"C"⊢¬cc"B"` | ۲۲. | ||
| `cc"B"⇔cc"C"⊢cc"B"⇒cc"C"`, `cc"B"⇔cc"C"⊢cc"C"⇒cc"B"` | ۲۳. | ||
| وضع دو شرطی | `cc"B"⇒cc"C",cc"C"⇒cc"B"⊢cc"B"⇔cc"C"` | ۲۴. | |
| نقض دو شرطی | `cc"B"⇔cc"C"⊢¬cc"B"⇔¬cc"C"` | ۲۵. | |
| `¬cc"B"⇔¬cc"C"⊢cc"B"⇔cc"C"` | ۲۶. |
■ تمرین
۲.۳۰ قواعد دست آمده بالا را موجه کنید.
۲.۳۱ موردهای زیر را ثابت کنید.
a. `⊢(∀x)(∀y)A_۱^۲(x,y)⇒` `(∀x)A_۱^۲(x,x)`
| حل: | ||
| فرض | `(∀x)(∀y)A_۱^۲(x,y)` | ۱. |
| ۱، قاعده A۴ | `(∀y)A_۱^۲(x,y)` | ۲. |
| ۲، قاعده A۴ | `A_۱^۲(x,x)` | ۳. |
| ۳، Gen | `(∀x)A_۱^۲(x,x)` | ۴. |
| ۱-۴ | `(∀x)(∀y)A_۱^۲(x,y)⊢` `(∀x)A_۱^۲(x,x)` | ۵. |
| ۱-۵، نتیجه ۲.۶ | `⊢(∀x)(∀y)A_۱^۲(x,y)⇒` `(∀x)A_۱^۲(x,x)` | ۶. |
b. `⊢[(∀x)cc"B"]∨[(∀x)cc"C"]⇒(∀x)(cc"B"∨cc"C")`
c. `⊢¬(∃x)cc"B"⇒(∀x)¬cc"B"`
d. `⊢(∀x)cc"B"⇒(∀x)(cc"B"∨cc"C")`
e. `(∀x)(∀y)(A_۱^۲(x,y)⇒¬A_۱^۲(y,x))⇒(∀x)¬A_۱^۲(x,x)`
f. `⊢[(∃x)cc"B"⇒(∀x)cc"C"]⇒(∀x)(cc"B"⇒cc"C")`
g. `(∀x)(cc"B"∨cc"C")⇒[(∀x)cc"B"]∨(∃x)cc"C"`
h. `⊢(∀x)(A_۱^2(x,x)⇒(∃y)A_۱^۲(x,y))`
i. `⊢(∀x)(cc"B"⇒cc"C")⇒[(∀x)¬cc"C"⇒(∀x)¬cc"B"]`
j. `⊢(∃y)[A_۱^۱(y)⇒(∀y)A_۱^۱(y)]`
k.`⊢[(∀x)(∀y)(cc"B"(x,y)⇒` `cc"B"(y,x))∧(∀x)(∀y)(∀z)(cc"B"(x,y)∧` `cc"B"(y,z)⇒cc"B"(x,z))]⇒` `(∀x)(∀y)(cc"B"(x,y)⇒cc"B"(x,x))`
l. `⊢(∃x)A_1^2(x,x)⇒(∃x)(∃y)A_1^2(x,y)`
۲.۳۲ فرض کنید `cc"B"` و `cc"C"` فرمول هستند و `x` در `cc"B"` آزاد نیست. موارد زیر را ثابت کنید.
a. `⊢cc"B"⇒(∀x)cc"B"`
b. `⊢(∃x)cc"B"⇒cc"B"`
c. `⊢(cc"B"⇒(∀x)cc"C")⇔(∀x)(cc"B"⇒cc"C"`
d. `⊢((∃x)cc"C"⇒cc"B")⇔(∀x)(cc"C"⇒cc"B")`
در این مرحله، به یک قاعده دست-آوردنی نیازمندیم تا به موجب آن بتوانیم بخش `cc"C"` از فرمول `cc"B"` را با فرمولی جایگزین کنیم که اثبات آن هم‌ارز اثبات `cc"C"` است. برای این منظور ابتدا باید نتیجه کمکی زیر را ثابت کنیم.
■ لم ۲.۸
برای هر فومول `cc"B"` و `cc"C"` داریم
`⊢(∀x)(cc"B"⇔cc"C")⇒((∀x)cc"B"⇔(∀x)cc"C")`
برهان:
| فرض | `(∀x)(cc"B"⇔cc"C")` | ۱. |
| فرض | `(∀x)cc"B"` | ۲. |
| ۱، قاعده A۴ | `cc"B"⇔cc"C"` | ۳. |
| ۲، قاعده A۴ | `cc"B"` | ۴. |
| ۳، ۴، حذف دو شرطی | `cc"C"` | ۵. |
| ۵، Gen | `(∀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"` | ۸. |
| اثبات مانند ۸ | `(∀x)(cc"B"⇔cc"C")⊢(∀x)cc"C"⇒(∀x)cc"B"` | ۹. |
| ۸، ۹، وضع دو شرطی | `(∀x)(cc"B"⇔cc"C")⊢(∀x)cc"B"⇔(∀x)cc"C"` | ۱۰ |
| ۱-۱۰، نتیجه ۲.۶ | `⊢(∀x)(cc"B"⇔cc"C")⇒((∀x)cc"B"⇔(∀x)cc"C")` | ۱۱. |
■ قضیه ۲.۹
اگر `cc"C"` یک زیر فرمول `cc"B"` باشد و `cc"B"'` از جایگزینی صفر یا بیشتر از رویداد `cc"C"` در `cc"B"` با یک فرمول `cc"D"` بدست آمده باشد. نیز هر متغیر آزاد `cc"C"` یا `cc"D"` که متغیر پابند `cc"B"` باشد در لیست `y_۱,...,y_k` روی داده باشد. آنگاه:
a. `⊢[(∀y_۱)…(∀y_k)(cc"C"⇔cc"D")]⇒(cc"B"⇔cc"B"′)` (قضیه هم‌ارزی)
b. اگر `⊢cc"C"⇔cc"D"` آنگاه `⊢cc"B"⇔cc"B"′` (قضیه جایگزینی)
c. اگر `⊢cc"C"⇔cc"D"` و `⊢cc"B"` آنگاه `⊢cc"B"'`
مثال:
a. `⊢(∀x)(A_۱^۱(x)⇔A_۲^۱(x))⇒[(∃x)A_۱^۱(x)⇔(∃x)A_۲^۱(x)]`
برهان:
a. از استقرا ↜ روی تعداد رابطها و سورها در `cc"B"` استفاده می‌کنیم.
توجه داشته باشید که اگر صفر رویداد جایگزین شود، `cc"B"'` همان `cc"B"` خواهد بود و فرمول مورد اثبات موردی از توتولوژی `A⇒(B⇔B)` است.
همچنین توجه داشته باشید که اگر `cc"C"` با `cc"B"` یکسان باشد و این رویداد `cc"C"` با `cc"D"` جایگزین شود، فرمولی که باید ثابت شود، `[(∀y_۱)…(∀y_k)(cc"C"⇔cc"D")]⇒(cc"B"⇔cc"B"')`، توسط تمرین ۲.۲۷.d قابل دست آوری است.
بنابراین، می‌توان فرض کرد که `cc"C"` بخش سره‌ای از `cc"B"` است و حداقل یک رویداد `cc"C"` جایگزین‌شده است. فرض استقرای ما این است که نتیجه برای همه فرمول‌هایی با تعداد رابطها و سورهای کمتر از `cc"B"` برقرار است.
حالت ۱. `cc"B"` یک فرمول اتمی است. پس `cc"C"` نمی‌تواند بخش سره `cc"B"` باشد.
حالت ۲. فرض کنید `cc"B"` به قرار `¬ℰ` باشد. بنا به فرض استقرا داریم:
`⊢[(∀y_۱) … (∀y_k)(cc"C" ⇔ cc"D")] ⇒ (ℰ ⇔ ℰ ′)`
از این رو، با یک مورد مناسب از توتولوژی:
`(cc"C"⇒(cc"A"⇔cc"B"))⇒(cc"C"⇒(¬cc"A"⇔¬cc"B"))`
و MP خواهیم داشت:
`[(∀y_۱)…(∀y_k)(cc"C"⇔cc"D")]⇒(cc"B"⇔cc"B"′)`
حالت ۳. `cc"B"` به قرار `ℰ⇒γ` است. `cc"B"'` را `ℰ'⇒γ'` بگیرید. بنا به فرض استقرا داریم:
`⊢[(∀y_۱)…(∀y_k)(cc"C"⇔cc"D")]⇒(ℰ⇔ℰ′)`
و
` ⊢[(∀y_۱) … (∀y_k)(cc"C"⇔cc"D")]⇒(γ⇔γ′).`
با یک مورد مناسب از توتولوژی:
`(A ⇒ (B ⇔ C)) ∧ (A ⇒ (D ⇔ E))` ⇒ `(A ⇒ [(B ⇒ D) ⇔ (C ⇒ E)])`
می‌توان نوشت:
`⊢ [(∀y_۱) … (∀y_k)(cc"C" ⇔ cc"D")] ⇒ (cc"B" ⇔ cc"B" ′)`.
حالت ۴. `cc"B"` به قرار `(∀x)ℰ` است. فرض کنید `cc"B"'` از قرار `(∀x)ℰ'` باشد. بنا به فرض استقرا داریم:
`⊢ [(∀y_1) … (∀y_k) (cc"C" ⇔ cc"D")] ⇒ (ℰ ⇔ ℰ′)`
در این حالت، `x` در `(∀y_۱) ... (∀y_k) (cc"C" ⇔ cc"D")` به صورت آزاد رخ نمی‌دهد، زیرا اگر چنین بود، در `cc"C"` یا `cc"D"` آزاد خواهد بود و از آنجا که در `cc"B"` پابند است، یکی از متغیرهای `y_۱, …, y_k` نیست و در `(∀y۱) … (∀yk) (cc"C" ⇔ cc"D")` آزاد نخواهد بود. بنابراین، با استفاده از بنداشت (A۵) می‌توان
`⊢(∀y_۱)…(∀yk)(cc"C"⇔cc"D")⇒(∀x)(ℰ⇔ℰ')`
را به دست آورد. اما، توسط لم ۲.۸ داریم:
`⊢ (∀x)(ℰ ⇔ ℰ) ⇒ ((∀x)ℰ ⇔ (∀x)ℰ ')`.
سپس توسط یک توتولوژی مناسب و MP داریم:
`⊢ [(∀y_۱) … (∀y_k) (cc"C" ⇔ cc"D")] ⇒ (cc"B" ⇔ cc"B"' )`.
b. از `⊢ cc"C" ⇔ cc"D"`، با چندین کاربرد Gen می‌توان `⊢(∀y_۱)...(∀y_k)(cc"C"⇔cc"D")` را به دست آورد. سپس توسط (a) و MP خواهیم داشت `⊢cc"B"⇔cc"B"'`.
c. توسط (b) و MP و حذف دوشرطی.
■ تمرین
۲.۳۳ موردهای زیر را ثابت کنید.
a. `⊢(∃x)¬cc"B"⇔¬(∀x)cc"B"`
حل:
با کاربرد قضیه جایگزینی و این که `⊢¬¬cc"B"⇔cc"B"`. جایگزینی `¬(∀x)¬¬cc"B"` با کوته نوشت آن، یعنی `(∃x)¬cc"B"`.
b. `⊢(∀x)cc"B"⇔¬(∃x)¬cc"B"`
c. `⊢(∃x)(cc"B"⇒¬(cc"C"∨cc"D"))⇒(∃x)(cc"B"⇒¬cc"C"∧¬cc"D")`
d. `⊢(∀x)(∃y)(cc"B"⇒cc"C")⇔(∀x)(∃y)(¬cc"B"∨cc"C")`
e. `⊢(∀x)(cc"B"⇒¬cc"C")⇔¬(∃x)(cc"B"∧cc"C")`
۲.۳۴ با یک مثال نقض نشان دهید که نمی‌توانیم سورهای `(∀y_۱)…(∀y_k)` در گزاره ۲.۹(a) را حذف کنیم.
۲.۳۵ اگر `cc"C"` از `cc"B"` با پاک کردن همه سورهای `(∀x)` یا `(∃x)` که دامنه آنها حاوی `x` آزاد نیست به دست آمد باشد، ثابت کنید که `⊢cc"B"⇔cc"C"`.
۲.۳۶ برای هر فرمول `cc"B"` در زیر، فرمول `cc"C"` را طوری بیابید که `⊢cc"C"⇔¬cc"B"` و رابط‌های نقیض در `cc"C"` فقط برای فرمول‌های اتمی اعمال شده باشند.
a. `(∀x)(∀y)(∃z)A_۱^۳(x,y,z)`
b. `(∀ε)(ε>۰⇒``(∃cc"D")(cc"D">۰∧(∀x)(|x−c|<cc"D"⇒``|f(x)−f(c)|<ε))`
c. `(∀ε)(ε>۰⇒(∃n)(∀m)(m>n⇒|a_m−b|<ε))`
۲.۳۷ فرض کنید `cc"B"` فرمولی باشد که حاوی ⇒ و ⇔ نباشد. سورهای کلی و وجودی را با یک دیگر جابجا، نیز ∧ و ∨ را با یک دیگر جابجا کنید. نتیجه `cc"B"^**` را همزاد `cc"B"` می‌نامند.
a.
`⊢cc"B"` اگر و تنها اگر `⊢¬cc"B"^**`
`⊢cc"B"⇒cc"C"` اگر و تنها اگر `⊢cc"C"^**⇒cc"B"^**`
`⊢cc"B"⇔cc"C"` اگر و تنها اگر `⊢cc"B"^**⇔cc"C"^**`
`(∃x)(cc"B"∨cc"C")⇔[((∃x)cc"B")∨(∃x)cc"C"]`. [راهنمایی: تمرین (c)۲.۲۷ را بکار بزنید.]
b.
نشان دهید که نتایج همزادی در (a) برای (i) - (iii) برای نظریه‌های دلخواه برقرار نیست.
■ قاعده C
در ریاضیات روشی به قرار زیر برای استدلال است که بسیار رایج است.
فرض کنید فرمولی به صورت `(∃x)cc"B"(x)` را ثابت کرده باشیم. در این صورت می‌گوییم، فرض کنید `b` یک شی باشد به قسمی که `cc"B"(b)`. سپس، برهان را ادامه می‌دهیم و سرانجام به فرمولی می‌رسیم که شی `b` را که به‌طور دلخواه انتخاب شده در بر نمی‌گیرد.
برای مثال، فرض کنید می‌خواهیم نشان دهیم که:
`(∃x)(cc"B"(x)⇒cc"C"(x)),(∀x)cc"B"(x)⊢(∃x)cc"C"(x).`
| فرض | `(∃x)(cc"B"(x)⇒cc"C"(x))` | ۱. |
| فرض | `(∀x)cc"B" (x)` | ۲. |
| ۱ | `cc"B"(b)⇒cc"C"(b)` برای برخی `b` | ۳. |
| ۲، قاعده A۴ | `cc"B"(b)` | ۴. |
| ۳، ۴، MP | `cc"C"(b)` | ۵. |
| ۵، قاعده E۴ | `(∃x)cc"C"(x)` | ۶. |
به نظر می‌رسد چنین برهانی بر مبنای شهود کاملاً پذیرفتنی باشد. در واقع نیز، می‌توانیم بدون گزینش دلخواه شی `b` در مرحله ۳ به همان نتیجه برسیم. این کار را می‌توان به صورت زیر انجام داد:
| فرض | `(∀x)cc"B" (x)` | ۱. |
| فرض | `(∀x)¬cc"C"(x)` | ۲. |
| ۱، قاعده A۴ | `cc"B" (x)` | ۳. |
| ۲، قاعده A۴ | `¬cc"C"(x)` | ۴. |
| ۳، ۴، وضع شرطی | `¬(cc"B" (x)⇒cc"C" (x))` | ۵. |
| ۵، Gen | `(∀x)¬(cc"B"(x)⇒cc"C"(x))` | ۶. |
| ۱-۶ | `(∀x)cc"B"(x),(∀x)¬cc"C"(x)``⊢(∀x)¬(cc"B"(x)⇒cc"C"(x)) ` | ۷. |
| ۱-۷، نتیجه ۲.۶ | `(∀x)cc"B"(x)⊢(∀x)¬cc"C"(x)⇒``x)¬(cc"B"(x)⇒cc"C"(x))` | ۸. |
| ۸، عکس نقیض | `(∀x)cc"B"(x)⊢¬(∀x)¬(cc"B"(x)⇒``cc"C"(x))⇒¬(∀x)¬cc"C"(x)` | ۹. |
| کوته‌نوشت ۹ | `(∀x)cc"B"(x)⊢``(∃x)(cc"B"(x)⇒``cc"C" (x))``⇒(∃x)cc"C"(x)` | ۱۰ |
| ۱۰، MP | `(∃x)(cc"B"(x)⇒cc"C"(x))`, `(∀x)cc"B"(x)⊢(∃x)cc"C"(x)` | ۱۱. |
به طور کلی، هر wf که بتوان آن را با استفاده از تعداد محدود از گزینش‌های (اشیاء) دلخواه اثبات کرد، بدون اعمال چنین انتخابی نیز قابل اثبات است. قاعده‌ای را که به ما اجازه میدهد از `(∃x)cc"B"(x)` به `cc"B"(b)` برسیم، قاعده «C» (C برای «Choice») می‌نامیم. به طور دقیق‌تر، قاعده C در یک تئوری مرتبه اول K به صورت زیر تعریف می‌شود:
قاعده C:
`Γ⊢_C cc"B"` اگر و فقط اگر دنباله‌ای از wfهای `cc"D"_۱,…, cc"D"_n` وجود داشته باشد به قسمی که `cc"D"_n` همان `cc"B"` باشد و چهار شرط زیر برقرار باشد:
۱. برای هر `i<n`،
`cc"D"_i` یک بنداشت K است، یا
`cc"D"_i` در `Γ` است، یا
`cc"D"_i` با MP یا Gen از wfهای پیشین در دنباله بدست آمده است، یا
یک `(∃x)cc"C"(x)` مقدم وجود دارد به قسمی که `cc"D"_i` عبارت از `cc"C" (d)` است، که در آن `d` یک ثابت انفرادی جدید است (قاعده C).
۲. به عنوان بنداشت‌ها در شرط ۱.(a)، ما همچنین می‌توانیم از همه بنداشت‌های منطقی استفاده کنیم که شامل ثابت‌های انفرادی جدیدی هستند که قبلاً با اعمال قاعده C در دنباله معرفی شده‌اند.
۳. هیچ کاربرد Gen با استفاده از متغیری آزاد در برخی `(∃x)cc"C"(x)` که قاعده C قبلاً برای آن اعمال شده است، انجام نمی‌شود.
۴. `cc"B"` شامل هیچ یک از ثابت‌های انفرادی جدید معرفی شده در دنباله در هیچ کاربستن قاعده C نیست.
در مورد دلیل گنجاندن شرط ۳ باید چند کلمه گفت. اگر استفاده از قاعده C روی فرمول `(∃x)cc"C"(x)` نتیجه `cc"C"(d)` را به دست دهد، آنگاه شی مورد ارجاع توسط `d` ممکن است به مقادیر متغیرهای آزاد در `(∃x)cc"C"(x)` بستگی داشته باشد. به طوری که یک شی ممکن است `cc"C" (x)` را برای همه مقادیر متغیرهای آزاد در `(∃x)cc"C"(x)` برآورده↝ نکند. به عنوان مثال، بدون بند ۳، می‌توانیم به شیوه زیر عمل کنیم:
| فرض | `(∀x)(∃y)A_۱^۲(x,y)` | ۱. |
| ۱، قاعده A۴ | `(∃y)A_۱^۲(x,y)` | ۲. |
| ۲، قاعده C | `A_۱^۲(x,d)` | ۳. |
| ۳، Gen | `(∀x)A_۱^۲(x,d)` | ۴. |
| ۴، قاعده E۴ | `(∃y)(∀x)A_۱^۲ (x,y)` | ۵. |
اما، تعبیری وجود دارد که `(∀x)(∃y)A_1^2(x,y)` درست است اما `(∃y)(∀x)A_1^2(x,y)` نادرست است. دامنه را مجموعه اعداد صحیح در نظر و تعبیر `A_1^2(x,y)` را `x<y` بگیرید.
■ قضیه ۲.۱۰
اگر `Γ⊢_C cc"B"`، آنگاه `Γ⊢ cc"B",`. افزون بر این، از برهان زیر به راحتی می‌توان دریافت که، اگر کاربرد Gen در برهان جدید `cc"B"` از `Γ` با استفاده از یک متغیر مشخص وجود داشته باشد و بر روی یک فرمول وابسته به فرمول خاصی از `Γ` اعمال شود، آنگاه چنین کاربرد Gen در برهان اصلی وجود می‌داشت.*
به نظر می‌رسد اولین فرمول بندی نسخه‌ای از قاعده C مشابه آنچه در اینجا ارائه شده است از Rosser (1953) باشد.
Rosser, J.B (1953).Logic for Mathematicians. McGraw-Hill (second edition, Chelsea, 1978)
برهان:
فرض کنید:
`(∃y_۱)\mathcal{C}_۱(y_۱), … , (∃y_k)\mathcal{C}_k(y_k)`
فرمول‌هایی هستند که به ترتیب رویداد قاعده C در برهان `Γ⊢_C cc"B"` اعمال شده باشند، نیز `d_۱,…, d_k` ثابت‌های انفرادی جدید مربوطه باشند.
در این صورت:
`Γ،\mathcal{C}_۱(d_۱),…,\mathcal{C}_k(d_k))⊢cc"B"`.
اکنون، طبق شرط ۳ تعریف بالا، نتیجه ۲.۶ قابل کار زدن است، که نتیجه میدهد:
`Γ, \mathcal{C}_۱(d_۱),…,\mathcal{C}_(k-۱)(d_(k-۱))⊢\mathcal{C}_k(d_k)⇒cc"B"`
حالا، `d_k` را در همه جا با یک متغیر `z` که در برهان وجود ندارد جایگزین می‌کنیم. خواهیم داشت:
`Γ, \mathcal{C}_۱(d_۱),…,\mathcal{C}_(k-۱)(d_(k-۱))⊢\mathcal{C}_k(z)⇒cc"B"`
و با کار زدن Gen داریم:
`Γ, \mathcal{C}_۱(d_۱),…,\mathcal{C}_(k-۱)(d_(k-۱))⊢(∀z)\mathcal{C}_k(z)⇒cc"B")`
از اینجا بنا به تمرین ۲.۳۲(d):
`Γ, \mathcal{C}_۱(d_۱),…,\mathcal{C}_(k-۱)(d_(k-۱))⊢(∃y_k)\mathcal{C}_k(y_k)⇒cc"B"`
اما
`Γ, \mathcal{C}_۱(d_۱),…,\mathcal{C}_(k-۱)(d_(k-۱))⊢(∃y_k)\mathcal{C}_k(y_k)`
اکنون با MP خواهیم داشت:
`Γ, \mathcal{C}_۱(d_۱),…,\mathcal{C}_(k-۱)(d_(k-۱))⊢cc"B"`
با تکرار این استدلال می‌توان عناصر دنباله `\mathcal{C}_(k−۱)(d_(k−۱)), …, \mathcal{C}_۱(d_۱)` را یکی بعد از دیگری حذف کرد تا سرانجام به `Γ⊢cc"B"` برسیم.
■ مثال:
`⊢(∀x)(cc"B"(x)⇒cc"C"(x))⇒((∃x)cc"B"(x)⇒(∃x)cc"C"(x))`
| فرض | `(∀x)(cc"B"(x)⇒cc"C" (x))` | ۱. |
| فرض | `(∃x)cc"B"(x)` | ۲. |
| ۲، قاعده C | `cc"B"(d)` | ۳. |
| ۱، قاعده A۴ | `cc"B"(d)⇒cc"C"(d)` | ۴. |
| ۳، ۴، MP | `cc"C"(d)` | ۵. |
| ۵، قاعده E۴ | `(∃x)cc"C"(x)` | ۶. |
| ۱-۶ | `(∀x)(cc"B"(x)⇒cc"C"(x)),``(∃x)cc"B"(x)⊢cc"C"(∃x)cc"C"(x)` | ۷. |
| ۷، قضیه ۲.۱۰ | `(∀x)(cc"B"(x)⇒cc"C"(x)),``(∃x)cc"B"(x)⊢(∃x)cc"C"(x)` | ۸. |
| ۱-۸، نتیجه ۲.۶ | `(∀x)(cc"B"(x)⇒cc"C"(x))⊢``(∃x)cc"B"(x)⇒(∃x)cc"C"(x)` | ۹. |
| ۱-۹، نتیجه ۲.۶ | `⊢(∀x)(cc"B"(x)⇒cc"C"(x))⇒``((∃x)cc"B"(x)⇒(∃x)cc"C"(x))` | ۱۰. |
■ خلاصه (۱ - ۲ - ۳)
■ بنداشت‌های منطقی
(A۱) `cc"A" ⇒ (cc"B" ⇒ cc"A")`
(A۲) `((cc"A" ⇒ (cc"B" ⇒ cc"C")) ⇒ ((cc"A" ⇒ cc"B") ⇒ (cc"A" ⇒ cc"C"))`
(A۳) `(¬cc"A" ⇒ ¬cc"B") ⇒ ((¬cc"A" ⇒ cc"B") ⇒ cc"A")`
(A۴) `(∀x_i)cc"B"(x_i)⇒cc"B"(t)`
در (A۴) `cc"B"(x_i)` فرمول ℒ و `t` ترم ℒ است و افزون بر این `t` در `cc"B"(x_i)` برای `x_i` آزاد است. [↝-↝ ]
☜: در (A۴) وقتی `t` متغیر `x_i` باشد داریم:
(A۴') `(∀x_i)cc"B"(x_i)⇒cc"B"`
(A۵) `(∀x_i)((cc"B"⇒cc"C"))⇒(cc"B"⇒(∀x_i)cc"C")`
به شرط آنکه `cc"B"` شامل رویداد آزاد `x_i` نباشد.
■ (۲.۳.۳) قواعد استنتاج
۱- قیاس استثنایی (Modus ponens): `cc"C"` از `cc"B"` و `cc"B"⇒cc"C"` بدست می‌آید. (↝ - ↝) [با کوته‌نوشت: MP]
`cc"B"` , `cc"B"⇒cc"C"`
———————————
`cc"C"`
۲- تعمیم (Generalization): `(∀x_i)cc"B"` از `cc"B"` بدست می‌آید. (↝) [با کوته‌نوشت: Gen]
`cc"B"`
———————————
`(∀x_i)cc"B"`
[توجه: به `x_i` در قاعده تعمیم متغیر سوردار شده گفته می‌شود.]
■ فراقضیه استنتاج
اگر
`Γ,cc"B"⊢cc"C"`
آنگاه
`Γ⊢cc"B"⇒cc"C"`
به شرط آنکه در استنتاج `Γ,cc"B"⊢cc"C"` از قاعده تعمیم با متغیرهای سوردارشده که در `cc"B"` آزاد هستند استفاده نشده باشد.
■ قواعد دست آمدنی
قاعده ویژه‌ساز A۴
`(∀x)cc"B"⊢cc"B"`
قاعده وجودی E۴
`cc"B"(x)⊢(∃x)cc"B"(x)`
قاعده C:
`Γ⊢_C cc"B"` اگر و فقط اگر دنباله‌ای از wfهای `cc"D"_۱,…, cc"D"_n` وجود داشته باشد به قسمی که `cc"D"_n` همان `cc"B"` باشد و چهار شرط زیر برقرار باشد:
۱. برای هر `i<n`،
`cc"D"_i` یک بنداشت K است، یا
`cc"D"_i` در `Γ` است، یا
`cc"D"_i` با MP یا Gen از wfهای پیشین در دنباله بدست آمده است، یا
یک `(∃x)cc"C"(x)` مقدم وجود دارد به قسمی که `cc"D"_i` عبارت از `cc"C" (d)` است، که در آن `d` یک ثابت انفرادی جدید است.
۲. به عنوان بنداشت‌ها در شرط ۱.(a)، ما همچنین می‌توانیم از همه بنداشت‌های منطقی استفاده کنیم که شامل ثابت‌های انفرادی جدیدی هستند که قبلاً با اعمال قاعده C در دنباله معرفی شده‌اند.
۳. هیچ کاربرد Gen با استفاده از متغیری آزاد در برخی `(∃x)cc"C"(x)` که قاعده C قبلاً برای آن اعمال شده است، انجام نمی‌شود.
۴. `cc"B"` شامل هیچ یک از ثابت‌های انفرادی جدید معرفی شده در دنباله در هیچ کاربستن قاعده C نیست.
■ تمرین
برای اثبات تمرینات ۲.۴۵-۲.۳۸ از قاعده C و قضیه ۲.۱۰ استفاده کنید.
۲.۳۸ `⊢(∃x)(cc"B"(x)⇒cc"C"(x))⇒((∀x)cc"B"(x)⇒(∃x)cc"C"(x))`
۲.۳۹ `¬(∃y)(∀x))(A_۱^۲(x,y)⇔¬A_۱^۲(x,x))`
۲.۴۰ `⊢[(∀x)(A_۱^۱(x)⇒``A_۲^۱(x)∨A_۳^۱(x))∧``¬(∀x)(A_۱^۱(x)⇒``A_۲^۱(x))]⇒``(∃x)(A_۱^۱(x)∧A_۳^۱(x))`
۲.۴۱ `⊢[(∃x)cc"B"(x)]∧[(∀x)cc"C"(x)]⇒``(∃x)(cc"B"(x)∧cc"C"(x))`
۲.۴۲ `⊢(∃x)cc"C"(x)⇒(∃x)(cc"B"(x)∨cc"C"(x))`
۲.۴۳ `⊢(∃x)∃y)cc"B"(x,y)⇔(∃y)(∃x)cc"B"(x,y)`
۲.۴۴ `⊢(∃x)(∀y)cc"B"(x,y)⇒``(∀y)(∃x)cc"B"(x,y)`
۲.۴۵ `⊢(∃x)(cc"B"(x)∧cc"C"(x))⇒``((∃x)cc"B"(x))∧(∃x)cc"C"(x)`
۲.۴۶ در دست آوری‌های ادعایی زیر چه چیزی خطا است؟
a.
| فرض | `(∃x)cc"B"(x)` | ۱. |
| ۱، قاعده C | `cc"B"(d)` | ۲. |
| فرض | `(∃x)cc"C"(x)` | ۳. |
| ۳، قاعده C | `cc"C"(d)` | ۴. |
| ۲، ۴، وضع عطفی | `cc"B"(d)∧cc"C"(d)` | ۵. |
| ۵، قاعده E۴ | `(∃x)(cc"B"(x)∧cc"C"(x))` | ۶. |
| ۱-۶، قضیه ۲.۱۰ | `(∃x)cc"B"(x),` `(∃x)cc"C"(x)⊢``(∃x)(cc"B"(x)∧cc"C"(x))` | ۷. |
