Учитывая доказательства A → B и A, когда мы получим доказательство B?

В интуиционистской математике предложение истинно только тогда, когда его доказательство было получено на опыте. Следуя семантике BHK, доказательство A → B — это алгоритм, который при наличии доказательства A даст доказательство B. Таким образом, с доказательством A → B и доказательством A существует очевидный способ получить справку Б.

Мой вопрос, однако, о том, когда происходит доказательство B. Достаточно ли подумать об алгоритме, подумать о доказательстве А и сопоставить их? Или мне действительно нужно вычислить доказательство B в нормальной форме? Обратите внимание, что вопрос является рекурсивным: учитывая, что доказательства A → B и A сами по себе являются доказательствами, должны ли мы иметь их нормальные формы, чтобы заключить что-либо осмысленное?

Я думаю об этом с точки зрения теории типов Мартина-Лёфа. Здесь мы могли бы думать об этом как о различии между ленивой и нетерпеливой оценкой. Для MLTT (и любой разумной теории типов для использования в математике) выполняется сильная нормализация, поэтому между ними нет формальной разницы. Однако, если доказательство fA → B сложное, а доказательство aA большое, мы находим существенное различие между неоцененным f aи соответствующим оцененным доказательством B.

Может быть, это всего лишь вопрос определения «доказательства», и оба имеют смысл. Я также могу представить, что разные философы расходятся во мнениях, поэтому меня интересуют любые ответы.

Вопрос: является ли «семантика BHK» тем же самым, что и «семантика Гейтинга», последняя, ​​как обсуждалось в «Доказательствах и типах», Girard, LaFont, Taylor irif.univ-paris-diderot.fr/~mellies/mpri/mpri-ens /biblio/… Их обсуждение интерпретирует (как я понимаю) A-->B как отображение от доказательств A к доказательствам B, но не обязательно конструктивное отображение. В то время как ваше обсуждение (и гугление BHK) делает его определенно конструктивным.
Да, они такие же. «конструктивный» подразумевается в теории типов. По крайней мере, для целей этого вопроса доказательства A → B должны быть конструктивными. Кроме того, если я правильно думаю, учитывая, что доказательства имеют форму конечных деревьев, карты, которые мы можем представить, и конструктивные карты должны совпадать.
вы спрашиваете, должны ли доказательства иметь нормальные формы или результаты «оценивания» доказательств? поскольку доказательство является алгоритмом, я склонен думать, что доказательства должны иметь не нормальную форму, а их результаты. подумайте о 2+2 против 3+1. нормальная форма результата: 4. Но вы можете использовать разные алгоритмы в каждом случае. Я не уверен, что такие алгоритмы можно свести к алгоритму нормальной формы. Это кажется неправильным, но я признаю, что это выше моего понимания.
@mobileink, я предполагаю, что каждое доказательство имеет нормальную форму, и, по сути, спрашиваю, достаточно ли воображения ненормальной формы, чтобы сказать, что утверждение интуитивно верно.
хорошо. пусть S будет предложением. предположим, что у нас есть 2 доказательства S, p1 и P2. Что означает, что «каждое доказательство» имеет нормальную форму? если они имеют одну и ту же нормальную форму, они (фактически) являются одним и тем же доказательством в разных формах, точно так же, как 2+2 v. 4. если у них разные нормальные формы, как они могут доказать одно и то же? (Между прочим, я не уверен, но я считаю, что мы не можем показать, что для каждого предложения существует не более 1 доказательства.) Что касается стратегии оценки (ленивый против строгого), это не влияет на достоверность. если вы можете «вообразить» доказательство в любой форме, которое действительно строит вывод, вы можете утверждать, что оно истинно.
кроме того, и, возможно, это ближе к тому, что вам нужно, вам не нужно иметь доказательство в руках, так сказать, чтобы доказать что-то интуитивно. достаточно иметь (конструктивный) метод для получения такого доказательства. подумайте о том, чтобы доказать, что какое-то огромное число имеет какое-то простое свойство, например «делиться на 47». На то, чтобы записать реальное доказательство, могут уйти столетия. Но если вы CA запишете алгоритм и покажете, что он (в конце концов) даст доказательство, то все готово, вы предоставили доказательство.
это более или менее то, что говорит @jobermark.
возможно, вам будет полезно прочитать несколько первых глав книги HOTT ( homotopytypetheory.org/book ).
Пусть S равно ℕ, и рассмотрим доказательства 0, 1, 1 + 1 и 2. Каждое из них имеет нормальную форму, соответственно 0, 1, 2 и 2. Нормальные формы разные, но все они доказывают одно и то же. (что натуральные числа существуют). Будут доказательства без нормальных форм, когда логика, с которой мы работаем, несовместима, поскольку нет нормализованных доказательств ⊥. Я рад, что 1 + 1 обычно является действительным доказательством ℕ в данном конструктивном формализме, но меня беспокоит, насколько это тривиально.
Например, в формализме ультрафинитарных рассуждений, который предусматривает, что алгоритмы должны быть полиномиально ограниченными по времени, 2 ^ 2 не будет действительным доказательством ℕ, потому что мы не можем возводить в степень унарные числа. Но мы можем металогически поразмыслить над выражением и отметить, что 4 является действительным доказательством ℕ. Таким образом, с философской точки зрения может иметь смысл провести различие между доказательствами в нормальной форме и общими синтаксическими доказательствами. Если мы на самом деле не можем представить себе нормальную форму 1000 ^ 1000, какой смысл говорить, что у меня была интуиция в качестве доказательства ℕ?
Что же касается «вам не нужно, так сказать, иметь доказательство на руках, чтобы доказать что-то интуиционистски», то это утверждение вывода. Я согласен, что было бы очень удобно — чрезвычайно удобно — чтобы это было правдой, но это не повод для веры. И я много читал книги по HoTT, но это конкретно практическая математическая книга, и она не затрагивает философию. Он хорош для изложения формальной системы, но не пытается обосновать ее интуитивно. Действительно, когда книга была впервые опубликована, не было реальных доказательств ее конструктивности. Это
почему у нас есть модель кубических наборов.

