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

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

درآمد به منطق

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

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

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

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"_۴)$
$(D_{۴})$ $(cc"D"_۴)$ , Gen	$(\forall x_{۱}) C$ $(∀x_۱)cc"C"$	$(D_{۵})$ $(cc"D"_۵)$

در اینجا، $(D_{۱})$ $(cc"D"_۱)$ و $(D_{۲})$ $(cc"D"_۲)$ به $B$ $cc"B"$ بستگی دارند. $(D_{۳})$ $(cc"D"_۳)$ به $(\forall x_{۱}) B \Rightarrow C$ $(∀x_۱)cc"B"⇒cc"C"$ بستگی دارد. $(D_{۴})$ $(cc"D"_۴)$ به $B$ $cc"B"$ و $(\forall x_{۱}) B \Rightarrow C$ $(∀x_۱)cc"B"⇒cc"C"$ بستگی دارد. $(D_{۵})$ $(cc"D"_۵)$ به $B$ $cc"B"$ و $(\forall x_{۱}) B \Rightarrow C$ $(∀x_۱)cc"B"⇒cc"C"$ بستگی دارند.

■ قضیه ۲.۴

اگر $C$ $cc"C"$ به $B$ $cc"B"$ در استنتاج $Γ, B ⊢ C$ $Γ,cc"B"⊢cc"C"$ بستگی نداشته باشد آنگاه $Γ ⊢ C$ $Γ⊢cc"C"$ .

اثبات:

فرض کنید $D_{۱} \dots ، D_{n}$ $cc"D"_۱ …، cc"D"_n$ استنتاج $C$ $cc"C"$ از $Γ$ $Γ$ و $B$ $cc"B"$ باشد، که در آن $C$ $cc"C"$ به $B$ $cc"B"$ بستگی ندارد. (در این استنتاج $D_{n}$ $cc"D"_n$ همان $C$ $cc"C"$ است.)

اکنون بنا بر استقرا فرض می‌کنیم این قضیه برای همه استنتاج‌های با طول کمتر از $n$ $n$ برقرار است.

گر $C$ $cc"C"$ یک بنداشت باشد یا عضو $Γ$ $Γ$ باشد آنگاه $Γ ⊢ C$ $Γ⊢cc"C"$ .

اگر $C$ $cc"C"$ نتجه مستقیم یک یا دو فرمول قبلی توسط MP یا Gen باشد آنگاه، از آنجا که $C$ $cc"C"$ به $B$ $cc"B"$ بستگی ندارد، این فرمول‌های قبلی نیز وابستگی ندارند.

بنا بر فرض استقرا، این فرمول‌های قبلی تنها از $Γ$ $Γ$ قابل استنتاج هستند.

در نتیجه، $C$ $cc"C"$ هم چنین است.

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

فرض کنید، در برهانی که نشان دهنده استنتاج $Γ, B ⊢ C$ $Γ,cc"B"⊢cc"C"$ است، هیچ موردی از قاعده Gen (تعمیم) برای فرمولی که به $B$ $cc"B"$ بستگی دارد و در آن متغیر سوردارشده یک متغیر آزاد در $B$ $cc"B"$ است، کارزده نشده باشد. در این صورت داریم $Γ ⊢ B \Rightarrow C$ $Γ⊢cc"B"⇒cc"C"$ .

اثبات:

گیریم $D_{۱}, \dots, D_{n}$ $cc"D"_۱, …,cc"D"_n$ استنتاج $C$ $cc"C"$ از $Γ$ $Γ$ و $B$ $cc"B"$ باشد، که فرض قضیه را برمی‌آورد. (در این استنتاج $D_{n}$ $cc"D"_n$ همان $C$ $cc"C"$ است.)

می‌خواهیم با استقرا نشان دهیم که برای هر $i \leq n$ $i≤ n$ داریم $Γ ⊢ B \Rightarrow D_{i}$ $Γ⊢cc"B"⇒cc"D"_i$ .

اگر $D_{i}$ $cc"D"_i$ یک بنداشت یا متعلق به $Γ$ $Γ$ باشد، از آنجا که↝ $D_{i} \Rightarrow (B \Rightarrow D_{i})$ $cc"D"_i⇒(cc"B"⇒cc"D"_i)$ یک بنداشت است داریم↝ $Γ ⊢ B \Rightarrow D_{i}$ $Γ⊢cc"B"⇒cc"D"_i$ .

اگر $D_{i}$ $cc"D"_i$ همان $B$ $cc"B"$ باشد، پس $Γ ⊢ B \Rightarrow D_{i}$ $Γ⊢cc"B"⇒cc"D"_i$ ، زیرا، بنا به قضیه ۲.۱، $⊢ B \Rightarrow B$ $⊢cc"B"⇒cc"B"$ .

