نظریه اصل موضوعی منطق گزاره‌ای ۱

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

درآمد به منطق

معرفی نظریه اصل موضوعی و قضیه استنتاج

۱- سرآغاز

۱۱- برخی ویژگی‌های دستگاه 𝓛

۲- نظریه صوری

۱۲- یک کاربرد برای شمای بنداشتی A۱: α⇒(β⇒α)).

۳- معرفی زبان صوری 𝓛

۱۳- لم. ⊢𝓛 α ⇒ α

۴- فرمول در 𝓛

۱۴- β, ¬β ⊢ ς

۵- معرفی رابط‌های ∧، ∨ و ≡

۱۵- مثال: ¬β ⊢ β ⇒ ς

۶- اصول موضوعه در نظریه 𝓛

۱۶- قضیه استنتاج

۷- قاعده استنتاج در نظریه 𝓛

۱۷- دو نتیجه

۸- برهان در 𝓛

۱۸- میان قضیه‌ها

۹- قضیه در 𝓛

۱۹- تمرین *

۱۰- مثال قضیه

۲۰- کلاس خارج قسمت در 𝓛

■ سرآغاز

در دو یادداشت «مقدمات نظریه برهان» و «نظریه برهان / استنتاج طبیعی» به این نکته اشاره شد که رویکرد اصل موضوعی(↝) یکی از دو روش↝ اصلی برای گسترش نظریه برهان است. هدف ما در این قسمت و سه قسمت بعد گسترش نظریه برهان برای منطق گزاره‌ای به شیوه اصل موضوعی (Axiomatic method) است.

[** در این چهار قسمت دو واژه «اصل موضوع» و «بنداشت» هر دو معادل «آکسیوم (Axiom)» به کار گرفته شده است. **]

قسمت یکم (این قسمت) معرفی دستگاه اصل موضوعی 𝓛 (تئوری 𝓛) و روش کار با آن است. در قسمت دوم به اثبات استواری، تمامیت(↝↝) و سازگاری(↝↝) 𝓛 می‌پردازیم. در قسمت سوم استقلال اصول موضوعه را نشان داده، سپس به منطق‌های چند ارزشی نگاه خواهیم کرد. در قسمت چهارم به معرفی و مرور سایر دستگاه‌های بنداشتی گزاره‌ای می‌پردازیم.

منبع و مرجع اصلی ما در چهار قسمت «نظریه اصل موضوعی منطق گزاره‌ای» متن:

Mendelson, Elliott. Introduction to mathematical logic. 6th, ed, CRC Press, Taylor & Francis Group. 2015.

است.

■ نظریه صوری

یک نظریه صوری (Formal theory) عبارت است از:

۱. یک زبان صوری.

۲. مجموعه تصمیم پذیر از فرمول (wff) در زبان صوری نظریه که مجموعه اصول موضوعه (Axioms set) نامیده میشود. به هر عضو این مجموعه یک اصل موضوع (Axiom) نظریه گقته می‌شود.

۳. مجموعه‌ای متناهی از قواعد استنتاج.

تئوری 𝓛

تئوری 𝓛

■ معرفی زبان صوری 𝓛

آ- واژگان ابتدایی زبان صوری 𝓛 به قرار زیر است:

۱. حروف گزاره‌ای به قرار:

{p۱, p۲, p۳, . . .}.

۲. رابط‌های ابتدایی به قرار:

{¬, ⇒}.

[در زبان 𝓛، بجای "~" و "⊃" (نعل اسبی) که تاکنون به کار می‌بردیم به ترتیب از نمادهای ¬ و ⇒ استفاده می‌کنیم.]

۳. نمادهای ویژه به قرار {) ,(}.

■ فرمول در 𝓛

۱.۱- همه حروف گزاره‌ای فرمو‌های 𝓛 هستند.

۱.۲- اگر α و β ‌فرمول‌های 𝓛 باشند آنگاه:

(¬α)
و
(α ⇒ β)

نیز فرمول‌های 𝓛 هستند.

۱.۳- یک عبارت فرمول 𝓛 است اگر و تنها اگر بتوان نشان داد بر مبنای ۱.۱ و ۱.۲ به دست آمده است.