Ответы (1)

Интуиционизм шире того алгоритмического конструктивизма, с которым вы его отождествляете. Доказательство должно существовать в абстрактном смысле, поскольку мы уверены, что при наличии достаточного количества ресурсов его можно построить. Нам не нужно строить его для каждого случая или предоставлять единый конвергентный алгоритм, который единообразно обрабатывает все случаи. Нам просто нужно доказать, что мы можем сделать это для любого конкретного случая.

Мы должны пережить завершение своей способности найти доказательство. Мы только пытаемся быть очень уверенными в том, что мы не преследуем потенциальное противоречие будущей интуиции, конструируя доказательство. Мы не требуем, чтобы он был математически полезен или полностью формализовал его в алгоритме. Таким образом, просто зная A -> B и A действительно достаточно - не из-за формализма, а потому, что, зная их, мы знаем, что можем добавить доказательства и получить доказательство, какими бы ни были возникающие проблемы фактического выражения (например, сложности внутренних проблем отображения между параметрами, используемыми в двух алгоритмах.)

Это становится особенно актуальным, когда речь идет о реальных числах. Мы можем интуиционистски доказать что-то обо всех действительных числах, имея дело с любой произвольной последовательностью цифр. Но, конечно, полное доказательство никогда не может быть написано без именования последовательностей, что невозможно. Таким образом, теоретически может быть постоянно увеличивающийся объем работы по выравниванию переменных в двух доказательствах для все более и более обширных областей применения, и мы не хотим, чтобы это имело значение.

Большинству конструктивистов требуется больше: сходящийся процесс с фиксированным числом входных данных, который может максимально приблизить нас к результату, так что простое его выполнение всегда будет приближать нас как можно ближе. (Таким образом, шаг конкатенации, который объединяет доказательства A -> B и самого A, должен быть фактически выполнен, и любая странность, связанная с разным количеством параметров, отображаемых вместе, может иметь значение.)

В такого рода конструктивизме действительные числа как точки в каком-то смысле не существуют. Только реальное как структурированный континуум.

Брауэр, в своей мотивации из двух переживаний времени, явно считал, что оба релевантны. И он попытался исследовать базовые интуитивные представления континуума способами, которые современные конструктивисты обычно считают неконструктивными, посредством интуиции «последовательностей беззаконного выбора». Конструктивисты, чьи цели выходят за рамки интуитивизма, обычно считают релевантными только «последовательности законного выбора» и рассматривают действительное число только как искусственную точку сходимости набора рациональных чисел.

«Но, конечно, полное доказательство никогда не может быть написано без названий последовательностей». Почему? Мы постоянно доказываем что-то обо всех натуральных числах, не называя всех натуральных чисел. Доказательство — это алгоритм, который принимает произвольное число в качестве входных данных и производит доказательство для этого числа. Все, что меняется в случае с действительными числами, заключается в том, что алгоритм принимает действительное число (обычно представляемое как функция некоторого вида, возможно, с некоторыми дополнительными свойствами). Мы можем говорить о функции без явного перечисления ее диапазона.
Кроме того, «мы только пытаемся быть очень уверенными, что не ищем потенциального противоречия». Кажется, это не совсем то, если у вас нет дополнительных объяснений. Интуитивизм заключается в том, чтобы иметь возможность вообразить любое действительное доказательство, а не извлекать из математики то, что мы можем, пока не достигнем ⊥.
Хорошо, но последовательности выбора — это иной вид представления вещественного числа, чем может принять современный конструктивист. Он вводит второй слой бесконечности, а исчерпать можно только один. По конструктивистским стандартам нет места для обработки всех бесконечных последовательностей цифр таким образом, без вовлечения сходимости. Конструктивное доказательство должно иметь допуск там, где оно останавливается. Интуитивист — нет. Я пытаюсь уловить различие, которое вы игнорируете. Суть конструктивизма в том, чтобы быть конструктивным. Суть интуитивизма в надежной разработке интуиции.
Учитывая доказательства A → B и A, когда мы получим доказательство B?
СпросиСетьПолитика конфиденциальности1y, 0v