Ну Колмогоров и Йоханссон посчитали так же и независимо друг от друга создали минимальную логику. Но она не интуиционистская. В интуиционистской из противоречия следует что угодно.

Прикольно

А в натуральной дедукции есть принцип взрыва ?

Натуральная дедукция не логика

Тут уже и Metamath упомянули и ACL2... Если кому интересно - я сделал свою "высокоуровневую надстройку" над метаматом. Доказательства - читаемые, синтаксис выражений и определения - синтаксически отделены от аксиом. Транслятор туда-сюда работает, сделал vscode extension для языка, ну чтобы приятно навигацию можно было делать, распарсеные файлы кешируются, поэтому после первичного распарсивания все довольно быстро грузится. А для вообще молниеносных операций есть ещё http- сервер, который в опертивке все держит и моментально дает подсказки. Вобщем стараюсь все для человека делать, а не наоборот. Такие дела.

Это способ представления исчислений

Естественный вывод Гентцена -- это способ записывать доказательства. В любой логике. Сам Гентцен для классической писал.

Скидывай

Посмотрим

Спасибо

для трансляции полной базы теорем метамата требуется 8 гб и относительно много времени (у меня на 16-ти ядрах 2.5 мин занимает)

8 гигов оперативки?

предыдущая версия на с++ была написана - вот там был адъ и израиль - для трансляции меньшей базы 27 гб (sic!) требовалось.

А это на чём создано

да, -Xmx8G для jvm нужно дать

А можно не надо столько оперативки

создано на этом:  https://github.com/area9innovation/flow9

можно кусочек базы теорем метамата откусить и оттранслировать меньше - не вопрос. Просто аккуратно откусить надо, чтобы синт. конструкции не порушить

Кажется, кроме того, что хорошие программы на плюсах должны есть меньше, чем хорошие программы на яве