■ معرفی رابط‌های ∧، ∨ و ≡

همانطور که می‌توان دید، رابط‌های ∧، ∨ و ≡ در واژگان ابتدایی 𝓛 نیستند. این رابط‌ها را در 𝓛 به عنوان رابط‌های تعریفی مطابق زیر تعریف می‌کنیم:

(D۱) (α ∧ β) ≝ ¬(α ⇒ ¬β)

(D۲) (α ∨ β) ≝ (¬α ⇒ β)

(D۳) (α ≡ β) ≝ (α ⇒ β) ∧ (β ⇒ α)

☚:

هر آنچه در مورد فرمول در Pℓ در یادداشت «نگارش صورت و الگوریتم آن» گفته شد در مورد فرمول‌ در 𝓛 نیز برقرار است.

■ اصول موضوعه در نظریه 𝓛

اگر ،β ‌،α و ς فرمول‌های 𝓛 باشند آنگاه:

(A۱) α ⇒ (β ⇒ α)

(A۲) ((α ⇒ (β ⇒ ς)) ⇒ ((α ⇒ β) ⇒ (α ⇒ ς))

(A۳) (¬α ⇒ ¬β) ⇒ ((¬α ⇒ β) ⇒ α)

بن‌داشت‌های (اصول موضوعه / Axioms) نظریه 𝓛 هستند.

☚:

 β ‌،α و ς در بالا فرا-متغیر هستند و بنابراین A۲ ،A۱ و A۳ شماهای بنداشتی (Axioms schemas / طرحواره‌های اصل موضوعی) هستند. برای مثال، فرمول‌های زیر موردهای بنداشت A۱ هستند.

۱- α ⇒ (α ⇒ α)

۲- α ⇒ (¬α ⇒ α)

۳- ~β ⇒ ((α ⇒ β) ⇒ ~β )

■ قاعده استنتاج در نظریه 𝓛

تنها قاعده استنتاج در 𝓛 قیاس استثنایی (M.P) است:

از α و α ⇒ β داریم β.

■ برهان در 𝓛

یک برهان (↝ و ↝) در 𝓛 یک دنباله:

β۱, …, βk

از فرمول‌ها (wfs) است به قسمی که، برای هر i، βi یا یک اصل موضوع 𝓛 یا βi نتیجه مستقیم برخی از فرمول‌های قبلی در دنباله به موجب یکی از قواعد استنتاج است.

■ قضیه در 𝓛

یک قضیه (↝ و ↝ و ↝) در 𝓛 یک فرمول β در 𝓛 است به قسمی که β آخرین فرمول یک برهان در 𝓛 باشد. به چنین برهانی اثبات β در 𝓛 گفته می‌شود.

■ مثال قضیه:

نشان دهید:⊢𝓛 (α ⇒ β) ⇒ (α ⇒ α)⚪⚪
شمای A۱α ⇒ (β ⇒ α )۱.
شمای A۲((α ⇒ (β ⇒ α)) ⇒ ((α ⇒ β) ⇒ (α ⇒ α))۲.
۱، ۲، M.P(α ⇒ β) ⇒ (α ⇒ α)■۳.

بنابراین، (α ⇒ β) ⇒ (α ⇒ α) یک قضیه 𝓛 است.

☚: همان طور که در این مثال دیده می‌شود عناصر دنباله:

۳۲۱
(α⇒β) ⇒ (α⇒α). ((α⇒(β⇒α)) ⇒ ((α⇒β) ⇒ (α⇒α)), α ⇒ (β⇒α ),

فرمول‌ها (wfs) است به قسمی که، هر عنصر دنباله یک اصل موضوع 𝓛 یا نتیجه مستقیم برخی از فرمول‌های قبلی در دنباله به موجب یکی از قواعد استنتاج است.

■ برخی ویژگی‌های دستگاه 𝓛

ویژگی‌های زیر را می‌توان برای دستگاه 𝓛 برشمرد. اثبات آن‌ها به همان شیوه است در دستگاه NdPℓ آمده است.

• ۱. یکنوایی (Monotonicity)،

• ۲. استنتاج با مجموعه مقدمات نامتناهی،

• ۳. ترایایی استنتاج،

• ۴. استنتاج عضوی.

■ یک کاربرد برای شمای بنداشتی A۱: α⇒(β⇒α)).

گیریم δ یک شمای فرمول دلخواه در 𝓛 باشد. آنگاه

(Int): ⊢𝓛 δ ⇒ axiom

 که در آن axiom یکی از شماهای A۲ ،A۱ و A۳ است.

برهان:⊢𝓛 δ ⇒ axiom⚪⚪
مورد شمای A۱axiom  ⇒ (δ ⇒ axiom )۱.
۱،  axiom، M.Pδ ⇒ axiom ۲.

■ لم. ⊢𝓛 α ⇒ α

⊢𝓛 α ⇒ α.

• [۸.۱] برهان↝:

مورد A۲(α⇒((α⇒α)⇒α)) ⇒ ((α⇒(α⇒α)) ⇒ (α⇒α))

.۱

مورد A۱α⇒((α⇒α)⇒α)۲.
از ۱، ۲، M.Pα⇒((α⇒α)⇒α)۳.
مورد A۱((α⇒(α⇒α)) ⇒ (α⇒α))۴.
از ۱، ۲، M.Pα ⇒ α■۵.

[خواننده نباید از مرحله ظاهراً بی‌هدف در سطر ۱ برهان دلسرد شود. در بسیاری از برهان‌ها، ما در واقع با نتیجه مورد نظر (در اینجا β⇒β) شروع می‌کنیم، و سپس به دنبال بنداشت مناسبی خواهیم گشت که ممکن است توسط M.P به آن نتیجه منجر شود. آمیزه‌ای از نبوغ و آزمون منجر به یافتن مورد مناسبی از اصول موضوع (در اینجا A۲) خواهد شد.]

برای بقیه این قسمت، مگر خلاف آن گفته شود، از گذاشتن اندیس '𝓛' در ⊢ چشم پوشی می‌کنیم.

■ مثال (۱.۴۷.a/p.۳۰/ed.۶):

نشان دهید:⊢ (¬α ⇒ α) ⇒ α⚪⚪
مورد A۳(¬α ⇒ ¬α) ⇒ ((¬α ⇒ α) ⇒ α)۱.
از ۱، لم.۸.۱↝، M.P(¬α ⇒ α) ⇒ α■۲.

■ مثال (۱.۴۷.b/p.۳۰/ed.۶):

نشان دهید:α ⇒ β, β ⇒ ς ⊢ α ⇒ ς⚪⚪
مقدمهα ⇒ β۱.
مقدمهβ ⇒ ς۲.
بنداست A۲(α ⇒ (β⇒ς)) ⇒ ((α⇒β) ⇒ (α⇒ς))۳.
مورد A۱(β⇒ς) ⇒ (α ⇒ (β⇒ς))۴.
از ۲، ۴، M.Pα ⇒ (β⇒ς)۵.
از ۳، ۵، M.P(α⇒β) ⇒ (α⇒ς)۶.
از ۱، ۶، M.Pα ⇒ ς■۷.

■ تمرین (۱.۴۷.c/p.۳۰/ed.۶):

نشان دهید:α ⇒ (β⇒ς) ⊢ β ⇒ (α⇒ς)⚪

■  β, ¬β ⊢ ς

نشان دهید:

β, ¬β ⊢ ς.↝

برای اثبات ابتدا نشان می‌دهیم:

(E۱): ¬β ⊢ β ⇒ ς,

در این صورت، یعنی برقراری E۱ داریم:

مقدمه ¬β۱.
مقدمه β۲.
۱، E۱β ⇒ ς۳.
۲، ۳، M.Pς۴.

در مثال بعدی اثبات E۱ آمده است.■

■ مثال: ¬β ⊢ β ⇒ ς

نشان دهید:¬β ⊢ β ⇒ ς⚪⚪
مقدمه¬β ۱.
A۱(¬β⇒(¬ς⇒¬β))۲.
A1(¬α⇒(¬β⇒¬α)) ⇒ (β⇒(¬β⇒(¬ς⇒¬β)))۳.
۲، ۳، M.Pβ ⇒ (¬β⇒(¬ς⇒¬β))۴.
A1¬β ⇒ (β⇒¬β)۵.
۱، ۵، M.Pβ ⇒ ¬β۶.
A۲(β ⇒ (¬β⇒(¬ς⇒¬β))) ⇒ ((β⇒¬β)⇒(β⇒(¬ς⇒¬β)))۷.
۴، ۷، M.P(β⇒¬β) ⇒ (β⇒(¬ς⇒¬β))۸.
۶، ۸، M.Pβ⇒(¬ς⇒¬β)۹.
A۲(β ⇒ ((¬ς⇒¬β)⇒((¬ς⇒β)⇒ς))) ⇒ ((β⇒(¬ς⇒¬β))⇒(β⇒((¬ς⇒β)⇒ς)))۱۰.
A۳(¬ς ⇒ ¬β)⇒((¬ς ⇒ β) ⇒ ς)۱۱.
Int، ۱۱β⇒((¬ς⇒¬β)⇒((¬ς⇒β)⇒ς))۱۲.
۱۰، ۱۲، M.Pβ⇒(¬ς⇒¬β))⇒(β⇒((¬ς⇒β)⇒ς))۱۳.
۹، ۱۳، M.Pβ⇒((¬ς⇒β)⇒ς)۱۴.
A۲(β⇒((¬ς⇒β)⇒ς)) ⇒ ((β⇒(¬ς⇒β)⇒ς))⇒(β⇒ς))۱۵.
۱۴، ۱۵، M.Pβ⇒(¬ς⇒β)⇒ς))⇒(β ⇒ ς)۱۶.
۱۴، ۱۶، M.P β ⇒ ς■۱۷.

