Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.mccme.ru/nir/uir/16GB.doc Дата изменения: Sun Feb 19 16:52:54 2012 Дата индексирования: Tue Oct 2 01:36:01 2012 Кодировка: koi8-r Поисковые слова: http news.cosmoport.com 2005 04 18 1.htm

На шестнадцатом семинаре (20.04.10) Г.Б. Шабат сделал доклад на тему
«Базовые языки»

Попробуем для начала провести строгую формализацию базового языка нижнего
уровня.

Модель: язык АРИФМЕТИКИ. (Арифметика развивает дедукцию не хуже геометрии.)

Введём следующие понятия:

Константы: 0, 1.
Переменные: x, x|, x||, x|||, . (здесь | - «насечка» почему не единица?)

Термы (~ подлежащие): это константы и переменные, связанные символами +, *,
(.); если t, u - термы, то (t+u), (t*u) - тоже термы.
Как понимать знаки + и *?

Предикаты (~ сказуемые): это символы =, [], [pic].
Если t, u - термы, то [t = u] - формула.

Математика - наука про то, что что-нибудь равно чему-нибудь и про то, что
что-то из чего-то следует.

Элементарный предикат «F(x, x|, x||,.)=0», где [pic].
Элементарные предикаты говорят, что набор переменных лежит на
гиперповерхности.
Если F, G - формулы, то [pic] - также формулы.

Соглашение.
[pic].
Импликации в алфавит не встроены!
Если F - формула со свободным вхождением переменной y, то
[pic] и [pic]
- тоже формулы. В них y уже связан.

Формула - это утверждение о свободных переменных.
Формулы без свободных переменных - это теоремы.

Проект.
1. Синтез. Как породить все формулы?
2. Анализ. Данная последовательность символов - это формула или нет?
3.Как определить эквивалентность двух формул?

На каком языке программирования удобно реализовать проект? (Было бы удобно
на старом Бейсике.)

Дадим несколько определений:
[pic]
[pic]
[pic]
[pic]
Чтобы поупражняться, сформулируем на нашем языке несколько теорем:
- утверждение Евклида о бесконечности множества простых чисел:
[pic]
- проблему близнецов:
[pic]
- последнюю теорему Ферма для степени 3
[pic]
- результат Матиясевича:
[pic] [pic]
А что такое an? Мы только что даже куб расписывали через произведение.

(Можно ли сохранить формальность и добиться читаемости человеком?)

Проект. Создать библиотеку теорем арифметики.

Все ли теоремы формулируемы на таком языке?
Оказывается, не все: не формулируется теорема Ван-дер-Вардена о разбитии
последовательности чисел на две части (Почему? Можно ли просто объяснить?).
Какие дополнительные сокращения нужно ввести в язык?