Primitiv rekursiv funktion - Primitive recursive function

I beräkningsteorin är en primitiv rekursiv funktion grovt sett en funktion som kan beräknas av ett datorprogram vars slingor alla är "för" -slingor (det vill säga en övre gräns för antalet iterationer för varje slinga kan bestämmas innan man går in i slinga). Primitiva rekursiva funktioner utgör en strikt delmängd av de allmänna rekursiva funktionerna som också är totala funktioner .

Betydelsen av primitiva rekursiva funktioner ligger i det faktum att de flesta beräkningsbara funktioner som studeras i talteori (och mer allmänt i matematik) är primitiva rekursiva. Till exempel är addition och division , den faktoriella och exponentiella funktionen och funktionen som returnerar n: e primtalet alla primitiva rekursiva. För att visa att en beräkningsbar funktion är primitiv rekursiv räcker det faktiskt med att visa att dess tidskomplexitet begränsas ovan av en primitiv rekursiv funktion av ingångsstorleken. Av detta följer att det är svårt att utforma en beräkningsbar funktion som inte är primitiv rekursiv, även om vissa är kända (se § Begränsningar nedan).

Uppsättningen primitiva rekursiva funktioner är känd som PR i beräkningskomplexitetsteori .

Definition

De primitiva rekursiva funktionerna är bland de talteoretiska funktionerna, som är funktioner från de naturliga talen (icke-negativa heltal) {0, 1, 2, ...} till de naturliga talen. Dessa funktioner tar n argument för ett naturligt tal n och kallas n - ary .

De primitiva primitiva rekursiva funktionerna ges av dessa axiom :

  1. Konstant funktion : 0-arets konstanta funktion 0 är primitiv rekursiv.
  2. Efterföljarfunktion : Den 1-ariga efterföljarfunktionen S , som returnerar efterföljaren till sitt argument (se Peano-postulat ), är primitiv rekursiv. Det vill säga S ( k ) = k + 1.
  3. Projektionsfunktion : Ett par i ≥1 och ni , definierar en n -ary -funktion: P i n ( x 1 , ..., x n ) = x i , en sådan funktion är primitiv rekursiv.

Mer komplexa primitiva rekursiva funktioner kan erhållas genom att tillämpa operationerna som ges av dessa axiom:

  1. Sammansättning : Med tanke på en k -ary primitiv rekursiv funktion f , och k antal m -ary primitiva rekursiva funktioner g 1 , ..., g k , sammansättningen av f med g 1 , ..., g k , dvs m -ary funktion är primitiv rekursiv.

Exempel. Vi tar f ( x ) som S ( x ) definierat ovan. Denna f är en 1-ary primitiv rekursiv funktion. Och så är g ( x ) = S ( x ). Så h ( x ) definierat som f ( g ( x )) = S ( S ( x )) är också en primitiv rekursiv 1-ary-funktion. Informellt sett är h ( x ) funktionen som förvandlar x till x +2.

  1. Primitiv rekursion : Med tanke på f , en k -ary primitiv rekursiv funktion, och g , en ( k +2) -ary primitiv rekursiv funktion, definieras ( k +1) -ary-funktionen h som den primitiva rekursionen av f och g , dvs funktionen h är primitiv rekursiv när

Exempel. Antag att f ( x ) = P 1 1 ( x ) = x och g ( x , y , z ) = S ( P 2 3 ( x , y , z )) = S ( y ). Sedan är h (0, x ) = x och h ( S ( y ), x ) = g ( y , h ( y , x ), x ) = S ( h ( y , x )). Nu h (0,1) = 1, h (1,1) = S ( h (0,1)) = 2, h (2,1) = S ( h (1,1)) = 3. Denna h är en 2-arig primitiv rekursiv funktion. Vi kan kalla det "tillägg".

