(فرا) قضیه استنتاج

منطق محمولات و نظریه مدل

درآمد به منطق

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

۱- مقدمه	۹- قضیه ۲.۴
۲- ویژگی‌های تئوری‌های مرتبه اول	۱۰- قضیه ۲.۵: قضیه استنتاج
۳- قضیه ۲.۱	۱۱- نتیجه ۲.۶: پیامد استنتاج (۱)
۴- قضیه ۲.۲	۱۲- نتیجه ۲.۷: پیامد استنتاج (۲)
۵- تعریف: سازگاری تئوری	۱۳- گسترش قضیه‌های ۲.۴ تا ۲.۷
۶- نتیجه ۲.۳. سازگاری حساب محمولات مرتبه اول	۱۴- مثال: کارزدن قضیه استنتاج
۷- درباره قضیه استنتاج	۱۵- تمرین
۸- وابستگی فرمولی

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

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

۱- مراد از مجموعه شمارا (Denumerable set) یک مجموعه‌ شمارای نامتناهی است مگر آنکه با صراحت قید شده باشد.

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

■ مقدمه

$\forall x (M a n (x) \to M or t a l (x))$ $∀x (Man(x)→Mortal(x))$

در یادداشت (منطق محمولات: نظریه‌های مرتبه اول) در باره تئوری‌های مرتبه اول (حساب محمولات)، بنداشت‌های منطقی، بنداشت‌های سره و قواعد استنتاج شرح درخور آمده است. در این یادداشت به ویژگی‌های این دستگاه‌ه و معرفی و اثبات (فرا)قضیه استنتاج برای این دستگاه‌ها می‌پردازیم.

■ ۲.۴ ویژگی‌های تئوری‌های مرتبه اول

همه نتایج در این بخش به یک تئوری مرتبه اول دلخواه K اشاره می‌کند. بجای نوشتن↝ $⊢_{K} B$ $⊢_K cc"B"$ ، گاهی اوقات تنها $⊢ B$ $⊢ cc"B"$ را می‌نویسیم، افزون بر این، به تئوری‌های مرتبه اول صرفاً با عنوان تئوری اشاره خواهیم کرد، مگر اینکه چیزی خلاف آن گفته شود.

■ قضیه ۲.۱

هر فرمول $B$ $cc"B"$ در K که موردی از یک توتولوژی است یک قضیه ↝ K است و می‌توان آن را فقط با کارزدن بنداشت‌های (A۱) تا (A۳) و MP ثابت کرد.

اثبات:

فرض کنید فرمول $B$ $cc"B"$ از توتولوژی $C$ $cc"C"$ توسط جانشین سازی بدست آمده باشد. بنا بر تمامیت ℒ، برهانی برای $C$ $cc"C"$ در ℒ وجود دارد. در چنین برهانی، از همان جانشین سازی فرمول‌های K برای حروف محمولی استفاده کنید که در بدست آوردن $B$ $cc"B"$ از $C$ $cc"C"$ استفاده شده است. و هر حرف گزاره‌ای در برهان که در $C$ $cc"C"$ نیست را با فرمول دلخواهی از K جانشین کنید. در این صورت، دنباله حاصل از فرمول‌ها برهان $B$ $cc"B"$ است، و این برهان فقط از بنداشت‌های (A۱) تا (A۳) و MP استفاده می‌کند.

■ قضیه ۲.۲

هر قضیه ↝ یک حساب محمولات مرتبه اول منطقاً معتبر است.

اثبات:

بنداشت‌های (A۱) تا (A۳) بنا به ویژگی (VII) انگاشت صدق↝↝ منطقاً معتبر هستند. (صفحه ۵۸ را ببینید). و بنا بر (X) و (XI) بنداشت‌های ( A۴) و ( A۵) منطقاً معتبر هستند.

بنا بر ویژگی‌های (III) و (VI)، قواعد استنتاج MP و Gen اعتبار منطقی را حفظ می‌کنند، بنابراین، هر قضیه یک حساب محمولات منطقاً معتبر است.

مثال:

فرمول

$(\forall x_{۲}) (\exists x_{۱}) A_{۱}^{۲} (x_{۱}, x_{۲}) \Rightarrow (\exists x_{۱}) (\forall x_{۲}) A_{۱}^{۲} (x_{۱}, x_{۲})$ $(∀x_۲)(∃x_۱)A_۱^۲(x_۱, x_۲)⇒(∃x_۱)(∀x_۲)A_۱^۲(x_۱, x_۲)$

یک قضیه برای هر حساب مرتبه اول نیست، چراکه منطقاً معتبر نیست. (مثال ۵ صفحه ۶۳ را ببینید.)

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

تئوری K سازگار است اگر هیچ فرمول $B$ $cc"B"$ و نقیض آن $\neg B$ $¬cc"B"$ هر دو در K قابل اثبات نباشند. یک تئوری ناسازگار است اگر سازگار نباشد.

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

هر حساب محمولات مرتبه اول سازگار است. ↜

اثبات:

اگر فرمول $B$ $cc"B"$ و نقیض آن $\neg B$ $¬cc"B"$ هر دو قضیه یک حساب محمولات مرتبه اول باشند، از قضیه ۲.۲ داریم هر دو $B$ $cc"B"$ و نقیض آن $\neg B$ $¬cc"B"$ منطقاً معتبر خواهند بود، که ممکن نیست.

توجه داشته باشید که در یک تئوری ناسازگار K، هر فرمول ℒ از K در K اثبات شدنی است. در واقع، فرض کنید که فرمول $B$ $cc"B"$ و $\neg B$ $¬cc"B"$ هر دو در K اثبات شدنی باشند. از آنجا که فرمول

