Beslutbarhet av första ordningens teorier om de reella talen

Inom matematisk logik är ett första ordningens språk av de reella talen mängden av alla välformade meningar av första ordningens logik som involverar universella och existentiella kvantifierare och logiska kombinationer av likheter och ojämlikheter i uttryck över reella variabler. Motsvarande första ordningens teori är den uppsättning meningar som faktiskt är sanna för de reella talen. Det finns flera olika sådana teorier, med olika uttryckskraft, beroende på vilka primitiva operationer som får användas i uttrycket. En grundläggande fråga i studiet av dessa teorier är om de är avgörbara : det vill säga, finns det en algoritm som kan ta en mening som indata och producera ett svar "ja" eller "nej" på frågan om meningen är sant i teorin.

Teorin om verkliga slutna fält är teorin där de primitiva operationerna är multiplikation och addition; detta innebär att i denna teori är de enda talen som kan definieras de reella algebraiska talen . Som bevisats av Tarski är denna teori avgörbar; se Tarski–Seidenbergs teorem och kvantifierareliminering . Nuvarande implementeringar av beslutsförfaranden för teorin om verkliga slutna fält är ofta baserade på kvantifierareliminering genom cylindrisk algebraisk nedbrytning .

Tarskis exponentialfunktionsproblem rör utvidgningen av denna teori till en annan primitiv operation, exponentialfunktionen . Det är ett öppet problem huruvida denna teori är avgörbar, men om Schanuels gissningar håller så skulle avgörbarheten av denna teori följa. Däremot är utvidgningen av teorin om verkliga slutna fält med sinusfunktionen obeslutbar eftersom detta tillåter kodning av den obestämbara teorin om heltal (se Richardsons teorem ) .

Ändå kan man hantera det oavgjorda fallet med funktioner som sinus genom att använda algoritmer som inte nödvändigtvis alltid avslutas. I synnerhet kan man designa algoritmer som endast krävs för att avsluta för indataformler som är robusta , det vill säga formler vars tillfredsställbarhet inte ändras om formeln är något störd. Alternativt är det också möjligt att använda rent heuristiska metoder.

Se även

• Konstruktion av de reella talen – Axiomatiska definitioner av de reella talen
• Tarskis axiomatisering av verkligheten