Tolkning. Funktionen h fungerar som en for loop från 0 upp till värdet av dess första argument. Resten av argumenten för h , betecknade här med x i ( i = 1, ..., k ), är en uppsättning initiala villkor för For -slingan som kan användas av den under beräkningar men som inte kan ändras av den. Funktionerna f och g på höger sida av ekvationerna som definierar h representerar slingans kropp, som utför beräkningar. Funktion f används bara en gång för att utföra inledande beräkningar. Beräkningar för efterföljande steg i slingan utförs av g . Den första parametern för g matas med det "aktuella" värdet för For loop -indexet. Den andra parametern av g matas resultatet av For -loopens tidigare beräkningar, från tidigare steg. Resten av parametrarna för g är de oföränderliga initiala förhållandena för For -slingan som nämnts tidigare. De kan användas av g för att utföra beräkningar men de kommer inte själva att ändras av g .

De primitiva rekursiva funktionerna är de grundläggande funktionerna och de som erhålls från de grundläggande funktionerna genom att tillämpa dessa operationer ett begränsat antal gånger.

Projektionsfunktionernas roll

Projektionsfunktionerna kan användas för att undvika uppenbar styvhet när det gäller arten av funktionerna ovan; genom att använda kompositioner med olika projektionsfunktioner är det möjligt att överföra en delmängd av argumenten för en funktion till en annan funktion. Till exempel, om g och h är 2-ariga primitiva rekursiva funktioner då

är också primitiv rekursiv. En formell definition som använder projektionsfunktioner är

Svag primitiv rekursion

Föregångarfunktionen på en plats är primitiv rekursiv. Det följer omedelbart av startfunktionerna S och P 1 2 genom regeln om primitiv rekursion. Fischer, Fischer & Beigel tog bort den implicita föregångaren från rekursionsregeln och ersatte den med den svagare regeln

De bevisade att föregångarfunktionen fortfarande kunde definieras, och därför "svag" primitiv rekursion definierar också de primitiva rekursiva funktionerna.

Konvertering av predikat till numeriska funktioner

I vissa inställningar är det naturligt att överväga primitiva rekursiva funktioner som tar in ingångar som blandar tal med sanningsvärden (det är t för sant och f för falskt), eller som producerar sanningvärden som utgångar. Detta kan åstadkommas genom att identifiera sanningsvärdena med siffror på något fast sätt. Till exempel är det vanligt att identifiera sanningsvärdet t med siffran 1 och sanningsvärdet f med talet 0. När denna identifiering har gjorts kan den karakteristiska funktionen för en uppsättning A , som alltid returnerar 1 eller 0, vara ses som ett predikat som berättar om ett nummer är i uppsättningen A . En sådan identifiering av predikat med numeriska funktioner kommer att antas för resten av denna artikel.

Datorspråk definition

Ett exempel på ett primitivt rekursivt programmeringsspråk är ett som innehåller grundläggande aritmetiska operatorer (t.ex. + och-, eller LÄGG TILL och SUBTRAKT), villkor och jämförelse (OM-DÅ, LIK, Mindre än) och begränsade slingor, t.ex. för slinga , där det finns en känd eller beräknbar övre gräns för alla slingor (FOR i FRÅN 1 TILL n, med varken i eller n som kan ändras av slingkroppen). Inga kontrollstrukturer av större allmänhet, till exempel medan loopar eller IF-THEN plus GOTO , tillåts i ett primitivt rekursivt språk.

Den LOOP språk , som infördes i en 1967 artikel av Albert R. Meyer och Dennis M. Ritchie , är ett sådant språk. Dess datorkraft sammanfaller med de primitiva rekursiva funktionerna. En variant av LOOP språket är Douglas Hofstadter s Bloop i Gödel, Escher, Bach . Att lägga till obegränsade loopar (WILE, GOTO) gör språket allmänt rekursivt och Turing-komplett , liksom alla verkliga datorprogrammeringsspråk.