■ تمرین (۱.۴۷.d/p.۳۰/ed.۶):

نشان دهید:(¬α ⇒ ¬β) ⇒ (β ⇒ α)⚪

■ قضیه استنتاج↜

[۹.۱] فرض کنید Γ یک مجموعه فرمول و نیز β و ς فرمول باشند. در این صورت:

اگر:

Γ, β ⊢ ς,

آنگاه

Γ ⊢ β ⇒ ς.

به ویژه اگر β ⊢ ς آنگاه β⇒ς.

• اثبات (Herbrand, 1930)↧:

Herbrand, J. (1930) Recherches sur la théorie de la démonstration. Travaux de la Société des Sciences et des Lettres de Varsovie, III, 33, 33–160.

فرض کنید:

ς۱, . . ., ςn

که در آن ς = ςn است یک برهان↝ برای:

Γ U {β} ⊢ ς↝

باشد.

[به عبارت دیگر داریم:

Γ U {β} ⊢ ς⚪
 ς۱۱.
 

.
.
.

.
.
.

 ςkk.
 

.
.
.

.
.
.

 ςn = ς■n.

]

می‌خواهیم با استقرا روی اندیس j نشان دهیم برای ۱≤j≤n داریم:

(I۱):Γ ⊢ β ⇒ ςj.