اگر $j$ $j$ و $k$ $k$ کوچکتر از $i$ $i$ وجود داشته باشد به قسمی که $D_{k}$ $cc"D"_k$ همان $D_{j} \Rightarrow D_{i}$ $cc"D"_j⇒cc"D"_i$ باشد، آنگاه، با فرض استقرا $Γ ⊢ B \Rightarrow D_{j}$ $Γ ⊢ cc"B" ⇒ cc"D"_j$ و $Γ ⊢ B \Rightarrow (D_{j} \Rightarrow D_{i})$ $Γ ⊢ cc"B" ⇒ (cc"D"_j ⇒ cc"D"_i )$ .

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

$⊢ (B \Rightarrow (D_{j} \Rightarrow D_{i})) \Rightarrow ((B \Rightarrow D_{j}) \Rightarrow (B \Rightarrow D_{i}))$ $⊢(cc"B"⇒(cc"D"_j⇒cc"D"_i))⇒((cc"B"⇒cc"D"_j)⇒(cc"B"⇒cc"D"_i))$ .

بنابراین، با دوبار کارزدن MP داریم $Γ ⊢ B \Rightarrow D_{i}$ $Γ⊢cc"B"⇒cc"D"_i$ .

سرانجام، فرض کنید $j$ $j$ کوچکتر از $i$ $i$ وجود دارد به قسمی که $D_{i}$ $cc"D"_i$ عبارت باشد از $(\forall x_{k}) D_{j}$ $(∀x_k)cc"D"_j$ .

در این صورت، بنا به فرض استقرا، یعنی $Γ ⊢ B \Rightarrow D_{j}$ $Γ⊢ cc"B"⇒cc"D"_j$ ، و فرض قضیه یا $D_{i}$ $cc"D"_i$ به $B$ $cc"B"$ بستگی ندارد یا $x_{k}$ $x_k$ یک متغیر آزاد $B$ $cc"B"$ نیست.

اگر $D_{j}$ $cc"D"_j$ به $B$ $cc"B"$ بستگی نداشته باشد، بنا به قضیه ۲.۴، $Γ ⊢ D_{j}$ $Γ⊢cc"D"_j$ و در نتیجه با کار زدن Gen داریم $Γ ⊢ (\forall x_{k}) D_{j}$ $Γ ⊢ (∀x_k)cc"D"_j$ . بنابراین، $Γ ⊢ D_{i}$ $Γ⊢cc"D"_i$ .

اکنون با بنداشت (A۱) داریم $⊢ D_{i} \Rightarrow (B \Rightarrow D_{i})$ $⊢cc"D"_i⇒(cc"B"⇒cc"D"_i)$ .

بنابراین بنا بر MP داریم $Γ ⊢ B \Rightarrow D_{i}$ $Γ⊢cc"B"⇒cc"D"_i$ .

از طرف دیگر، اگر $x_{k}$ $x_k$ یک متغیر آزاد $B$ $cc"B"$ نباشد، با توجه به بنداشت (A۵)،

$⊢ (\forall x_{k}) (B \Rightarrow D_{j}) \Rightarrow (B \Rightarrow (\forall x_{k}) D_{j})$ $⊢(∀x_k)(cc"B"⇒cc"D"_j)⇒(cc"B"⇒(∀x_k)cc"D"_j)$ .

از آنجا که $Γ ⊢ B \Rightarrow D_{j}$ $Γ⊢cc"B"⇒cc"D"_j$ ، از Gen داریم $Γ ⊢ (\forall x_{k}) (B \Rightarrow D_{j})$ $Γ⊢(∀x_k)(cc"B"⇒cc"D"_j)$ . و اکنون از MP داریم $Γ ⊢ B \Rightarrow (\forall x_{k}) D_{j}$ $Γ⊢cc"B"⇒(∀x_k)cc"D"_j$ . یعنی $Γ ⊢ B \Rightarrow D_{i}$ $Γ⊢cc"B"⇒cc"D"_i$ .

این استقرا را کامل می‌کند، و قضیه ما دقیقاً حالت خاص $i = n$ $i=n$ است.

فرض قضیه ۲.۵ تا اندازه‌ای دست و پا گیر است. نتایج ضعیف‌تر زیر اغلب مفیدتر هستند.

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

اگر در استنتاج $Γ, B ⊢ C$ $Γ,cc"B"⊢cc"C"$ از قاعده تعمیم با متغیرهای سوردارشده که در $B$ $cc"B"$ آزاد هستند استفاده نشده باشد آنگاه $Γ ⊢ B \Rightarrow C$ $Γ⊢cc"B"⇒cc"C"$ .