Definitionen av primitiva rekursiva funktioner innebär att deras beräkning stannar vid varje ingång (efter ett begränsat antal steg). Å andra sidan, den stopproblemet är oavgörbara för allmän rekursiva funktioner, även om de är total . Det vill säga det finns program som stoppar varje ingång, men för vilka detta inte kan verifieras av en algoritm.

Exempel

De flesta talteoretiska funktioner som kan definieras med rekursion på en enda variabel är primitiva rekursiva. Grundläggande exempel inkluderar additions- och avkortade subtraktionsfunktioner .

Tillägg

Intuitivt kan tillägg definieras rekursivt med reglerna:

,

För att passa in i en strikt primitiv rekursiv definition definierar du:

Här S ( n ) är "efterföljaren till n " (dvs., n 1), P 1 1 är identitetsfunktionen , och P 2 3 är utsprånget funktionen som tar 3 argument och returnerar den andra en. Funktioner f och g som krävs av ovanstående definition av den primitiva rekursion operationen är respektive spelas av P 1 1 och sammansättningen av S och P 2 3 .

Subtraktion

Eftersom primitiva rekursiva funktioner använder naturliga tal snarare än heltal, och de naturliga talen inte stängs under subtraktion, studeras en stympad subtraktionsfunktion (även kallad "korrekt subtraktion") i detta sammanhang. Denna begränsade subtraktionsfunktion sub ( a , b ) [eller ba ] returnerar b - a om detta inte är negativt och returnerar 0 annars.

Den föregångare Funktionen fungerar som motsatsen till efterträdare funktionen och rekursivt definieras av regler:

föregående (0) = 0,
pred ( n + 1) = n .

Dessa regler kan omvandlas till en mer formell definition genom primitiv rekursion:

föregående (0) = 0,
pred (S ( n )) = P 1 2 ( n , pred ( n )).

Den begränsade subtraktionsfunktionen är definierbar från föregångarfunktionen på ett sätt som är analogt med hur tillägg definieras från efterföljaren:

sub (0, x ) = P 1 1 ( x ),
sub (S ( n ), x ) = pred ( P 2 3 ( n , sub ( n , x ), x )).

Här motsvarar sub ( a , b ) ba ; För enkelhetens skull har argumentens ordning ändrats från "standard" -definitionen för att passa kraven på primitiv rekursion. Detta kan lätt åtgärdas med hjälp av komposition med lämpliga utsprång.

Andra operationer på naturliga tal

Exponentiering och primitetstest är primitiva rekursiva. Med tanke på primitiva rekursiva funktioner e , f , g och h , är en funktion som returnerar värdet av g när ef och värdet av h annars primitivt rekursivt.

Operationer på heltal och rationella tal

Genom att använda Gödel -numreringar kan de primitiva rekursiva funktionerna utökas för att fungera på andra objekt som heltal och rationella tal . Om heltal kodas av Gödel -tal på ett standard sätt är de aritmetiska operationerna inklusive addition, subtraktion och multiplikation primitiva rekursiva. På samma sätt, om rationalerna representeras av Gödel -tal, är fältoperationerna alla primitiva rekursiva.

Använd i första ordningens Peano-aritmetik

I första ordningens Peano-aritmetik finns det oändligt många variabler (0-ary-symboler) men inga k-ary- icke-logiska symboler med k> 0 andra än S, +, *och ≤. För att definiera primitiva rekursiva funktioner måste man således använda följande trick av Gödel.

Genom att använda en Gödel -numrering för sekvenser , till exempel Gödel's β -funktion , kan alla ändliga talföljder kodas av ett enda tal. Ett sådant tal kan därför representera den primitiva rekursiva funktionen tills ett givet n.

Låt h vara en 1-ary primitiv rekursionsfunktion definierad av:

där C är en konstant och g är en redan definierad funktion.

Med hjälp av Godels β -funktion, för alla sekvenser av naturliga tal (k 0 , k 1 ,…, k n ), finns det naturliga tal b och c så att för varje i ≤ n, β (b, c, i) = k i . Vi kan således använda följande formel för att definiera h ; mer exakt, m = h ( n ) är en stenografi för följande:

och ekvationen till g , som redan är definierad, är i själva verket stenografi för någon annan redan definierad formel (liksom β, vars formel ges här ).

Generaliseringen till någon k-ary primitiv rekursionsfunktion är trivial.

Förhållande till rekursiva funktioner

Den bredare klassen av partiella rekursiva funktioner definieras genom att introducera en obegränsad sökoperator . Användningen av denna operatör kan resultera i en partiell funktion , det vill säga en relation med högst ett värde för varje argument, men behöver inte nödvändigtvis ha något värde för något argument (se domän ). En motsvarande definition säger att en partiell rekursiv funktion är en som kan beräknas av en Turing -maskin . En total rekursiv funktion är en partiell rekursiv funktion som definieras för varje ingång.

Varje primitiv rekursiv funktion är total rekursiv, men inte alla totala rekursiva funktioner är primitiva rekursiva. Den Ackermann-funktionen A ( m , n ) är ett välkänt exempel på en total rekursiv funktion (i själva verket bevisbara totalt), som inte är primitivt rekursiv. Det finns en karakterisering av de primitiva rekursiva funktionerna som en delmängd av de totala rekursiva funktionerna med hjälp av Ackermann -funktionen. Denna karakterisering säger att en funktion är primitiv rekursiv om och bara om det finns ett naturligt tal m så att funktionen kan beräknas av en Turing -maskin som alltid stannar inom A ( m , n ) eller färre steg, där n är summan av argumenten för den primitiva rekursiva funktionen.

En viktig egenskap hos de primitiva rekursiva funktionerna är att de är en rekursivt uppräkningsbar delmängd av uppsättningen av alla totala rekursiva funktioner (vilket inte i sig är rekursivt räknbart). Detta innebär att det finns en enda beräkningsbar funktion f ( m , n ) som räknar upp de primitiva rekursiva funktionerna, nämligen:

  • För varje primitiv rekursiv funktion g finns det en m så att g ( n ) = f ( m , n ) för alla n , och
  • För varje m är funktionen h ( n ) = f ( m , n ) primitiv rekursiv.

f kan uttryckligen konstrueras genom att iterativt upprepa alla möjliga sätt att skapa primitiva rekursiva funktioner. Således är det bevisligen totalt. Man kan använda ett diagonaliseringsargument för att visa att f inte är rekursivt primitivt i sig: hade det varit så skulle h ( n ) = f ( n , n ) +1 vara. Men om detta motsvarar någon primitiv rekursiv funktion finns det en m så att h ( n ) = f ( m , n ) för alla n , och sedan h ( m ) = f ( m , m ), vilket leder till motsägelse.

Uppsättningen av primitiva rekursiva funktioner är emellertid inte den största rekursivt uppräkningsbara delmängden av uppsättningen av alla totala rekursiva funktioner. Till exempel är uppsättningen av bevisligen totala funktioner (i Peano -aritmetik) också rekursivt uppräknelig, eftersom man kan räkna upp alla bevis för teorin. Även om alla primitiva rekursiva funktioner bevisligen är totala, är det motsatta inte sant.

Begränsningar

Primitiva rekursiva funktioner tenderar att överensstämma mycket nära vår intuition om vad en beräkningsbar funktion måste vara. Förvisso är de initiala funktionerna intuitivt beräkningsbara (i sin enkelhet), och de två operationer genom vilka man kan skapa nya primitiva rekursiva funktioner är också mycket okomplicerade. Uppsättningen primitiva rekursiva funktioner inkluderar dock inte alla möjliga totala beräkningsbara funktioner - detta kan ses med en variant av Cantors diagonala argument . Detta argument ger en total beräkningsbar funktion som inte är primitiv rekursiv. En skiss av beviset är följande:

De primitiva rekursiva funktionerna i ett argument (dvs. unary -funktioner) kan räknas upp beräknat . Denna uppräkning använder definitionerna av de primitiva rekursiva funktionerna (som i huvudsak bara är uttryck med kompositionen och primitiva rekursionsoperationer som operatorer och de grundläggande primitiva rekursiva funktionerna som atomer), och kan antas innehålla varje definition en gång, även om samma funktion kommer att förekomma många gånger på listan (eftersom många definitioner definierar samma funktion; helt enkelt att komponera av identitetsfunktionen genererar oändligt många definitioner av någon primitiv rekursiv funktion). Detta innebär att den n: e definitionen av en primitiv rekursiv funktion i denna uppräkning effektivt kan bestämmas utifrån n . Om man använder någon Gödel -numrering för att koda definitioner som tal, beräknas denna n -tionde definition i listan av en primitiv rekursiv funktion av n . Låt f n beteckna den unära primitiva rekursiva funktionen som ges av denna definition.

Definiera nu "utvärderingsfunktionen" ev med två argument, av ev ( i , j ) = f i ( j ) . Klart ev är total och beräkningsbar, eftersom man effektivt kan bestämma definitionen av f i , och att vara en primitiv rekursiv funktion f i sig själv är total och beräkningsbar, så f i ( j ) definieras alltid och effektivt beräkningsbar. Ett diagonalt argument visar dock att funktionen ev för två argument inte är primitiv rekursiv.

Antag att ev var primitiv rekursiv, då skulle den unära funktionen g definierad av g ( i ) = S ( ev ( i , i )) också vara primitiv rekursiv, eftersom den definieras av kompositionen från efterföljarfunktionen och ev . Men då förekommer g i uppräkningen, så det finns ett tal n så att g = f n . Men nu ger g ( n ) = S ( ev ( n , n )) = S ( f n ( n )) = S ( g ( n )) en motsättning.

Detta argument kan tillämpas på alla klasser av beräkningsbara (totala) funktioner som kan räknas upp på detta sätt, som förklaras i artikeln Maskin som alltid stannar . Observera dock att de delvis beräkningsbara funktionerna (de som inte behöver definieras för alla argument) uttryckligen kan räknas upp, till exempel genom att räkna upp Turing -maskinkodningar.

Andra exempel på totala rekursiva men inte primitiva rekursiva funktioner är kända:

Några vanliga primitiva rekursiva funktioner

Följande exempel och definitioner är från Kleene (1952) s. 223–231 - många visas med bevis. De flesta förekommer också med liknande namn, antingen som bevis eller som exempel, i Boolos-Burgess-Jeffrey 2002 s. 63–70; de lägger till logaritmen lo (x, y) eller lg (x, y) beroende på den exakta härledningen.

I det följande observerar vi att primitiva rekursiva funktioner kan vara av fyra typer:

  1. kortfattade funktioner : "talteoretiska funktioner" från {0, 1, 2, ...} till {0, 1, 2, ...},
  2. predikat : från {0, 1, 2, ...} till sanningsvärden {t = true, f = false},
  3. propositionella anslutningar : från sanningsvärden {t, f} till sanningsvärden {t, f},
  4. representerar funktioner : från sanningsvärden {t, f} till {0, 1, 2, ...}. Många gånger kräver ett predikat en representativ funktion för att konvertera predikatets utsignal {t, f} till {0, 1} (notera ordningen "t" till "0" och "f" till "1" matchar med ~ sg () definierat Nedan). Per definition är en funktion φ ( x ) en "representerande funktion" för predikatet P ( x ) om φ endast tar värden 0 och 1 och producerar 0 när P är sant ".

