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

Поделись знанием:
Перейти к: навигация, поиск

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





Аксиомы

Язык арифметики Пресбургера включает константы 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) является формализацией принципа математической индукции. Она не может быть эквивалентно заменена никакой конечной системой аксиом. Таким образом арифметика Пресбургера не является конечно аксиоматизируемой.

См. также

Напишите отзыв о статье "Арифметика Пресбургера"

Литература

  • Cooper, D. C., 1972, «Theorem Proving in Arithmetic without Multiplication» in B. Meltzer and D. Michie, eds., Machine Intelligence. Edinburgh University Press: 91-100.
  • Ferrante, Jeanne, 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, "[www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps «Super-Exponential Complexity of Presburger Arithmetic.]» Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7: 27-41.
  • G. Nelson and D. C. Oppen (Apr. 1978). «[doi.acm.org/10.1145/512760.512775 "A simplifier based on efficient decision algorithms"]». Proc. 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages: 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» in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves. Warszawa: 92-101.
  • Pugh, William, 1991, «[doi.acm.org/10.1145/125826.125848 The Omega test: a fast and practical integer programming algorithm for dependence analysis,]».
  • Reddy, C. R., and D. W. Loveland, 1978, «[doi.acm.org/10.1145/800133.804361 Presburger Arithmetic with Bounded Quantifier Alternation.]» ACM Symposium on Theory of Computing: 320—325.
  • Верещагин, Шень. Лекции по математической логике и теории алгоритмов. — МЦНМО, 2002.

Ссылки

  • [www.stefan-baur.de/priv.studies.studienarbeit.html Online-Proofer] Java-апплет, проверяющий формулы арифметики Пресбургера на истинность.  (нем.)

Отрывок, характеризующий Арифметика Пресбургера

– Ты лучше не беспокойся. Мне что нужно, я просить не стану, сам возьму.
– Да что ж, я так…
– Ну, и я так.
– Прощай.
– Будь здоров…
… и высоко, и далеко,
На родиму сторону…
Жерков тронул шпорами лошадь, которая раза три, горячась, перебила ногами, не зная, с какой начать, справилась и поскакала, обгоняя роту и догоняя коляску, тоже в такт песни.


Возвратившись со смотра, Кутузов, сопутствуемый австрийским генералом, прошел в свой кабинет и, кликнув адъютанта, приказал подать себе некоторые бумаги, относившиеся до состояния приходивших войск, и письма, полученные от эрцгерцога Фердинанда, начальствовавшего передовою армией. Князь Андрей Болконский с требуемыми бумагами вошел в кабинет главнокомандующего. Перед разложенным на столе планом сидели Кутузов и австрийский член гофкригсрата.
– А… – сказал Кутузов, оглядываясь на Болконского, как будто этим словом приглашая адъютанта подождать, и продолжал по французски начатый разговор.
– Я только говорю одно, генерал, – говорил Кутузов с приятным изяществом выражений и интонации, заставлявшим вслушиваться в каждое неторопливо сказанное слово. Видно было, что Кутузов и сам с удовольствием слушал себя. – Я только одно говорю, генерал, что ежели бы дело зависело от моего личного желания, то воля его величества императора Франца давно была бы исполнена. Я давно уже присоединился бы к эрцгерцогу. И верьте моей чести, что для меня лично передать высшее начальство армией более меня сведущему и искусному генералу, какими так обильна Австрия, и сложить с себя всю эту тяжкую ответственность для меня лично было бы отрадой. Но обстоятельства бывают сильнее нас, генерал.
И Кутузов улыбнулся с таким выражением, как будто он говорил: «Вы имеете полное право не верить мне, и даже мне совершенно всё равно, верите ли вы мне или нет, но вы не имеете повода сказать мне это. И в этом то всё дело».
Австрийский генерал имел недовольный вид, но не мог не в том же тоне отвечать Кутузову.
– Напротив, – сказал он ворчливым и сердитым тоном, так противоречившим лестному значению произносимых слов, – напротив, участие вашего превосходительства в общем деле высоко ценится его величеством; но мы полагаем, что настоящее замедление лишает славные русские войска и их главнокомандующих тех лавров, которые они привыкли пожинать в битвах, – закончил он видимо приготовленную фразу.