Geometric logic
ગાણિતિક તર્કશાસ્ત્રમાં, ભૌમિતિક તર્કશાસ્ત્ર એ સુસંગત તર્કશાસ્ત્રનું અનંત સામાન્યીકરણ છે, જે સ્કોલેમને કારણે પ્રથમ ક્રમના તર્કશાસ્ત્રનું પ્રતિબંધ છે જે સૈદ્ધાંતિક રીતે સાબિત કરી શકાય તેવું છે. ભૌમિતિક તર્કશાસ્ત્ર ઘણા ગાણિતિક સિદ્ધાંતોને વ્યક્ત કરવામાં સક્ષમ છે અને ટોપોસ સિદ્ધાંત સાથે ગાઢ જોડાણ ધરાવે છે. વ્યાખ્યાઓ પ્રથમ ક્રમના તર્કશાસ્ત્રનો સિદ્ધાંત ભૌમિતિક છે જો તેને માત્ર એવા સ્વરૂપના સ્વયંસિદ્ધ સિદ્ધાંતોનો ઉપયોગ કરીને સ્વયંસિદ્ધ કરી શકાય કે જ્યાં I અને J એ સૂત્રોના અસંબદ્ધ સંગ્રહ છે, સૂચકાંકો કે દરેક અનંત હોઈ શકે છે અને સૂત્ર φ એ અણુઓ અથવા અણુઓના નિષેધો છે. જો બધા સ્વયંસિદ્ધ મર્યાદિત હોય (એટલે કે, દરેક સ્વયંસિદ્ધ માટે, I અને J બંને મર્યાદિત હોય), તો સિદ્ધાંત સુસંગત છે. પ્રમેય દરેક પ્રથમ ક્રમ સિદ્ધાંત સુસંગત રૂઢિચુસ્ત વિસ્તરણ ધરાવે છે. મહત્વ ઉપરોક્ત પ્રમેયના આઠ પરિણામોની યાદી બનાવે છે જે તેના મહત્વને સમજાવે છે (ફૂટનોટ્સ અને મોટાભાગના સંદર્ભોને બાદ કરતા): G3c જેવા ક્રમિક કલનશાસ્ત્રના સંદર્ભમાં, સ્વયંસિદ્ધ તરીકે વિશેષ સુસંગત અસરોને માળખાકીય નિયમો (નબળાઈ, સંકોચન અને કટ) ની સ્વીકાર્યતાને અસર કર્યા વિના સીધા અનુમાન નિયમોમાં રૂપાંતરિત કરી શકાય છે; સમાન શબ્દોમાં, સુસંગત સિદ્ધાંતો "ચોક્કસ સરળ સ્વરૂપમાં કુદરતી કપાત નિયમો દ્વારા વ્યક્ત કરી શકાય તેવા સિદ્ધાંતો છે જેમાં માત્ર અણુ સૂત્રો જ નિર્ણાયક ભાગ ભજવે છે"; સુસંગત અસરો અનુક્રમ બનાવે છે જે ગ્લિવેંકો વર્ગ આપે છે. આ કિસ્સામાં, પ્રથમ ક્રમના બારના પ્રમેય તરીકે ઓળખાતું પરિણામ જણાવે છે કે જો દરેક Ii: 0 ≤ i ≤ n એ સુસંગત સૂચિતાર્થ છે અને ક્રમિક I1, છે. . . , માં I0 શાસ્ત્રીય રીતે સાબિત કરી શકાય તેવું છે તો તે અંતઃપ્રેરણાત્મક રીતે સાબિત કરી શકાય તેવું છે; સુસંગત/ભૌમિતિક સિદ્ધાંતોના ઘણા ઉદાહરણો છેઃ તમામ બીજગણિત સિદ્ધાંતો, જેમ કે જૂથ સિદ્ધાંત અને વીંટી સિદ્ધાંત, તમામ આવશ્યક રીતે બીજગણિત સિદ્ધાંતો, જેમ કે શ્રેણી સિદ્ધાંત, ક્ષેત્રોનો સિદ્ધાંત, સ્થાનિક વીંટીઓનો સિદ્ધાંત, જાળી સિદ્ધાંત, પ્રોજેક્ટિવ ભૂમિતિ, અલગથી બંધ સ્થાનિક વીંટીઓનો સિદ્ધાંત (ઉર્ફ "સખત રીતે હેન્સેલિયન સ્થાનિક વીંટીઓ") અને ટોર્શન અબેલિયન જૂથોના અનંત સિદ્ધાંત; સુસંગત/ભૌમિતિક સિદ્ધાંતો ટોપોઇ (મેકલેન અને મોર્ડિક 1992, પ્રકરણ X) વચ્ચેના ભૌમિતિક આકારવાદ સાથે પુલબેક દ્વારા સાચવવામાં આવે છે; એક નમૂનાના સમૂહમાં ફિલ્ટર કરેલ કોલિમિટ્સ C′D તર્ક પ્રોગ્રામિંગમાંથી હોર્ન કલમોનું સામાન્યીકરણ કરે છે, જ્યાં D એ અણુ હોવું જરૂરી છે; હકીકતમાં, તેઓ વિસંગત તર્ક કાર્યક્રમોની "કલમો" નું સામાન્યીકરણ કરે છે, જ્યાં D ને અણુઓનું વિચ્છેદન કરવાની મંજૂરી છે. સુસંગત સિદ્ધાંતો માટે અસરકારક પ્રમેય-પુરાવો, (ઠરાવના સંબંધમાં) સાપેક્ષ સરળતા અને સ્પષ્ટતા સાથે, સ્વચાલિત થઈ શકે છે. બેઝેમ અને અન્ય લોકોએ નોંધ્યું છે તેમ, સ્કોલેમાઈઝેશનની ગેરહાજરી (નવા કાર્ય પ્રતીકોની રજૂઆત) એ કોઈ વાસ્તવિક મુશ્કેલી નથી, અને ક્લોઝલ સ્વરૂપમાં બિન-રૂપાંતર સામાન્ય ગાણિતિક દલીલોની રચનાને વધુ સારી રીતે જાળવી રાખવાની મંજૂરી આપે છે. નોંધો ગ્રંથસૂચિ (બે ગ્રંથો, ઓક્સફર્ડ લોજિક ગાઈડ્સ 43 અને 44, તૈયારીમાં ત્રીજો ગ્રંથ) વધુ વાંચન ભૂમિતિ તર્કશાસ્ત્ર