در گام یکم: (I۱) را برای j=۱ ثابت می‌کنیم.

می‌گوییم ς۱ باید:

یا یک عضو Γ باشد↝،
یا یک شمای اصل موضوع باشد،
یا خود β باشد.

اگر ς۱ عضو Γ باشد از بنداشت A۱: ς۱⇒(β⇒ς۱) و M.P داریم:

Γ ⊢ β ⇒ ς۱.

اگر ς۱ یک بنداشت باشد باز هم از A۱ و M.P داریم:

Γ ⊢ β ⇒ ς۱.

اگر ς۱ خود β باشد آنگاه بنا بر لم ۸.۱ (⊢β⇒β) داریم:

Γ ⊢ β ⇒ ς۱.

در گام دوم: فرض می‌کنیم برای همه k‌های کوچکتر از عدد طبیعی j (یعنی k<j) داریم:

Γ ⊢ β ⇒ ςk.

اکنون می‌گوییم ςj (برای j>k) باید:

۱. یا یک عضو Γ باشد↝،
۲. یا یک شمای اصل موضوع باشد،
۳. یا خود β باشد،
۴. یا:

با کارزدن M.P از برخی ςℓ و ςm به دست آمده باشد، به قسمی که:

 ℓ < j, m < j,

و ςm به صورت ςℓ ⇒ ςj باشد.