توجه: به عبارت دیگر، اگر بتوانیم برای $Γ, B ⊢ C$ $Γ,cc"B"⊢cc"C"$ بدون استفاده از قاعده تعمیم بر روی متغیرهای آزاد $B$ $cc"B"$ برهان بیاوریم، می‌توانیم برای $Γ ⊢ B \Rightarrow C$ $Γ⊢cc"B"⇒cc"C"$ نیز برهان بیاوریم.

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

اگر $B$ $cc"B"$ یک فرمول بسته باشد و داشته باشیم $Γ, B ⊢ C$ $Γ,cc"B"⊢cc"C"$ آنگاه خواهیم داشت $Γ ⊢ B \Rightarrow C$ $Γ⊢cc"B"⇒cc"C"$ .

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

در قضیه‌های ۲.۴ تا ۲.۷ نتیجه افزون زیر را می‌توان از اثبات‌ها بدست آورد.

اثبات جدید $Γ ⊢ B \Rightarrow C$ $Γ⊢cc"B"⇒cc"C"$ (که در قضیه ۲.۴، دیدیم، یعنی $Γ ⊢ C$ $Γ⊢cc"C"$ ) از قاعده Gen در فرمولی استفاده می‌کند که به برخی فرمول مانند $ε$ $ε$ در $Γ$ $Γ$ بستگی دارد. این در صورتی است که در اثبات اصلی $Γ ⊢ B \Rightarrow C$ $Γ⊢cc"B"⇒cc"C"$ قاعده Gen برای همان متغیر سوردار شده و بر روی فرمولی که به $ε$ $ε$ بستگی دارد کار زده شود.

(در اثبات قضیه ۲.۵، باید توجه داشت که $D_{j}$ $cc"D"_j$ به یک مقدمه $ε$ $ε$ از $Γ$ $Γ$ در اثبات اصلی بستگی دارد اگر و فقط اگر $B \Rightarrow D_{j}$ $cc"B"⇒cc"D"_j$ در اثبات جدید به $ε$ $ε$ وابسته باشد.)

این نتیجه‌گیری تکمیلی زمانی مفید خواهد بود که بخواهیم قضیه استنتاج را چندین بار پشت سر هم به یک استنتاج معین اعمال کنیم - برای مثال، برای به دست آوردن

$Γ ⊢ D \Rightarrow (B \Rightarrow C)$ $Γ ⊢ cc"D" ⇒ (cc"B" ⇒ cc"C")$

از

$Γ, D, B ⊢ C$ $Γ, cc"D", cc"B" ⊢ cc"C"$ .

که از این پس بخش جدایی ناپذیر بیان قضیه‌های ۲.۴ تا ۲.۷ در نظر گرفته خواهند شد.

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

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

فرض	$(\forall x_{۱}) (\forall x_{۲}) B$ $(∀x_۱)(∀x_۲)cc"B"$	۱.
(A۴)	$(\forall x_{۱}) (\forall x_{۲}) B \Rightarrow (\forall x_{۲}) B$ $(∀x_۱)(∀x_۲)cc"B"⇒(∀x_۲)cc"B"$	۲.
۱, ۲, MP	$(\forall x_{۲}) B$ $(∀x_۲)cc"B"$	۳.
(A۴)	$(\forall x_{۲}) B \Rightarrow B$ $(∀x_۲)cc"B"⇒cc"B"$	۴.
۳, ۴, MP	$B$ $cc"B"$	۵.
Gen	$(\forall x_{۱}) B$ $(∀x_۱)cc"B"$	۶.
Gen	$(\forall x_{۲}) (\forall x_{۱}) B$ $(∀x_۲)(∀x_۱)cc"B"$	۷.

بنابراین، از ۱ تا ۷ داریم:

$(\forall x_{۱}) (\forall x_{۲}) B ⊢ (\forall x_{۲}) (\forall x_{۱}) B$ $(∀x_۱)(∀x_۲)cc"B"⊢(∀x_۲)(∀x_۱)cc"B"$

و این در حالی است که در این استنتاج کاربردی از تعمیم وجود ندارد که در آن متغیر سوردار شده یک متغیر آزاد $(\forall x_{۱}) (\forall x_{۲}) B$ $(∀x_۱)(∀x_۲)cc"B"$ باشد. بنابراین، بنابر نتیجه ۲.۷ داریم:

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

قضیه‌های زیر را بدست آورید.

۲.۲۷:

a. $⊢ (\forall_{x}) (B \Rightarrow C) \Rightarrow ((\forall_{x}) B \Rightarrow (\forall_{x}) C$ $⊢(∀_x)(cc"B"⇒cc"C")⇒((∀_x)cc"B"⇒(∀_x)cc"C"$

حل:

فرض	$(\forall_{x}) (B \Rightarrow C)$ $(∀_x)(cc"B"⇒cc"C")$	۱.
فرض	$(\forall x) B$ $(∀x)cc"B"$	۲.
(A۴)	$(\forall_{x}) (B \Rightarrow C) \Rightarrow (B \Rightarrow C)$ $(∀_x)(cc"B"⇒cc"C")⇒(cc"B"⇒cc"C")$	۳.
۱, ۳, MP	$B \Rightarrow C$ $cc"B"⇒cc"C"$	۴.
(A۴)	$(\forall x) B \Rightarrow B$ $(∀x)cc"B"⇒cc"B"$	۵.
۲, ۵, MP	$B$ $cc"B"$	۶.
۴, ۶, MP	$(\forall x) C$ $(∀x)cc"C"$	۷.
۷, Gen	cc"C"	۸.
۱-۸	$(\forall x) (B \Rightarrow C), (\forall x) B ⊢ (\forall x) C$ $(∀x)(cc"B"⇒cc"C"),(∀x)cc"B"⊢(∀x)cc"C"$	۹.
۱-۲, ۲.۶	$(\forall x) (B \Rightarrow C) ⊢ (\forall x) B \Rightarrow (\forall x) C$ $(∀x)(cc"B"⇒cc"C")⊢(∀x)cc"B"⇒(∀x)cc"C"$	۱۰
۱, ۱۰, ۲.۶	$⊢ (\forall x) (B \Rightarrow C) \Rightarrow ((\forall x) B \Rightarrow (\forall x) C)$ $⊢(∀x)(cc"B"⇒cc"C")⇒((∀x)cc"B"⇒(∀x)cc"C")$	۱۱.

b. $⊢ (\forall x) (B \Rightarrow C) \Rightarrow ((\exists x) B \Rightarrow (\exists x) C$ $⊢ (∀x)(cc"B" ⇒ cc"C") ⇒ ((∃x)cc"B" ⇒ (∃x)cc"C"$

c. $⊢ (\forall x) (B \land C) \Leftrightarrow ((\forall x) B \land (\forall x)) C$ $⊢(∀x)(cc"B"∧cc"C")⇔((∀x)cc"B"∧(∀x))cc"C"$

d. $⊢ (\forall y_{1}) \dots (\forall y_{n}) B \Rightarrow B$ $⊢(∀y_1)…(∀y_n)cc"B"⇒cc"B"$

e. $\neg (\forall x) B \Rightarrow (\exists x) \neg B$ $¬(∀x)cc"B" ⇒ (∃x) ¬cc"B"$

۲.۲۸:

فرض کنید K یک تئوری مرتبه اول باشد و $K^{#}$ $K^#$ یک تئوری بنداشتی با بنداشت‌های زیر باشد:

a. $(\forall y_{1}) \dots (\forall y_{n}) B,$ $(∀y_1)…(∀y_n)cc"B",$

که در آن $B$ $cc"B"$ (هر) بنداشی از K است و $y_{۱}, \dots, y_{n} (n \geq ۰)$ $y_۱,…,y_n(n≥۰)$ (هر) متغیر هستند (برای $n = 0$ $n=0$ هیچ متغیر).

b. $(\forall y_{۱}) \dots (\forall y_{n}) (B \Rightarrow C) \Rightarrow$ $(∀y_۱)…(∀y_n)(cc"B"⇒cc"C")⇒$ $[(\forall y_{۱}) \dots (\forall y_{n}) B \Rightarrow$ $[(∀y_۱)…(∀y_n)cc"B"⇒$ $(\forall y_{۱}) \dots (\forall y_{n}) C]$ $(∀y_۱)…(∀y_n)cc"C"]$

که در آن $B$ $cc"B"$ و $C$ $cc"C"$ فرمول و $y_{۱} \dots, y_{n}$ $y_۱ …, y_n$ متغیر هستند.

علاوه بر این، تنها قاعده استنتاج $K^{#}$ $K^#$ قیاس استثنایی دارد.

نشان دهید که $K^{#}$ $K^#$ قضایای یکسان با K دارد. بنابراین، به قیمت اضافه کردن بنداشت‌های بیشتر، می‌توان از قاعده تعمیم صرف نظر کرد.

راهنمایی:

فرض کنید $⊢_{K} B$ $⊢_Kcc"B"$ . با استقرا روی تعداد گام‌های برهان $B$ $cc"B"$ در K نشان دهید که برای هر متغیرهای

$y_{۱}, \dots, y_{n} (n \geq ۰)$ $y_۱,…,y_n(n≥۰)$

داریم:

$⊢ K^{#} (\forall y_{۱}) ... (\forall y_{n}) B .$ $⊢K^#(∀y_۱)...(∀y_n)cc"B".$

۲.۲۹:

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

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

■ مقدمه

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

■ قضیه ۲.۱

■ قضیه ۲.۲

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

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

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

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

■ قضیه ۲.۴

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

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

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

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

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

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

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