Natural deduction
તર્ક અને પ્રૂફ થિયરીમાં, નેચરલ ડિડક્શન એ એક પ્રકારનું પ્રૂફ કેલ્ક્યુલસ છે જેમાં તાર્કિક તર્કને તર્કની "નેચરલ" રીત સાથે નજીકથી સંબંધિત અનુમાન નિયમો દ્વારા વ્યક્ત કરવામાં આવે છે. આ હિલ્બર્ટ-શૈલીની પ્રણાલીઓથી વિપરીત છે, જે તેના બદલે અનુમાનાત્મક તર્કના તાર્કિક નિયમોને વ્યક્ત કરવા માટે શક્ય તેટલા સ્વયંસિદ્ધ શબ્દોનો ઉપયોગ કરે છે. હિલ્બર્ટ, ફ્રેજ અને રસેલ (જુઓ, દા. ત. હિલ્બર્ટ પ્રણાલી) ની પ્રણાલીઓમાં સામાન્ય અનુમાનાત્મક તર્કના સ્વયંસિદ્ધીકરણો સાથેના અસંતોષના સંદર્ભમાં કુદરતી કપાતનો વિકાસ થયો. આવા સ્વયંસિદ્ધીકરણોનો ઉપયોગ રસેલ અને વ્હાઇટહેડ દ્વારા તેમના ગાણિતિક ગ્રંથ પ્રિન્સિપિયા મેથેમેટિકા માં સૌથી વધુ પ્રખ્યાત રીતે કરવામાં આવ્યો હતો. 1926માં પોલેન્ડમાં લ્યુકાસીવિક્ઝ દ્વારા તર્કની વધુ કુદરતી સારવારની હિમાયત કરતા પરિસંવાદોની શ્રેણી દ્વારા પ્રેરિત થઈને, જેસ્કોવ્સ્કીએ વધુ કુદરતી કપાતને વ્યાખ્યાયિત કરવાના પ્રારંભિક પ્રયાસો કર્યા, સૌપ્રથમ 1929માં આકૃતિના સંકેતનો ઉપયોગ કરીને, અને બાદમાં 1934 અને 1935માં કાગળોની શ્રેણીમાં તેમની દરખાસ્તને અપડેટ કરી. તેમની દરખાસ્તો ફિચ-શૈલીના કલન (અથવા ફિચના આકૃતિઓ) અથવા સુપ્સ પદ્ધતિ જેવા વિવિધ સંકેતો તરફ દોરી ગઈ, જેના માટે લેમોને તેના આધુનિક સ્વરૂપમાં સિસ્ટમ એલ. નેચરલ ડિડક્શન નામનો એક પ્રકાર આપ્યો હતો, જે જર્મન ગણિતશાસ્ત્રી ગેરહાર્ડ જેન્ટ્ઝેન દ્વારા 1933માં ગોટિન્જેન યુનિવર્સિટીના ગાણિતિક વિજ્ઞાનના ફેકલ્ટીને આપવામાં આવેલા એક નિબંધમાં સ્વતંત્ર રીતે પ્રસ્તાવિત કરવામાં આવ્યો હતો. નેચરલ ડિડક્શન શબ્દ (અથવા તેના બદલે, તેના જર્મન સમકક્ષ નેચુર્લિચેસ શ્લીસેન) તે પેપરમાં રચવામાં આવ્યો હતોઃ જેન્ટ્ઝન સંખ્યા સિદ્ધાંતની સુસંગતતા સ્થાપિત કરવાની ઇચ્છાથી પ્રેરિત હતો. તેઓ સુસંગતતા પરિણામ માટે જરૂરી મુખ્ય પરિણામ, કટ એલિમિનેશન થીયરમ-હૌપ્ટસાટ્ઝ-સીધા કુદરતી ડિડક્શન માટે સાબિત કરવામાં અસમર્થ હતા. આ કારણોસર તેમણે તેમની વૈકલ્પિક પદ્ધતિ, ક્રમિક કલન રજૂ કરી, જેના માટે તેમણે શાસ્ત્રીય અને અંતર્જ્ઞાની તર્કશાસ્ત્ર બંને માટે હૌપ્ટસાટ્ઝને સાબિત કર્યું. 1961 અને 1962માં પરિસંવાદોની શ્રેણીમાં પ્રવિત્ઝે નેચરલ ડિડક્શન કેલ્ક્યુલીનો વ્યાપક સારાંશ આપ્યો હતો અને જેન્ટ્ઝેનના મોટાભાગના કાર્યને ક્રમિક કેલ્ક્યુલી સાથે નેચરલ ડિડક્શન માળખામાં પરિવહન કર્યું હતું. તેમનો 1965 નો મોનોગ્રાફ નેચરલ ડિડક્શનઃ એ પ્રૂફ-થિયોરેટિકલ સ્ટડી નેચરલ ડિડક્શન પર સંદર્ભ કાર્ય બનવાનો હતો, અને તેમાં મોડલ અને સેકન્ડ ઓર્ડર લોજિક માટેના ઉપયોગોનો સમાવેશ થતો હતો. નેચરલ ડિડક્શનમાં, અનુમાનના નિયમોને વારંવાર લાગુ કરીને પરિસરના સંગ્રહમાંથી પ્રસ્તાવ કાઢવામાં આવે છે. આ લેખમાં રજૂ કરવામાં આવેલી પદ્ધતિ જેન્ટ્ઝેન અથવા પ્રાવિટ્ઝની રચનાની એક નાની વિવિધતા છે, પરંતુ માર્ટિન-લોફના તાર્કિક ચુકાદાઓ અને જોડાણોના વર્ણનનું નજીકથી પાલન કરે છે. ચુકાદાઓ અને દરખાસ્તો ચુકાદો એ એવી વસ્તુ છે જે જાણી શકાય તેવું છે, એટલે કે જ્ઞાનનો હેતુ છે. જો કોઈ હકીકતમાં તેને જાણે છે તો તે સ્પષ્ટ છે. આમ "વરસાદ પડી રહ્યો છે" એ ચુકાદો છે, જે તે વ્યક્તિ માટે સ્પષ્ટ છે જે જાણે છે કે ખરેખર વરસાદ પડી રહ્યો છે; આ કિસ્સામાં વ્યક્તિ બારીની બહાર જોઈને અથવા ઘરની બહાર નીકળીને ચુકાદાના પુરાવા સરળતાથી શોધી શકે છે. જો કે, ગાણિતિક તર્કશાસ્ત્રમાં, પુરાવા ઘણીવાર સીધા અવલોકનક્ષમ નથી, પરંતુ વધુ મૂળભૂત સ્પષ્ટ ચુકાદાઓમાંથી તારણ કાઢવામાં આવે છે. કપાતની પ્રક્રિયા એ છે જે સાબિતી બનાવે છે; બીજા શબ્દોમાં કહીએ તો, જો કોઈની પાસે તેનો પુરાવો હોય તો ચુકાદો સ્પષ્ટ થાય છે. તર્કશાસ્ત્રમાં સૌથી મહત્વપૂર્ણ ચુકાદાઓ "એ સાચું છે" સ્વરૂપના હોય છે. અક્ષર A એ દરખાસ્તનું પ્રતિનિધિત્વ કરતી કોઈપણ અભિવ્યક્તિ માટે વપરાય છે; તેથી સત્ય ચુકાદાઓ માટે વધુ આદિમ ચુકાદાની જરૂર પડે છેઃ "A એ એક દરખાસ્ત છે". અન્ય ઘણા ચુકાદાઓનો અભ્યાસ કરવામાં આવ્યો છે; ઉદાહરણ તરીકે, "A ખોટો છે" (શાસ્ત્રીય તર્ક જુઓ), "A સમય t પર સાચો છે" (અસ્થાયી તર્ક જુઓ), "A આવશ્યકપણે સાચો છે" અથવા "A સંભવતઃ સાચો છે" (મોડલ તર્ક જુઓ), "M પ્રોગ્રામમાં τ પ્રકાર છે" (પ્રોગ્રામિંગ ભાષાઓ અને પ્રકાર સિદ્ધાંત જુઓ), "A ઉપલબ્ધ સંસાધનોમાંથી પ્રાપ્ત કરી શકાય તેવું છે" (રેખીય તર્ક જુઓ), અને અન્ય ઘણા. શરૂ કરવા માટે, આપણે સૌથી સરળ બે ચુકાદાઓ "એ એક દરખાસ્ત છે" અને "એ સાચું છે", જે અનુક્રમે "એ પ્રોપ" અને "એ સાચું" તરીકે સંક્ષિપ્ત છે. ચુકાદો "એ પ્રોપ" એ ના માન્ય પુરાવાઓની રચનાને વ્યાખ્યાયિત કરે છે, જે બદલામાં દરખાસ્તોની રચનાને વ્યાખ્યાયિત કરે છે. આ કારણોસર, આ ચુકાદા માટેના અનુમાન નિયમોને કેટલીકવાર રચના નિયમો તરીકે ઓળખવામાં આવે છે. ઉદાહરણ તરીકે, જો આપણી પાસે બે દરખાસ્તો A અને B હોય (એટલે કે, ચુકાદાઓ "A પ્રોપ" અને "B પ્રોપ" સ્પષ્ટ છે), તો આપણે સંયોજન દરખાસ્ત A અને B બનાવીએ છીએ, જે પ્રતીકાત્મક રીતે "" તરીકે લખાય છે. આપણે આને અનુમાન નિયમના સ્વરૂપમાં લખી શકીએ છીએઃ જ્યાં અનુમાન નિયમને વધુ સંક્ષિપ્ત બનાવવા માટે કૌંસને અવગણવામાં આવે છેઃ આ અનુમાન નિયમ યોજનાબદ્ધ છેઃ A અને B ને કોઈપણ અભિવ્યક્તિ સાથે ત્વરિત કરી શકાય છે. અનુમાન નિયમનું સામાન્ય સ્વરૂપ છેઃ જ્યાં દરેક ચુકાદો છે અને અનુમાન નિયમને "નામ" નામ આપવામાં આવ્યું છે. રેખાની ઉપરના ચુકાદાઓને પરિસર તરીકે ઓળખવામાં આવે છે, અને રેખાની નીચેના ચુકાદાઓ તારણો છે. અન્ય સામાન્ય તાર્કિક દરખાસ્તો ડિસજંક્શન (), નેગેશન (), ઇમ્પ્લિકેશન (), અને લોજિકલ અચળાંકો સત્ય () અને અસત્ય () છે. તેમની રચનાના નિયમો નીચે મુજબ છે. પરિચય અને નાબૂદી હવે આપણે "એક સાચા" ચુકાદાની ચર્ચા કરીએ છીએ. નિષ્કર્ષમાં તાર્કિક જોડાણ રજૂ કરતા અનુમાન નિયમો પરિચય નિયમો તરીકે ઓળખાય છે. સંયોજન રજૂ કરવા માટે, એટલે કે, એ અને બી દરખાસ્તો માટે "એ અને બી સાચું" તારણ કાઢવા માટે, "એ સાચું" અને "બી સાચું" માટે પુરાવા જરૂરી છે. એક અનુમાન નિયમ તરીકેઃ તે સમજવું આવશ્યક છે કે આવા નિયમોમાં પદાર્થો દરખાસ્તો છે. એટલે કે, ઉપરોક્ત નિયમ ખરેખર આના માટે સંક્ષિપ્ત છેઃ આ પણ લખી શકાય છેઃ આ સ્વરૂપમાં, પ્રથમ આધારને રચનાના નિયમ દ્વારા સંતુષ્ટ કરી શકાય છે, જે અગાઉના સ્વરૂપના પ્રથમ બે પરિસર આપે છે. આ લેખમાં આપણે "પ્રોપ" ચુકાદાઓને જ્યાં સમજાય છે ત્યાં બહાર કાઢીશું. શૂન્ય કિસ્સામાં, કોઈ પણ વ્યક્તિ કોઈ પણ આધારમાંથી સત્ય મેળવી શકતી નથી. જો દરખાસ્તનું સત્ય એકથી વધુ રીતે સ્થાપિત કરી શકાય, તો અનુરૂપ સંયોજકમાં બહુવિધ પરિચય નિયમો હોય છે. નોંધ લો કે નલરી કેસમાં, એટલે કે, જૂઠાણું માટે, કોઈ પરિચય નિયમો નથી. આમ કોઈ પણ સરળ ચુકાદાઓમાંથી જૂઠાણાનું અનુમાન ક્યારેય કરી શકતું નથી. સંયોજન દરખાસ્ત વિશેની માહિતીને તેના ઘટકો વિશેની માહિતીમાં કેવી રીતે વિકસાવવી તે વર્ણવવા માટે બેવડાથી પરિચય નિયમો એ નાબૂદી નિયમો છે. આમ, "એ વાય બી સાચું" માંથી, આપણે "એ સાચું" અને "બી સાચું" તારણ કાઢી શકીએ છીએઃ અનુમાન નિયમોના ઉપયોગના ઉદાહરણ તરીકે, જોડાણની વિનિમયશીલતાને ધ્યાનમાં લો. જો એ. વાય. બી. સાચું હોય, તો બી. વાય. એ. સાચું છે; આ વ્યુત્પત્તિ અનુમાનના નિયમોની રચના કરીને એવી રીતે દોરી શકાય છે કે નીચલા અનુમાનનો પરિસર આગામી ઉચ્ચ અનુમાનના નિષ્કર્ષ સાથે મેળ ખાય. આપણે અત્યાર સુધી જે અનુમાન આંકડા જોયા છે તે સૂચિતાર્થ પરિચય અથવા વિચ્છેદન નાબૂદીના નિયમો જણાવવા માટે પૂરતા નથી; આ માટે, આપણને કાલ્પનિક વ્યુત્પત્તિ વિશે વધુ સામાન્ય કલ્પનાની જરૂર છે. કાલ્પનિક વ્યુત્પત્તિઓ ગાણિતિક તર્કશાસ્ત્રમાં વ્યાપક કામગીરી એ ધારણાઓમાંથી તર્ક છે. ઉદાહરણ તરીકે, નીચેની વ્યુત્પત્તિને ધ્યાનમાં લોઃ આ વ્યુત્પત્તિ બી ના સત્યને સ્થાપિત કરતી નથી; તેના બદલે, તે નીચેની હકીકતને સ્થાપિત કરે છેઃ જો એ (બી) સાચું હોય તો બી સાચું છે. તર્કશાસ્ત્રમાં, એક કહે છે કે "ધારો કે એ (બી) સાચું છે, આપણે બતાવીએ છીએ કે બી સાચું છે"; બીજા શબ્દોમાં કહીએ તો, ચુકાદો "બી સાચું" ધારેલા ચુકાદા "એ (બી) સાચું" પર આધારિત છે. આ એક કાલ્પનિક વ્યુત્પત્તિ છે, જેને આપણે નીચે પ્રમાણે લખીએ છીએઃ અર્થઘટન છેઃ "બી સાચું એ એ વાય (બી વાય સી) સાચું માંથી વ્યુત્પન્ન છે". અલબત્ત, આ ચોક્કસ ઉદાહરણમાં આપણે ખરેખર "બી ટ્રુ" નું વ્યુત્પત્તિ "એ. વાય. (બી. વાય. સી.) ટ્રુ" માંથી જાણી શકીએ છીએ, પરંતુ સામાન્ય રીતે આપણે પ્રાયોરી વ્યુત્પત્તિને જાણતા નથી. કાલ્પનિક વ્યુત્પત્તિઓનું સામાન્ય સ્વરૂપ છેઃ દરેક કાલ્પનિક વ્યુત્પત્તિમાં ટોચની લીટી પર લખાયેલ પૂર્વવર્તી વ્યુત્પત્તિઓ (ડી. આઈ.) નો સંગ્રહ હોય છે, અને નીચેની લીટી પર લખાયેલ સફળ ચુકાદો (જે.) હોય છે. દરેક પરિસર પોતે એક કાલ્પનિક વ્યુત્પત્તિ હોઈ શકે છે. (સરળતા માટે, અમે ચુકાદાને આધાર-ઓછી વ્યુત્પત્તિ તરીકે માનીએ છીએ.) કાલ્પનિક ચુકાદાની કલ્પનાને સૂચિતાર્થના સંયોજક તરીકે આંતરિક કરવામાં આવે છે. પરિચય અને નાબૂદીના નિયમો નીચે મુજબ છે. પરિચયના નિયમમાં, યુ નામના પૂર્વવર્તીને નિષ્કર્ષમાં મુક્ત કરવામાં આવે છે. પૂર્વધારણાના અવકાશને મર્યાદિત કરવા માટેની આ એક પદ્ધતિ છેઃ તેના અસ્તિત્વનું એકમાત્ર કારણ "બી સાચું" સ્થાપિત કરવાનું છે; તેનો ઉપયોગ અન્ય કોઈ હેતુ માટે કરી શકાતો નથી, અને ખાસ કરીને, તેનો ઉપયોગ પરિચયની નીચે કરી શકાતો નથી. ઉદાહરણ તરીકે, "A′ (B′ (A′B)) સાચા" ની વ્યુત્પત્તિને ધ્યાનમાં લોઃ આ સંપૂર્ણ વ્યુત્પત્તિને કોઈ અસંતુષ્ટ આધાર નથી; જો કે, પેટા-વ્યુત્પત્તિઓ કાલ્પનિક છે. દાખલા તરીકે, "બી. (એ. બી.) સાચું" ની વ્યુત્પત્તિ પૂર્વવર્તી "એ સાચું" (નામ યુ) સાથે કાલ્પનિક છે. કાલ્પનિક વ્યુત્પત્તિઓ સાથે, હવે આપણે વિચ્છેદન માટે નાબૂદી નિયમ લખી શકીએ છીએઃ શબ્દોમાં કહીએ તો, જો A * B સાચું હોય, અને આપણે "A" સાચું "અને" B સાચું "બંનેમાંથી" C સાચું "મેળવી શકીએ, તો C ખરેખર સાચું છે. નોંધ લો કે આ નિયમ "એ સાચું" અથવા "બી સાચું" માટે પ્રતિબદ્ધ નથી. શૂન્ય-એરી કેસમાં, એટલે કે. જૂઠાણું માટે, આપણે નીચેનો નાબૂદી નિયમ મેળવીએ છીએઃ આને આ રીતે વાંચવામાં આવે છેઃ જો જૂઠાણું સાચું હોય, તો કોઈપણ દરખાસ્ત C સાચું છે. નકારાત્મકતા એ સૂચિતાર્થ જેવી જ છે. પરિચય નિયમ પૂર્વધારણાના નામ યુ, અને અનુગામી પી, એટલે કે, પ્રપોઝિશન પી નિષ્કર્ષ A માં ન થવું જોઈએ, એમ બંનેને વિસર્જિત કરે છે. આ નિયમો યોજનાકીય હોવાથી, પરિચય નિયમનો અર્થઘટન છેઃ જો "A સાચું" માંથી આપણે દરેક દરખાસ્ત p માટે "p સાચું" મેળવી શકીએ, તો A ખોટો હોવો જોઈએ, એટલે કે, "A સાચું નહીં". નાબૂદી માટે, જો A અને A નહીં બંને સાચા હોવાનું દર્શાવવામાં આવે, તો ત્યાં એક વિરોધાભાસ છે, જે કિસ્સામાં દરેક દરખાસ્ત C સાચી છે. કારણ કે સૂચિતાર્થ અને નિષેધ માટેના નિયમો ખૂબ સમાન છે, તે જોવાનું એકદમ સરળ હોવું જોઈએ કે A અને A સમાન નથી, એટલે કે, દરેક અન્યમાંથી વ્યુત્પન્ન છે. સુસંગતતા, સંપૂર્ણતા અને સામાન્ય સ્વરૂપો એક સિદ્ધાંતને સુસંગત કહેવામાં આવે છે જો જૂઠાણું સાબિત ન થાય (કોઈ ધારણાઓથી નહીં) અને જો દરેક પ્રમેય અથવા તેની નકારાત્મકતા તર્કના અનુમાન નિયમોનો ઉપયોગ કરીને સાબિત કરી શકાય તો તે પૂર્ણ થાય છે. આ સમગ્ર તર્ક વિશેના નિવેદનો છે, અને સામાન્ય રીતે મોડેલની કેટલીક કલ્પના સાથે જોડાયેલા હોય છે. જો કે, સુસંગતતા અને સંપૂર્ણતાની સ્થાનિક કલ્પનાઓ છે જે અનુમાન નિયમો પર શુદ્ધ વાક્યરચના તપાસ છે, અને મોડેલોને કોઈ અપીલની જરૂર નથી. આમાંથી પ્રથમ સ્થાનિક સુસંગતતા છે, જેને સ્થાનિક રિડ્યુસિબિલિટી તરીકે પણ ઓળખવામાં આવે છે, જે કહે છે કે સંયોજકની રજૂઆત ધરાવતી કોઈપણ વ્યુત્પત્તિ અને તેના તરત જ નાબૂદીને આ ચકરાવો વિના સમકક્ષ વ્યુત્પત્તિમાં ફેરવી શકાય છે. તે નાબૂદીના નિયમોની મજબૂતાઈ પર એક તપાસ છેઃ તેઓ એટલા મજબૂત ન હોવા જોઈએ કે તેઓ તેમના પરિસરમાં પહેલેથી જ સમાવિષ્ટ જ્ઞાનનો સમાવેશ કરતા નથી. ઉદાહરણ તરીકે, સંયોજનોનો વિચાર કરો. બંને રીતે, સ્થાનિક પૂર્ણતા કહે છે કે નાબૂદીના નિયમો એટલા મજબૂત છે કે જોડણીને તેના પરિચય નિયમ માટે યોગ્ય સ્વરૂપોમાં વિઘટિત કરી શકાય છે. ફરીથી સંયોજન માટેઃ આ ધારણાઓ કરી-હોવર્ડ આઇસોમોર્ફિઝમનો ઉપયોગ કરીને લેમ્બડા કલનમાં β-ઘટાડો (બીટા ઘટાડો) અને η-રૂપાંતર (ઇટા રૂપાંતર) ને બરાબર અનુરૂપ છે. સ્થાનિક પૂર્ણતા દ્વારા, આપણે જોઈએ છીએ કે દરેક વ્યુત્પત્તિને સમકક્ષ વ્યુત્પત્તિમાં રૂપાંતરિત કરી શકાય છે જ્યાં મુખ્ય સંયોજક રજૂ કરવામાં આવે છે. હકીકતમાં, જો સમગ્ર વ્યુત્પત્તિ પરિચય પછી નાબૂદીના આ ક્રમનું પાલન કરે છે, તો તેને સામાન્ય કહેવામાં આવે છે. સામાન્ય વ્યુત્પત્તિમાં તમામ નાબૂદીઓ પરિચયની ઉપર થાય છે. મોટાભાગના તર્કશાસ્ત્રમાં, દરેક વ્યુત્પત્તિમાં સમકક્ષ સામાન્ય વ્યુત્પત્તિ હોય છે, જેને સામાન્ય સ્વરૂપ કહેવાય છે. સામાન્ય સ્વરૂપોનું અસ્તિત્વ સામાન્ય રીતે માત્ર કુદરતી કપાતનો ઉપયોગ કરીને સાબિત કરવું મુશ્કેલ છે, જો કે આવા અહેવાલો સાહિત્યમાં અસ્તિત્વ ધરાવે છે, ખાસ કરીને 1961માં ડાગ પ્રાવિટ્ઝ દ્વારા. કટ-ફ્રી ક્રમિક કલન પ્રસ્તુતિ દ્વારા આડકતરી રીતે આ બતાવવું ખૂબ સરળ છે. પ્રથમ અને ઉચ્ચ ક્રમના વિસ્તરણ અગાઉના વિભાગનો તર્ક એ એક-ક્રમાંકિત તર્કનું ઉદાહરણ છે, એટલે કે, એક જ પ્રકારની વસ્તુ સાથેનો તર્કઃ દરખાસ્તો. આ સરળ માળખાના ઘણા વિસ્તરણની દરખાસ્ત કરવામાં આવી છે; આ વિભાગમાં આપણે તેને બીજા પ્રકારની વ્યક્તિઓ અથવા શરતો સાથે વિસ્તૃત કરીશું. વધુ ચોક્કસપણે, આપણે એક નવા પ્રકારનો ચુકાદો ઉમેરીશું, "ટી એ એક શબ્દ છે" (અથવા "ટી શબ્દ") જ્યાં ટી યોજનાકીય છે. આપણે ચલોનો ગણતરીપાત્ર સમૂહ V, કાર્ય પ્રતીકોનો અન્ય ગણતરીપાત્ર સમૂહ F નક્કી કરીશું અને નીચેના રચના નિયમો સાથે શરતો બનાવીશુંઃ અને દરખાસ્તો માટે, આપણે આગાહીઓના ત્રીજા ગણતરીપાત્ર સમૂહ P ને ધ્યાનમાં લઈએ છીએ, અને નીચેના રચના નિયમ સાથે શરતો પર અણુ આગાહીઓને વ્યાખ્યાયિત કરીએ છીએઃ રચનાના પ્રથમ બે નિયમો એવા શબ્દની વ્યાખ્યા પ્રદાન કરે છે જે અસરકારક રીતે બીજગણિત અને મોડેલ સિદ્ધાંત શબ્દમાં વ્યાખ્યાયિત કરેલા સમાન છે, જો કે અભ્યાસના તે ક્ષેત્રોનું ધ્યાન કુદરતી કપાતથી તદ્દન અલગ છે. રચનાનો ત્રીજો નિયમ અણુ સૂત્રને અસરકારક રીતે વ્યાખ્યાયિત કરે છે, જેમ કે પ્રથમ ક્રમના તર્કમાં અને ફરીથી મોડેલ સિદ્ધાંતમાં. આમાં રચનાના નિયમોની જોડી ઉમેરવામાં આવે છે, જે માત્રાત્મક દરખાસ્તો માટે સંકેતલિપીને વ્યાખ્યાયિત કરે છે; એક સાર્વત્રિક (β) અને અસ્તિત્વ (HE) પરિમાણ માટેઃ સાર્વત્રિક પરિમાણમાં પરિચય અને નાબૂદીના નિયમો હોય છેઃ અસ્તિત્વના પરિમાણમાં પરિચય અને નાબૂદીના નિયમો હોય છેઃ આ નિયમોમાં, સંકેતલિપી [t/x] A એ કેપ્ચરને ટાળીને, A માં x ના દરેક (દૃશ્યમાન) ઉદાહરણ માટે t ના અવેજી માટે વપરાય છે. પહેલાની જેમ નામ પરની સુપરસ્ક્રિપ્ટ્સ એ ઘટકો માટે વપરાય છે જે વિસર્જિત થાય છેઃ શબ્દ a એ આઈ. ટી. આઈ. ના નિષ્કર્ષમાં આવી શકતો નથી (આવા શબ્દો આઈગનવેરિયેબલ્સ અથવા પરિમાણો તરીકે ઓળખાય છે), અને એચ. ઈ. ઈ. માં યુ અને વી નામની પૂર્વધારણાઓ કાલ્પનિક વ્યુત્પત્તિમાં બીજા આધાર પર સ્થાનિક છે. અગાઉના વિભાગોનો પ્રસ્તાવાત્મક તર્ક નિર્ણાયક હોવા છતાં, પરિમાણો ઉમેરવાથી તર્ક અનિશ્ચિત બને છે. અત્યાર સુધી, ક્વોન્ટિફાઇડ એક્સ્ટેન્શન્સ ફર્સ્ટ-ઓર્ડર છેઃ તેઓ પ્રપોઝિશનને ક્વોન્ટિફાઇડ ઓબ્જેક્ટ્સના પ્રકારોથી અલગ પાડે છે. ઉચ્ચ ક્રમના તર્ક એક અલગ અભિગમ અપનાવે છે અને તેમાં માત્ર એક જ પ્રકારની દરખાસ્તો હોય છે. પરિમાણકો પરિમાણના ક્ષેત્ર તરીકે સમાન પ્રકારની દરખાસ્તો ધરાવે છે, જે રચનાના નિયમોમાં પ્રતિબિંબિત થાય છેઃ ઉચ્ચ ક્રમના તર્ક માટે પરિચય અને નાબૂદી સ્વરૂપોની ચર્ચા આ લેખના અવકાશની બહાર છે. પ્રથમ ક્રમ અને ઉચ્ચ ક્રમના તર્ક વચ્ચે રહેવું શક્ય છે. ઉદાહરણ તરીકે, બીજા ક્રમના તર્કમાં બે પ્રકારની દરખાસ્તો હોય છે, એક પ્રકારની શરતો પરની માત્રા, અને બીજી પ્રકારની પ્રથમ પ્રકારની દરખાસ્તો પરની માત્રા. કુદરતી કપાતની વિવિધ પ્રસ્તુતિઓ વૃક્ષ જેવી પ્રસ્તુતિઓ કાલ્પનિક ચુકાદાઓને આંતરિક બનાવવા માટે ઉપયોગમાં લેવાતી જેન્ટ્ઝેનની વિસર્જિત ટિપ્પણીઓને સાચા ચુકાદાઓના વૃક્ષને બદલે અનુક્રમના વૃક્ષ તરીકે સાબિતી રજૂ કરીને ટાળી શકાય છે. અનુક્રમિક પ્રસ્તુતિઓ જેસ્કોવ્સ્કીની કુદરતી કપાતની રજૂઆતો ફિચ-શૈલીના કલન (અથવા ફિચના આકૃતિઓ) અથવા સુપ્સ પદ્ધતિ જેવા વિવિધ સંકેતો તરફ દોરી ગઈ, જેમાંથી લેમોને સિસ્ટમ એલ તરીકે ઓળખાતી વિવિધતા આપી. આવી પ્રસ્તુતિ પ્રણાલીઓ, જેને વધુ સચોટ રીતે કોષ્ટક તરીકે વર્ણવવામાં આવે છે, તેમાં નીચેનાનો સમાવેશ થાય છે. 1940: એક પાઠ્યપુસ્તકમાં, ક્વિને ચોરસ કૌંસમાં રેખા સંખ્યાઓ દ્વારા પૂર્વવર્તી અવલંબન સૂચવ્યું, જેમાં સુપ્સના 1957ના રેખા-સંખ્યાના સંકેતની ધારણા કરવામાં આવી હતી. 1950: એક પાઠ્યપુસ્તકમાં, અવલંબન સૂચવવા માટે સાબિતીની દરેક લીટીની ડાબી બાજુએ એક અથવા વધુ ફૂદડીનો ઉપયોગ કરવાની પદ્ધતિ દર્શાવવામાં આવી. આ ક્લેનની ઊભી પટ્ટીઓની સમકક્ષ છે. (તે સંપૂર્ણપણે સ્પષ્ટ નથી કે ક્વિનનું તારાંકન મૂળ 1950ની આવૃત્તિમાં દેખાયું હતું કે પછીની આવૃત્તિમાં ઉમેરવામાં આવ્યું હતું.) 1957: દ્વારા પાઠ્યપુસ્તકમાં સાબિત થતા વ્યવહારુ તર્ક પ્રમેયનો પરિચય. આ નિર્ભરતાને સૂચવે છે (એટલે કે. પૂર્વવર્તી દરખાસ્તો) દરેક લીટીની ડાબી બાજુએ લીટી સંખ્યાઓ દ્વારા. 1963: કુદરતી કપાત અનુમાન નિયમો પર આધારિત ક્રમિક તાર્કિક દલીલોની રેખાઓના પૂર્વવર્તી અવલંબનને સૂચવવા માટે રેખા સંખ્યાઓના સમૂહનો ઉપયોગ કરે છે. 1965: 'બાય' નું આખું પાઠ્યપુસ્તક 'સપેઝ' પર આધારિત પદ્ધતિનો ઉપયોગ કરીને તર્ક સાબિતીનો પરિચય છે. 1967: એક પાઠ્યપુસ્તકમાં, સંક્ષિપ્તમાં બે પ્રકારના વ્યવહારુ તર્ક પુરાવાઓનું પ્રદર્શન કરવામાં આવ્યું હતું, એક પ્રણાલી દરેક લીટીની ડાબી બાજુએ પૂર્વવર્તી દરખાસ્તોના સ્પષ્ટ અવતરણોનો ઉપયોગ કરે છે, બીજી પ્રણાલી નિર્ભરતા સૂચવવા માટે ડાબી બાજુએ ઊભી પટ્ટી-રેખાઓનો ઉપયોગ કરે છે. પુરાવા અને પ્રકાર સિદ્ધાંત કુદરતી કપાતની રજૂઆત અત્યાર સુધી સાબિતીની ઔપચારિક વ્યાખ્યા આપ્યા વિના દરખાસ્તોની પ્રકૃતિ પર કેન્દ્રિત રહી છે. સાબિતીની કલ્પનાને ઔપચારિક બનાવવા માટે, આપણે કાલ્પનિક વ્યુત્પત્તિઓની રજૂઆતમાં થોડો ફેરફાર કરીએ છીએ. અમે પૂર્વજોને પ્રૂફ વેરિયેબલ્સ સાથે લેબલ કરીએ છીએ (વેરિયેબલ્સના કેટલાક ગણતરીપાત્ર સમૂહ V માંથી), અને વાસ્તવિક પ્રૂફ સાથે અનુગામીને શણગારે છે. પૂર્વજો અથવા પૂર્વધારણાઓને ટર્નસ્ટાઇલ () દ્વારા અનુગામીથી અલગ કરવામાં આવે છે. આ ફેરફાર કેટલીકવાર સ્થાનિક પૂર્વધારણાઓના નામ હેઠળ આવે છે. નીચેની આકૃતિ પરિવર્તનનો સારાંશ આપે છે. જ્યારે તેમની ચોક્કસ રચના સુસંગત ન હોય ત્યારે પૂર્વધારણાઓનો સંગ્રહ કુલુ તરીકે લખવામાં આવશે. સાબિતીઓને સ્પષ્ટ કરવા માટે, આપણે સાબિતી વિનાના ચુકાદા "એ સાચું" થી ચુકાદા તરફ આગળ વધીએ છીએઃ "π એ (એ સાચું) નો પુરાવો છે", જેને પ્રતીકાત્મક રીતે "π: એ સાચું" તરીકે લખવામાં આવે છે. પ્રમાણભૂત અભિગમને અનુસરીને, ચુકાદા "π પ્રૂફ" માટે પુરાવાઓને તેમના પોતાના રચનાના નિયમો સાથે નિર્દિષ્ટ કરવામાં આવે છે. સૌથી સરળ સંભવિત પુરાવો લેબલ થયેલ પૂર્વધારણાનો ઉપયોગ છે; આ કિસ્સામાં પુરાવો લેબલ પોતે જ છે. સંક્ષિપ્તતા માટે, આપણે આ લેખના બાકીના ભાગમાં ચુકાદાના લેબલને સાચું મૂકીશું, એટલે કે, "એ" લખો. ચાલો આપણે સ્પષ્ટ પુરાવાઓ સાથે કેટલાક જોડાણોની ફરીથી તપાસ કરીએ. સંયોજન માટે, આપણે સંયોજનના પુરાવાના સ્વરૂપને શોધવા માટે પરિચય નિયમને જોઈએ છીએઃ તે બે સંયોજનના પુરાવાની જોડી હોવી જોઈએ. આમઃ નાબૂદીના નિયમો E1 અને E2 ડાબી કે જમણી બાજુની કાંજંક્ટ પસંદ કરે છે; આમ સાબિતી એ અંદાજોની જોડી છે-પ્રથમ (fst) અને બીજું (snd). સૂચિતાર્થ માટે, પરિચય સ્વરૂપ પૂર્વધારણાને સ્થાનિક બનાવે છે અથવા જોડે છે, જે λ નો ઉપયોગ કરીને લખવામાં આવે છે; આ વિસર્જિત લેબલને અનુરૂપ છે. નિયમમાં, " તાઇ, યુઃ એ" એ વધારાની પૂર્વધારણા યુ સાથે મળીને પૂર્વધારણાઓના સંગ્રહ માટે વપરાય છે. સ્પષ્ટ રીતે ઉપલબ્ધ પુરાવાઓ સાથે, કોઈ વ્યક્તિ પુરાવાઓ વિશે હેરફેર કરી શકે છે અને તર્ક કરી શકે છે. સાબિતીઓ પરની મુખ્ય કામગીરી એ અન્ય સાબિતીમાં ઉપયોગમાં લેવાતી ધારણા માટે એક સાબિતીની અવેજી છે. આને સામાન્ય રીતે અવેજી પ્રમેય તરીકે ઓળખવામાં આવે છે, અને બીજા ચુકાદાની ઊંડાઈ (અથવા માળખા) પર ઇન્ડક્શન દ્વારા સાબિત કરી શકાય છે. અવેજી પ્રમેય જો એ અને એ, યુઃ એ. પી. પી. પી. 2: બી, તો પછી બી. અત્યાર સુધી ચુકાદામાં "એ" નું સંપૂર્ણ તાર્કિક અર્થઘટન કરવામાં આવ્યું છે. પ્રકાર સિદ્ધાંતમાં, પદાર્થોના વધુ કોમ્પ્યુટેશનલ દૃષ્ટિકોણ માટે તાર્કિક દૃષ્ટિકોણની આપ-લે થાય છે. તાર્કિક અર્થઘટનમાં દરખાસ્તોને હવે પ્રકારો તરીકે જોવામાં આવે છે, અને સાબિતીઓને લેમ્બડા કલનમાં કાર્યક્રમો તરીકે જોવામાં આવે છે. આમ "π: A" નું અર્થઘટન એ છે કે "પ્રોગ્રામમાં પ્રકાર A છે". તાર્કિક જોડાણોને પણ એક અલગ વાંચન આપવામાં આવે છેઃ સંયોજનને ઉત્પાદન (×) તરીકે જોવામાં આવે છે, સૂચિતાર્થને કાર્ય તીર (→), વગેરે તરીકે જોવામાં આવે છે. જો કે, તફાવતો માત્ર કોસ્મેટિક છે. પ્રકાર સિદ્ધાંત રચના, પરિચય અને નાબૂદીના નિયમોની દ્રષ્ટિએ કુદરતી કપાત પ્રસ્તુતિ ધરાવે છે; હકીકતમાં, વાચક અગાઉના વિભાગોમાંથી સરળ પ્રકાર સિદ્ધાંત તરીકે ઓળખાય છે તેનું સરળતાથી પુનઃનિર્માણ કરી શકે છે. તર્ક અને પ્રકાર સિદ્ધાંત વચ્ચેનો તફાવત મુખ્યત્વે પ્રકારો (દરખાસ્તો) થી કાર્યક્રમો (પુરાવાઓ) તરફ ધ્યાન કેન્દ્રિત કરવાનું છે. પ્રકાર સિદ્ધાંત મુખ્યત્વે પ્રોગ્રામ્સની કન્વર્ટિબિલિટી અથવા રિડ્યુસિબિલિટીમાં રસ ધરાવે છે. દરેક પ્રકાર માટે, તે પ્રકારના કેનોનિકલ પ્રોગ્રામ્સ છે જે ઈરીડ્યુસિબલ છે; આ કેનોનિકલ સ્વરૂપો અથવા મૂલ્યો તરીકે ઓળખાય છે. જો દરેક પ્રોગ્રામને કેનોનિકલ સ્વરૂપમાં ઘટાડી શકાય, તો પ્રકાર સિદ્ધાંતને સામાન્ય (અથવા નબળું સામાન્ય) કહેવામાં આવે છે. જો કેનોનિકલ સ્વરૂપ અનન્ય હોય, તો સિદ્ધાંતને મજબૂત રીતે સામાન્ય બનાવતો હોવાનું કહેવાય છે. સામાન્યતા એ મોટાભાગના બિન-તુચ્છ પ્રકારનાં સિદ્ધાંતોનું એક દુર્લભ લક્ષણ છે, જે તાર્કિક વિશ્વથી એક મોટું પ્રસ્થાન છે. (યાદ કરો કે લગભગ દરેક તાર્કિક વ્યુત્પત્તિ સમાન સામાન્ય વ્યુત્પત્તિ ધરાવે છે.) કારણને સ્કેચ કરવા માટેઃ પુનરાવર્તિત વ્યાખ્યાઓને સ્વીકારતા પ્રકાર સિદ્ધાંતોમાં, એવા પ્રોગ્રામ્સ લખવાનું શક્ય છે જે ક્યારેય મૂલ્યમાં ઘટાડો કરતા નથી; આવા લૂપિંગ પ્રોગ્રામ્સને સામાન્ય રીતે કોઈપણ પ્રકાર આપી શકાય છે. ખાસ કરીને, લૂપિંગ પ્રોગ્રામમાં δ પ્રકાર હોય છે, જો કે "δ સાચું" નો કોઈ તાર્કિક પુરાવો નથી. આ કારણોસર, પ્રકારો તરીકેની દરખાસ્તો; પ્રોગ્રામ્સના દાખલા તરીકે પુરાવાઓ માત્ર એક જ દિશામાં કામ કરે છે, જો એમ હોય તોઃ પ્રકાર સિદ્ધાંતને તર્ક તરીકે અર્થઘટન સામાન્ય રીતે અસંગત તર્ક આપે છે. ઉદાહરણોઃ આશ્રિત પ્રકાર સિદ્ધાંત તર્કની જેમ, પ્રકાર સિદ્ધાંતમાં ઘણા વિસ્તરણ અને પ્રકારો છે, જેમાં પ્રથમ ક્રમ અને ઉચ્ચ ક્રમના સંસ્કરણોનો સમાવેશ થાય છે. એક શાખા, જેને આશ્રિત પ્રકાર સિદ્ધાંત તરીકે ઓળખવામાં આવે છે, તેનો ઉપયોગ સંખ્યાબંધ કમ્પ્યુટર-સહાયિત પ્રૂફ સિસ્ટમ્સમાં થાય છે. આશ્રિત પ્રકાર સિદ્ધાંત ક્વોન્ટિફાયરને પ્રોગ્રામ્સ પર શ્રેણીબદ્ધ કરવાની મંજૂરી આપે છે. આ પરિમાણિત પ્રકારો τ અને HE ને બદલે Π અને  નિષ્પાદન તરીકે લખવામાં આવે છે, અને નીચેના રચના નિયમો ધરાવે છેઃ આ પ્રકારો અનુક્રમે તીર અને ઉત્પાદન પ્રકારોના સામાન્યીકરણ છે, જેમ કે તેમના પરિચય અને નાબૂદી નિયમો દ્વારા સાક્ષી છે. સંપૂર્ણ સામાન્યતામાં આશ્રિત પ્રકારનો સિદ્ધાંત ખૂબ જ શક્તિશાળી છેઃ તે પ્રોગ્રામ્સના પ્રકારોમાં સીધા જ પ્રોગ્રામ્સના લગભગ કોઈપણ કલ્પનીય ગુણધર્મને વ્યક્ત કરવામાં સક્ષમ છે. આ સામાન્યતા તીવ્ર કિંમતે આવે છે-ક્યાં તો ટાઇપચેકિંગ અનિશ્ચિત છે (એક્સ્ટેન્શનલ પ્રકાર સિદ્ધાંત), અથવા એક્સ્ટેન્શનલ તર્ક વધુ મુશ્કેલ છે (ઇન્ટેન્શનલ પ્રકાર સિદ્ધાંત). આ કારણોસર, કેટલાક આશ્રિત પ્રકાર સિદ્ધાંતો મનસ્વી કાર્યક્રમો પર માત્રાત્મકતાને મંજૂરી આપતા નથી, પરંતુ આપેલ નિર્ણાયક અનુક્રમણિકા ક્ષેત્રના કાર્યક્રમો સુધી મર્યાદિત છે, ઉદાહરણ તરીકે પૂર્ણાંકો, શબ્દમાળાઓ અથવા રેખીય કાર્યક્રમો. આશ્રિત પ્રકાર સિદ્ધાંતો પ્રકારોને કાર્યક્રમો પર આધાર રાખવાની મંજૂરી આપે છે, તેથી સ્વાભાવિક પ્રશ્ન એ છે કે કાર્યક્રમો માટે પ્રકારો અથવા અન્ય કોઈ સંયોજન પર આધાર રાખવો શક્ય છે કે કેમ. આવા પ્રશ્નોના ઘણા પ્રકારનાં જવાબો છે. પ્રકાર સિદ્ધાંતમાં એક લોકપ્રિય અભિગમ એ છે કે પ્રોગ્રામ્સને પ્રકારો પર પ્રમાણિત કરવાની મંજૂરી આપવી, જેને પેરામેટ્રિક પોલીમોર્ફિઝમ તરીકે પણ ઓળખવામાં આવે છે; આમાંથી બે મુખ્ય પ્રકારો છેઃ જો પ્રકારો અને પ્રોગ્રામ્સને અલગ રાખવામાં આવે, તો પછી વ્યક્તિ કંઈક વધુ સારી વર્તણૂકવાળી પ્રણાલી મેળવે છે જેને પ્રેડીકેટિવ પોલીમોર્ફિઝમ કહેવાય છે; જો પ્રોગ્રામ અને પ્રકાર વચ્ચેનો તફાવત અસ્પષ્ટ હોય, તો વ્યક્તિ ઉચ્ચ-ક્રમના તર્કનું પ્રકાર-સૈદ્ધાંતિક એનાલોગ મેળવે છે, જેને ઇમ્પ્રેડીકેટિવ પોલીમોર્ફિઝમ તરીકે પણ ઓળખવામાં આવે છે. સાહિત્યમાં નિર્ભરતા અને બહુરૂપતાના વિવિધ સંયોજનોને ધ્યાનમાં લેવામાં આવ્યા છે, જેમાં સૌથી પ્રસિદ્ધ હેન્ક બેરેન્ડ્રેગ્ટનું લેમ્બડા ક્યુબ છે. તર્ક અને પ્રકાર સિદ્ધાંતનું આંતરછેદ એક વિશાળ અને સક્રિય સંશોધન ક્ષેત્ર છે. નવા તર્કશાસ્ત્રને સામાન્ય રીતે સામાન્ય પ્રકારના સૈદ્ધાંતિક સેટિંગમાં ઔપચારિક બનાવવામાં આવે છે, જેને તાર્કિક માળખા તરીકે ઓળખવામાં આવે છે. બાંધકામની ગણતરી અને એલ. એફ. જેવા લોકપ્રિય આધુનિક તાર્કિક માળખા ઉચ્ચ-ક્રમ આધારિત પ્રકાર સિદ્ધાંત પર આધારિત છે, જેમાં નિર્ણાયકતા અને અભિવ્યક્તિની શક્તિની દ્રષ્ટિએ વિવિધ વિનિમય છે. આ તાર્કિક માળખાઓને હંમેશા કુદરતી કપાત પ્રણાલી તરીકે નિર્દિષ્ટ કરવામાં આવે છે, જે કુદરતી કપાત અભિગમની વૈવિધ્યતાનો પુરાવો છે. શાસ્ત્રીય અને મોડલ તર્કશાસ્ત્ર સરળતા માટે, અત્યાર સુધી રજૂ કરાયેલા તર્કશાસ્ત્ર અંતર્જ્ઞાનવાદી રહ્યા છે. શાસ્ત્રીય તર્ક વધારાના સ્વયંસિદ્ધ અથવા બાકાત મધ્યના સિદ્ધાંત સાથે અંતઃપ્રેરણાત્મક તર્કને વિસ્તરે છેઃ કોઈપણ દરખાસ્ત p માટે, દરખાસ્ત p·p સાચી છે. આ નિવેદન દેખીતી રીતે પરિચય અથવા નાબૂદી નથી; ખરેખર, તેમાં બે અલગ જોડાણો સામેલ છે. જેન્ટ્ઝેનની બાકાત મધ્યની મૂળ સારવાર નીચેની ત્રણ (સમકક્ષ) ફોર્મ્યુલેશનમાંથી એક સૂચવે છે, જે હિલ્બર્ટ અને હેયટિંગની પ્રણાલીઓમાં પહેલેથી જ સમાન સ્વરૂપોમાં હાજર હતાઃ (XM3 એ ફક્ત E ની દ્રષ્ટિએ વ્યક્ત કરાયેલ XM2 છે.) બાકાત મધ્યની આ સારવાર, શુદ્ધતાવાદીના દૃષ્ટિકોણથી વાંધાજનક હોવા ઉપરાંત, સામાન્ય સ્વરૂપોની વ્યાખ્યામાં વધારાની ગૂંચવણો રજૂ કરે છે. માત્ર પરિચય અને નાબૂદીના નિયમોની દ્રષ્ટિએ શાસ્ત્રીય કુદરતી કપાતની તુલનાત્મક રીતે વધુ સંતોષકારક સારવારની દરખાસ્ત સૌપ્રથમ 1992 માં પેરિગોટ દ્વારા λμ નામના શાસ્ત્રીય લેમ્બડા કલનનાં સ્વરૂપમાં કરવામાં આવી હતી. તેમના અભિગમની મુખ્ય સમજ એ હતી કે સત્ય-કેન્દ્રિત ચુકાદાને વધુ શાસ્ત્રીય કલ્પના સાથે બદલવો, જે ક્રમિક કલનની યાદ અપાવે છેઃ સ્થાનિક સ્વરૂપમાં, એ ને બદલે, તેમણે એ નો ઉપયોગ કર્યો હતો, જેમાં એ સમાન દરખાસ્તોનો સંગ્રહ હતો. એ ને સંયોજન તરીકે અને એ ને વિચ્છેદ તરીકે ગણવામાં આવતો હતો. આ માળખું અનિવાર્યપણે શાસ્ત્રીય ક્રમિક ગણતરીમાંથી સીધું ઉઠાવવામાં આવ્યું છે, પરંતુ λμ માં નવીનતા એ એલ. આઈ. એસ. પી. અને તેના વંશજોમાં જોવા મળતી કોલસી અથવા થ્રો/કેચ મિકેનિઝમની દ્રષ્ટિએ શાસ્ત્રીય કુદરતી કપાત સાબિતીઓને ગણતરીત્મક અર્થ આપવાનું હતું. (આ પણ જુઓઃ પ્રથમ વર્ગ નિયંત્રણ.) અન્ય મહત્વપૂર્ણ વિસ્તરણ મોડલ અને અન્ય તર્કશાસ્ત્ર માટે હતું જેને માત્ર સત્યના મૂળભૂત ચુકાદા કરતાં વધુ જરૂર છે. આનું સૌપ્રથમ 1965માં પ્રાવિટ્ઝ દ્વારા કુદરતી કપાત શૈલીમાં એલેથિક મોડલ લોજિક એસ4 અને એસ5 માટે વર્ણન કરવામાં આવ્યું હતું, અને ત્યારથી સંબંધિત કાર્યોનો મોટો જથ્થો એકત્રિત થયો છે. એક સરળ ઉદાહરણ આપવા માટે, મોડલ તર્ક S4 માટે એક નવા ચુકાદાની જરૂર છે, "A માન્ય", જે સત્યના સંદર્ભમાં સ્પષ્ટ છેઃ જો "A સાચું" સ્વરૂપ "B સાચું" ની કોઈ ધારણાઓ હેઠળ ન હોય, તો "A માન્ય". આ સ્પષ્ટ ચુકાદાને નીચેના પરિચય અને નાબૂદીના નિયમો સાથે એકીકૃત સંયોજક એ ("જરૂરી એ" વાંચો) તરીકે આંતરિક કરવામાં આવ્યો છેઃ નોંધ કરો કે આધાર "એ માન્ય" પાસે કોઈ વ્યાખ્યાયિત નિયમો નથી; તેના બદલે, માન્યતાની સ્પષ્ટ વ્યાખ્યાનો ઉપયોગ તેના સ્થાને થાય છે. જ્યારે પૂર્વધારણાઓ સ્પષ્ટ હોય ત્યારે આ સ્થિતિ સ્થાનિક સ્વરૂપમાં વધુ સ્પષ્ટ બને છે. આપણે "ω; એ સાચું" લખીએ છીએ જ્યાં ω પહેલાની જેમ સાચી પૂર્વધારણાઓ ધરાવે છે, અને ω માન્ય પૂર્વધારણાઓ ધરાવે છે. જમણી બાજુએ માત્ર એક જ ચુકાદો છે "A સાચો"; અહીં માન્યતાની જરૂર નથી કારણ કે "ω A માન્ય" વ્યાખ્યા દ્વારા "ω; ω A સાચો" સમાન છે. પરિચય અને નાબૂદી સ્વરૂપો પછી છેઃ મોડલ પૂર્વધારણાઓ પૂર્વધારણા નિયમ અને અવેજી પ્રમેયની તેમની પોતાની આવૃત્તિ ધરાવે છે. મોડલ અવેજી પ્રમેય જો ω; ω: A સાચું અને ω, u: (A માન્ય); ω: C સાચું, તો પછી ω; ω [π1/u] π2: C સાચું. પૂર્વધારણાઓના અલગ સંગ્રહોમાં ચુકાદાઓને અલગ પાડવાનું આ માળખું, જેને બહુ-ઝોન અથવા બહુપરીમાણીય સંદર્ભો તરીકે પણ ઓળખવામાં આવે છે, તે ખૂબ જ શક્તિશાળી અને વિસ્તૃત છે; તે ઘણા વિવિધ મોડલ તર્કશાસ્ત્ર માટે, અને રેખીય અને અન્ય સબસ્ટ્રક્ચરલ તર્કશાસ્ત્ર માટે પણ લાગુ કરવામાં આવ્યું છે, કેટલાક ઉદાહરણો આપવા માટે. જો કે, મોડલ તર્કની પ્રમાણમાં ઓછી પ્રણાલીઓને કુદરતી કપાતમાં સીધી ઔપચારિક બનાવી શકાય છે. આ પ્રણાલીઓના પુરાવા-સૈદ્ધાંતિક લાક્ષણિકતાઓ આપવા માટે, લેબલિંગ અથવા ઊંડા અનુમાનની પ્રણાલીઓ જેવા વિસ્તરણ. સૂત્રોમાં લેબલનો ઉમેરો નિયમો લાગુ પડે છે તે શરતોને વધુ સારી રીતે નિયંત્રિત કરવાની મંજૂરી આપે છે, વિશ્લેષણાત્મક ઝાંખીની વધુ લવચીક તકનીકોને લાગુ કરવાની મંજૂરી આપે છે, જેમ કે લેબલ કપાતના કિસ્સામાં કરવામાં આવ્યું છે. લેબલ્સ ક્રિપ્કે સિમેન્ટિક્સમાં વિશ્વોના નામકરણને પણ મંજૂરી આપે છે; ક્રિપ્કે સિમેન્ટિક્સમાં મોડલ લોજિક્સની ફ્રેમ શરતોને વર્ણસંકર તર્કના કુદરતી કપાત ઔપચારિકરણમાં અનુમાન નિયમોમાં રૂપાંતરિત કરવા માટે એક પ્રભાવશાળી તકનીક રજૂ કરે છે. ઘણા પુરાવા સિદ્ધાંતોના ઉપયોગનું સર્વેક્ષણ કરે છે, જેમ કે એવરોન અને પોટિંગરના હાઇપરસીક્વેન્ટ્સ અને S5 અને B જેવા મોડલ તર્કશાસ્ત્ર માટે બેલનેપના ડિસ્પ્લે લોજિક. અન્ય પાયાના અભિગમો સાથે સરખામણી ક્રમિક કલન ક્રમિક કલન એ ગાણિતિક તર્કના પાયા તરીકે કુદરતી કપાતનો મુખ્ય વિકલ્પ છે. નેચરલ ડિડક્શનમાં માહિતીનો પ્રવાહ દ્વિ-દિશાત્મક હોય છેઃ નાબૂદીના નિયમો માહિતીને ડીકન્સ્ટ્રક્શન દ્વારા નીચે તરફ વહે છે, અને પરિચયના નિયમો માહિતીને એસેમ્બલી દ્વારા ઉપર તરફ વહે છે. આમ, નેચરલ ડિડક્શન પ્રૂફમાં સંપૂર્ણપણે બોટમ-અપ અથવા ટોપ-ડાઉન રીડિંગ હોતું નથી, જે તેને પ્રૂફ સર્ચમાં ઓટોમેશન માટે અયોગ્ય બનાવે છે. આ હકીકતને સંબોધવા માટે, 1935માં જેન્ટ્ઝેને તેમના ક્રમિક કલનનો પ્રસ્તાવ મૂક્યો હતો, જોકે શરૂઆતમાં તેમણે તેને વિધેયાત્મક તર્કની સુસંગતતાને સ્પષ્ટ કરવા માટે એક તકનીકી ઉપકરણ તરીકે ઈરાદો રાખ્યો હતો. ક્લિને, તેમના 1952 ના પુસ્તક ઇન્ટ્રોડક્શન ટુ મેટામાથેમેટિક્સમાં, આધુનિક શૈલીમાં ક્રમિક કલનની પ્રથમ રચના આપી હતી. ક્રમિક કલનમાં તમામ અનુમાન નિયમોમાં સંપૂર્ણ રીતે તળિયેથી ઉપરનું વાંચન હોય છે. અનુમાનના નિયમો ટર્નસ્ટાઇલની બંને બાજુના ઘટકો પર લાગુ થઈ શકે છે. (કુદરતી કપાતથી અલગ પાડવા માટે, આ લેખ અનુક્રમે યોગ્ય ટેકને બદલે ડબલ તીરનો ઉપયોગ કરે છે.) કુદરતી કપાતના પરિચય નિયમોને ક્રમિક કલનમાં યોગ્ય નિયમો તરીકે જોવામાં આવે છે, અને માળખાકીય રીતે ખૂબ સમાન છે. બીજી બાજુ નાબૂદીના નિયમો ક્રમિક કલનમાં ડાબા નિયમોમાં ફેરવાય છે. એક ઉદાહરણ આપવા માટે, વિચ્છેદનને ધ્યાનમાં લો; જમણા નિયમો પરિચિત છેઃ ડાબી બાજુએઃ સ્થાનિક સ્વરૂપમાં કુદરતી કપાતના ષ્ણ E નિયમને યાદ કરો. પ્રસ્તાવ A ષ્ણ B, જે ષ્ણ E માં આધારનો અનુગામી છે, તે ડાબા નિયમ ષ્ણ L માં નિષ્કર્ષની પૂર્વધારણામાં ફેરવાય છે. આમ, ડાબેરી નિયમોને એક પ્રકારના ઊંધી નાબૂદીના નિયમ તરીકે જોઈ શકાય છે. આ અવલોકનને નીચે પ્રમાણે સચિત્ર કરી શકાય છેઃ ક્રમિક કલનમાં, ડાબી અને જમણી બાજુના નિયમો લૉક-સ્ટેપમાં કરવામાં આવે છે જ્યાં સુધી કોઈ પ્રારંભિક ક્રમ સુધી પહોંચતું નથી, જે કુદરતી કપાતમાં નાબૂદી અને પરિચયના નિયમોના મિલન બિંદુને અનુરૂપ છે. આ પ્રારંભિક નિયમો ઉપરછલ્લી રીતે નેચરલ ડિડક્શનના પૂર્વધારણાના નિયમ જેવા જ છે, પરંતુ સિક્વેન્ટ કેલ્ક્યુલસમાં તેઓ ડાબી અને જમણી દરખાસ્તના સ્થાનાંતરણ અથવા હાથ મિલાવવાનું વર્ણન કરે છેઃ સિક્વેન્ટ કેલ્ક્યુલસ અને નેચરલ ડિડક્શન વચ્ચેનો પત્રવ્યવહાર એ ધ્વનિ અને સંપૂર્ણતા પ્રમેયોની જોડી છે, જે બંને પ્રેરક દલીલ દ્વારા સાબિત કરી શકાય છે. એ. આર. ટી. ની ધ્વનિ. જો એ. એ. હોય, તો એ. એ. ની સંપૂર્ણતા. જો એ, તો એ. આ પ્રમેયો દ્વારા તે સ્પષ્ટ છે કે ક્રમિક કલન સત્યની કલ્પનાને બદલતું નથી, કારણ કે દરખાસ્તોનો સમાન સંગ્રહ સાચો રહે છે. આમ, ક્રમિક કલન વ્યુત્પત્તિઓમાં પહેલાંની જેમ જ સાબિતી પદાર્થોનો ઉપયોગ કરી શકાય છે. ઉદાહરણ તરીકે, સંયોજનોનો વિચાર કરો. જમણો નિયમ પરિચય નિયમ સાથે લગભગ સમાન છે ડાબો નિયમ, જો કે, કેટલાક વધારાના અવેજી કરે છે જે અનુરૂપ નાબૂદી નિયમોમાં કરવામાં આવતા નથી. તેથી ક્રમિક કલનમાં પેદા થતા પુરાવાઓના પ્રકારો કુદરતી કપાત કરતા અલગ છે. ક્રમિક કલન β-સામાન્ય η-લાંબા સ્વરૂપ તરીકે ઓળખાતા પુરાવા ઉત્પન્ન કરે છે, જે કુદરતી કપાત પુરાવાના સામાન્ય સ્વરૂપની પ્રમાણભૂત રજૂઆતને અનુરૂપ છે. જો કોઈ કુદરતી કપાતનો ઉપયોગ કરીને આ પુરાવાઓનું વર્ણન કરવાનો પ્રયાસ કરે છે, તો તે ઇન્ટરકલેશન કેલ્ક્યુલસ (પ્રથમ જ્હોન બાયર્ન્સ દ્વારા વર્ણવેલ) તરીકે ઓળખાય છે, જેનો ઉપયોગ કુદરતી કપાત માટે સામાન્ય સ્વરૂપની કલ્પનાને ઔપચારિક રીતે વ્યાખ્યાયિત કરવા માટે થઈ શકે છે. નેચરલ ડિડક્શનનો અવેજી પ્રમેય માળખાકીય નિયમ અથવા માળખાકીય પ્રમેયનું સ્વરૂપ લે છે જે ક્રમિક કલનમાં કટ તરીકે ઓળખાય છે. કટ (અવેજી) જો એ. પી. 1: એ અને એ. પી. 2: સી, તો એ. પી. 2: સી. મોટા ભાગના સારી રીતે વર્તવામાં આવેલા તર્કશાસ્ત્રમાં, કટ એ અનુમાન નિયમ તરીકે બિનજરૂરી છે, જો કે તે મેટા-પ્રમેય તરીકે સાબિત થાય છે; કટ નિયમની અનાવશ્યકતાને સામાન્ય રીતે ગણતરીની પ્રક્રિયા તરીકે રજૂ કરવામાં આવે છે, જેને કટ નાબૂદી તરીકે ઓળખવામાં આવે છે. કુદરતી કપાત માટે આનો એક રસપ્રદ ઉપયોગ છે; સામાન્ય રીતે અમર્યાદિત સંખ્યામાં કેસોને કારણે કુદરતી કપાતમાં સીધા ચોક્કસ ગુણધર્મો સાબિત કરવા અત્યંત કંટાળાજનક હોય છે. ઉદાહરણ તરીકે, દર્શાવવાનો વિચાર કરો કે આપેલ દરખાસ્ત કુદરતી કપાતમાં સાબિત કરી શકાતી નથી. એક સરળ પ્રેરક દલીલ નિષ્ફળ જાય છે કારણ કે ઇ અથવા ઇ જેવા નિયમો જે મનસ્વી દરખાસ્તો રજૂ કરી શકે છે. જો કે, આપણે જાણીએ છીએ કે ક્રમિક કલન કુદરતી કપાતના સંદર્ભમાં પૂર્ણ છે, તેથી તે ક્રમિક કલનમાં આ અસમર્થતા બતાવવા માટે પૂરતું છે. હવે, જો કટ અનુમાન નિયમ તરીકે ઉપલબ્ધ ન હોય, તો પછી તમામ ક્રમિક નિયમો કાં તો જમણી કે ડાબી બાજુએ સંયોજક રજૂ કરે છે, તેથી ક્રમિક વ્યુત્પત્તિની ઊંડાઈ અંતિમ નિષ્કર્ષમાં સંયોજક દ્વારા સંપૂર્ણપણે બંધાયેલી હોય છે. આમ, અપ્રમાણિકતા દર્શાવવી ખૂબ સરળ છે, કારણ કે ધ્યાનમાં લેવા માટે માત્ર મર્યાદિત સંખ્યામાં કિસ્સાઓ છે, અને દરેક કેસ સંપૂર્ણપણે નિષ્કર્ષની પેટા-દરખાસ્તોથી બનેલો છે. આનું એક સરળ ઉદાહરણ વૈશ્વિક સુસંગતતા પ્રમેય છેઃ "સત્ય" સાબિત કરી શકાય તેવું નથી. ક્રમિક કલન સંસ્કરણમાં, આ સ્પષ્ટ રીતે સાચું છે કારણ કે એવો કોઈ નિયમ નથી કે જેમાં નિષ્કર્ષ તરીકે "ષ્ણૂ" હોઈ શકે! પુરાવા સિદ્ધાંતવાદીઓ ઘણીવાર આવા ગુણધર્મોને કારણે કટ-ફ્રી ક્રમિક કલન ફોર્મ્યુલેશન પર કામ કરવાનું પસંદ કરે છે. નોંધો સંદર્ભો (એમ. ઇ. સ્ઝાબોમાં તાર્કિક કપાતમાં તપાસ) પણ જુઓ. ધ કલેક્ટેડ વર્ક્સ ઓફ ગેરહાર્ડ જેન્ટ્ઝન. નોર્થ-હોલેન્ડ પબ્લિશિંગ કંપની, 1969.) પોલ ટેલર અને યવેસ લાફોન્ટ દ્વારા ભાષાંતર અને પરિશિષ્ટો સાથે. પોલિશ તર્ક 1920-39 માં પુનઃમુદ્રિત, આવૃત્તિ. સ્ટોર્સ મેકકોલ. યુનિવર્સિટી ડિગલી સ્ટડી ડી સિએના, એપ્રિલ 1983 ખાતે ટૂંકા અભ્યાસક્રમ માટે વ્યાખ્યાન નોંધે છે. પીએચડી થીસિસ. એમ. એસ. સી. થીસીસ. બાહ્ય કડીઓ લેબોરિયો, ડેનિયલ ક્લેમેન્ટ, "કુદરતી કપાતનો પરિચય". એસિડ પર ડોમિનો. કુદરતી કપાતને ડોમિનોજની રમત તરીકે જોવામાં આવે છે. પેલેટિયર, જેફ, "એ હિસ્ટ્રી ઓફ નેચરલ ડિડક્શન એન્ડ એલિમેન્ટરી લોજિક ટેક્સ્ટબુક્સ". લેવી, મિશેલ, એ પ્રપોઝિશનલ પ્રોવર. લોજિકલ કેલ્ક્યુલી ડિડક્ટિવ રિઝનિંગ પ્રૂફ થિયરી પ્રૂફની પદ્ધતિઓ