Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

Арифметика Прессбургера це теорія першого порядку яка описує натуральні числа з додаванням але на відміну від арифметики

Арифметика Пресбургера

Арифметика Пресбургера

Арифметика Прессбургера — це теорія першого порядку яка описує натуральні числа з додаванням, але на відміну від арифметики Пеано, виключає висловлювання щодо множення. Названа в честь польського математика , котрий в 1929 році запропонував відповідну систему аксіом в логіці першого порядку, а також показав її .

У цьому розділі ми описуємо вирази безлічі [1] [ 24 вересня 2015 у Wayback Machine.] в . Відзначимо відразу ж, що з такою сигнатурою елімінація кванторів неможлива. Справді, формула [2] [ 24 вересня 2015 у Wayback Machine.], справжня для парних Х , не є еквівалентною ніякої бескванторной формули. Тому нам потрібно, перш ніж проводити елімінацію кванторів, розширити сигнатуру. Наведений приклад формули підказує, яке розширення нам необхідно. Розглянемо рахункове сімейство двомісних предикатних символів 2″′, 3″′, 4″′,.... Символ С″′  буде інтерпретуватися як рівність по модулю С. Іншими словами, формула Х буде істинною в нашій інтерпретації, якщо  порівняти з по модулю  (залишки по модулю  рівні;  кратно).

Важливо мати на увазі, що індекс  в  не є змінною: у нас не триміснийпредикат, а рахункове сімейство двомісних предикатів.

Таке розширення не міняє класу виразність предикатів, оскільки, наприклад,  можна виразити як [3] [ 24 вересня 2015 у Wayback Machine.]. Зате після цього всяка формула еквівалентна бескванторной, як показує наступна теорема (звана теоремою про елімінації кванторів в Арифметика Прессбургера).

Аксіоми

Мова арифметики Прессбургера включає константи 0, 1, одну операцію + і предикат рівності =. Аксіоми мають вигляд:

  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), де P — формула першого порядку включаючи 0, 1, +, = і одну вільну змінну x.

Слід зауважити, що (5) насправді не одна аксіома, а схема аксіом, що представляє нескінченну безліч аксіом, по одній, для кожної формули P. (5) є формалізацією принципу математичної індукції. Вона не може бути еквівалентно замінена ніякою скінченною системою аксіом. Таким чином арифметика Прессбургера не є скінченно аксіоматизовною.

Властивості

довів що арифметика Прессбургера є:

  • несуперечливою: Не існує такого твердження в арифметиці Прессбургера яке може бути виведене з аксіом, разом з своїм запереченням.
  • повною: Для кожного твердження в алфавіті арифметики Прессбургера, незалежно від того чи можливо довести його з аксіом чи можна довести його заперечення.
  • розвязною: Існує алгоритм який дозволяє сказати чи дане твердження буде істинним або хибним.

Розв'язність арифметики Прессбургера може бути показана за допомогою елімінації кванторів, доповненим аргументацією про арифметичні рівняння.

Арифметика Пеано, яка являє собою арифметику Прессбургера доповнену операцією множення, не є розв'язною, внаслідок негативної відповіді Задачі розв'язності. За теоремою Геделя про неповноту, арифметика Пеано є неповною і її несуперечливість не є внутрішньо доведеною.

Див. також

Література

  • Верещагин Н.К., Шень А. — Языки и исчисления стор. 114, 121, 224
  • Барвайс Д. — Справочная книга по математической логике. Часть 3: теория рекурсии
  • Cooper, D. C., 1972, "Theorem Proving in Arithmetic without Multiplication" in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91–100.
  • , and Charles W. Rackoff, 1979. The Computational Complexity of Logical Theories. Lecture Notes in Mathematics 718. Springer-Verlag.
  • Fischer, M. J., and Michael O. Rabin, 1974, "" Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7: 27–41.
  • G. Nelson and D. C. Oppen (Apr. 1978). "A simplifier based on efficient decision algorithms". Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 141—150.
  • , 1929, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt" in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
  • Pugh, William, 1991, "The Omega test: a fast and practical integer programming algorithm for dependence analysis, [ 22 листопада 2008 у Wayback Machine.]".
  • Reddy, C. R., and D. W. Loveland, 1978, "Presburger Arithmetic with Bounded Quantifier Alternation." ACM Symposium on Theory of Computing: 320–325.

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

