Конструктивные объекты
Sep. 12th, 2011 07:20 amИз комментариев к предыдущей записи вынесу, пожалуй, пару точек зрения. Одна из них заключается в счетности непротиворечивых теорий независимо от аксиоматики, включая те, что аксиоматизируют несчетные множества; другая же — в недоумении, почему мы пользуемся классическим матаппаратом, чтобы показать неконструктивность континуума.
На первую ответ простой: аксиоматизировать объект не значит построить его. Континуум продолжит быть просто названием, символом, буковкой, которую мы переставляем в логических выводах туда-сюда. Как невидимый единорог, в отношение которого тоже можно и теорем счетное множество доказать, и диссертацию защитить. Никто не мешает.
Другое дело с конструктивными объектами. Любой из них можно определить индуктивно с помощью правил как при описании нового языка, без аксиоматики. Известно, что любая конструкция, которой можно в общем случае научить оперировать другого человека или машину, неизбежно окажется определимой таким образом.
На вторую же точку зрения ответ чуть сложнее. Начнем с того, что выбор теории, доказательство ее непротиворечивости, построение модели, выбор объекта для построения (в отличие от предъявления этого объекта) — необходимые для работы с современной математикой вещи. Они, естественно, лежат за пределами чистой конструктивной математики и логики первого порядка. К примеру, определить конструктивные вещественные числа, конечно, можно, но выбрать этот объект случайно и привязать его к природе невозможно.
Не все знают, что такое λ-исчисление. Чаще всего с этим термином связывают систему λΚβη, иногда типизированные ее варианты. Однако, более общее значение термина — это раздел математической логики, занимающийся изучением целого класса подобных систем и их свойств, центральное место среди которых, действительно, занимает бестиповая λΚβη. Более точно, λ-исчисление — это применение классического матаппарата к изучению λ-теорий и их моделей.
Отсюда виден ответ: чисто конструктивная математика с заранее известными объектами и операциями над ними достаточна для инженерных задач как язык описания и способ вычисления, ровно который возможно автоматизировать с помощью программ компьютерной алгебры. Однако, чтобы вообще говорить о конструктивной математике и заниматься ее развитием, необходим классический матаппарат, и в этом нет никакого противоречия: именно он дает нам возможность отличить конструктивные определения объектов от неформальных.
На первую ответ простой: аксиоматизировать объект не значит построить его. Континуум продолжит быть просто названием, символом, буковкой, которую мы переставляем в логических выводах туда-сюда. Как невидимый единорог, в отношение которого тоже можно и теорем счетное множество доказать, и диссертацию защитить. Никто не мешает.
Другое дело с конструктивными объектами. Любой из них можно определить индуктивно с помощью правил как при описании нового языка, без аксиоматики. Известно, что любая конструкция, которой можно в общем случае научить оперировать другого человека или машину, неизбежно окажется определимой таким образом.
На вторую же точку зрения ответ чуть сложнее. Начнем с того, что выбор теории, доказательство ее непротиворечивости, построение модели, выбор объекта для построения (в отличие от предъявления этого объекта) — необходимые для работы с современной математикой вещи. Они, естественно, лежат за пределами чистой конструктивной математики и логики первого порядка. К примеру, определить конструктивные вещественные числа, конечно, можно, но выбрать этот объект случайно и привязать его к природе невозможно.
Не все знают, что такое λ-исчисление. Чаще всего с этим термином связывают систему λΚβη, иногда типизированные ее варианты. Однако, более общее значение термина — это раздел математической логики, занимающийся изучением целого класса подобных систем и их свойств, центральное место среди которых, действительно, занимает бестиповая λΚβη. Более точно, λ-исчисление — это применение классического матаппарата к изучению λ-теорий и их моделей.
Отсюда виден ответ: чисто конструктивная математика с заранее известными объектами и операциями над ними достаточна для инженерных задач как язык описания и способ вычисления, ровно который возможно автоматизировать с помощью программ компьютерной алгебры. Однако, чтобы вообще говорить о конструктивной математике и заниматься ее развитием, необходим классический матаппарат, и в этом нет никакого противоречия: именно он дает нам возможность отличить конструктивные определения объектов от неформальных.
