توجه:

صورت، معنی و فرامنطق؛ دستگاه استنتاج طبیعی  آخرین ویرایش: ۱۳۹۵/۰۷/۰۱ 

 (ج). بنای دستگاه/صوری استنتاج

 مقدمه:

در قسمت قبل در مثال‌های ۱، ۲ و ۳ به ترتیب نشان دادیم:

مثال ۱(pq) (~q~p) یک استنتاج معتبر سمانتیکی است.

مثال ۲p(qr), p(qr) (pq)r یک استنتاج سمانتیکی نامعتبر است.

مثال ۲- ((p•q)r)) ((pr)(qr))   یک استنتاج سمانتیکی معتبر است.

 

آن‌طور که دیدیم، روند اثبات در مثال‌های بالا بدین قرار بود که، نشان دهیم هر تعبیر که برای مقدمات مدل است برای نتیجه نیز مدل است و برای خلاف آن بدین قرار که، نشان دهیم دست‌کم یک تعبیر وجود دارد که برای مقدمات مدل است ولی برای نتیجه مدل نیست (مثال ۲). ازاین‌جهت، این‌گونه روند گسترش به نظریه مبتنی بر مدل [نیز معناشناختی مبتنی بر مدل] موسوم است که در آن واژه بنیاد بر تعبیر (مدل) است.

در این قسمت بر آنیم تا برای مثال (~q~p) را از (pq)  نه در یک روند تعبیری که  در روندی نحوی / لفظی دست آوری نماییم (اشتقاق نحوی). این روند به نظریه برهان [ برهان شناسینظریه مبتنی بر برهان / معناشناسی مبتنی بر نظریه برهان ]  موسوم است. 

درواقع این روند بر این فرض‌بنیادی استوار است که مفهوم اصلی، ازاین‌جهت که چه معنایی به  عبارت‌های زبان در اینجا  LC نظیر شود، همانا به‌جای روند تعبیر، برهان خواهد بود.  به‌عبارت‌دیگر در این روند برهان صوری اعتبار بجای تعبیر خواهد نشست. بنابراین، در این قسمت آنچه از تعبیر، به شمول مقدار معنایی، مدل و جدول ارزش گفته موقتی به کنار نهاده و آنچه داریم زبان صوری و فرمول است و بس.

