Если есть исполнение, есть и модель.
Какое, например, исполнение, если взять чекер выводов исчисления высказываний?
Нельзя брать только часть (чекер). В целом же, на сколько я понял, модель примерно такая - на входе есть некое описание структур, в нём выделяются структуры каждая отдельно, в них выделяются подстановочные составляющие, для каждой подстановки производится поиск возможных вариантов, варианты замещают каждую подстановку и каждая такая комбинация повторно обрабатывается в этом же цикле, начиная с поиска новых подстановок. Далее по нахождении "неделимой" подстановки, процесс заканчивается. Результатом является дерево вывода с вариантом подстановки в каждом листе. В целом получаем алгоритм, в котором нет низкоуровневых деталей вроде алгоритма поиска подстановки, используемых при этом структур данных и т.д., но есть общая модельная часть (то есть как и любая модель - не полностью соответствующая действительности).
Вообще, конечно, как раз то, как выглядят выводы во внутреннем формате Metamath, можно считать программами на конкатенативном языке, но придание им семантики будет сильно зависеть от того, какие же аксиомы / правила вывода определены, потому что именно это (для Metamath — не более и не менее, никаких примитивных правил вывода там нет, мы определяем всё) задаёт, из чего такие «программы» состоят и какие из них корректны.
Правила вывода есть, они указаны выше. А мы задаём ограничения, в рамках которых применяются правила.
Это вам может быть легко довериться, что авторы чекера не наделали трудновыявляемых и значительных для смысла результатов ошибок, а людям, которые собираются полагаться на такие системы значительно, может оказаться важным убедиться в корректности поближе — возможно просмотром кода.
Конечно, код должен быть доступен, как минимум в виде псевдо-алгоритма, той самой модели исполнения. А лучше в полном виде, что бы была возможность выявить ошибки в реализации общего алгоритма.
А каким способом достигается большая выразительность?
Разными. Ну как вот языки программирования позволяют писать выражения по-человечески и при этом не писать лишних скобок? Грамматики, парсинг с приоритетами, такие штуки.
То есть просто следование модели представления данных, привычной пользователям. Правильно? Но что мешает следовать такой модели на прологе? Исключаем при этом общие для всех проблемы отсутствия математических символов на клавиатуре. Да, иногда будут лишние скобки, но разве это так критично?
не путайте системы автоматического вывода и системы автоматической проверки, в обсуждаемом случае необходимо только второе.
На основе систем проверки делают системы вывода, и наоборот.
Ладно, допустим вы говорите, что можно на прологе написать некий встроенный DSL и уже вместе с ним напасть на ZFC (а конкретно уметь представлять её аксиомы, выводы в ней и проверять эти выводы на корректность). Давайте. Можно взять ZF, и даже её кусок, только чур оставить хотя бы одну схему аксиом и включить аксиому бесконечности. Возьмётесь?
Напасть можно на что угодно, но проблема всё равно останется прежней. Есть аксиомы и доказанные теоремы, далее следуют правила вывода, применение которых к аксиомам и теоремам позволяет строить новые теоремы. Собственно формализация аксиом и доказанных теорем на прологе тривиальна - обычное правило. А вот применение к таким правилам пролога правил вывода (не равно правилам пролога) есть то самое место, где встречается сложность. В системах автоматического вывода правила вывода встроены в систему на низком уровне, реализованы на том языке, на котором писалась система. В прологе так же придётся эти правила реализовывать, поэтому от, как вы выразились, "будет написан целиком новый язык", не уйти, но вопрос в сложности такого подхода - меньше эта сложность, чем стандартный подход с реализацией правил вывода на низкоуровневом языке или больше. Оценку сложности дать сложно (каламбурнее - лучше запоминается :) ). Точная оценка может быть после реализации, но реализация здесь нетривиальная и требует прилично времени. Ну а потом уже можно хоть ZFC, хоть всю математику "вводить".
А помимо времени на реализацию ваше требование включения понятия "бесконечность" многое "портит". То есть с конечными структурами оперировать привычно, понятно как, а бесконечные структуры внутри компьютера требуют несколько иных подходов. Они, конечно же, вполне реализуемы, но не по тем правилам, которые привычны для конечных структур. То есть проверка для конечной структуры возможна простым перебором, а для бесконечности - ну в общем очевидно. Определение конечных структур так же можно задавать реккурентно с указанием последнего шага, а вот у бесконечных последнего шага нет, нет завершения любой процедуры обхода, есть вечное её продолжение, значит нужен некий соответствующий признак и его логичный учёт в модели исполнения, а это всё опять требует продумывания, поскольку в программировании хорошо продуманы лишь конечные структуры и подходы.
В общем вы так смело возложили на меня обязанность "сделать конфетку", но я вам пытаюсь показать, что объём работы будет немаленький.