Насколько я понимаю, в Metamath ограниченное количество терминов.
Там интересная вещь в том, что даже то, что считается «базовыми» символами алфавита любого, для примера, языка первого порядка, в Metamath вводится явно. [Можно на основе Metamath построить, например, λ-исчисление (мне кажется, и любую «серьёзную» теорию типов), и он будет работать так же хорошо, а помощники построения доказательства (кажется, там несколько есть, судя по тому, что как-то давно читал) будут работать тоже.] Кстати, потому там скобки нигде не опускаются и есть обозначения довольно разные синтаксически — формулы не делятся на подформулы явно, хотя этим делением можно было бы считать вывод метаутверждения о корректности формулы. Но системе нужен только факт корректности формулы, а не конкретный вид доказательства этого факта.
Это было прелюдией перед словами о том, что свою систему Metamath можно расширять практически чем угодно. Какими угодно символами — точно. Синтаксис какой угодно уже не введёшь, а то могут появиться неоднозначно читаемые формулы. Но тут Metamath не уникален.
