Metamath: введение в язык

Ниже идёт конспективное изложение языка Metamath из документа metamath.pdf. На сайте metamath.org собрано большое количество доказательств различных теорем формальной логики, теории множеств и т.п. математических дисциплин. Предполагается, что подобные доказательства, записанные на языке Metamath, являются формально безупречными и могут быть проверены многочисленными парсерами, понимающими синтаксис этого языка.

Языки и исчисления

Любая формальная теория является некоторым языком со своим алфавитом, словами и способами получения (вывода) новых слов (см. книгу). Символом может быть что угодно, лишь бы мы могли однозначно отличать один символ от другого.
Слово -- конечная, произвольная цепочка (упорядоченная последовательность) символов.

Язык -- это некоторое подмножество всех слов. Обычно существуют правила, позволяющие понять принадлежит данное слово языку или нет. Часто слово языка называется правильно построенной формулой (wff - well formed formula).

Исчислением - это язык в котором задано множество слов (формул), называемых аксиомами и правила вывода (получения) новых формул. Правило вывода -- это предписание, при помощи которого из формул определённого вида получается новая формула.

Базовый синтаксис Metamath

Документ Metamath (текстовый файл с расширением *.mm) начинается с определения констант и переменных.
Константы - это все символы языка которые нельзя менять (например, в арифметике: 0 1 + ( )).
Переменные - это слова, на место которых можно подставлять другие слова. Константы и переменные могут состоять из нескольких ASСII символов и всегда разделяются пробелом:

$c константы_через_пробел $.	- все константы и символы языка (const),
$v переменные_через_пробел $.	- перечень всех переменных (var),
$d var var $.	- эти переменные должны быть различны (disjoint) (запрет присутствия общих переменных при подстановках).

Переменные обязаны иметь фиксированный тип (логическая формула, терм, целое число и т.п). Тип - это произвольная константа, задаваемая внутри $c ... $.. Объявление типа сопровождается уникальным именем, меткой (label), которая ставится перед командой $f ... $. Для объявления слова аксиомой служит $a, а для теоремы с доказательством - $p. Некоторые аксиомы или теоремы могут требовать посылок или гипотез $e ... $.

label $f const var $.	- объявление типа переменной (“floating” hypothesis),
label $e const symb ... symb $.	- гипотеза перед $a или $p (“essential” hypothesis), symb = const | var
label $a const symb ... symb $.	- аксиома,
label $p const symb ... symb $= proof $.	- утверждение, доказательство которого содержится в блоке proof.

Кроме этого существуют комментарии, команды подключения дополнительных файлов и блоки директив языка:

На этом описание базового синтаксиси Metamath окончено.

Исчисление высказываний

Рассмотрим пример исчисления высказываний с импликацией P -> Q и отрицанием !Q. В этом исчислении выводятся все правильно построенные логические формулы вида P -> Q, P -> ( Q -> R ), !!P -> P и т.п. Ниже, слева приведено описание такого исчисления с двумя аксиомами wn, wi. Эти аксиомы рекурсивно определяют что такое правильно построенная формула. Теорема th1 предъявляет пример такой формулы и доказательство.

MM> read demo1.mm           (загрузка)
MM> verify proof *          (проверка доказательств)

В первой строчке файла объявлено 6 констант, среди которых зарезервирован также символ |- (выводимость). Во второй строке объявлено 4 переменных P, Q, R, S. Следующие 4 строки определяют тип этих переменных как правильно построенных формул (wff - константа исчисления).

Аксиома wn описывает как к произвольной формуле можно "присоединить" отрицание, а wi задаёт правило построения формулы с импликацией. Эти аксиомы подразумевают описание переменных, которые в них участвуют (в порядке появления в строке). Подобные описания называются гипотезами. Для аксиомы wn такая гипотеза одна (что подставлять вместо P), а для wi - гипотез должно быть 2 (для P и Q).

Наконец, последняя команда с меткой th1 и 11-ю символами между $p ... $=, является теоремой. Она утверждает, что строка "wff ( ! S -> ( R -> P ) )" - это правильно построенная формула. Доказательство теоремы находится между символами $= и $. Подчеркнём, что Metamath ни чего не знает о смысле wff. Это просто константа языка, как и все другие.

Metamath проверяет доказательство слева на право при помощи стека. Первоначально стек пустой. На первом шаге Metamath видит гипотезу wS и помещает её в стек:

[ 1: wff S ].

[ 1: wff ! S ].

[ 3: wff P, 2: wff R, 1: wff ! S ].

[ 2: wff ( R -> P ), 1: wff ! S ].

[ 1: wff ( S -> ( R -> P ) ) ].  

Обратная польская нотация

Использование стека приводит к тому, что все доказательства формируются по принципу обратной польской нотации (придуманной Лукашевичем). Например wP wQ wi это P->Q (бинарная операция -> ставится после её аргументов P и Q).

Разберём более сложный пример для формулы: (P->(Q->R))->((P->Q)->(P->R)).
Будем последовательно записывать каждую связку в обратной польской нотации:

(P->( wQ wR wi))->((wP wQ wi)->(wP wR wi)),
(wP (wQ wR wi) wi)->((wP wQ wi) (wP wR wi) wi),
(wP (wQ wR wi) wi) ((wP wQ wi) (wP wR wi) wi) wi
wP wQ wR wi wi wP wQ wi wP wR wi wi wi.

wP wQ wR wi wi wP wQ wi wP wR wi wi wi,
wP (wQ wR wi) wi wP wQ wi wP wR wi wi wi,
(wP (wQ wR wi) wi) wP wQ wi wP wR wi wi wi,
(wP (wQ wR wi) wi) (wP wQ wi) wP wR wi wi wi,
(wP (wQ wR wi) wi) (wP wQ wi) (wP wR wi) wi wi,
(wP (wQ wR wi) wi) ((wP wQ wi) (wP wR wi) wi) wi.

Из подобных, достаточно длинных последовательностей состоят доказательства Metamath.

Аксиомы Лукашевича

Рассмотрим теперь несколько более содержательных теорем. Для этого добавим три аксиомы Лукашевича и правило вывода modus ponens (из формул P и P->Q выводится формула Q):

В аксиомах и правиле вывода стоит константа "|-", интерпретируемая как "выводится". Первая аксиома требует описания двух переменных (что подставлять вместо P и Q), вторая - трёх, а третья - снова двух. Правило вывода mp, фактически, также является аксиомой. Однако она, кроме обязательных заданий двух переменных P и Q, содержит две посылки min и maj, которые также должны находится в стеке, чтобы правило сработало. Таким образом, если wi требует перед собой в стеке 2-х элементов, то для mp их должно быть 4.

Опишем вывод производного правила P->(Q->R) |- (P->Q)->(P->R) с именем a2i. Это теорема исчисления ($p), зависящая от трёх переменных P, Q, R типа wff (они таковыми сделаны раньше при помощи директивы $f). Последовательность имён переменных соответствует тому, как они появлялись в описании теоремы (первые две строки a2i.1 и a2i) Четвёртым аргументом теоремы выступает гипотеза a2i.1, между $e и $.:

Каждая строка доказательства (после $=) формирует последовательность символов, приведенную после двоеточия в комментариях (пробелы для краткости опущены). Первые 4 последовательности находятся в стеке перед применением правила mp. Первые две - это выражения (wff), которые будут подставлены в переменные P, Q правила. Вторые две (min, maj) - посылки ($e) правила mp. В них, в соответствии с правилом mp, должен уже стоять символ "|-", а не "wff" как ранее.

Производное правило вывода a2i можно использовать в последующих доказательствах.
Получим, например, правило P->Q, P->(Q->R) |- P->R с тремя переменными и двумя посылками mpd.1 и mpd.2:

Производное правило mpd в базовом файле set.mm системы Metamath используются для вывода теоремы P -> P ("идентичность высказывания"). Эта теорема, в отличии от правил, не содержит гипотез:

Компактная запись трёх приведенных доказательств может быть получена командой MM> show proof *:

a2i:
13   min=a2i.1     $e |-  P→(Q→R )
17   maj=ax-2      $a |-  (P→(Q→R))→((P→Q)→(P→R))
18   a2i=mp        $a |-  (P→Q)→(P→R)
mpd:
 7   min=mpd.1     $e |-  P→Q
11   a2i.1=mpd.2   $e |-  P→(Q→R)
12   maj=a2i       $p |-  (P→Q)→(P→R)
13   mpd=mp        $a |-  P→R
id:
 8   mpd.1=ax-1    $a |-  P→(P→P)
13   mpd.2=ax-1    $a |-  P→((P→P)→P)
14   id=mpd        $p |-  P→P

Приведём также вывод теоремы ( P -> P ) без использования производных правил:

Обратим внимание, что в первой строке нельзя использовать более компактную запись "wP wP ax-1", так как она приведёт к строке "|- P->(P->P)", тогда как для применения правила mp там должна стоять подстановка для переменной P, т.е. правильно построенная формула "wff P->(P->P)".

Пустыми строками отделено первое применение правила mp в результате которого формируется вторая посылка maj финального применения mp. В результате этого возникает последовательность ( P->P ), совпадающая с содержанием теоремы id1, поэтому она считается доказанной.

Теория с термами

Рассмотрим теперь пример из арифметики, которая имеет переменные двух типов - термы и wff.
Пусть в этой теории есть две аксиомы:

(A1) (t = r → (t = s → r = s))           транзитивность равенства
(A2) (t + 0) = t                         прибавление нуля

1. (t + 0) = t                           (по аксиоме A2)
2. (t + 0) = t                           (по аксиоме A2)
3. ((t + 0) = t → ((t + 0) = t → t = t)) (по аксиоме A1)
4. ((t + 0) = t → t = t)                 (правило mp применяется к шагу 2 и 3)
5. t = t                                 (правило mp применяется к шагу 1 и 4)

Опишем этот же вывод на языке Metamath. Для этого создадим файл в котором определим константы и 5 переменных. Переменные t,r,s будут типа term, а переменные P,Q - формулами wff:

Сохраняем этот вывод в текстовом файле demo.mm. Запускаем программу metamath.exe и в консоли набираем:

MM> read demo.mm
MM> verify proof *