S2S (mathematics)
ગણિતમાં, S2S એ બે અનુગામીઓ સાથેનો મોનાડિક સેકન્ડ ઓર્ડર થિયરી છે. તે જાણીતા સૌથી વધુ અભિવ્યક્ત કુદરતી નિર્ણાયક સિદ્ધાંતોમાંનું એક છે, જેમાં ઘણા નિર્ણાયક સિદ્ધાંતો S2S માં અર્થઘટન કરી શકાય છે. તેની નિર્ણાયકતા 1969માં રાબિન દ્વારા સાબિત કરવામાં આવી હતી. મૂળભૂત ગુણધર્મો S2S ના પ્રથમ ક્રમના પદાર્થો મર્યાદિત દ્વિસંગી તાર છે. સેકન્ડ ઓર્ડર ઓબ્જેક્ટ્સ એ મર્યાદિત દ્વિસંગી સ્ટ્રિંગ્સના મનસ્વી સમૂહો (અથવા યુનરી પ્રેડિકેટ્સ) છે. S2S શબ્દમાળાઓ પર s → s0 અને s → s1 વિધેયો ધરાવે છે, અને s ωS (સમકક્ષ, S (s)) નો અર્થ સ્ટ્રિંગ s સમૂહ S સાથે સંબંધિત છે. કેટલાક ગુણધર્મો અને સંમેલનોઃ મૂળભૂત રીતે, લોઅરકેસ અક્ષરો પ્રથમ ક્રમના પદાર્થોનો સંદર્ભ આપે છે, અને મોટા અક્ષરો બીજા ક્રમના પદાર્થોનો સંદર્ભ આપે છે. સમૂહોનો સમાવેશ S2S ને બીજો ક્રમ બનાવે છે, જેમાં "મોનાડિક" k> 1 માટે k-ary વિધેય ચલની ગેરહાજરી સૂચવે છે. શબ્દમાળાઓ s અને t નું જોડાણ એ st દ્વારા સૂચવવામાં આવે છે, અને તે સામાન્ય રીતે S2S માં ઉપલબ્ધ નથી, s → 0s પણ નહીં. શબ્દમાળાઓ વચ્ચેનો ઉપસર્ગ સંબંધ વ્યાખ્યાયિત કરી શકાય તેવો છે. સમાનતા એ આદિમ છે, અથવા તેને s = t′S (S (s) ′S (t)) અને S = T′S (S (s) ′T (s) તરીકે વ્યાખ્યાયિત કરી શકાય છે. શબ્દમાળાની જગ્યાએ, n → 2n + 1 અને n → 2n + 2 સાથે કુદરતી સંખ્યાઓનો ઉપયોગ કરી શકાય છે (ઉદાહરણ તરીકે) પરંતુ અન્ય કોઈ કામગીરી નથી. તમામ દ્વિસંગી તારોનો સમૂહ ક્લેન તારાનો ઉપયોગ કરીને {0,1} * દ્વારા સૂચવવામાં આવે છે. {0,1} * ના મનસ્વી ઉપગણને કેટલીકવાર વૃક્ષો સાથે ઓળખવામાં આવે છે, ખાસ કરીને {0,1}-લેબલવાળા વૃક્ષ {0,1} * તરીકે; {0,1} * સંપૂર્ણ અનંત દ્વિસંગી વૃક્ષ બનાવે છે. સૂત્રની જટિલતા માટે, શબ્દમાળા પરના ઉપસર્ગ સંબંધને સામાન્ય રીતે પ્રથમ ક્રમ તરીકે ગણવામાં આવે છે. તેના વિના, તમામ સૂત્રો Δ12 સૂત્રોની સમકક્ષ નહીં હોય. S2S માં વ્યક્ત કરી શકાય તેવા ગુણધર્મો માટે (તમામ દ્વિસંગી શબ્દમાળાઓના સમૂહને વૃક્ષ તરીકે જોવું), દરેક નોડ માટે, ડાબી સબટ્રી અને જમણી સબટ્રી અને બાકીની વચ્ચે માત્ર O (1) બિટ્સનો સંપર્ક કરી શકાય છે (સંચાર જટિલતા જુઓ). નિશ્ચિત k માટે, શબ્દમાળાઓથી k (એટલે કે. k) ની નીચેની પ્રાકૃતિક સંખ્યાઓને એક સમૂહ દ્વારા એન્કોડ કરી શકાય છે. વધુમાં, s, t ુણ s01t જ્યાં t એ t ના દરેક અક્ષરને બમણો કરે છે તે ઇન્જેક્ટિવ છે, અને s ુણ {s01t: t ણી {0,1} *} એ S2S વ્યાખ્યાયિત કરી શકાય તેવું છે. તેનાથી વિપરીત, સંચાર જટિલતા દલીલ દ્વારા, S1S (નીચે) માં સમૂહની જોડી એક સમૂહ દ્વારા સંકેતલિપી કરી શકાતી નથી. S2S ની નબળાઈઓઃ નબળા S2S (WS2S) માટે તમામ સમૂહો મર્યાદિત હોવા જરૂરી છે (નોંધ કરો કે કોનિગના લેમ્માનો ઉપયોગ કરીને S2S માં મર્યાદિતતા વ્યક્ત કરી શકાય છે). '1' શબ્દમાળાઓમાં ન દેખાય તે જરૂરી કરીને S1S મેળવી શકાય છે, અને WS1S ને પણ મર્યાદિતતાની જરૂર છે. ડબલ્યુ. એસ. 1. એસ. પણ પ્રેસબર્ગર અંકગણિતને 2 ની ઘાત માટે વિધેય સાથે અર્થઘટન કરી શકે છે, કારણ કે સમૂહનો ઉપયોગ નિશ્ચિત ઉમેરા સાથે અમર્યાદિત દ્વિસંગી સંખ્યાઓનું પ્રતિનિધિત્વ કરવા માટે થઈ શકે છે. નિર્ણયની જટિલતા S2S નિર્ણાયક છે, અને S2S, S1S, WS2S, WS1S દરેકમાં ઘાતાંકોની રેખીય રીતે વધતી જતી સાંકળને અનુરૂપ પૂરક નિર્ણયની જટિલતા નથી. નીચલા બાઉન્ડ માટે, તે σ11 WS1S વાક્યોને ધ્યાનમાં લેવા માટે પૂરતું છે. સિંગલ સેકન્ડ ઓર્ડર ક્વોન્ટિફાયરનો ઉપયોગ અંકગણિત (અથવા અન્ય) ગણતરીની દરખાસ્ત કરવા માટે થઈ શકે છે, જે પ્રથમ ક્રમના ક્વોન્ટિફાયરનો ઉપયોગ કરીને ચકાસી શકાય છે જો આપણે ચકાસી શકીએ કે કઈ સંખ્યાઓ સમાન છે. આ માટે, જો આપણે યોગ્ય રીતે સંખ્યા 1. m ને એન્કોડ કરીએ, તો આપણે દ્વિસંગી રજૂઆત i1i2.im સાથે સંખ્યાને i1 1 i2 2 તરીકે એન્કોડ કરી શકીએ છીએ. રક્ષકોના પરીક્ષણને ભેળવીને અને ચલ નામોનો ફરીથી ઉપયોગ કરીને, બિટ્સની સંખ્યા ઘાતાંકોની સંખ્યામાં રેખીય હોય છે. ઉપલા બાઉન્ડ માટે, નિર્ણય પ્રક્રિયા (નીચે) નો ઉપયોગ કરીને, કે-ફોલ્ડ ક્વોન્ટિફાયર અલ્ટરનેશન સાથેના વાક્યો વાક્યની લંબાઈ (સમાન સ્થિરાંકો સાથે) ના કે + ઓ (1)-ફોલ્ડ એક્સ્પોનેન્શિયેશનને અનુરૂપ સમયમાં નક્કી કરી શકાય છે. સ્વયંસિદ્ધીકરણ WS2S ને ચોક્કસ મૂળભૂત ગુણધર્મો વત્તા ઇન્ડક્શન યોજના દ્વારા સ્વયંસિદ્ધ કરી શકાય છે. S2S ને આંશિક રીતે આ રીતે સ્વયંસિદ્ધ કરી શકાય છેઃ (1) HE! s..................... હંમેશની જેમ, જો φ માં મુક્ત ચલ દર્શાવવામાં ન આવે, તો આપણે સ્વયંસિદ્ધનું સાર્વત્રિક સમાપન લઈએ છીએ. જો આગાહીઓ માટે સમાનતા આદિમ હોય, તો એક વિસ્તરણતા પણ ઉમેરે છે S = T ષ્ણ ષ્ણ ષ્ણ (S (s) ષ્ણ ષ્ણ ષ્ણ (s)). આપણી પાસે સમજણ હોવાથી, ઇન્ડક્શન એ સ્કીમાને બદલે એક નિવેદન હોઈ શકે છે. S1S નું અનુરૂપ સ્વયંસિદ્ધીકરણ પૂર્ણ થયું છે. જો કે, S2S માટે, સંપૂર્ણતા ખુલ્લી છે (2021 મુજબ). જ્યારે S1S માં એકરૂપતા હોય છે, ત્યાં કોઈ S2S વ્યાખ્યાયિત કરી શકાય તેવું (પરિમાણોને પણ મંજૂરી આપે છે) પસંદગી કાર્ય નથી કે જે ખાલી ન હોય તેવા સમૂહ S ને આપવામાં આવે તો તે S નું તત્વ આપે છે, અને સમજણ યોજનાઓને સામાન્ય રીતે પસંદગીના સ્વયંસિદ્ધના વિવિધ સ્વરૂપો સાથે વધારવામાં આવે છે. જો કે, (1)-(4) જ્યારે ચોક્કસ સમાનતા રમતો માટે નિર્ધારકતા યોજના સાથે વિસ્તૃત કરવામાં આવે ત્યારે પૂર્ણ થાય છે. S2S ને Π13 વાક્યો દ્વારા પણ સ્વયંસિદ્ધ કરી શકાય છે (આદિમ તરીકે શબ્દમાળાઓ પરના ઉપસર્ગ સંબંધનો ઉપયોગ કરીને). જો કે, તે મર્યાદિત રીતે સ્વયંસિદ્ધ નથી, અને જો આપણે ઇન્ડક્શન સ્કીમા અને અન્ય વાક્યોના મર્યાદિત સમૂહને ઉમેરીએ તો પણ તેને σ13 વાક્યો દ્વારા સ્વયંસિદ્ધ કરી શકાતું નથી (આ તેના Π12-CA0 સાથેના જોડાણથી અનુસરે છે). S2S સાથે સંબંધિત સિદ્ધાંતો દરેક મર્યાદિત k માટે, ત્રિ-પહોળાઈ ≤ k (અને અનુરૂપ વૃક્ષ વિઘટન) સાથે ગણી શકાય તેવા આલેખનો મોનાડિક સેકન્ડ ઓર્ડર (MSO) સિદ્ધાંત S2S માં અર્થઘટન કરી શકાય છે (જુઓ કોરસેલનો પ્રમેય). ઉદાહરણ તરીકે, વૃક્ષોનો એમએસઓ સિદ્ધાંત (આલેખ તરીકે) અથવા શ્રેણી-સમાંતર આલેખ નિર્ણાયક છે. અહીં (એટલે કે. બંધાયેલ વૃક્ષની પહોળાઈ માટે), આપણે શિરોબિંદુઓ (અથવા ધાર) ના સમૂહ માટે પરિમિતતા પરિમાણકનું અર્થઘટન પણ કરી શકીએ છીએ, અને નિશ્ચિત પૂર્ણાંકના સમૂહ મોડ્યુલોમાં શિરોબિંદુઓ (અથવા ધાર) ની ગણતરી પણ કરી શકીએ છીએ. અગણિત આલેખને મંજૂરી આપવાથી સિદ્ધાંતમાં ફેરફાર થતો નથી. ઉપરાંત, સરખામણી માટે, S1S બંધાયેલ પાથવિડ્થના જોડાયેલા આલેખનું અર્થઘટન કરી શકે છે. તેનાથી વિપરીત, અમર્યાદિત ત્રિ-પહોળાઈના આલેખના દરેક સમૂહ માટે, તેનું અસ્તિત્વ (એટલે કે. 11) જો આપણે શિરોબિંદુઓ અને ધાર બંને પર આગાહીઓને મંજૂરી આપીએ તો એમ. એસ. ઓ. સિદ્ધાંત અનિશ્ચિત છે. આમ, એક અર્થમાં, S2S ની નિર્ણાયકતા શ્રેષ્ઠ શક્ય છે. અમર્યાદિત ત્રિ-પહોળાઈવાળા આલેખમાં મોટી ગ્રીડ માઇનર્સ હોય છે, જેનો ઉપયોગ ટ્યુરિંગ મશીનનું અનુકરણ કરવા માટે થઈ શકે છે. એસ2એસમાં ઘટાડો કરીને, ગણતરીપાત્ર ક્રમની એમએસઓ થિયરી નિર્ણાયક છે, જેમ કે તેમના ક્લાઈન-બ્રોવર ક્રમ સાથે ગણતરીપાત્ર વૃક્ષોની એમએસઓ થિયરી છે. જો કે, (, <) નો MSO સિદ્ધાંત અનિશ્ચિત છે. ઓર્ડિનલ્સ <ω2 નો MSO સિદ્ધાંત નિર્ણાયક છે; ω2 માટે નિર્ણાયકતા ZFC થી સ્વતંત્ર છે (કોન (ZFC + નબળા કોમ્પેક્ટ કાર્ડિનલ) ધારીને). ઉપરાંત, ઓર્ડિનલ્સ પર મોનાડિક સેકન્ડ ઓર્ડર લોજિકનો ઉપયોગ કરીને ઓર્ડિનલની વ્યાખ્યા કરી શકાય છે, જો કે તે ઓર્ડિનલ એડિશન અને ગુણાકાર દ્વારા નિર્ધારિત નિયમિત કાર્ડિનલ્સમાંથી મેળવી શકાય છે. S2S ચોક્કસ મોડલ તર્કશાસ્ત્રની નિર્ણાયકતા માટે ઉપયોગી છે, જેમાં ક્રિપ્કે સિમેન્ટિક્સ કુદરતી રીતે વૃક્ષો તરફ દોરી જાય છે. S2S + U (અથવા માત્ર S1S + U) અનિશ્ચિત છે જો U એ અનબાઉન્ડિંગ ક્વોન્ટિફાયર છે-UX φ (X) જો કેટલાક મનસ્વી રીતે મોટા મર્યાદિત X માટે φ (X) ધરાવે છે. જો કે, WS2S + U, અનંત માર્ગો પર માત્રાત્મકતા સાથે પણ, નિર્ણાયક છે, S2S પેટા સૂત્રો સાથે પણ જેમાં U નથી. સૂત્ર જટિલતા દ્વિસંગી શબ્દમાળાઓનો સમૂહ S2S માં વ્યાખ્યાયિત કરી શકાય છે જો તે નિયમિત હોય (એટલે કે. નિયમિત ભાષા બનાવે છે). S1S માં, સેટ પરનું (યુનરી) વિધેય (પરિમાણ-મુક્ત) વ્યાખ્યાયિત કરી શકાય તેવું છે જો તે ω-નિયમિત ભાષા છે. S2S માટે, એવા સૂત્રો માટે કે જે તેમના મુક્ત ચલોનો ઉપયોગ ફક્ત 1 ન હોય તેવા શબ્દમાળાઓ પર કરે છે, અભિવ્યક્તિ S1S માટે સમાન છે. દરેક S2S સૂત્ર φ (S1,., Sk), (k મુક્ત ચલ સાથે) અને દ્વિસંગી તારના મર્યાદિત વૃક્ષ T માટે, φ (S1 θT,., Sk θT) ની ગણતરી |T | માં સમય રેખીય રીતે કરી શકાય છે (જુઓ કોરસેલનો પ્રમેય), પરંતુ ઉપર નોંધ્યા મુજબ, સૂત્રના કદમાં ઓવરહેડને પુનરાવર્તિત ઘાતાંકીય કરી શકાય છે (વધુ ચોક્કસપણે, સમય છે). S1S માટે, દરેક સૂત્ર Δ11 સૂત્ર અને Π02 અંકગણિત સૂત્રોના બુલિયન સંયોજનની સમકક્ષ છે. વધુમાં, દરેક S1S સૂત્ર સૂત્રના પરિમાણોના અનુરૂપ ω-ઓટોમેટન દ્વારા સ્વીકૃતિ સમાન છે. ઓટોમેટન એક નિર્ધારક પેરિટી ઓટોમેટન હોઈ શકે છેઃ પેરિટી ઓટોમેટન દરેક સ્થિતિ માટે પૂર્ણાંક અગ્રતા ધરાવે છે, અને સ્વીકારે છે કે અનંત રીતે જોવા મળતી સર્વોચ્ચ પ્રાથમિકતા ઘણીવાર વિચિત્ર (વૈકલ્પિક રીતે, સમ) હોય છે. S2S માટે, વૃક્ષ ઓટોમેટા (નીચે) નો ઉપયોગ કરીને, દરેક સૂત્ર Δ12 સૂત્રની સમકક્ષ હોય છે. વધુમાં, દરેક S2S સૂત્ર માત્ર ચાર પરિમાણો સાથે સૂત્રની સમકક્ષ હોય છે, HE S τ τ τ. (એમ ધારીને કે આપણી ઔપચારિકતામાં ઉપસર્ગ સંબંધ અને અનુગામી કાર્યો બંને છે). S1S માટે, ત્રણ પરિમાણકો પૂરતા છે, અને WS2S અને WS1S માટે, બે પરિમાણો પૂરતા છે; WS2S અને WS1S માટે અહીં ઉપસર્ગ સંબંધની જરૂર નથી. જો કે, મુક્ત સેકન્ડ ઓર્ડર વેરિયેબલ્સ સાથે, દરેક S2S સૂત્રને સેકન્ડ ઓર્ડર અંકગણિતમાં માત્ર Π11 ટ્રાન્સફાઇનાઇટ રિકર્શન દ્વારા વ્યક્ત કરી શકાતું નથી (રિવર્સ ગણિત જુઓ). RCA0 + (સ્કીમા) {τ: τ એ સાચું S2S વાક્ય છે} એ (સ્કીમા) ની સમકક્ષ છે {τ: τ એ Π13 વાક્ય છે જે Π12-CA0} માં સાબિત કરી શકાય છે. બેઝ થિયરી પર, સ્કિમા (સ્કિમા ઓવર k) τS τω τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ મર્યાદિત પ્રેરણાને કારણે, Π12-CA0 એ સાબિત કરતું નથી કે તમામ સાચા (પ્રમાણભૂત નિર્ણય પ્રક્રિયા હેઠળ) Π13 S2S નિવેદનો વાસ્તવમાં સાચા છે, તેમ છતાં આવા દરેક વાક્ય Π12-CA0 સાબિત કરી શકાય તેવું છે. વધુમાં, દ્વિસંગી તાર S અને T ના સમૂહને જોતાં, નીચેની બાબતો સમકક્ષ છેઃ (1) T એ S થી ગણતરી કરી શકાય તેવા દ્વિસંગી તાર બહુપદી સમયના અમુક સમૂહમાંથી S2S વ્યાખ્યાયિત કરી શકાય છે. (2) T ની ગણતરી કેટલીક રમત માટે જીતવાની સ્થિતિના સમૂહમાંથી કરી શકાય છે, જેની ચૂકવણી એ Π02 (S) સમૂહોનું મર્યાદિત બુલિયન સંયોજન છે. (3) T ને S માંથી અંકગણિતમાં વ્યાખ્યાયિત કરી શકાય છે (અંકગણિત સૂત્રો + ઓછામાં ઓછા નિશ્ચિત-બિંદુ તર્ક) (4) T એ ઓછામાં ઓછા β-મોડેલમાં છે (એટલે કે. એક ω-મોડેલ કે જેનું સમૂહ-સૈદ્ધાંતિક પ્રતિરૂપ સંક્રમક હોય છે) જેમાં S હોય છે અને તે Π12-CA0 ના તમામ Π13 પરિણામોને સંતોષે છે. S1S અને S2S ના નમૂના પ્રમાણભૂત નમૂના ઉપરાંત (જે S1S અને S2S માટે અનન્ય MSO નમૂના છે), S1S અને S2S માટે અન્ય નમૂનાઓ છે, જે ડોમેનના તમામ ઉપગણને બદલે કેટલાકનો ઉપયોગ કરે છે (હેન્કિન સિમેન્ટિક્સ જુઓ). દરેક S ω માટે, S માં પુનરાવર્તિત સેટ પ્રમાણભૂત S1S મોડેલનું પ્રાથમિક પેટા મોડલ બનાવે છે, અને ટ્યુરિંગ જોઇન અને ટ્યુરિંગ રિડ્યુસિબિલિટી હેઠળ બંધ ω ના ઉપગણના દરેક બિન-ખાલી સંગ્રહ માટે સમાન છે. આ S1S વ્યાખ્યાયિત સમૂહોની સાપેક્ષ પુનરાવર્તિતતા અને એકરૂપતા પરથી અનુસરે છેઃ-φ (s) (s ના કાર્ય તરીકે) ની ગણતરી φ ના પરિમાણો અને s ના મર્યાદિત સમૂહ માટે φ (s) ના મૂલ્યોમાંથી કરી શકાય છે (તેનું કદ φ માટે નિર્ધારિત ઓટોમેટનમાં સ્થિતિઓની સંખ્યા દ્વારા બંધાયેલ છે). - HE S φ (S) માટે સાક્ષી k પસંદ કરીને અને S ના S નો મર્યાદિત ટુકડો પસંદ કરીને મેળવી શકાય છે, અને વારંવાર S ને વિસ્તારી શકાય છે જેથી દરેક એક્સ્ટેંશન દરમિયાન સૌથી વધુ પ્રાથમિકતા k હોય અને એક્સ્ટેંશનને k ઉપરની પ્રાથમિકતાઓને ફટકાર્યા વિના φ ને સંતોષતા S માં પૂર્ણ કરી શકાય (આને ફક્ત પ્રારંભિક S માટે જ મંજૂરી છે). ઉપરાંત, લેક્સિકોગ્રાફિક રીતે ઓછામાં ઓછી ટૂંકી પસંદગીઓનો ઉપયોગ કરીને, S1S સૂત્ર φ 'એવું છે કે φ' ⇒φ અને HE Sφ (S) φ! Sφ '(S) (એટલે કે. એકરૂપકરણ; φમાં મુક્ત ચલ દર્શાવવામાં ન હોઈ શકે; φ 'માત્ર સૂત્ર φ પર આધાર રાખે છે. S2S ના ન્યૂનતમ મોડેલમાં દ્વિસંગી શબ્દમાળાઓ પરની તમામ નિયમિત ભાષાઓનો સમાવેશ થાય છે. તે પ્રમાણભૂત મોડેલનું પ્રાથમિક પેટા મોડલ છે, તેથી જો S2S પરિમાણ-મુક્ત વ્યાખ્યાયિત વૃક્ષોનો સમૂહ ખાલી ન હોય, તો તેમાં નિયમિત વૃક્ષનો સમાવેશ થાય છે. નિયમિત ભાષાને નિયમિત {0,1}-લેબલ થયેલ સંપૂર્ણ અનંત દ્વિસંગી વૃક્ષ તરીકે પણ ગણી શકાય (શબ્દમાળાઓ પરના અનુમાન સાથે ઓળખાય છે). લેબલ કરેલું વૃક્ષ નિયમિત છે જો તે પ્રારંભિક શિરોબિંદુ સાથે શિરોબિંદુ-લેબલ કરેલ મર્યાદિત નિર્દેશિત આલેખને અનરોલ કરીને મેળવી શકાય; પ્રારંભિક શિરોબિંદુથી પહોંચી શકાય તેવા આલેખમાં (નિર્દેશિત) ચક્ર અનંત વૃક્ષ આપે છે. નિયમિત વૃક્ષોના આ અર્થઘટન અને એન્કોડિંગ સાથે, દરેક સાચું S2S વાક્ય પહેલેથી જ પ્રાથમિક કાર્ય અંકગણિતમાં સાબિત થઈ શકે છે. તે બિન-નિયમિત વૃક્ષો છે જેને નિર્ધારણ માટે બિન-અનુમાનિત સમજણની જરૂર પડી શકે છે (નીચે). ત્યાં અનિયમિત છે (એટલે કે. બિન-નિયમિત ભાષાઓ ધરાવતા) S1S (અને સંભવતઃ S2S) ના નમૂનાઓ (પ્રમાણભૂત પ્રથમ ક્રમના ભાગ સાથે અને વગર બંને) ગણતરીપાત્ર સંતોષ સંબંધ સાથે. જો કે, સ્ટ્રિંગ્સના પુનરાવર્તિત સમૂહોનો સમૂહ સમજણ અને નિર્ધારકતાની નિષ્ફળતાને કારણે S2S નું મોડેલ બનાવતો નથી. S2S ની નિર્ણાયકતા નિર્ણાયકતાનો પુરાવો એ દર્શાવે છે કે દરેક સૂત્ર બિનનિર્ધારણીય વૃક્ષ ઓટોમેટન દ્વારા સ્વીકૃતિની સમકક્ષ છે (વૃક્ષ ઓટોમેટન અને અનંત વૃક્ષ ઓટોમેટન જુઓ). એક અનંત વૃક્ષ ઓટોમેટન મૂળથી શરૂ થાય છે અને વૃક્ષની ઉપર જાય છે, અને દરેક વૃક્ષની ડાળી સ્વીકારે છે. બિનનિર્ધારિત વૃક્ષ ઓટોમેટન સ્વીકારે છે કે જો ખેલાડી 1 પાસે જીતવાની વ્યૂહરચના હોય, જ્યાં ખેલાડી 1 માન્ય (વર્તમાન સ્થિતિ અને ઇનપુટ માટે) નવી સ્થિતિઓની જોડી (p0, p1) પસંદ કરે છે, જ્યારે ખેલાડી 2 શાખા પસંદ કરે છે, જો 0 પસંદ કરવામાં આવે તો p0 અને અન્યથા p1 માં સંક્રમણ સાથે. સહ-બિનનિર્ધારણીય ઓટોમેટન માટે, તમામ પસંદગીઓ ખેલાડી 2 દ્વારા કરવામાં આવે છે, જ્યારે નિર્ધારક માટે, (પી0, પી1) રાજ્ય અને ઇનપુટ દ્વારા નક્કી કરવામાં આવે છે; અને રમત ઓટોમેટન માટે, બંને ખેલાડીઓ શાખા અને રાજ્યને સેટ કરવા માટે મર્યાદિત રમત રમે છે. શાખા પરની સ્વીકૃતિ શાખા પર અનંત વાર જોવા મળતી સ્થિતિઓ પર આધારિત હોય છે; સમાનતા ઓટોમેટા અહીં પૂરતા પ્રમાણમાં સામાન્ય છે. સૂત્રોને ઓટોમેટામાં રૂપાંતરિત કરવા માટે, બેઝ કેસ સરળ છે, અને નોનડેટર્મિનિઝમ અસ્તિત્વના પરિમાણો હેઠળ ક્લોઝર આપે છે, તેથી આપણે ફક્ત પૂરકતા હેઠળ ક્લોઝરની જરૂર છે. સમાનતા રમતોની સ્થિતિ નિર્ધારણનો ઉપયોગ કરીને (જ્યાં આપણને અભેદ્ય સમજણની જરૂર છે), ખેલાડી 1 જીતવાની વ્યૂહરચનાનું અસ્તિત્વ ન હોવાને કારણે ખેલાડીને 2 જીતવાની વ્યૂહરચના S મળે છે, જેમાં સહ-બિનનિર્ધારણીય વૃક્ષ ઓટોમેટન તેની સ્વસ્થતાની ચકાસણી કરે છે. ઓટોમેટનને પછી નિર્ધારક બનાવી શકાય છે (જ્યાં આપણને સ્થિતિઓની સંખ્યામાં ઘાતાંકીય વધારો મળે છે), અને આમ Sનું અસ્તિત્વ બિન-નિર્ધારક ઓટોમેટન દ્વારા સ્વીકારને અનુરૂપ છે. નિર્ધારકતાઃ ZFC માં, બોરેલ રમતો નક્કી કરવામાં આવે છે, અને Π02 સૂત્રોના બુલિયન સંયોજનો (મનસ્વી વાસ્તવિક પરિમાણો સાથે) માટેનો નિર્ધારકતા પુરાવો પણ અહીં એક વ્યૂહરચના આપે છે જે ફક્ત વર્તમાન સ્થિતિ અને વૃક્ષની સ્થિતિ પર આધાર રાખે છે. તેનો પુરાવો પ્રાથમિકતાઓની સંખ્યા પર ઇન્ડક્શન દ્વારા છે. ધારો કે કે પ્રાથમિકતાઓ છે, જેમાં સૌથી વધુ પ્રાથમિકતા કે છે, અને કે ખેલાડી 2 માટે યોગ્ય સમાનતા ધરાવે છે. દરેક સ્થિતિ માટે (વૃક્ષની સ્થિતિ + રાજ્ય) ઓછામાં ઓછી ક્રમિક α (જો કોઈ હોય તો) એવી રીતે સોંપો કે ખેલાડી 1 પાસે જીતવાની વ્યૂહરચના હોય જેમાં તમામ દાખલ કરેલ (એક અથવા વધુ પગલાં પછી) અગ્રતા k સ્થિતિઓ (જો કોઈ હોય તો) <α લેબલ ધરાવતી હોય. જો પ્રારંભિક સ્થિતિ લેબલ થયેલ હોય તો ખેલાડી 1 જીતી શકે છેઃ દરેક વખતે જ્યારે પ્રાથમિકતા k સ્થિતિ સુધી પહોંચે છે, ત્યારે ક્રમમાં ઘટાડો થાય છે, અને વધુમાં ઘટાડાની વચ્ચે, ખેલાડી 1 k-1 પ્રાથમિકતાઓ માટે વ્યૂહરચનાનો ઉપયોગ કરી શકે છે. જો સ્થિતિ લેબલ વગરની હોય તો ખેલાડી 2 જીતી શકે છેઃ કે-1 પ્રાથમિકતાઓ માટેના નિર્ધારણ દ્વારા, ખેલાડી 2 પાસે એક વ્યૂહરચના હોય છે જે જીતે છે અથવા લેબલ વગરની અગ્રતા કે સ્થિતિમાં પ્રવેશ કરે છે, જે કિસ્સામાં ખેલાડી 2 ફરીથી તે વ્યૂહરચનાનો ઉપયોગ કરી શકે છે. વ્યૂહરચનાને સ્થિતિસ્થાપક બનાવવા માટે (કે પર ઇન્ડક્શન દ્વારા), સહાયક રમત રમતી વખતે, જો બે પસંદ કરેલી સ્થિતિસ્થાપક વ્યૂહરચનાઓ સમાન સ્થિતિ તરફ દોરી જાય, તો નીચલા α સાથે વ્યૂહરચના સાથે ચાલુ રાખો, અથવા તે જ α (અથવા ખેલાડી 2 માટે) નીચી પ્રારંભિક સ્થિતિ માટે (જેથી આપણે વ્યૂહરચનાને મર્યાદિત રીતે ઘણી વખત બદલી શકીએ). ઓટોમેટા નિર્ધારણઃ સહ-બિનનિર્ધારણીય વૃક્ષ ઓટોમેટા નક્કી કરવા માટે, ω-ઓટોમેટાને ધ્યાનમાં લેવું પૂરતું છે, શાખાની પસંદગીને ઇનપુટ તરીકે ગણવી, ઓટોમેટન નક્કી કરવું અને તેનો ઉપયોગ નિર્ધારક વૃક્ષ ઓટોમેટન માટે કરવો. નોંધ લો કે આ બિનનિર્ધારિત વૃક્ષ ઓટોમેટા માટે ડાબી તરફ જવા માટેના નિર્ધારણ તરીકે કામ કરતું નથી (એટલે કે. s → s0) જમણી શાખાની સામગ્રી પર આધાર રાખી શકે છે; બિનનિર્ધારણવાદથી વિપરીત, નિર્ધારક વૃક્ષ ઓટોમેટા ચોક્કસપણે બિન-ખાલી સમૂહોને પણ સ્વીકારી શકતા નથી. બિનનિર્ધારિત ω-ઓટોમેટન M નક્કી કરવા માટે (સહ-બિનનિર્ધારિત માટે, પૂરક લો, નોંધ્યું છે કે નિર્ધારક પેરિટી ઓટોમેટા પૂરક હેઠળ બંધ છે), આપણે એમની સંભવિત સ્થિતિઓના સમૂહને સંગ્રહિત કરતા દરેક નોડ સાથે સાફ્રા વૃક્ષનો ઉપયોગ કરી શકીએ છીએ, અને ઉચ્ચ અગ્રતા સ્થિતિઓ સુધી પહોંચવાના આધારે નોડ બનાવટ અને કાઢી નાંખી શકીએ છીએ. વિગતો માટે, જુઓ અથવા. સ્વીકૃતિની નિર્ણાયકતાઃ ખાલી વૃક્ષની બિનનિર્ધારણીય સમાનતા ઓટોમેટન દ્વારા સ્વીકૃતિ એ મર્યાદિત આલેખ G પરની સમાનતા રમતને અનુરૂપ છે. ઉપરોક્ત સ્થિતિસ્થાપક (જેને સ્મૃતિહીન પણ કહેવાય છે) નિર્ધારકતાનો ઉપયોગ કરીને, આને મર્યાદિત રમત દ્વારા અનુકરણ કરી શકાય છે જે જ્યારે આપણે લૂપ સુધી પહોંચીએ ત્યારે સમાપ્ત થાય છે, જેમાં લૂપમાં સર્વોચ્ચ અગ્રતા સ્થિતિ પર આધારિત જીતની સ્થિતિ હોય છે. એક ચપળ ઓપ્ટિમાઇઝેશન ક્વાસીપોલિનોમિયલ ટાઇમ અલ્ગોરિધમ આપે છે, જે બહુપદી સમય હોય છે જ્યારે પ્રાથમિકતાઓની સંખ્યા પૂરતી ઓછી હોય છે (જે સામાન્ય રીતે વ્યવહારમાં થાય છે). વૃક્ષોનો સિદ્ધાંતઃ વૃક્ષો પર એમ. એસ. ઓ. તર્કની નિર્ણાયકતા માટે (એટલે કે. આલેખ કે જે વૃક્ષો છે), પ્રથમ ક્રમની વસ્તુઓ માટે મર્યાદિતતા અને મોડ્યુલર ગણતરી પરિમાણો સાથે પણ, આપણે ગણતરીપાત્ર વૃક્ષોને સંપૂર્ણ દ્વિસંગી વૃક્ષમાં જોડી શકીએ છીએ અને S2S ની નિર્ણાયકતાનો ઉપયોગ કરી શકીએ છીએ. ઉદાહરણ તરીકે, નોડ s માટે, આપણે તેના ચિલ્ડ્રનને s1, s01, s001, વગેરે દ્વારા રજૂ કરી શકીએ છીએ. અગણિત વૃક્ષો માટે, આપણે શેલાહ-સ્ટુપ પ્રમેય (નીચે) નો ઉપયોગ કરી શકીએ છીએ. આપણે કાર્ડિનાલિટી ω1 ધરાવતા સેટ ફર્સ્ટ ઓર્ડર ઓબ્જેક્ટ્સ માટે પ્રેડિકેટ પણ ઉમેરી શકીએ છીએ, અને કાર્ડિનાલિટી ω2 માટે પ્રેડિકેટ, અને તેથી અનંત નિયમિત કાર્ડિનલ્સ માટે. બંધાયેલ વૃક્ષની પહોળાઈના આલેખ વૃક્ષોનો ઉપયોગ કરીને અર્થઘટન કરી શકાય છે, અને ધાર પર આગાહી કર્યા વિના આ બંધાયેલ જૂથની પહોળાઈના આલેખને પણ લાગુ પડે છે. અન્ય નિર્ણાયક સિદ્ધાંતો સાથે S2S નું સંયોજન મોનડિક સિદ્ધાંતોના વૃક્ષ વિસ્તરણઃ શેલાહ-સ્ટુપ પ્રમેય દ્વારા, જો મોનડિક રીલેશ્નલ મોડેલ M નિર્ણાયક હોય, તો તેનું વૃક્ષ પ્રતિરૂપ પણ એવું જ છે. ઉદાહરણ તરીકે, (ઔપચારિકરણની મોડ્યુલો પસંદગી) S2S એ {0,1} નું વૃક્ષ પ્રતિરૂપ છે. વૃક્ષ પ્રતિરૂપમાં, પ્રથમ ક્રમના પદાર્થો વિસ્તરણ દ્વારા ક્રમબદ્ધ M ના તત્વોના મર્યાદિત ક્રમ છે, અને M-સંબંધ Pi ને Pi '(vd1,., vdk) ′Pi (d1,., dk) સાથે Pi' ખોટી સાથે મેપ કરવામાં આવે છે અન્યથા (dj ωM, અને v એ M ના તત્વોનો (સંભવતઃ ખાલી) ક્રમ છે. આ સાબિતી S2S નિર્ણાયકતા સાબિતી જેવી જ છે. દરેક તબક્કે, એ (બિનનિર્ધારણીય) ઓટોમેટનને ઇનપુટ તરીકે એમ ઓબ્જેક્ટ્સ (સંભવતઃ સેકન્ડ ઓર્ડર) નું ટુપલ મળે છે, અને એમ સૂત્ર નક્કી કરે છે કે કયા સ્થિતિ સંક્રમણોની મંજૂરી છે. ખેલાડી 1 (ઉપર મુજબ) મેપિંગ ચાઈલ્ડ સ્થિતિ પસંદ કરે છે જેને સૂત્ર દ્વારા મંજૂરી આપવામાં આવી છે (વર્તમાન સ્થિતિ આપવામાં આવી છે), અને ખેલાડી 2 ચાલુ રાખવા માટે ચાઈલ્ડ (નોડની) પસંદ કરે છે. બિન-નિર્ધારિત ઓટોમેટન દ્વારા અસ્વીકાર જોવા માટે, દરેક (નોડ, સ્થિતિ) માટે (બાળક, સ્થિતિ) જોડીનો સમૂહ પસંદ કરો જેથી દરેક પસંદગી માટે, ઓછામાં ઓછી એક જોડી હિટ થાય, અને જેથી તમામ પરિણામી માર્ગો અસ્વીકાર તરફ દોરી જાય. મોનાડિક સિદ્ધાંતને પ્રથમ ક્રમના સિદ્ધાંત સાથે જોડવુંઃ ફેફરમેન-વોટ પ્રમેય નીચે પ્રમાણે વિસ્તરે છે/લાગુ પડે છે. જો M એ MSO મોડેલ છે અને N એ ફર્સ્ટ ઓર્ડર મોડેલ છે, તો પછી M એ (થિયરી (M), થિયરી (N)) ઓરેકલની સાપેક્ષમાં નિર્ણાયક રહે છે, ભલે M ને તમામ કાર્યો M → N સાથે વધારવામાં આવે, જ્યાં M ને તેના પ્રથમ પદાર્થો સાથે ઓળખવામાં આવે છે, અને દરેક s bul M માટે આપણે N ની અસંગત નકલનો ઉપયોગ કરીએ છીએ, જેમાં ભાષા તે મુજબ સુધારવામાં આવે છે. ઉદાહરણ તરીકે, જો N એ (, 0, +, ⋅) હોય, તો આપણે (ફંક્શન f) િલીવ s HE r bul Ns f (s) + Ns r = 0Ns કહી શકીએ છીએ. જો M એ S2S હોય (અથવા વધુ સામાન્ય રીતે, કેટલાક મોનડિક મોડેલનું વૃક્ષ પ્રતિરૂપ), તો ઓટોમેટા હવે N-સૂત્રોનો ઉપયોગ કરી શકે છે, અને આમ f: M → Nk ને M સમૂહોના ટુપલમાં રૂપાંતરિત કરી શકે છે. મતભેદ જરૂરી છે કારણ કે અન્યથા સમાનતા સાથે દરેક અનંત N માટે, વિસ્તૃત S2S અથવા માત્ર WS1S અનિશ્ચિત છે. ઉપરાંત, (સંભવતઃ અપૂર્ણ) સિદ્ધાંત T માટે, T ના M-ઉત્પાદનોની TM થિયરી (થિયરી (M), T) ઓરેકલની સાપેક્ષમાં નિર્ણાયક છે, જ્યાં TM નું મોડેલ દરેક s bul M માટે T ના મનસ્વી ડિસજોઈન્ટ મોડેલ Ns નો ઉપયોગ કરે છે (ઉપર મુજબ, M એ એક MSO મોડેલ છે; થિયરી (Ns) s પર આધારિત હોઈ શકે છે). સાબિતી સૂત્રની જટિલતા પર ઇન્ડક્શન દ્વારા છે. જો વિધેય f મુક્ત હોય તો f (s) સહિત મુક્ત Ns ચલની સૂચિને વિરુદ્ધ માની લો. ઇન્ડક્શન દ્વારા, એક દર્શાવે છે કે વિ નો ઉપયોગ ફક્ત |vs | મુક્ત ચલ સાથે એન-સૂત્રોના મર્યાદિત સમૂહ દ્વારા થાય છે. આમ, આપણે શું શક્ય છે તેનો જવાબ આપવા માટે N (અથવા T) નો ઉપયોગ કરીને તમામ સંભવિત પરિણામોનું પ્રમાણ નક્કી કરી શકીએ છીએ, અને યાદીની શક્યતાઓ (અથવા મર્યાદાઓ) આપવામાં આવે તો, M. માં અનુરૂપ વાક્યને S2S ના વિસ્તરણમાં કોડિંગ કરી શકીએ છીએઃ સ્ટ્રિંગ્સ પરના દરેક નિર્ણાયક વિધેયને (રેખીય સમય એન્કોડિંગ અને ડીકોડિંગ સાથે) S2S (ઉપરના વિસ્તરણ સાથે પણ) ની નિર્ણાયકતા માટે એન્કોડેડ વિધેય સાથે એન્કોડ કરી શકાય છે. પુરાવોઃ બિનનિર્ધારિત અનંત વૃક્ષ ઓટોમેટનને જોતાં, આપણે મર્યાદિત દ્વિસંગી લેબલવાળા વૃક્ષોના સમૂહને (લેબલ ધરાવતા કે જેના પર ઓટોમેટન કામ કરી શકે છે) મર્યાદિત રીતે ઘણા વર્ગોમાં વિભાજિત કરી શકીએ છીએ, જેમ કે જો સંપૂર્ણ અનંત દ્વિસંગી વૃક્ષ સમાન વર્ગના વૃક્ષોથી બનેલું હોઈ શકે, તો સ્વીકૃતિ માત્ર વર્ગ અને પ્રારંભિક સ્થિતિ (એટલે કે. જણાવો કે ઓટોમેટન વૃક્ષમાં પ્રવેશ કરે છે). (પંપીંગ લેમ્મા સાથે એકદમ સામ્યતા નોંધો.) ઉદાહરણ તરીકે (પેરિટી ઓટોમેટન માટે), સમાન વર્ગને વૃક્ષો સોંપો જો તેમની પાસે સમાન વિધેય હોય જે આપેલ હોય પ્રારંભિક _ સ્થિતિ અને (સ્થિતિ, ઉચ્ચતમ _ અગ્રતા _ પહોંચી) જોડીનો સમૂહ Q ખેલાડી 1 (એટલે કે. બિનનિર્ધારણવાદ) એક સાથે તમામ શાખાઓને Q ના તત્વોને અનુરૂપ થવા માટે દબાણ કરી શકે છે. હવે, દરેક k માટે, વૃક્ષોનો મર્યાદિત સમૂહ (કોડિંગ માટે યોગ્ય) પસંદ કરો જે ઓટોમેટા 1-k માટે સમાન વર્ગ સાથે સંબંધિત હોય, જેમાં k પર સુસંગત વર્ગની પસંદગી હોય. વિધેયને એન્કોડ કરવા માટે, k = 1 નો ઉપયોગ કરીને કેટલાક બિટ્સને એન્કોડ કરો, પછી k = 2 નો ઉપયોગ કરીને વધુ બિટ્સ, અને તેથી વધુ. સંદર્ભો વધારાનો સંદર્ભઃ ગાણિતિક તર્ક ગણતરી સિદ્ધાંત પુરાવા ધરાવતા લેખો