$B \Rightarrow (\neg B \Rightarrow C)$ $cc"B"⇒(¬cc"B" ⇒ cc"C")$

موردی از یک توتولوژی است(↝) از قضیه ۲.۱ می‌دانیم که این فرمول در K اثبات شدنی است. از اینجا با دو بار کاربرد MP خواهیم داشت $⊢ C$ $⊢cc"C"$ .

از این ملاحظه برمی‌آید که، اگر برخی فرمول تئوری K قضیه K نباشد آنگاه K سازگار است.

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

قضیه استنتاج (قضیه ۱.۹) برای حساب گزاره‌ها را نمی‌توان بدون اصلاح به تئوری‌های مرتبه اول آورد. برای نمونه، برای هر فرمول $B$ $cc"B"$ داریم

$B ⊢_{K} (\forall x_{i}) B$ $cc"B"⊢_K(∀x_i)cc"B"$ ,

اما همیشه چنین نیست که

$⊢_{K} B \Rightarrow (\forall x_{i}) B$ $⊢_K cc"B"⇒(∀x_i)cc"B"$ .

اکنون، دامنه‌ای را در نظر بگیرید که شامل حداقل دو عنصر $c$ $c$ و $d$ $d$ باشد. فرض کنید K یک حساب محمولات باشد و $B$ $cc"B"$ را به قرار $A_{۱}^{۱} (x_{۱})$ $A_۱^۱(x_۱)$ بگیرید. $A_{۱}^{۱}$ $A_۱^۱$ را به عنوان یک ویژگی که فقط برای $c$ $c$ برقرار است تعبیر کنید.

در این صورت $A_{۱}^{۱} (x_{۱})$ $A_۱^۱(x_۱)$ با هر دنباله $s = (s_{۱}, s_{۲}, \dots)$ $s=(s_۱, s_۲, …)$ که در آن $s_{۱} = c$ $s_۱ = c$ برآورده می‌شود.

اما $(\forall x_{۱}) A_{۱}^{۱} (x_{۱})$ $(∀x_۱)A_۱^۱(x_۱)$ با هیچ دنباله‌‌ای برآورده نمی‌شود. از این رو، فرمول:

$A_{۱}^{۱} (x_{۱}) \Rightarrow (\forall x_{۱}) A_{۱}^{۱} (x_{۱})$ $A_۱^۱(x_۱)⇒(∀x_۱)A_۱^۱(x_۱)$

در این تعبیر درست نیست و بنابراین منطقاً معتبر هم نیست. از اینجا، بنا به قضیه ۲.۲، $A_{۱}^{۱} (x_{۱}) \Rightarrow (\forall x_{۱}) A_{۱}^{۱} (x_{۱})$ $A_۱^۱(x_۱)⇒(∀x_۱)A_۱^۱(x_۱)$ یک قضیه K نیست.

با این حال، ممکن است صورتی اصلاح شده، اما همچنان سودمند، از قضیه استنتاج را بدست ‌آورد.

■ وابستگی فرمولی

فرض کنید $B$ $cc"B"$ یک فرمول در مجموعه فرمول $Γ$ $Γ$ باشد و فرض کنید که یک استنتاج $D_{۱}, ..., D_{n}$ $cc"D"_۱,...,cc"D"_n$ از $Γ$ $Γ$ به همراه توجیه برای هر مرحله در استنتاج به ما داده شده است. می‌گوییم: $D_{i}$ $cc"D"_i$ در این برهان بستگی به $B$ $cc"B"$ دارد اگر و تنها اگر:

$D_{i}$ $cc"D"_i$ همان $B$ $cc"B"$ است و توجیه $D_{i}$ $cc"D"_i$ تعلق آن به $Γ$ $Γ$ است، یا
$D_{i}$ $cc"D"_i$ به عنوان یک نتیجه مستقیم کارزدن MP یا Gen به برخی از فرمول‌های قبلی دنباله توجیه می‌شود، جایی که حداقل یکی از این فرمول‌های قبلی به $B$ $cc"B"$ بستگی دارد.

مثال:

$B, (\forall x_{۱}) B \Rightarrow C ⊢ (\forall x_{۱}) C$ $cc"B", (∀x_۱)cc"B"⇒cc"C"⊢(∀x_۱)cc"C"$

فرض	$B$ $cc"B"$	$(D_{۱})$ $(cc"D"_۱)$
$(D_{۱})$ $(cc"D"_۱)$ , Gen	$(\forall x_{۱}) B$ $(∀x_۱)cc"B"$	$(D_{۲})$ $(cc"D"_۲)$
فرض	$(\forall x_{۱}) B \Rightarrow C$ $(∀x_۱)cc"B"⇒cc"C"$	$(D_{۳})$ $(cc"D"_۳)$
$(D_{۲})$ $(cc"D"_۲)$ , $(D_{۳})$ $(cc"D"_۳)$ , MP	$C$ $cc"C"$	$(D_{۴})$ $(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".$

۲.۲۹:

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

document.write('<img src="' + img1 + '">'); منطق محمولات: زبان، تعبیر و مدل (۲)

■ مقدمه

■ ۲.۴ ویژگی‌های تئوری‌های مرتبه اول

■ قضیه ۲.۱

■ قضیه ۲.۲

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

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

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

■ وابستگی فرمولی

■ قضیه ۲.۴

■ قضیه ۲.۵: قضیه استنتاج

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

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

■ گسترش قضیه‌های ۲.۴ تا ۲.۷

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

تمرین (۷۳) (۲.۲۷ - ۲.۲۹):

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