История изменений

Хмм, похоже что является. Определяем Аксиомы Пеано, но чтоб с 0 начиналось а не с 1. Вводим операцию «x + y», операцию «x - y», деления, умножения и остатка от деления определяем, потом операции битового логического сдвига влево и вправо - так можно сдвигами нарезать число от 0 до inf на бесконечный массив байтов по 8 бит каждый — получим ленту для brainfuck и возможность по ней ходить в любую сторону. А сама программа брейнфака, состоящая из 8 инструкций > < + - . , [ ] - делаем отдельный массив для этих инструкций по три бита на инструкцию. Ну а дальше определяем что вот эта инструкция делает такие-то изменения на ленте.

Только я тогда не совсем понимаю, что значит несводимость логики первого порядка к логике второго порядка? Если брейнфак выразим в логике первого порядка, то я могу скомпилить Coq в этот брейнфак — разве это не будет выражение логики одного порядка в логике другого порядка?

Хмм, похоже что является. Определяем Аксиомы Пеано, но чтоб с 0 начиналось а не с 1. Вводим операцию «x + y», операцию «x - y», деления, умножения и остатка от деления определяем, потом операции битового логического сдвига влево и вправо - так можно сдвигами нарезать число от 0 до inf на бесконечный массив байтов по 8 бит каждый — получим ленту для brainfuck и возможность по ней ходить в любую сторону. А сама программа брейнфака, состоящая из 8 инструкций > < + - . , [ ] - делаем отдельный массив для этих инструкций по три бита на инструкцию. Ну а дальше определяем что вот эта инструкция делает такие-то изменения на ленте.