آن جه خواهد آمد هم‌اکنون در فصل ده کتاب، قسمت ۷، دستگاه استنتاجی، بر پایه زبان نمادین LC به‌تفصیل گسترانده شده. در ادامه، آنچه گسترانده شده را موجز و  کمی متفاوت مرور می‌کنیم. این دستگاه، که به شمول مفاهیمی چون قواعد استنتاج، برهان صوری، افزونگی و کارآمدی است، را زین‌پس دستگاه CND [برای:Copi's Natural Deduction] خواهیم نامید. 

برای یادآوری، در جدول ۱ در زیر نه قاعده استنتاج  آمده است.  

فرض کنید:  f مجموعه فرمول‌های LC باشد. یک قاعده استنتاج نحوی [یا فقط قاعده استنتاج] در یک دستگاه نحوی، یک رابطه به صراحت  تعریف‌شده بین فرمول‌ها(یعنی، f) و مجموعه‌های فرمول(یعنی، مجموعه توانی f) است، به قسمی که، بتوان تصمیم گرفت آیا هر فرمول در این رابطه با هر مجموعه فرمول دلخواه(یعنی، هر عضو دلخواه مجموعه توانی f) است یا نه؟ بنابراین هر قاعده استنتاج یک رابطه تصمیم پذیر است.

۹ قاعده استنتاج نحوی 
~β, α β
————————  
     
۲. α , α β
———————  
     β
۱.
(αβ ) , ~α
—————————       
       β
۴. (α β), (β γ)
———————————       
     α γ
۳.
   α β
————————       
α (α β)
۶. (α β)•(γ λ), (αγ )
————————————————      
            βλ
۵.
  α ,  β
—————————       
  α • β
۸.  α β
—————     
   α
۷.
       α
—————      
αβ
۹.
جدول ۱.    ۹ قاعده استنتاج نحوی

  گرهارد گنتزن - Gerhard Gentzen

زندگی‌نامه

بر آن بودم تا فرمالیسمی بنا کنم هر چه بیشتر نزدیک به استدلال، آن‌گونه که هست. این بود که حساب استنتاج طبیعی به وجود آمد.  __گرهارد گنتزن Gerhard Gentzen, "Investigations into Logical Deduction", American Philosophical Quarterly, Vol. 1, No. 4 (Oct., 1964), pp. 288-306

 

Gerhard Gentzen

گرهارد گنتزن(Gerhard Gentzen - ۱۹۴۵ - ۱۹۰۹)  ریاضیدان و منطقی آلمانی در  برگن (شهری واقع در جزیره روگن آلمان) پا به دنیا گشود. پدر وی که یک حقوق‌دان بود در جنگ جهانی اول کشته شد. وی در ۱۹۲۸م تحصیلات متوسطه را به پایان برد و از همان موقع توان استثنایی وی در ریاضیات آشکار گردید. تحصیل ریاضیات را از سال ۱۹۲۸م به ترتیب در دانشگاه‌های گریفزوالد(Greifswald)،  گوتینگن، برلین و مونیخ ادامه داد. سرانجام در  ۱۹۳۳م از دانشگاه گوتینگن دکتری خود را دریافت کرد. پس از مدتی استراحت برای بازیابی سلامت به‌عنوان دستیار هیلبرت در دانشگاه کوتینگتن به کار ادامه داد. گنتزن به‌ویژه همکار اصلی هیلبرت در برنامه اصل موضوعی کردن ریاضیات بود. ازجمله کارهای وی معرفی دستگاه‌های استنتاج طبیعی/Natural deduction systems و دستگاه حساب  دنبالک‌ها /Sequent calculus systems است.

گرهارد گنتزن(Gerhard Gentzen - ۱۹۴۵ - ۱۹۰۹

گنتزن در زمان جنگ دوم به‌عنوان مدرس در مؤسسه ریاضی دانشگاه آلمانی پراگ در چک مشغول کار شد و در روزهای پایانی جنگ در اعتراض مردم پراگ به اشغال، همراه با سایر اعضای آلمانی دانشگاه دستگیر و ۴ روز بعد از دستگیری و آمدن روس‌ها به آنان تحویل شد. وی که سابقه حمایت از نازی‌ها را داشت تحت شرایط بدی در بازداشت روس‌ها باقی ماند و سه ماه بعد به علت سوءتغذیه درگذشت. ___برگرفته از:

http://www-history.mcs.st-andrews.ac.uk/Biographies/Gentzen.html

دو مقاله از گنتزن: پژوهش‌های استنتاج منطقی I؛   پژوهش‌های استنتاج منطقی II.

 

 

  مرور جند تعریف:

(ج).۱. استنتاج: 

Turnstile

 گیریم S={α۱, α۲, . . ., αn} یک مجموعه فرمول‌ باشد. گوییم فرمول β در دستگاه CND از S  دست آمدنی [همچنین:  β نتیجه استنتاجی S، یا  β نتیجه برهانی S، یا  β نتیجه نحوی S] است و نوشته:

(آ'):     S CNDβ

اگر و فقط اگر دنباله متناهی فرمول‌های:

(ب'):       <β۱β۲,  . . .,  βm>

وجود دارد، به قسمی که؛

 ۱- هر عضو این دنباله متعلق به S یا در رابطه با یکی از  قواعد استنتاج و زیرمجموعه‌ای از عناصر قبلی‌ دنباله باشد؛
و بعلاوه
۲-  βm همان βباشد.

می‌توان در S β به‌جای S اعضای آن را فهرست کرد و نوشت:

 α۱, α۲, . . ., αn CNDβ 

به (آ') در بالا یک استنتاج معتبر نحوی [یا فقط استنتاج] و به دنباله  β۱, β۲, . . .,βmیک برهان در دستگاه CND گفته می‌شود. بعلاوه به مجموعه S مقدمان استنتاج می‌گویند.

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

وقتی نام دستگاه استنتاجی موردبحث از زمینه معلوم است (آ') را به‌صورت زیر می‌نویسند:

S β

 گرچه نماد '⊢' یک نماد فرازبانی (موسوم به Turnstile/گردان در) است ولی S β طبق تعریف برابر با دنباله (ب') آن‌گونه که گفته شد است.

مراد از  S, α β  استنتاج  S{α}β  است.

 

(ج).۲  خاصیت این‌همانی αα. یک استنتاج معتبر نحوی است.

اثبات:
در دنباله تک عنصری<α۱=α>  آخرین عنصر، یعنی α، یک مقدمه αα است. بنابراین طبق تعریف،  دنباله <α> یک برهان  αα است. این خاصیت که نتیجه مستقیم تعریف برهان در دستگاه CND  است را خاصیت این‌همانی می‌نامیم.

(ج).۳  هم‌ارزی نحوی:

صورت‌های گزاره‌ای αو β را هم‌ارزی نحوی  گوییم اگر و فقط اگر  αβ و  βα. در این صورت می‌نویسیم  α⊢⊣β.

 به‌آسانی می‌توان نشان داد هم‌ارزی نحوی یک رابطه هم‌ارزی در مجموعه فرمول‌ها است.

 

 

(ج).۴  قاعده جایگزینی نحوی:

اکنون قاعده جایگزینی نحوی را معرفی می‌کنیم؛ قاعده‌ای که طبق آن مجازیم از هر فرمول، فرمول حاصل از جایگزینی هر مؤلفه دلخواه آن را با هر عبارت به گونه نحوی هم‌ارز با آن مؤلفه، دست آوریم. [با  قاعده جایگزینی در کتاب مقایسه نمایید.] برای قاعده جایگزینی نحوی ۱۰ مورد کاربرد به‌عنوان هم‌ارزی‌های مقدماتی نحوی به شرح جدول زیر معرفی می‌کنیم.

هم‌ارزی‌های نحوی مقدماتی — کاربرد قاعده جایگزینی نحوی 
(αβ) ⊢⊣(βα)   
(α β) ⊢⊣ (β α)
۱۱. ~(α β) ⊢⊣(~α~β)
~(αβ)⊢⊣ (~α ~β)
۱۰.
[α (β γ)] ⊢⊣ [(α β)(α γ)]
[α (β γ)] ⊢⊣ [(α β)(α γ)]
۱۳. [(α β) γ] ⊢⊣ [α (β γ)]
[(αβ)∨γ] ⊢⊣ [α(βγ)]
۱۲.
α β⊢⊣ ~β ~α ۱۵. α ⊢⊣~~α ۱۴.
(α β ) ⊢⊣[(α β)(~α ~β)]
(α β ) ⊢⊣[(α β)(α β)]
۱۷. (α β) ⊢⊣(~β α) ۱۶.
α ⊢⊣(αα )
α ⊢⊣ (α α)
۱۹. [(α β) γ] ⊢⊣ [α (β γ)] ۱۸.
جدول ۲. ۱۰ مورد کاربرد قاعده جایگزینی

 

 

(ج).۵.  اثبات اعتبار یک استنتاج نحوی، به‌وسیله برهان است.

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

 ((p•q)r)) CND ((pr)(qr))

یک استنتاج معتبر نحوی است.

 

مقدمه (p•q)r ۱.
۱ و هم‌ارزی ۱۶ ~(p•q)r ۲.
۲ و هم‌ارزی ۱۰ (~p~q)r ۳.
۳ و هم‌ارزی ۱۳ (~pr)(~qr) ۴.
۴ و هم‌ارزی ۱۶ (pr)(qr) ۵.

 

 

(ج).۶  ناسازگاری نحوی:

گوییم  دستگاه CND یک دستگاه صوری ناسازگار است اگر و فقط اگر در آن فرمول β وجود داشته باشد، به قسمی که β از {~β} دست آمدنی است، یعنی داشته‌ باشیم: {~β} β. در غیر این صورت CND را دستگاه صوری سازگار گوییم.  گیریم دستگاه CND ناسازگار؛ در این صورت فرمول  β هست که از ~β دست آمدنی است. اما بنا بر و  فرمول βx که در آن x فرمول دلخواه است نیز از دست آمدنی است. اما ازβx  و~β و قاعده  می‌توان x را به دست آورد. بنابراین اگر دستگاه CND ناسازگار باشد آنگاه هر فرمولی دست آمدنی است. آشکار است که چنین دستگاه استنتاجی دارای هیچ دیدگاه وجودی نیست و خانه از پای‌بست ویران است. نشان دادن سازگاری دستگاه CND را در بند (د.) خواهیم دید.

 

(ج).۷  قضیه در دستگاه استنتاجی:

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

 

(ج).۷.۱   تعریف قضیه در دستگاه استنتاجی: 

فرمول α را یک قضیه در یک دستگاه استنتاجی گوییم(همچنین α را در  این دستگاه اثبات شدنی گوییم)، اگر  α بدون هیچ مقدمه یا فرض در این دستگاه دست آمدنی باشد. به‌عبارت‌دیگر، α نتیجه نحوی یک استنتاج با مجموعه مقدمات  تهی باشد. قضیه بودن α را دستگاه‌های استنتاجی به‌صورت  {}α نشان می‌دهند. همان‌طور که مشاهده می‌شود مقدمات این استنتاج یک مجموعه تهی است. ازآنجاکه یک و فقط یک مجموعه تهی وجود دارد، برای قضیه بودن فرمول  α به نوشتن α بسنده می‌گردد.

ازآنجاکه در دستگاه CND هر قاعده استنتاج دارای مجموعه مقدمات ناتهی با شماهای(صورت نوعی) مشخص است، مفهوم قضیه در دستگاه CND دارای مصداق نیست. اگر یک قاعده استنتاج موسوم به‌قاعده برهان شرطی به دستگاه CND بیفزاییم و حاصل را دستگاه CND+Cp بنامیم، آنگاه مفهوم قضیه در این دستگاه دارای مجموعه مصداق ناتهی خواهد بود.

 

(ج).۸   قاعده برهان شرطی در CND+Cp:

 

 

 

 

© 1987 - 2017 KHcc Sc.