|
|
Я не уверен, но по-моему вы с Дмитрием смешиваете две вещи - язык логики первого порядка (который кодирует в себе, действительно, процедуру верификации доказательства - с вариациями в виде интуиционизма, например; это та самая шняга с кванторами, птичками и стрелочками) и теории первого порядка - например, ZF (аксиоматика Пеано - другой пример), которая есть язык логики + электрификация аксиоматизация теории множеств Кантора, которую Гильберт называл раем потому, что из множеств, действительно, можно изготовить все математические объекты.
Так вот - первая про математические доказательства, а вторая - про множества, и это типа разные вещи.
(Читать комментарии) Добавить комментарий:
|
|