در سه حالت اول به همان شیوه که برای j =۱ نشان داده شد می‌توان نوشت:

Γ ⊢ β ⇒ ςj.

برای حالت آخر بنا بر فرض استقرا داریم:

d۱: Γ ⊢ β ⇒ ςℓ,

d۲: Γ ⊢ β ⇒ (ςℓ ⇒ ςj) و

از d۲ و شمای بنداشت A۲، یعنی:

⊢ (β ⇒ (ςℓ ⇒ ςj)) ⇒ ((β ⇒ ςℓ) ⇒ (β ⇒ ςj))

و M.P می‌نویسیم:

d۳: ⊢ ((β ⇒ ςℓ) ⇒ (β ⇒ ςj)).

سرانجام از d۳، d۱ و M.P داریم:

Γ ⊢ β ⇒ ςj.

اکنون دیگر اثبات به روش استقرایی کامل شده است و برای j =n  اثبات قضیه استنتاج به پایان ‌می‌رسد.

☚: برهان آمده در اینجا (بالا) یک برهان سازنده (Constructive) است. به عبارت دیگر، این برهان ساختن استنتاج β⇒ς از Γ را از استنتاج داده‌شده ς از Γ و β میسر می‌سازد.

☚: در برهان آمده در اینجا (بالا)، از شمای اصل موضوع A3، یعنی:

(A۳) (¬α ⇒ ¬β) ⇒ ((¬α ⇒ β) ⇒ α)

استفاده نشده است.

■ دو نتیجه

[۱۰.۱].

a. β ⇒ ς, ς ⇒ δ ⊢ β ⇒ δ

b. β ⇒ (ς ⇒ δ), ς ⊢ β ⇒ δ

برهان برای a:β ⇒ ς, ς ⇒ δ ⊢ β ⇒ δ⚪⚪
فرضβ ⇒ ς۱.
فرضς ⇒ δ۲.
فرضβ۳.
۱، ۳، M.Pς۴.
۲، ۴، M.Pδ■۵.

بنابراین:

β ⇒ ς, ς ⇒ δ, β ⊢ δ.

از اینجا و بنا بر قضیه استنتاج داریم:

β ⇒ ς, ς ⇒ δ ⊢ β ⇒ δ■■

برهان برای b:β ⇒ (ς ⇒ δ), ς ⊢ β ⇒ δ⚪
فرضβ ⇒ (ς ⇒ δ)۱.
فرضς ۲.
فرضβ۳.
۱، ۳، M.P‌ς ⇒ δ۴.
۲، ۴، M.Pδ۵.
A۱δ ⇒ (β ⇒ δ)۶.
۵، ۶، M.Pβ ⇒ δ■۷.

بنابراین:

β ⇒ (ς ⇒ δ), ς, β ⊢ δ

از اینجا و بنا بر قضیه استنتاج داریم:

β ⇒ ς, ς ⇒ δ ⊢ β ⇒ δ■■

■ میان قضیه‌ها

