Herbrandization
તાર્કિક સૂત્રનું હેરબ્રાન્ડાઇઝેશન (જેક્સ હેરબ્રાન્ડના નામ પરથી નામ આપવામાં આવ્યું છે) એ એક એવી રચના છે જે સૂત્રના સ્કોલેમાઇઝેશન સાથે બેવડી છે. થોરાલ્ફ સ્કોલેમે તેમના લોવેનહેમ-સ્કોલેમ પ્રમેય (સ્કોલેમ 1920) ના પુરાવાના ભાગરૂપે પ્રીનેક્સ સ્વરૂપમાં સૂત્રોના સ્કોલેમીઝેશનને ધ્યાનમાં લીધું હતું. હર્બ્રાન્ડે હર્બ્રાન્ડાઇઝેશનની આ બેવડી કલ્પના સાથે કામ કર્યું હતું, જે હર્બ્રાન્ડના પ્રમેય (હર્બ્રાન્ડ 1930) ને સાબિત કરવા માટે બિન-પ્રિનેક્સ સૂત્રોને પણ લાગુ કરવા માટે સામાન્યીકૃત કરવામાં આવ્યું હતું. પરિણામી સૂત્ર મૂળ સૂત્રની સમકક્ષ હોવું જરૂરી નથી. સ્કોલેમાઈઝેશનની જેમ, જે માત્ર સંતોષને જાળવી રાખે છે, હર્બ્રાન્ડાઈઝેશન સ્કોલેમાઈઝેશનની બેવડી માન્યતા જાળવી રાખે છેઃ પરિણામી સૂત્ર માન્ય છે જો અને માત્ર ત્યારે જ જો મૂળ સૂત્ર માન્ય હોય. વ્યાખ્યા અને ઉદાહરણો ચાલો પ્રથમ ક્રમના તર્કની ભાષામાં સૂત્ર બનીએ. આપણે ધારી શકીએ કે તેમાં કોઈ ચલ નથી કે જે બે અલગ અલગ પરિમાણો દ્વારા બંધાયેલ હોય, અને કોઈ ચલ બંધાયેલ અને મુક્ત બંને રીતે થતું નથી. (એટલે કે, આ શરતોને એવી રીતે સુનિશ્ચિત કરવા માટે પુનઃસ્થાપિત કરી શકાય છે કે પરિણામ એક સમકક્ષ સૂત્ર હોય). પછી તેનું હર્બ્રાન્ડાઇઝેશન નીચે પ્રમાણે મેળવવામાં આવે છેઃ પ્રથમ, કોઈપણ મુક્ત ચલને સ્થિર પ્રતીકો દ્વારા બદલો. બીજું, એવા ચલો પરના તમામ પરિમાણોને દૂર કરો કે જે ક્યાં તો (1) સાર્વત્રિક રીતે પરિમાણિત હોય અને નકારાત્મક સંકેતોની સમ સંખ્યાની અંદર હોય, અથવા (2) અસ્તિત્વમાં પ્રમાણબદ્ધ હોય અને નકારાત્મક સંકેતોની વિચિત્ર સંખ્યાની અંદર હોય. છેવટે, આવા દરેક ચલને કાર્ય પ્રતીક સાથે બદલો, જ્યાં એવા ચલ છે જે હજુ પણ પરિમાણિત છે, અને જેમના પરિમાણો સંચાલિત થાય છે. દાખલા તરીકે, સૂત્રનો વિચાર કરો. બદલવા માટે કોઈ મુક્ત ચલ નથી. ચલ એ પ્રકાર છે જેને આપણે બીજા પગલા માટે ધ્યાનમાં લઈએ છીએ, તેથી આપણે પરિમાણોને કાઢી નાખીએ છીએ અને. છેવટે, આપણે પછી અચળાંક સાથે બદલીએ છીએ (કારણ કે ત્યાં કોઈ અન્ય પરિમાણો સંચાલિત ન હતા), અને આપણે કાર્ય પ્રતીક સાથે બદલીએ છીએઃ સૂત્રનું સ્કોલેમાઈઝેશન એ જ રીતે મેળવવામાં આવે છે, સિવાય કે ઉપરના બીજા પગલામાં, આપણે ચલ પર પરિમાણો કાઢી નાખીશું જે ક્યાં તો (1) અસ્તિત્વમાં માત્રાત્મક અને નકારાત્મક સંખ્યાની સમ સંખ્યાની અંદર, અથવા (2) સાર્વત્રિક રીતે માત્રાત્મક અને નકારાત્મક સંખ્યાની વિચિત્ર સંખ્યાની અંદર છે. આમ, ઉપરથી તે જ ધ્યાનમાં લેતા, તેનું સ્કોલેમાઈઝેશન હશેઃ આ રચનાઓના મહત્વને સમજવા માટે, હર્બ્રાન્ડનો પ્રમેય અથવા લોવેનહેમ-સ્કોલેમ પ્રમેય જુઓ. આ પણ જુઓ પ્રિડિકેટ ફંકટર લોજિક રેફરન્સ સ્કોલેમ, ટી. "ગાણિતિક દરખાસ્તોની સંતોષકારકતા અથવા સાબિતતામાં લોજિકો-સંયુક્ત તપાસઃ એલ. લોવેનહેમ દ્વારા પ્રમેયનો સરળ પુરાવો અને પ્રમેયના સામાન્યીકરણ". (વેન હેઇજેનોર્ટ 1967 માં, 252-63.) હેરબ્રાન્ડ, જે. "પુરાવા સિદ્ધાંતમાં તપાસઃ સાચા પ્રસ્તાવોના ગુણધર્મો". (વેન હેઇજેનોર્ટ 1967 માં, 525-81.) વેન હેજેનોર્ટ, જે. ફ્રેજથી ગોડેલ સુધીઃ એ સોર્સ બુક ઇન મેથેમેટિકલ લોજિક, 1879-1931. હાર્વર્ડ યુનિવર્સિટી પ્રેસ, 1967. તર્ક સામાન્ય સ્વરૂપો (તર્ક)