Q0 (mathematical logic)
ક્યૂ0 એ પીટર એન્ડ્રુઝની સરળ-ટાઇપ કરેલા લેમ્બડા કલનની રચના છે, અને પ્રથમ ક્રમના તર્ક વત્તા સમૂહ સિદ્ધાંત સાથે તુલનાત્મક ગણિત માટે પાયો પૂરો પાડે છે. તે ઉચ્ચ ક્રમના તર્કનું એક સ્વરૂપ છે અને HOL પ્રમેય કહેવત પરિવારના તર્કશાસ્ત્ર સાથે નજીકથી સંબંધિત છે. સિદ્ધાંતો સાબિત કરતી પ્રણાલીઓ TPS અને ETPS એ Q0 પર આધારિત છે. ઓગસ્ટ 2009માં, ટી. પી. એસ. એ ઉચ્ચ ક્રમની પ્રમેય સાબિત કરતી પ્રણાલીઓ વચ્ચે સૌપ્રથમ સ્પર્ધા જીતી હતી. આ પ્રણાલીમાં માત્ર પાંચ સ્વયંસિદ્ધ છે, જેને આ રીતે કહી શકાયઃ (સ્વયંસિદ્ધ 2,3 અને 4 સ્વયંસિદ્ધ યોજના છે-સમાન સ્વયંસિદ્ધોના પરિવારો. સ્વયંસિદ્ધ 2 અને સ્વયંસિદ્ધ 3 ના ઉદાહરણો માત્ર ચલ અને સ્થિરાંકોના પ્રકારો દ્વારા બદલાય છે, પરંતુ સ્વયંસિદ્ધ 4 ના ઉદાહરણોમાં A અને B ને બદલે કોઈપણ અભિવ્યક્તિ હોઈ શકે છે.) સબ્સ્ક્રિપ્ટેડ "ઓ" એ બુલિયન મૂલ્યો માટેનું પ્રકાર પ્રતીક છે, અને સબ્સ્ક્રિપ્ટેડ "આઇ" એ વ્યક્તિગત (બિન-બુલિયન) મૂલ્યો માટેનું પ્રકાર પ્રતીક છે. આના ક્રમ કાર્યોના પ્રકારોનું પ્રતિનિધિત્વ કરે છે, અને વિવિધ કાર્ય પ્રકારોને અલગ પાડવા માટે કૌંસનો સમાવેશ કરી શકે છે. α અને β જેવા સબસ્ક્રિપ્ટેડ ગ્રીક અક્ષરો પ્રકાર પ્રતીકો માટે વાક્યરચના ચલ છે. બોલ્ડ કેપિટલ અક્ષરો જેમ કે,, અને ડબલ્યુએફએફ માટે વાક્યરચના ચલ છે, અને બોલ્ડ લોઅર કેસ અક્ષરો જેમ કે, ચલ માટે વાક્યરચના ચલ છે. તમામ મુક્ત ઘટનાઓમાં વાક્યરચના અવેજી સૂચવે છે. એકમાત્ર આદિમ અચળાંકો છે, જે દરેક પ્રકાર α ના સભ્યોની સમાનતાને સૂચવે છે, અને, વ્યક્તિઓ માટે વર્ણન સંચાલકને સૂચવે છે, જે બરાબર એક વ્યક્તિ ધરાવતા સમૂહનું અનન્ય તત્વ છે. પ્રતીકો λ અને કૌંસ ("[" અને "]") એ ભાષાનું વાક્યરચના છે. અન્ય તમામ પ્રતીકો આ સમાવતી શરતો માટે સંક્ષિપ્ત છે, જેમાં ક્વોન્ટિફાયર્સ τ અને HE નો સમાવેશ થાય છે. સ્વયંસિદ્ધ 4 માં, ઇન માટે મુક્ત હોવું જોઈએ, જેનો અર્થ છે કે અવેજી અવેજીના પરિણામે બંધાયેલા મુક્ત ચલની કોઈ ઘટનાઓનું કારણ નથી. સ્વયંસિદ્ધો વિશે સ્વયંસિદ્ધ 1 એ વિચારને વ્યક્ત કરે છે કે અને તે એકમાત્ર બુલિયન મૂલ્યો છે. સ્વયંસિદ્ધ યોજના 2α અને 3αβ વિધેયોના મૂળભૂત ગુણધર્મોને વ્યક્ત કરે છે. સ્વયંસિદ્ધ યોજના 4 એ λ સંકેતનની પ્રકૃતિને વ્યાખ્યાયિત કરે છે. સ્વયંસિદ્ધ 5 કહે છે કે પસંદગી સંચાલક વ્યક્તિઓ પરના સમાનતા કાર્યનો વ્યસ્ત છે. (એક દલીલને ધ્યાનમાં રાખીને, તે વ્યક્તિને વ્યક્તિ ધરાવતા સમૂહ/વિધેય સાથે મેપ કરો. Q0 માં, માટે સંક્ષિપ્ત છે, જે માટે સંક્ષિપ્ત છે.) આ સંચાલકને ચોક્કસ વર્ણન સંચાલક તરીકે પણ ઓળખવામાં આવે છે. માં, સ્વયંસિદ્ધ 4 ને પાંચ પેટા ભાગોમાં વિકસાવવામાં આવે છે જે અવેજની પ્રક્રિયાને તોડી પાડે છે. અહીં આપેલા સ્વયંસિદ્ધ સિદ્ધાંતની વૈકલ્પિક તરીકે ચર્ચા કરવામાં આવી છે અને પેટા ભાગોમાંથી સાબિત કરવામાં આવ્યો છે. લોજિકલ કોર એન્ડ્રુઝના એક્સ્ટેન્શન્સ આ તર્કને તમામ પ્રકારના સંગ્રહો માટે પસંદગી સંચાલકોની વ્યાખ્યાઓ સાથે વિસ્તરે છે, જેથી ′ એક પ્રમેય (સંખ્યા 5309) છે. બીજા શબ્દોમાં કહીએ તો, તમામ પ્રકારોમાં ચોક્કસ વર્ણન સંચાલક હોય છે. આ એક રૂઢિચુસ્ત વિસ્તરણ છે, તેથી જો કોર સુસંગત હોય તો વિસ્તૃત પ્રણાલી સુસંગત છે. તેઓ એક વધારાનો સ્વયંસિદ્ધ 6 પણ રજૂ કરે છે, જે જણાવે છે કે અનંતના સમકક્ષ વૈકલ્પિક સ્વયંસિદ્ધ સિદ્ધાંતો સાથે અનંત સંખ્યાબંધ વ્યક્તિઓ છે. પ્રકાર સિદ્ધાંત અને પ્રકાર સિદ્ધાંત પર આધારિત પુરાવા સહાયકોના અન્ય ઘણા ફોર્મ્યુલેશનથી વિપરીત, Q0 એ o અને i સિવાયના પાયાના પ્રકારો માટે પ્રદાન કરતું નથી, તેથી ઉદાહરણ તરીકે મર્યાદિત મુખ્ય સંખ્યાઓ સરળ પ્રકાર સિદ્ધાંતના અર્થમાં એક પ્રકારને બદલે સામાન્ય પીનો પૂર્વધારણાઓનું પાલન કરતી વ્યક્તિઓના સંગ્રહ તરીકે બનાવવામાં આવે છે. Q0 Q0 માં અનુમાનનો એક જ નિયમ છે. નિયમ આર. માંથી અને એક ઘટના દ્વારા ઇનની એક ઘટનાને બદલવાના પરિણામનું અનુમાન લગાવવું, જો કે ઇનની ઘટના તરત જ અગાઉની (ચલની ઘટના) નથી. અનુમાન R′ નો વ્યુત્પન્ન નિયમ H. નિયમ R′ પૂર્વધારણાઓના સમૂહમાંથી તર્કને સક્ષમ કરે છે. જો, અને, અને ની એક ઘટનાને એક ઘટના દ્વારા બદલીને મેળવવામાં આવે છે, તો પછી, પૂરી પાડવામાં આવેલ કેઃ ઇન ની ઘટના એ તરત જ પહેલાના ચલની ઘટના નથી, અને કોઈ ચલ મુક્ત નથી અને એક સભ્ય તેની બદલીની ઘટના પર બંધાયેલો નથી. નોંધઃ ઇન દ્વારા બદલવા પરનું પ્રતિબંધ એ સુનિશ્ચિત કરે છે કે કોઈ પણ ચલ પૂર્વધારણા બંનેમાં મુક્ત છે અને રિપ્લેસમેન્ટ થયા પછી બંનેમાં સમાન મૂલ્ય ધરાવવા માટે મર્યાદિત રહે છે. Q0 માટે કપાત પ્રમેય દર્શાવે છે કે નિયમ R′ નો ઉપયોગ કરીને પૂર્વધારણાઓમાંથી પુરાવાઓને પૂર્વધારણાઓ વિના અને નિયમ R નો ઉપયોગ કરીને પુરાવાઓમાં રૂપાંતરિત કરી શકાય છે. કેટલીક સમાન પ્રણાલીઓથી વિપરીત, Q0 માં અનુમાન સમાન અભિવ્યક્તિ સાથે WFF ની અંદર કોઈપણ ઊંડાઈ પર પેટા અભિવ્યક્તિને બદલે છે. તેથી ઉદાહરણ તરીકે આપેલ સ્વયંસિદ્ધઃ 1. 2. અને હકીકત એ છે કે, આપણે પરિમાણને દૂર કર્યા વિના આગળ વધી શકીએ છીએઃ 3. A અને B 4 માટે ત્વરિત. નિયમ R ને લીટી 3 નો ઉપયોગ કરીને લીટી 1 માં બદલી રહ્યા છીએ. નોંધો સંદર્ભો વધુ વાંચન વધુ ઊંડાણમાં Q0 નું વર્ણન; સ્ટેનફોર્ડ એન્સાયક્લોપેડિયા ઓફ ફિલોસોફીમાં ચર્ચના પ્રકાર સિદ્ધાંત પરના લેખનો એક ભાગ. ગાણિતિક તર્કશાસ્ત્ર પર એક ઝાંખી (Q0 ના વિવિધ અનુગામીઓ સહિત): ગણિતના પાયા. વંશાવળી અને ઝાંખી દોઈઃ 10.4444/100.111. કોમ્પ્યુટર વિજ્ઞાનમાં તર્કશાસ્ત્ર