[۱۱.۱] نشان دهید:¬¬β ⇒ β⚪⚪ a
A۳(¬β ⇒ ¬¬β) ⇒ ((¬β ⇒ ¬β) ⇒ β۱.
لم ۸.۱(¬β ⇒ ¬β)۲.
۱، ۲، .b.۱۰.۱(¬β ⇒ ¬¬β) ⇒ β۳.
A1¬¬β ⇒ (¬β ⇒ ¬¬β)۴.
۴، ۳، .a.۱۰.۱¬¬β ⇒ β■۵.

نشان دهید:¬¬β ⇒ β⚪⚪ b
A۳(¬¬¬β ⇒ ¬β) ⇒ ((¬¬¬β ⇒ β) ⇒ ¬¬β)۱.
a.۱۱.۱¬¬¬β ⇒ ¬β۲.
۱، ۲، .M.P(¬¬¬β ⇒ β) ⇒ ¬¬β۳.
A1β ⇒ (¬¬¬β ⇒ β)۴.
۴، ۳، .a.۱۰.۱β ⇒ ¬¬β■۵.

☚: مثال سرریز را ببینید.⊢ ¬β ⇒ (β ⇒ ς)⚪⚪ c
فرض¬β۱.
فرضβ۲.
A1β ⇒ (¬ς ⇒ β)۳.
A1¬β ⇒ (¬ς ⇒ ¬β)۴.
۲، ۳، M.P¬ς ⇒ β ۵.
۱، ۴، M.P¬ς ⇒ ¬β۶.
A۳(¬ς ⇒ ¬β) ⇒ ((¬ς ⇒ β) ⇒ ς)۷.
۶، ۷، M.P(¬ς ⇒ β) ⇒ ς ۸.
۵، ۶، M.Pς۹.
۱ - ۹¬β, β ⊢ ς ۱۰.
۱۰، قضیه استنتاج¬β ⊢ β ⇒ ς۱۱.
۱۱، قضیه استنتاج⊢ ¬β ⇒ (β ⇒ ς)■۱۲.

 ⊢ (¬ς ⇒ ¬β) ⇒ (β ⇒ ς)⚪⚪ d
فرض¬ς ⇒ ¬β۱.
A۳(¬ς ⇒ ¬β) ⇒ ((¬ς ⇒ β) ⇒ ς)۲.
A1β ⇒ (¬ς ⇒ β)۳.
۱، ۲، M.P(¬ς ⇒ β) ⇒ ς۴.
۴، ۳، .a.۱۰.۱β ⇒ ς۵.
۱ - ۵¬ς ⇒ ¬β ⊢ β ⇒ ς۶.
۶، قضیه استنتاج⊢ (¬ς ⇒ ¬β) ⇒ (β ⇒ ς)■۷.

(β ⇒ ς) ⇒ (¬ς ⇒ ¬β)⚪⚪ e
فرضβ ⇒ ς۱.
a.۱۱.۱¬¬β ⇒ β۲.
۲، ۱، a.۱۰.۱¬¬β ⇒ ς۳.
b.۱۱.۱ς ⇒ ¬¬ς۴.
۴، ۳، a.۱۰.۱¬¬β ⇒ ¬¬ς۵.
d.۱۱.۱(¬¬β ⇒ ¬¬ς) ⇒ (¬ς ⇒ ¬β)۶.
۵، ۶، M.P¬ς ⇒ ¬β۷.
۱ - ۷⇒ ς ⊢ ¬ς ⇒ ¬β۸.
۸، قضیه استنتاج⊢ (β ⇒ ς) ⇒ (¬ς ⇒ ¬β)■۹.

f⊢ β ⇒ (¬ς ⇒ ¬(β ⇒ ς)). 

آشکارا از M.P داریم:

β, β ⇒ ς ⊢ ς.

بنابراین، با دو بار کار زدن قضیه استنتاج خواهیم داشت:

⊢β ⇒ ((β ⇒ ς) ⇒ ς)).

بنابر e.۱۱.۱ می‌نویسیم:

((β ⇒ ς) ⇒ ς) ⇒ (¬ς ⇒ ¬(β ⇒ ς)).

اکنون بنا بر a.۱۱.۱ داریم:

⊢β ⇒ (¬ς ⇒ ¬(β ⇒ ς))■

 (β ⇒ ς) ⇒ ((¬β ⇒ ς) ⇒ ς)⚪⚪ g
