Stratifiering (matematik)

Stratifiering har flera användningsområden i matematik.

I matematisk logik

I matematisk logik är stratifiering varje konsekvent tilldelning av siffror till predikatsymboler som garanterar att det finns en unik formell tolkning av en logisk teori. Specifikt säger vi att en uppsättning satser av formen ${\displaystyle Q_{1}\wedge \dots \wedge Q_{ n}\wedge \neg Q_{n+1}\wedge \dots \wedge \neg Q_{n+m}\rightarrow P} är stratifierad om och endast om det finns en stratifieringstilldelning$ S som uppfyller följande villkor:

1. Om ett predikat P är positivt härlett från ett predikat Q (dvs P är huvudet på en regel och Q förekommer positivt i samma regel), måste stratifieringstalet för P vara större än eller lika med stratifieringen antal Q, kort sagt $S(P)\geq S(Q)$ .
2. Om ett predikat P härleds från ett negerat predikat Q (dvs. P är huvudet på en regel och Q förekommer negativt i samma regel), måste stratifieringstalet för P vara större än stratifieringstalet för Q , i korthet $S(P)>S(Q)$ .

Begreppet stratifierad negation leder till en mycket effektiv operativ semantik för stratifierade program i termer av den stratifierade minsta fixpunkten, som erhålls genom att iterativt applicera fixpointoperatorn på varje stratum av programmet, från det lägsta uppåt. Stratifiering är inte bara användbar för att garantera unik tolkning av Horn-klausulteorier .

I en specifik mängdlära

I New Foundations (NF) och relaterade mängdteorier sägs en formel ${\displaystyle \phi } på första ordningens logiks språk med likhet och medlemskap vara$ stratifierad om och endast om det finns en funktion $\ sigma$ som skickar varje variabel som förekommer i $\phi$ (betraktad som en syntaxpost) till ett naturligt tal (detta fungerar lika bra om alla heltal används) på ett sådant sätt att vilken atomformel som helst ${ \displaystyle x\in y}$ som visas i $\phi$ uppfyller $\sigma (x)+1=\sigma (y)$ och valfri atomformel $x=y$ som visas i $\phi$ uppfyller $\sigma (x)=\sigma (y)$ .

Det visar sig att det räcker att kräva att dessa villkor är uppfyllda endast när båda variablerna i en atomformel är bundna i mängden abstrakt { $\displaystyle \{x\mid \phi \}}$ under övervägande. En uppsättning abstrakt som uppfyller detta svagare villkor sägs vara svagt stratifierad .

Stratifieringen av New Foundations generaliserar lätt till språk med fler predikat och med termkonstruktioner. Varje primitivt predikat måste ha specificerade nödvändiga förskjutningar mellan värden på $\sigma$ vid dess (bundna) argument i en (svagt) stratifierad formel. I ett språk med termkonstruktioner måste termerna i sig tilldelas värden under ${\displaystyle \sigma } ,$ med fasta förskjutningar från värdena för vart och ett av deras (bundna) argument i en (svagt) stratifierad formel. Definierade termkonstruktioner hanteras snyggt genom att (möjligen bara implicit) använda teorin om beskrivningar: en term $(\iota x.\phi )$ (xet så att $\phi$ ) måste tilldelas samma värde under $\sigma$ som variabeln x.

En formel är stratifierad om och endast om det är möjligt att tilldela typer till alla variabler som förekommer i formeln på ett sådant sätt att det blir meningsfullt i en version TST av teorin om typer som beskrivs i New Foundations-artikeln, och detta är förmodligen det bästa sättet att förstå skiktningen av New Foundations i praktiken.

Begreppet stratifiering kan utvidgas till lambdakalkylen ; detta finns i tidningar av Randall Holmes.

En motivering för användningen av stratifiering är att ta itu med Russells paradox , den antinomin som anses ha underminerat Freges centrala verk Grundgesetze der Arithmetik (1902).   Quine, Willard Van Orman (1963) [1961]. Ur en logisk synvinkel (2:a upplagan). New York: Harper & Row . sid. 90. LCCN 61-15277 .

I topologi

Huvudartikel: Stratifierat utrymme

I singularitetsteorin finns det en annan innebörd, av en nedbrytning av ett topologiskt utrymme X i osammanhängande delmängder som var och en är en topologisk mångfald (så att i synnerhet en stratifiering definierar en uppdelning av det topologiska rummet). Detta är inte ett användbart begrepp när det är obegränsat; men när de olika skikten definieras av någon igenkännbar uppsättning villkor (till exempel att de är lokalt stängda ) och passar ihop hanterbart, tillämpas denna idé ofta i geometri. Hassler Whitney och René Thom definierade först formella villkor för stratifiering. Se Whitney stratifiering och topologiskt stratifierat utrymme .

I statistiken

Se stratifierad provtagning .