I det följande är märket "'", t.ex. a', det primitiva märket som betyder "efterträdaren till", vanligtvis tänkt som "+1", t.ex. en +1 = def a '. Funktionerna 16-20 och #G är av särskilt intresse när det gäller att konvertera primitiva rekursiva predikat till och extrahera dem från deras "aritmetiska" form uttryckt som Gödel-tal .

  1. Tillägg: a+b
  2. Multiplikation: a × b
  3. Exponentiering: a b
  4. Faktorisk a! : 0! = 1, a '! = a! × a '
  5. pred (a): (Föregångare eller minskning): Om a> 0 då a-1 annars 0
  6. Korrekt subtraktion a ∸ b: Om a ≥ b då ab annars 0
  7. Lägsta (a 1 , ... a n )
  8. Maximal (a 1 , ... a n )
  9. Absolut skillnad: | ab | = def (a ∸ b) + (b ∸ a)
  10. ~ sg (a): NOT [signum (a)]: Om a = 0 då 1 annat 0
  11. sg (a): signum (a): Om a = 0 då 0 annars 1
  12. en | b: (a delar b): Om b = k × a för några k då 0 annars 1
  13. Resten (a, b): resterna om b inte delar en "jämnt". Kallas även MOD (a, b)
  14. a = b: sg | a - b | (Kleenes konvention var att representera sant med 0 och falskt med 1; för närvarande, särskilt i datorer, är den vanligaste konventionen omvänd, nämligen att representera sant med 1 och falskt med 0, vilket innebär att sg till ~ sg ändras här och i nästa artikel)
  15. a <b: sg (a '∸ b)
  16. Pr (a): a är ett primtal Pr (a) = def a> 1 & NOT (existerar c) 1 <c <a [c | a]
  17. p i : i+1-st primtal
  18. (a) i : exponent för p i i: det unika x så att p i x | a & NOT (p i x ' | a)
  19. lh (a): "längden" eller antalet icke-försvinnande exponenter i a
  20. lo (a, b): (logaritm av a till bas b): Om a, b> 1 då den största x så att b x | en annan 0
I det följande är förkortningen x = def x 1 , ... x n ; prenumerationer kan tillämpas om betydelsen kräver det.
  • #A: En funktion φ som definieras uttryckligen från funktioner Ψ och konstanter q 1 , ... q n är primitiv rekursiv i Ψ.
  • #B: Den ändliga summan Σ y <z ψ ( x , y) och produkten Π y <z ψ ( x , y) är primitiva rekursiva i ψ.
  • #C: Ett predikat P erhållet genom att ersätta funktionerna χ 1 , ..., χ m för respektive variabler i ett predikat Q är primitivt rekursivt i χ 1 , ..., χ m , Q.
  • #D: Följande predikat är primitiva rekursiva i Q och R:
  • NOT_Q ( x ).
  • Q ELLER R: Q ( x ) VR ( x ),
  • Q OCH R: Q ( x ) & R ( x ),
  • Q IMPLIES R: Q ( x ) → R ( x )
  • Q motsvarar R: Q ( x ) ≡ R ( x )
  • #E: Följande predikat är primitiva rekursiva i predikatet R:
  • (Ey) y <z R ( x , y) där (Ey) y <z betecknar "det finns minst ett y som är mindre än z så att"
  • (y) y <z R ( x , y) där (y) y <z betecknar "för alla y mindre än z är det sant att"
  • μy y <z R ( x , y). Operatören μy y <z R ( x , y) är en begränsad form av den så kallade minimerings- eller mu-operatoren : Definieras som "det minsta värdet av y mindre än z så att R ( x , y) är sant; eller z om det inte finns något sådant värde. "
  • #F: Definition av fall: Funktionen som definieras så, där Q 1 , ..., Q m är ömsesidigt uteslutande predikat (eller "ψ ( x ) ska ha det värde som ges av den första klausulen som gäller), är primitiv rekursiv i φ 1 , ..., Q 1 , ... Q m :
φ ( x ) =
  • φ 1 ( x ) om Q 1 ( x ) är sant,
  • . . . . . . . . . . . . . . . . . . .
  • φ m ( x ) om Q m ( x ) är sant
  • φ m+1 ( x ) annars
  • #G: Om φ uppfyller ekvationen:
φ (y, x ) = χ (y, COURSE-φ (y; x 2 , ... x n ), x 2 , ... x n då φ är primitivt rekursivt i χ. Värdet COURSE-φ (y ; x 2 till n ) i funktionen kurs-av-värden kodar sekvensen av värden φ (0, x 2 till n ), ..., φ (y-1, x 2 till n ) för den ursprungliga funktionen.

Ytterligare primitiva rekursiva former

Några ytterligare former av rekursion definierar också funktioner som faktiskt är primitiva rekursiva. Definitioner i dessa former kan vara lättare att hitta eller mer naturliga för att läsa eller skriva. Kurs-av-värden rekursion definierar primitiva rekursiva funktioner. Vissa former av ömsesidig rekursion definierar också primitiva rekursiva funktioner.

De funktioner som kan programmeras i programmeringsspråket LOOP är exakt de primitiva rekursiva funktionerna. Detta ger en annan karakterisering av kraften i dessa funktioner. Den huvudsakliga begränsningen för LOOP-språket, jämfört med ett Turing-komplett språk , är att i LOOP-språket anges antalet gånger som varje loop ska köras innan slingan börjar köras.

Finitism och konsekvensresultat

De primitiva rekursiva funktionerna är nära besläktade med matematisk finitism , och används i flera sammanhang i matematisk logik där ett särskilt konstruktivt system önskas. Primitiv rekursiv aritmetik (PRA), ett formellt axiomsystem för de naturliga talen och de primitiva rekursiva funktionerna på dem, används ofta för detta ändamål.

PRA är mycket svagare än Peano -aritmetik , vilket inte är ett finitistiskt system. Ändå kan många resultat i talteori och bevisteori bevisas i PRA. Till exempel kan Gödels ofullständighetsteorem formaliseras till PRA, vilket ger följande sats:

Om T är en teori om aritmetiska uppfyller vissa hypoteser, med Gödel meningen G T , därefter PRA bevisar implikationen Con ( T ) → G T .

På samma sätt kan många av de syntaktiska resultaten i bevisteori bevisas i PRA, vilket innebär att det finns primitiva rekursiva funktioner som utför motsvarande syntaktiska transformationer av bevis.

I bevisteori och uppsättningsteori finns det ett intresse för finitistiska konsistensbevis , det vill säga konsistensbevis som själva är finitistiskt acceptabla. En sådan korrektur upprättar att konsistensen hos en teori T innebär konsistensen av en teori S genom att producera en primitiv rekursiv funktion som kan förvandla några bevis för en inkonsekvens från S till ett bevis på en inkonsekvens från T . En tillräcklig förutsättning för att ett konsekvensbevis ska vara finitistiskt är förmågan att formalisera det i PRA. Till exempel kan många konsekvenser resultera i uppsättningsteori som erhålls genom att tvinga omformuleras som syntaktiska bevis som kan formaliseras i PRA.

Historia

Rekursiva definitioner hade använts mer eller mindre formellt i matematik tidigare, men konstruktionen av primitiv rekursion spåras tillbaka till Richard Dedekinds sats 126 i hans Was sind und was sollen die Zahlen? (1888). Detta arbete var det första som gav ett bevis på att en viss rekursiv konstruktion definierar en unik funktion.

Primitiv rekursiv aritmetik föreslogs först av Thoralf Skolem 1923.

Den nuvarande terminologin myntades av Rózsa Péter (1934) efter att Ackermann 1928 bevisat att den funktion som idag är uppkallad efter honom inte var primitiv rekursiv, en händelse som föranledde behovet av att byta namn på det som fram till dess helt enkelt kallades rekursiva funktioner.

Se även

Anteckningar

Referenser