فرضβ ⇒ ς۱.
فرض¬β ⇒ ς۲.
e.۱۱.۱(β ⇒ ς) ⇒ (¬ς ⇒ ¬β)۳.
۱، ۳، M.P¬β ⇒ ¬ς۴.
e.۱۱.۱(¬β ⇒ ς) ⇒ (¬ς ⇒ ¬¬β)۵.
۲، ۵، M.P¬ς ⇒ ¬¬β۶.
A۳(¬ς ⇒ ¬¬β) ⇒ ((¬ς ⇒ ¬β) ⇒ ς)۷.
۶، ۷، M.P(¬ς ⇒ ¬β) ⇒ ς۸.
۴، ۸، M.Pς۹.
۱ - ۹β ⇒ ς, ¬β ⇒ ς ⊢ ς۱۰.
۱۰، قضیه استنتاجβ ⇒ ς ⊢ (¬β ⇒ ς) ⇒ ς۱۱.
۱۱، قضیه استنتاج⊢(β ⇒ ς) ⇒ ((¬β ⇒ ς) ⇒ ς)■۱۲.

■ تمرین (۴۸.۱)

نشان دهید فرمول‌های زیر قضیه‌های 𝓛 هستند.

 β ⇒ (β ∨ ς)⚪⚪ a
b.۱۱.۱β ⇒ ¬¬β۱.
c.۱۱.۱¬¬β ⇒ (¬β ⇒ ς )۲.
۱، ۲، a.۱۰.۱⇒ (¬β ⇒ ς )۳.
۳، ت.∨⇒ (β ∨ ς )■۴.

 β ⇒ (ς ∨ β)⚪ b

 ς ∨ β ⇒ β ∨ ς⚪⚪ c
فرض¬ς ⇒ β۱.
e.۱۱.۱(¬ς ⇒ β) ⇒ (¬β ⇒ ¬¬ς )۲.
۱، ۲، M.P¬β ⇒ ¬¬ς ۳.
a.۱۱.۱¬¬ς ⇒ ς۴.
۳، ۴، a.۱۰.۱¬β ⇒ ς ۵.
۱ - ۵¬ς ⇒ β ⊢ ¬β ⇒ ς۶.
۶، قضیه استنتاج⊢ (¬ς ⇒ β) ⇒ (¬β ⇒ ς )۷.
۷، ت.∨⊢ (ς ∨ β) ⇒ (β ∨ ς )۸.

d. β ∧ ς ⇒ β,

e.  β ∧ ς ⇒ ς,

f.  (β ⇒ δ) ⇒ ((ς ⇒ δ) ⇒ (β ∨ ς ⇒ δ)),

g. ((β ⇒ ς) ⇒ β) ⇒ β,

h. β ⇒ (ς ⇒ (β ∧ ς)).

■ تمرین *

[۴۹.۱] یک برهان کامل (بدون کار زدن قضیه استنتاج) برای c.۱۱.۱ بیاورید.

[☚: همان روندی که در اثبات قضیه استنتاج به کار برده شد را به کار بزنید. مثال سرریز  راببینید.]

■ کلاس خارج قسمت↝ در 𝓛

گیریم ℛ یک رابطه باشد، به قسمی که برای رابطه ℛ داشته باشیم: βℛς اگر و تنها اگر β≡ς قضیه تئوری 𝓛 باشد. (به عبارت دیگر، داشته باشیم: ⊢β ≡ ς.)

اکنون با توجه قضیه‌هایی که تا کنون ثابت شده است و مورد‌های تمرین ۱.۴۸ و تعریف ≡↝ می‌توان نشان داد ℛ یک رابطه هم‌ارزی است. یعنی داریم:

• βℛβ؛ [⊢ β ≡ β]

• اگر βℛς آنگاه ςℛβ؛ [اگر ⊢β ≡ ς آنگاه ⊢ς ≡ β]

• اگر βℛς و ςℛδ آنگاه βℛδ. [اگر ⊢β ≡ ς و ⊢ς ≡ δ آنگاه ⊢β ≡ ς]

بنابراین، [P] (یعنی، کلاس‌هم‌ارزی به نمایندگی P) شامل همه Q هایی است که P ≡ Q یک قضیه در 𝓛 است (یعنی، P و Q به گونه هم‌ارز اثبات شدنی هستند). به عبارت دیگر، برای یک تئوری صوری T کلاس خارج قسمت تئوری↝ با رابطه ℛ (آنگونه که تعریف شد) وجود دارد.

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

■ ■ ■ ■ ■

◄ توجه: