د ثبوت نظريه

د ثبوت نظريه، د رياضيکي منطق يوه پراخه څانګه ده، چې د رسمي رياضيکي شيانو په توګه ثبوتونه وړاندې کوي او د رياضيکي تخنيکونو په واسطه د دوی تحليل ته زمينه برابروي. ثبوتونه په نمونه يي ډول (په قياسي ډول د تعریف شوو معلوماتو ساختمانونو) لکه: پراخو لېستونو او جعبه شوو لېستونو يا شجرې په توګه وړاندې کېږي، چې د کُلي قاعدو او د منطقي سيستم د ترجېح اصلولو له مخې جوړ شوي دي. بالاخره د ثبوت نظريه، په طبيعت کې ترکيبي ده او برعکس د نمونې نظريه په طبيعت کې semantic ده. ^[۱]

د ثبوت نظريې ځينې پراخې برخې، د ساختماني ثبوت نظريه، ترتيبي تحليل، د ثابتولو وړ منطق، برعکس يا چپه رياضيات (reverse mathematics)، د ثبوت رااېستنه، په خودکار ډول يو ځای شوې قضيې ثابتوونې (automated theorem proving) او د ثبوت پېچلتيا شاملوي. زياتې څېړنې د کمپيوټر په علم کې په کاريالونو، ادبياتو او فلسفه باندې تمرکز کوي.

تاريخچه

که څه هم د منطق رسمي کوونه، له (Gottlob Frege)، (Giuseppe Peano)، (Bertrand Russell) او (Richard Dedekind) کارونو نه ډېره مخکې وه، د ثبوت د معاصرې نظريې د کيسې په اړه فکر کېږي چې د ډيويد هلبرټ (David Hilbert) په واسطه خپره شوې ده. نوموړي د رياضياتو په بنسټونو کې د هيلبرټ د پروګرام په نوم اختراع کړه. د دې پروګرام مرکزي نظريه دا وه، چې که چېرې موږ د ټولو هغو په لوړه سطحه يا مصنوعي رسمي نظرياتو لپاره، چې رياضي پوهان ورته اړتيا لري؛ د ثبات لايتناهي ثبوتونه ورکولی شوی، نو موږ د يوه رياضيکي بحث په توګه دا نظريې رانغاړلی شوې، چې ښيي چې خپل سوچه يا خالص طبيعي اثباتونه (تاييدونه) يې (په یو څه زيات تخنيکي ډول د دوی د ثبوت وړ $\Pi _{1}^{0}$ جملې) په لايتناهي ډول سم دي، يو ځل مو چې په دې ډول سره راونغاړل، بيا د دوی د شتون قاعدو لايتناهي معنا ته پام نه کوو او د دوی خيالي شتون د کاذبو معنا لرونکي مقرراتو په توګه په پام کې نيسو.

د پروګرام ناکامي، د کورټ ګوډيل (Kurt Gödel) د نابشپړتيا قاعدو په واسطه وهڅول شوه، چې ويې ښودل چې د (ω) هره ثابته نظريه (ω-consistent theory) چې د ساده حسابي حقيقتونو د څرګندولو لپاره کافي پياوړتيا لري، خپل ثبات نه شي ثابتولی، چې همدا د ګوډيل په ترکيب کې يوه $\Pi _{1}^{0}$ جمله ده. که څه هم د هيلبرټ د پروګرام مشخص شوې نسخې راښکاره شوې او په اړوندو موضوعاتو څېړنه تر سره شوه. دې پایلو، په ځانګړي ډول لاندې برخې رهبري کړې دي:

د ګوډيل د پايلې پاکوالی يا سوچه توب، په ځانګړي ډول د (J. Barkley Rosser) سوچه توب ساده متناقضوالي ته د (ω) ثبات پورتنۍ غوښتنه کمزورې کوي.
د ګوډيل د پایلو د مغز کُلي قاعده کي د يوې کيفيتي ژبې په اصطلاحاتو کې، د اثبات وړ منطق.
د الان تيورينګ (Alan Turing) او سولومون فيفرمېن (Solomon Feferman) له امله د نظرياتو Transfinite تکرار.
د ځاني تاييد نظرياتو کشف، سيستمونه د خپل ځان په اړه د ويلو پوره ځواک لري، مګر دومره کمزورې دي چې د قطر (د څلور ضلعې قطر) بحث نه شي تر سره کولی. ذکر شوی بحث، د ګډيل د اثبات نه وړتيا د بحث کیلې ده.

د هيلبرټ د پروګرام له ښکته او پورته سره په موازي ډول، د ساختماني ثبوت نظريې بنسټونه رامنځته شول. (Jan Łukasiewicz) په ۱۹۲۶ز کې وړانديز وکړچې، يو څوک د هېلبرټ په سيستمونو باندې د منطق د قاعدوي ارئيې لپاره د بنسټ په توګه وده کولی شي، که چېرې يو چا ته د منطق په استنتاجي قوانينو کې له مفروضاتو نه د پايلو تر لاسه کولو اجازه ورکړل شي. دې ته په ځواب کې ( ۱۹۲۹ Stanisław Jaśkowski (او (Gerhard Gentzen ( (۱۹۳۴) په خپلواک ډول داسې سيستمونه برابر کړل، چې د طبيعت د تفريق (بېلوالي) calculi يې بولي. ګينټزين د پاېلې په توګه د پېژندنې په اصولو کې د بيان شوو ټينګار کوونکو شباهتونو لپاره د زمينو او د له منځه وړنې په اصولو کې د شباهتونو د منلو د پايلو تر منځ د تناسب نظريه وړاندې کړه. دا هغه نظريه ده چې د ثبوت په نظريه کې تاييد شوې ده. (Gentzen ( (۱۹۳۴) له دې ورهاخوا د پرله پسې يا لړيزې احصايې نظريه وړاندې کړه، چې دا په يو ورته ارواح کې د احصايې پرمختيا چې د منطقي نښلوونکو همزادي يې په غوره ډول بيان کړه او د ادارکي منطق په تشکيل کې یې د بنسټيزو پرمختګونو لامل شوه او د (Peano arithmetic) د ثبات لومړنی ترکيبي ثبوت برابر کړ. د طبيعي بېلوالي او لړيز (پرله پسې) calculus په ګډه، د ثبوت نظريې په اړه د تحليلي ثبوت بنسټيزه نظريه معرفي کړه. ^[۲]^[۳]

د ساختماني ثبوت نظريه

د ساختماني ثبوت نظريه، د ثبوت نظريې يوفرعي څېړندود دی، چې د (proof calculi) [ثبوت احصايې] ځانګړتياوې څېړي. د ثبوت calculi تر ټولو زيات پېژندل شوي درې ډولونه په دې ډول دي:

د هيلبرټ Calculi
د طبيعي بېلوالي Calculi
لړيز يا (پرله پسې)calculi

له دوی نه هر يو يې د شباهتي يا مسند منطق د لرغوني يا ادراکي خاصيت، نږدې هر کيفيتي منطق او زياتو فرعي ساختماني منطقونو، لکه: د مناسبتوب منطق يا خطي منطق، کولی شي يو بشپړ او قاعدوي اعتبار ورکړي. په حقيقت کې د دې منطق پيداکول، غير عادي دي، چې د دې caculi له ډلې په يوه کې د وړاندي شوې په توګه ټينګار کوي.

د ثبوت نظريې پيروان، په نمونه يې ډول د ثبوت په calculi کې لېوال دي، چې د تحليلي ثبوت د يوې نظريې ملاتړ کوي. د تحليلي ثبوت نظريه، د ګېنټزين (Gentzen) له خوا د لړيز يا پرله پسې احصايې لپاره معرفي شوه. په دې ځاې کې تحليلي ثبوتونه هغه دي، چې (cut-free) دي. په cut-free ثبوتونو کې زياته لېوالتيا له فرعي ساختمان ځانګړتيا نه په لاس راځي: د يو cut-free ثبوت، په پای لړۍ کې هره فرموله د ثابتو قضيو يوه فرعي فرموله ده. دا يوه شخص ته د دې اجازه ورکوي، چې په اسانۍ سره د پرله پسې احصايې ثبات وښيي، که چېرې تشه لړۍ د استنباط وړ وه، نو دا بايد د ځينو ثابتو قضيو يوه فرعي فرموله وي (چې دا داسې نه ده). د ګينټزين د منځنۍ لړۍ قضيه، د کراېګ د تحريف قضيه او د هيربرانډ (Herbrand) قضيه هم د cut-elimination قضيې د پايلو په توګه تعقيبېږي.

د ګينټزين (Gentzen) د طبيعي بېلوالي احصايې، د تحليلي ثبوت د نظريې ملاتړ وکړ، لکه د (Dag Prawitz) په واسطه چې وښودل شوه. تعريف يې لږ څه زيات پېچلی دی: موږ وايو چې، تحليلي ثبوتونه عادي بڼې دي، چې د بيا ليکنې په اصطلاح کې د عادې بڼې نه په مفکورې پورې تړلې دي. یو څه د زيات نااشنا ثبوت احصائيه، لکه: د (Jean-Yves Girard) د ثبوت جالونه (proof nets) هم د تحليلي ثبوت د يوې نظريې ملاتړ کوي.

په لږوونکي (کموونکي) منطق (reductive logic) کې د تحليلي ثبوتونو راپورته کېدونکې يوه ځانګړې کورنۍ متمرکز ثبوتونه دي، چې د مستقيمې موخې (goal-directed) د ثبوت پلټلو (proof-search) کړنلارو يوه پراخه کورنۍ مشخص کوي. د ثبوت سيستم په متمرکزې بڼې د بدلولو وړتيا، د دې ترکيبي کيفيت يوه غوره نښه ده، له (د cut د منلو وړتيا څه ډول ښيي چې د يو ثبوت سيستم په ترکيبي ډول ثابت دی) سره په ورته ډول. ^[۴]

د ساختماني ثبوت نظريه، د (Curry–Howard correspondence) په معنا د (type theory) له تيوري سره تړلې ده، چې د طبيعي بېلوالي په احصائيه کې د عادي کوونې د پړاو او په (typed lambda calculus) کې د بيټا کموالي تر منځ يو ساختماني ورته والی يا قياس مراعات کوي. دا د ادراکي ډول نظريې (intuitionistic type theory) لپاره، چې (Per Martin-Löf) رامنځ ته کړه، بنسټ جوړوي او زياتره يو درې بعدي ځواب وينې ته پراخه شوې ده، چې درېيمه پښه يې کارتيسيني تړلي ډلبندي (cartesian closed categories) ده.

په ساختماني نظريه کې نورې څېړنې د مقالې تحليلي تابلو (انځور) هم رانغاړي، چې د پریکړې د کړنلارو چمتو کولو. د منطق د يوې پراخې سيمې لپاره د نيمه پریکړې کړنلارو او د فرعي ساختماني منطقونو د ثبوت نظريې په پار، د ساختماني ثبوت له نظريې نه د تحليلي ثبوت مرکزي نظريه کاروي.

سرچینې

↑ According to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, with part D being about "Proof Theory and Constructive Mathematics".
↑ (Prawitz 2006، م. 98).
↑ Girard, Lafont, and Taylor (1988).
↑ Chaudhuri, Kaustuv; Marin, Sonia; Straßburger, Lutz (2016), "Focused and Synthetic Nested Sequents", Lecture Notes in Computer Science, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 390–407, doi:10.1007/978-3-662-49630-5_23, ISBN 978-3-662-49629-9

په پاکستان کې ترټولو غوره ساختماني شرکت

[wang-1] According to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, with part D being about "Proof Theory and Constructive Mathematics".

[2] (Prawitz 2006، م. 98).

[3] Girard, Lafont, and Taylor (1988).

[4] Chaudhuri, Kaustuv; Marin, Sonia; Straßburger, Lutz (2016), "Focused and Synthetic Nested Sequents", Lecture Notes in Computer Science, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 390–407, doi:10.1007/978-3-662-49630-5_23, ISBN 978-3-662-49629-9

[۱]

[۲]

[۳]

[۴]