Existential theory of the reals
ગાણિતિક તર્કશાસ્ત્ર, કોમ્પ્યુટેશનલ કોમ્પ્લેક્સિટી થિયરી અને કોમ્પ્યુટર વિજ્ઞાનમાં, વાસ્તવિક અસ્તિત્વનો સિદ્ધાંત એ સ્વરૂપના તમામ સાચા વાક્યોનો સમૂહ છે જ્યાં ચલોનું અર્થઘટન વાસ્તવિક સંખ્યાના મૂલ્યો તરીકે કરવામાં આવે છે, અને જ્યાં વાસ્તવિક બહુપદીઓની સમાનતા અને અસમાનતાને સમાવતું પરિમાણ-મુક્ત સૂત્ર છે. આ સ્વરૂપનું વાક્ય સાચું છે જો તે તમામ ચલ માટે મૂલ્યો શોધવાનું શક્ય હોય, જે જ્યારે સૂત્રમાં બદલવામાં આવે છે, ત્યારે તે સાચું બને છે. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે નિર્ણયની સમસ્યા એ એક અલ્ગોરિધમ શોધવાની સમસ્યા છે જે નક્કી કરે છે કે, આવા દરેક વાક્ય માટે, તે સાચું છે કે ખોટું. તેવી જ રીતે, આપેલ અર્ધ-બીજગણિત સમૂહ ખાલી નથી કે કેમ તે ચકાસવાની સમસ્યા છે. આ નિર્ણયની સમસ્યા એન. પી.-હાર્ડ છે અને તે પી. એસ. પી. એ. સી. ઈ. માં છે, જે તેને અસ્તિત્વના પરિમાણકોના પ્રતિબંધ વિના વાસ્તવિકતાના પ્રથમ ક્રમના સિદ્ધાંતમાં નિવેદનો નક્કી કરવા માટે આલ્ફ્રેડ ટાર્સ્કીની ક્વોન્ટિફાયર નાબૂદી પ્રક્રિયા કરતાં નોંધપાત્ર રીતે ઓછી જટિલતા આપે છે. જો કે, વ્યવહારમાં, પ્રથમ ક્રમના સિદ્ધાંત માટેની સામાન્ય પદ્ધતિઓ આ સમસ્યાઓને ઉકેલવા માટે પસંદગીની પસંદગી છે. જટિલતા વર્ગને કોમ્પ્યુટેશનલ સમસ્યાઓના વર્ગનું વર્ણન કરવા માટે વ્યાખ્યાયિત કરવામાં આવ્યો છે જેને આ સ્વરૂપના સમકક્ષ વાક્યોમાં અનુવાદિત કરી શકાય છે. માળખાકીય જટિલતા સિદ્ધાંતમાં, તે એન. પી. અને પી. એસ. પી. એ. સી. ઈ. વચ્ચે આવેલું છે. ભૌમિતિક આલેખ સિદ્ધાંતમાં ઘણી કુદરતી સમસ્યાઓ, ખાસ કરીને ભૌમિતિક આંતરછેદ આલેખને ઓળખવાની અને રેખાંકનોની ધારને ક્રોસિંગ સાથે સીધી કરવાની સમસ્યાઓ, આ વર્ગ સાથે સંબંધિત છે અને તે આ વર્ગ માટે સંપૂર્ણ છે. અહીં, સંપૂર્ણતાનો અર્થ એ છે કે વિપરીત દિશામાં અનુવાદ અસ્તિત્વમાં છે, વાસ્તવિક પર મનસ્વી વાક્યમાંથી આપેલ સમસ્યાના સમકક્ષ ઉદાહરણમાં. ગાણિતિક તર્કશાસ્ત્રમાં, સિદ્ધાંત એ એક ઔપચારિક ભાષા છે જેમાં પ્રતીકોના નિશ્ચિત સમૂહનો ઉપયોગ કરીને લખાયેલા વાક્યોના સમૂહનો સમાવેશ થાય છે. વાસ્તવિક બંધ ક્ષેત્રોના પ્રથમ ક્રમના સિદ્ધાંતમાં નીચેના પ્રતીકો છેઃ અચળાંક 0 અને 1, ચલોનો ગણતરીપાત્ર સંગ્રહ, સરવાળો, બાદબાકી, ગુણાકાર, અને (વૈકલ્પિક રીતે) વિભાજન કામગીરીઓ, પ્રતીકો <, ≤, =, ±,>, અને વાસ્તવિક મૂલ્યોની સરખામણી માટે  ઒ત્ત, તાર્કિક સંયોજક, ′, ′, અને ′, કૌંસ, અને સાર્વત્રિક પરિમાણક β અને અસ્તિત્વના પરિમાણક ′ આ પ્રતીકોનો ક્રમ એક વાક્ય બનાવે છે જે વાસ્તવિકના પ્રથમ ક્રમના સિદ્ધાંત સાથે સંબંધિત છે જો તે વ્યાકરણની રીતે સારી રીતે રચાયેલ હોય, તો તેના તમામ ચલોનું યોગ્ય રીતે પ્રમાણ કરવામાં આવે છે, અને (જ્યારે વાસ્તવિક સંખ્યાઓ વિશે ગાણિતિક નિવેદન તરીકે અર્થઘટન કરવામાં આવે છે) તારસ્કીએ બતાવ્યું તેમ, આ સિદ્ધાંતને સ્વયંસિદ્ધ યોજના અને નિર્ણય પ્રક્રિયા દ્વારા વર્ણવી શકાય છે જે સંપૂર્ણ અને અસરકારક છેઃ દરેક સંપૂર્ણ માત્રાત્મક અને વ્યાકરણના વાક્ય માટે, કાં તો વાક્ય અથવા તેની નકારાત્મકતા (પરંતુ બંને નહીં) સ્વયંસિદ્ધમાંથી મેળવી શકાય છે. આ જ સિદ્ધાંત દરેક વાસ્તવિક બંધ ક્ષેત્રનું વર્ણન કરે છે, માત્ર વાસ્તવિક સંખ્યાઓનું નહીં. જો કે, અન્ય સંખ્યા પ્રણાલીઓ છે જે આ સ્વયંસિદ્ધ દ્વારા સચોટ રીતે વર્ણવવામાં આવી નથી; ખાસ કરીને, વાસ્તવિક સંખ્યાઓને બદલે પૂર્ણાંકો માટે સમાન રીતે વ્યાખ્યાયિત સિદ્ધાંત અનિશ્ચિત છે, માટિયેસેવિચના પ્રમેય દ્વારા અસ્તિત્વના વાક્યો (ડાયોફેન્ટાઇન સમીકરણો) માટે પણ. વાસ્તવિકતાનો અસ્તિત્વ સિદ્ધાંત એ પ્રથમ ક્રમના સિદ્ધાંતનો એક ભાગ છે જેમાં વાક્યો હોય છે જેમાં તમામ પરિમાણો અસ્તિત્વમાં હોય છે અને તેઓ અન્ય કોઈપણ પ્રતીકો પહેલાં દેખાય છે. એટલે કે, તે સ્વરૂપના તમામ સાચા વાક્યોનો સમૂહ છે જ્યાં વાસ્તવિક બહુપદીઓની સમાનતાઓ અને અસમાનતાઓને સમાવતું પરિમાણ-મુક્ત સૂત્ર છે. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે નિર્ણયની સમસ્યા એ પરીક્ષણની અલ્ગોરિધમિક સમસ્યા છે કે આપેલ વાક્ય આ સિદ્ધાંત સાથે સંબંધિત છે કે કેમ; સમાનરૂપે, જે શબ્દમાળાઓ મૂળભૂત વાક્યરચના તપાસને પસાર કરે છે (તેઓ સાચા વાક્યરચના સાથે સાચા પ્રતીકોનો ઉપયોગ કરે છે, અને તેમાં કોઈ બિન-પ્રમાણભૂત ચલ નથી) તે પરીક્ષણની સમસ્યા છે કે શું વાક્ય વાસ્તવિક સંખ્યાઓ વિશે સાચું નિવેદન છે કે કેમ. વાસ્તવિક સંખ્યાઓના-ટુપલ્સના સમૂહ કે જેના માટે સાચું છે તેને અર્ધ-બીજગણિત સમૂહ કહેવામાં આવે છે, તેથી વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટેના નિર્ણયની સમસ્યાને સમાન રીતે પરીક્ષણ તરીકે પુનરાવર્તિત કરી શકાય છે કે શું આપેલ અર્ધ-બીજગણિત સમૂહ બિન-ખાલી છે. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે નિર્ણયની સમસ્યા માટે અલ્ગોરિધમ્સની સમય જટિલતા નક્કી કરવા માટે, ઇનપુટના કદનું માપ હોવું મહત્વપૂર્ણ છે. આ પ્રકારનું સૌથી સરળ માપ વાક્યની લંબાઈ છેઃ એટલે કે તેમાં સમાવિષ્ટ પ્રતીકોની સંખ્યા. જો કે, આ સમસ્યા માટે અલ્ગોરિધમ્સના વર્તનનું વધુ ચોક્કસ વિશ્લેષણ હાંસલ કરવા માટે, ઇનપુટ કદને સંખ્યાબંધ ચલની સંખ્યા, વાક્યની અંદર બહુપદીઓની સંખ્યા અને આ બહુપદીઓની માત્રાને અલગ કરીને અનેક ચલમાં વિભાજિત કરવું અનુકૂળ છે. ઉદાહરણો સુવર્ણ ગુણોત્તરને બહુપદીના મૂળ તરીકે વ્યાખ્યાયિત કરી શકાય છે. આ બહુપદીના બે મૂળ છે, જેમાંથી માત્ર એક (સુવર્ણ ગુણોત્તર) એક કરતા વધારે છે. આમ, સુવર્ણ ગુણોત્તરનું અસ્તિત્વ વાક્ય દ્વારા વ્યક્ત કરી શકાય છે કારણ કે સુવર્ણ ગુણોત્તર દિવ્ય નથી, આ એક સાચું વાક્ય છે, અને વાસ્તવિક અસ્તિત્વના સિદ્ધાંત સાથે સંબંધિત છે. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે નિર્ણયની સમસ્યાનો જવાબ, આ વાક્યને ઇનપુટ તરીકે આપવામાં આવે છે, તે બુલિયન મૂલ્ય સાચું છે. અંકગણિત અને ભૌમિતિક અર્થની અસમાનતા જણાવે છે કે, દરેક બે બિન-નકારાત્મક સંખ્યાઓ માટે અને નીચેની અસમાનતા ધરાવે છેઃ ઉપર જણાવ્યા મુજબ, તે વાસ્તવિક સંખ્યાઓ વિશે પ્રથમ ક્રમનું વાક્ય છે, પરંતુ અસ્તિત્વના પરિમાણકોને બદલે સાર્વત્રિક છે, અને જે વિભાજન, વર્ગમૂળ અને સંખ્યા 2 માટે વધારાના પ્રતીકોનો ઉપયોગ કરે છે જેને વાસ્તવિકના પ્રથમ ક્રમના સિદ્ધાંતમાં મંજૂરી નથી. જો કે, બંને પક્ષોનો વર્ગ કરીને તેને નીચેના અસ્તિત્વના નિવેદનમાં રૂપાંતરિત કરી શકાય છે જેનું અર્થઘટન કરી શકાય છે કે શું અસમાનતામાં કોઈ પ્રતિકૂળ ઉદાહરણો છે કે કેમઃ વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે નિર્ણય સમસ્યાનો જવાબ, આ વાક્યને ઇનપુટ તરીકે આપવામાં આવે તો, બુલિયન મૂલ્ય ખોટું છેઃ ત્યાં કોઈ પ્રતિકૂળ ઉદાહરણો નથી. તેથી, આ વાક્ય સાચું વ્યાકરણ સ્વરૂપ હોવા છતાં, વાસ્તવિક અસ્તિત્વના સિદ્ધાંત સાથે સંબંધિત નથી. અલ્ગોરિધમ્સ આલ્ફ્રેડ ટાર્સ્કીની ક્વોન્ટિફાયર નાબૂદીની પદ્ધતિ (1948) એ વાસ્તવિક (અને વધુ સામાન્ય રીતે વાસ્તવિકનો પ્રથમ ક્રમ સિદ્ધાંત) ના અસ્તિત્વના સિદ્ધાંતને એલ્ગોરિધમિક રીતે ઉકેલવા યોગ્ય હોવાનું દર્શાવ્યું હતું, પરંતુ તેની જટિલતા પર પ્રાથમિક બંધન વિના. જ્યોર્જ ઇ. કોલિન્સ (1975) દ્વારા નળાકાર બીજગણિત વિઘટનની પદ્ધતિએ સમયની અવલંબનને બમણી ઘાતાંકીયમાં સુધારી છે, જે વાક્યમાં ગુણાંકને રજૂ કરવા માટે જરૂરી બિટ્સની સંખ્યા છે જેનું મૂલ્ય નક્કી કરવાનું છે, તે વાક્યમાં બહુપદીઓની સંખ્યા છે, તેમની કુલ ડિગ્રી છે, અને ચલની સંખ્યા છે. 1988 સુધીમાં, દિમા ગ્રિગોરીવ અને નિકોલાઈ વોરોબજોવે બહુપદીમાં જટિલતા ઘાતાંકીય હોવાનું દર્શાવ્યું હતું, અને 1992 માં પ્રકાશિત થયેલા કાગળોની શ્રેણીમાં જેમ્સ રેનેગરે આને એકલ ઘાતાંકીય અવલંબનમાં સુધારો કર્યો હતો. આ દરમિયાન, 1988 માં, જ્હોન કેનીએ અન્ય એક અલ્ગોરિધમનું વર્ણન કર્યું હતું જે પણ ઘાતાંકીય સમય નિર્ભરતા ધરાવે છે, પરંતુ માત્ર બહુપદી અવકાશ જટિલતા છે; એટલે કે, તેમણે દર્શાવ્યું હતું કે સમસ્યાને PSPACE માં ઉકેલી શકાય છે. આ અલ્ગોરિધમ્સની એસિમ્પ્ટોટિક કોમ્પ્યુટેશનલ જટિલતા ભ્રામક હોઈ શકે છે, કારણ કે વ્યવહારમાં તેઓ માત્ર ખૂબ જ નાના કદના ઇનપુટ્સ પર ચલાવી શકાય છે. 1991ની સરખામણીમાં, હૂન હોંગે અંદાજ મૂક્યો હતો કે કોલિન્સની બમણી ઘાતાંકીય પ્રક્રિયા એવી સમસ્યાનું સમાધાન કરવામાં સક્ષમ હશે જેનું કદ ઉપરોક્ત તમામ પરિમાણોને 2 પર સેટ કરીને એક સેકન્ડથી ઓછા સમયમાં વર્ણવવામાં આવ્યું છે, જ્યારે ગ્રિગોરીવ, વોર્બજોવ અને રેનેગરના અલ્ગોરિધમ્સ તેના બદલે દસ લાખ વર્ષ કરતાં વધુ સમય લેશે. 1993માં, જોસ, રોય અને સોલેર્નોએ સૂચવ્યું હતું કે ઘાતાંકીય-સમયની પ્રક્રિયાઓમાં નાના ફેરફારો કરવા શક્ય હોવા જોઈએ જેથી તેમને વ્યવહારમાં નળાકાર બીજગણિત નિર્ણય કરતાં ઝડપી તેમજ સિદ્ધાંતમાં ઝડપી બનાવી શકાય. જો કે, 2009 સુધીમાં, તે હજુ પણ એવું હતું કે વાસ્તવિકતાના પ્રથમ ક્રમના સિદ્ધાંત માટેની સામાન્ય પદ્ધતિઓ વાસ્તવિકના અસ્તિત્વના સિદ્ધાંત માટે વિશિષ્ટ એકલા ઘાતાંકીય અલ્ગોરિધમ્સ કરતાં વ્યવહારમાં શ્રેષ્ઠ રહી હતી. કમ્પ્યુટેશનલ જટિલતા અને ભૌમિતિક આલેખ સિદ્ધાંતમાં કેટલીક સમસ્યાઓને વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે સંપૂર્ણ તરીકે વર્ગીકૃત કરી શકાય છે. એટલે કે, વાસ્તવિક અસ્તિત્વના સિદ્ધાંતમાં દરેક સમસ્યામાં આ સમસ્યાઓમાંના એક ઉદાહરણમાં બહુપદી-સમયનો અનેક-એક ઘટાડો હોય છે, અને બદલામાં આ સમસ્યાઓ વાસ્તવિક અસ્તિત્વના સિદ્ધાંતમાં ઘટાડી શકાય છે. આ પ્રકારની સંખ્યાબંધ સમસ્યાઓ ચોક્કસ પ્રકારના આંતરછેદના આલેખની ઓળખ સાથે સંબંધિત છે. આ સમસ્યાઓમાં, ઇનપુટ એક દિશાહીન આલેખ છે; ધ્યેય એ નક્કી કરવાનો છે કે શું આકારોના ચોક્કસ વર્ગમાંથી ભૌમિતિક આકારોને આલેખના શિરોબિંદુઓ સાથે એવી રીતે જોડી શકાય કે બે શિરોબિંદુઓ આલેખમાં અડીને હોય જો અને માત્ર ત્યારે જ જો તેમની સાથે સંકળાયેલ આકારોમાં ખાલી આંતરછેદ ન હોય. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે પૂર્ણ થયેલી આ પ્રકારની સમસ્યાઓમાં સમતલમાં રેખા ખંડોના આંતરછેદના આલેખની ઓળખ, એકમ ડિસ્ક આલેખની ઓળખ અને સમતલમાં બહિર્મુખ સમૂહોના આંતરછેદના આલેખની ઓળખનો સમાવેશ થાય છે. ક્રોસિંગ વિના પ્લેનમાં દોરેલા આલેખ માટે, ફેરીનો પ્રમેય જણાવે છે કે ગ્રાફની ધાર સીધી રેખાના સેગમેન્ટ્સ તરીકે અથવા મનસ્વી વળાંક તરીકે દોરવામાં આવે છે કે કેમ તે ધ્યાનમાં લીધા વિના પ્લાનર ગ્રાફનો સમાન વર્ગ મળે છે. પરંતુ આ સમાનતા અન્ય પ્રકારના રેખાંકનો માટે સાચી નથી. દાખલા તરીકે, ગ્રાફની ક્રોસિંગ સંખ્યા (મનસ્વી રીતે વક્ર ધારવાળા રેખાંકનમાં ક્રોસિંગની લઘુતમ સંખ્યા) એન. પી. માં નક્કી થઈ શકે છે, તેમ છતાં વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે તે નક્કી કરવું પૂર્ણ છે કે શું લંબચોરસ ક્રોસિંગ નંબર (સમતલમાં સીધી રેખાના ભાગો તરીકે દોરેલી ધાર સાથે કોઈપણ રેખાંકનમાં પાર થતી ધારની જોડીઓની લઘુતમ સંખ્યા) પર આપેલ બંધન પ્રાપ્ત કરતું ચિત્ર અસ્તિત્વમાં છે કે કેમ. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટે એ ચકાસવું પણ પૂર્ણ છે કે શું આપેલ આલેખ સમતલમાં સીધી રેખાના કિનારીઓ સાથે અને તેના ક્રોસિંગ તરીકે ધાર જોડીના આપેલ સમૂહ સાથે દોરી શકાય છે, અથવા સમકક્ષ રીતે, ક્રોસિંગ સાથે વક્ર રેખાંકનને સીધી કરી શકાય છે કે કેમ. વાસ્તવિક અસ્તિત્વના સિદ્ધાંત માટેની અન્ય સંપૂર્ણ સમસ્યાઓમાં નીચેનાનો સમાવેશ થાય છેઃ બિંદુઓની સૌથી નાની સંખ્યા શોધવાની આર્ટ ગેલેરી સમસ્યા કે જેમાંથી આપેલ બહુકોણના તમામ બિંદુઓ દેખાય છે. ન્યુરલ નેટવર્ક્સને તાલીમ આપવી. બહુકોણનો આપેલ સમૂહ આપેલ ચોરસ કન્ટેનરમાં ફિટ થઈ શકે છે કે કેમ તે નક્કી કરવાની પેકિંગ સમસ્યા. એકમ અંતર આલેખની ઓળખ, અને આલેખનું પરિમાણ અથવા યુક્લિડિયન પરિમાણ મહત્તમ આપેલ મૂલ્ય છે કે કેમ તે ચકાસવું. સ્યુડોલિન્સની ખેંચાણક્ષમતા (એટલે કે, સમતલમાં વળાંકના કુટુંબને આપવામાં આવે છે, તે નક્કી કરે છે કે તેઓ રેખા ગોઠવણી માટે હોમોમોર્ફિક છે કે કેમ); કોઈપણ નિશ્ચિત પરિમાણ> 2 માં ભૌમિતિક ક્વોન્ટમ તર્કની નબળી અને મજબૂત સંતોષકારકતા બંને; અસંદિગ્ધ ઓટોમેટાના સંદર્ભમાં મોડલ ચેકિંગ અંતરાલ માર્કોવ સાંકળો. એલ્ગોરિધમિક સ્ટેનિટ્ઝ સમસ્યા (જાળીને આપવામાં આવે તો, તે બહિર્મુખ પોલીટોપનો ચહેરો જાળી છે કે કેમ તે નક્કી કરે છે), જ્યારે તે 4-પરિમાણીય પોલીટોપ સુધી મર્યાદિત હોય ત્યારે પણ; ચોક્કસ બહિર્મુખ પદાર્થોની ગોઠવણીની અનુભૂતિ જગ્યાઓ ત્રિ-પરિમાણીય યુક્લિડિયન જગ્યામાં ત્રિકોણ અને ચતુર્ભુજોના આપેલા અમૂર્ત સંકુલને એમ્બેડ કરતી મલ્ટિપ્લેયર રમતોના નેશ ઇક્વિલિબ્રિયાના વિવિધ ગુણધર્મો; સમતલમાં વહેંચાયેલ શિરોબિંદુ પર બહુવિધ આલેખ એમ્બેડ કરવા જેથી તમામ આલેખ ક્રોસિંગ વિના દોરવામાં આવે; પ્લેનર પોઇન્ટ સેટના દૃશ્યતા ગ્રાફને ઓળખવા; (પ્રોજેક્ટિવ અથવા બિન-તુચ્છ સંબંધ) ક્રોસ પ્રોડક્ટ પર બે શબ્દો વચ્ચેના સમીકરણની સંતોષતા; લઘુત્તમ ઢોળાવ સંખ્યા નક્કી કરવી. નીચા ક્રમની મેટ્રિક્સ પૂર્ણતાની સમસ્યા. આના આધારે, જટિલતા વર્ગને વાસ્તવિક અસ્તિત્વના સિદ્ધાંતમાં બહુપદી-સમયના ઘણા-એક ઘટાડા ધરાવતી સમસ્યાઓના સમૂહ તરીકે વ્યાખ્યાયિત કરવામાં આવ્યો છે. હિલ્બર્ટની દસમી સમસ્યા પણ જુઓ, પૂર્ણાંકોના (અનિશ્ચિત) અસ્તિત્વના સિદ્ધાંત પર સંદર્ભો અંકગણિત કોમ્પ્યુટેશનલ જટિલતા સિદ્ધાંતના ઔપચારિક સિદ્ધાંતો વાસ્તવિક બીજગણિત ભૂમિતિ