Статья 329

Таким образом, еще раз подтверждается прозрение Брауэра относительно логических корней неконструктивности.
Стоит отметить принципиальное отличие реализуемости от других видов логических семантик которые базируются на системах истинностных значений. Эквивалентные формулы имеют одинаковые истинностные значения, истинны в одних и тех же возможных мирах, но они обычно имеют различные реализации. Например, если реализация, то реализацией служит.
Еще одну переформулировку идеи Колмогорова о логике как исчислении задач дал Н.А. Шанин в 1956 г. Он сформулировал алгоритм конструктивной, который переводил формулу языка арифметики новая переменная, вводимая для обозначения объекта, который должен быть построен при доказательстве, формула классической логики с параметром. Таким образом, конструктивное истолкование формулы было сведено к построению объекта и доказательству обычного, классического утверждения о построенном объекте.