Presburger aritmetika

Presburgerova aritmetika  je teorie prvního řádu popisující přirozená čísla se sčítáním , ale na rozdíl od Peanovy aritmetiky vylučuje tvrzení o násobení . Pojmenován po polském matematikovi Mojžeši Presburgerovi , který v roce 1929 navrhl odpovídající systém axiomů v logice prvního řádu a také ukázal jeho řešitelnost .

Axiomy

Presburgerův aritmetický jazyk zahrnuje konstanty 0, 1, jednu operaci + a predikát rovnosti =. Axiomy vypadají takto:

1. ¬ (0= x +1)
2. x + 1 = y + 1 → x = y
3. x + 0 = x
4. ( x + y ) + 1 = x + ( y + 1)
5. ( P (0) ∧ ( P ( x )→ P ( x + 1))) → P ( y ), kde P  je vzorec prvního řádu obsahující 0, 1, +, = a jednu volnou proměnnou x .

Je třeba poznamenat, že (5) ve skutečnosti není jediný axiom, ale axiomové schéma představující nekonečnou množinu axiomů, jeden pro každou formuli P . (5) je formalizací principu matematické indukce . Nelze jej ekvivalentně nahradit žádným konečným systémem axiomů. Presburgerova aritmetika tedy není s konečnou platností axiomatizovatelná .

Viz také

• Peano aritmetika
• Robinsonova aritmetika
• Logika prvního řádu

Literatura

• Cooper, DC, 1972, "Dokazování věty v aritmetice bez násobení" v B. Meltzer a D. Michie, eds., Machine Intelligence . Edinburgh University Press: 91-100.
• Ferrante, Jeanne a Charles W. Rackoff, 1979. Výpočetní složitost logických teorií . Poznámky k přednáškám z matematiky 718. Springer-Verlag .
• Fischer, MJ a Michael O. Rabin , 1974, "Superexponenciální složitost Presburgerovy aritmetiky. " Sborník příspěvků SIAM-AMS Symposium in Applied Mathematics Vol .
• G. Nelson a DC Oppen. "Zjednodušovač založený na efektivních rozhodovacích algoritmech"   // Proc . 5. sympozium ACM SIGACT-SIGPLAN o principech programovacích jazyků: časopis. — Apr. 1978. - str. 141-150 .
• Mojżesz Presburger , 1929, „Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem ​​​​die Addition als einzige Operation hervortritt“ v Comptes Rendus du I congrès de Mathématiciens des Pays Slaves . Warszawa: 92-101.
• Pugh, William, 1991, " Test Omega: rychlý a praktický algoritmus celočíselného programování pro analýzu závislostí, ".
• Reddy, ČR a DW Loveland, 1978, " Presburger Arithmetic with Bounded Quantifier Alternation. » ACM Symposium on Theory of Computing : 320-325.

• Vereščagin, Shene. Přednášky z matematické logiky a teorie algoritmů. — MTsNMO, 2002.

Odkazy

• Online-Proofer Java je applet , který kontroluje pravdivost Presburgerových aritmetických vzorců.  (Němec)