Primitiv rekursiv setfunktion - Primitive recursive set function

I matematik är primitiva rekursiva setfunktioner eller primitiva rekursiva ordinalfunktioner analoger till primitiva rekursiva funktioner , definierade för uppsättningar eller ordinaler snarare än naturliga tal. De introducerades av Jensen & Karp (1971) .

Definition

En primitiv rekursiv setfunktion är en funktion från uppsättningar till uppsättningar som kan erhållas från följande grundfunktioner genom att upprepade gånger tillämpa följande regler för substitution och rekursion:

De grundläggande funktionerna är:

• Projektion: P _{n , m} ( x ₁ , ..., x _n ) = x _m
• Noll: F ( x ) = 0
• Angränsar ett element till en uppsättning : F ( x , y ) = x ∪ { y }
• Testa medlemskap: C ( x , y , u , v ) = x om u ∈ v , y annars.

Reglerna för att generera nya funktioner genom substitution är

• F ( x , y ) = G ( x , H ( x ), y )
• F ( x , y ) = G ( H ( x ), y )

där x och y är ändliga sekvenser av variabler.

Regeln för att generera nya funktioner genom rekursion är

• F ( z , x ) = G (∪ _{u ∈ z} F ( u , x ), z , x )

En primitiv rekursiv ordinalfunktion definieras på samma sätt, förutom att den initiala funktionen F ( x , y ) = x ∪ { y } ersätts av F ( x ) = x ∪ { x } (efterföljaren av x ). De primitiva rekursiva ordinalfunktionerna är desamma som de primitiva rekursiva uppsättningsfunktionerna som mappar ordinaler till ordinaler.

Man kan också lägga till fler initialfunktioner för att få en större klass av funktioner. Exempelvis är ordinalfunktionen ω ^α inte primitiv rekursiv, eftersom den konstanta funktionen med värdet ω (eller någon annan oändlig uppsättning) inte är primitiv rekursiv, så man kanske vill lägga till denna konstantfunktion till de initiala funktionerna.

referenser

• Jensen, Ronald B .; Karp, Carol (1971), "Primitiva rekursiva setfunktioner", Axiomatic Set Theory , Proc. Sympos. Pure Math., XIII, Del I, Providence, RI: Amer. Matematik. Soc., S. 143–176, ISBN  9780821802458 , MR  0281602