Arifmetika Pressburgera ce teoriya pershogo poryadku yaka opisuye naturalni chisla z dodavannyam ale na vidminu vid arifmetiki Peano viklyuchaye vislovlyuvannya shodo mnozhennya Nazvana v chest polskogo matematika kotrij v 1929 roci zaproponuvav vidpovidnu sistemu aksiom v logici pershogo poryadku a takozh pokazav yiyi U comu rozdili mi opisuyemo virazi bezlichi 1 24 veresnya 2015 u Wayback Machine v Vidznachimo vidrazu zh sho z takoyu signaturoyu eliminaciya kvantoriv nemozhliva Spravdi formula 2 24 veresnya 2015 u Wayback Machine spravzhnya dlya parnih H ne ye ekvivalentnoyu niyakoyi beskvantornoj formuli Tomu nam potribno persh nizh provoditi eliminaciyu kvantoriv rozshiriti signaturu Navedenij priklad formuli pidkazuye yake rozshirennya nam neobhidno Rozglyanemo rahunkove simejstvo dvomisnih predikatnih simvoliv 2 3 4 Simvol S bude interpretuvatisya yak rivnist po modulyu S Inshimi slovami formula H bude istinnoyu v nashij interpretaciyi yaksho porivnyati z po modulyu zalishki po modulyu rivni kratno Vazhlivo mati na uvazi sho indeks v ne ye zminnoyu u nas ne trimisnijpredikat a rahunkove simejstvo dvomisnih predikativ Take rozshirennya ne minyaye klasu viraznist predikativ oskilki napriklad mozhna viraziti yak 3 24 veresnya 2015 u Wayback Machine Zate pislya cogo vsyaka formula ekvivalentna beskvantornoj yak pokazuye nastupna teorema zvana teoremoyu pro eliminaciyi kvantoriv v Arifmetika Pressburgera AksiomiMova arifmetiki Pressburgera vklyuchaye konstanti 0 1 odnu operaciyu i predikat rivnosti Aksiomi mayut viglyad 0 x 1 x 1 y 1 x y x 0 x x y 1 x y 1 P 0 P x P x 1 P y de P formula pershogo poryadku vklyuchayuchi 0 1 i odnu vilnu zminnu x Slid zauvazhiti sho 5 naspravdi ne odna aksioma a shema aksiom sho predstavlyaye neskinchennu bezlich aksiom po odnij dlya kozhnoyi formuli P 5 ye formalizaciyeyu principu matematichnoyi indukciyi Vona ne mozhe buti ekvivalentno zaminena niyakoyu skinchennoyu sistemoyu aksiom Takim chinom arifmetika Pressburgera ne ye skinchenno aksiomatizovnoyu Vlastivostidoviv sho arifmetika Pressburgera ye nesuperechlivoyu Ne isnuye takogo tverdzhennya v arifmetici Pressburgera yake mozhe buti vivedene z aksiom razom z svoyim zaperechennyam povnoyu Dlya kozhnogo tverdzhennya v alfaviti arifmetiki Pressburgera nezalezhno vid togo chi mozhlivo dovesti jogo z aksiom chi mozhna dovesti jogo zaperechennya rozvyaznoyu Isnuye algoritm yakij dozvolyaye skazati chi dane tverdzhennya bude istinnim abo hibnim Rozv yaznist arifmetiki Pressburgera mozhe buti pokazana za dopomogoyu eliminaciyi kvantoriv dopovnenim argumentaciyeyu pro arifmetichni rivnyannya Arifmetika Peano yaka yavlyaye soboyu arifmetiku Pressburgera dopovnenu operaciyeyu mnozhennya ne ye rozv yaznoyu vnaslidok negativnoyi vidpovidi Zadachi rozv yaznosti Za teoremoyu Gedelya pro nepovnotu arifmetika Peano ye nepovnoyu i yiyi nesuperechlivist ne ye vnutrishno dovedenoyu Div takozhAksiomi Peano Logika pershogo poryadkuLiteraturaVereshagin N K Shen A Yazyki i ischisleniya stor 114 121 224 Barvajs D Spravochnaya kniga po matematicheskoj logike Chast 3 teoriya rekursii Cooper D C 1972 Theorem Proving in Arithmetic without Multiplication in B Meltzer and D Michie eds Machine Intelligence Edinburgh University Press 91 100 and Charles W Rackoff 1979 The Computational Complexity of Logical Theories Lecture Notes in Mathematics 718 Springer Verlag Fischer M J and Michael O Rabin 1974 Proceedings of the SIAM AMS Symposium in Applied Mathematics Vol 7 27 41 G Nelson and D C Oppen Apr 1978 A simplifier based on efficient decision algorithms Proc 5th ACM SIGACT SIGPLAN symposium on Principles of programming languages 141 150 1929 Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt in Comptes Rendus du I congres de Mathematiciens des Pays Slaves Warszawa 92 101 Pugh William 1991 The Omega test a fast and practical integer programming algorithm for dependence analysis 22 listopada 2008 u Wayback Machine Reddy C R and D W Loveland 1978 Presburger Arithmetic with Bounded Quantifier Alternation ACM Symposium on Theory of Computing 320 325

Дата публікації:
Топ