Сообщение Re[2]: Самопроверяющиеся теории от 05.03.2020 21:35
Изменено 05.03.2020 22:09 nikov
Re[2]: Самопроверяющиеся теории
Здравствуйте, nikov, Вы писали:
ЭФ>>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?
N>https://en.wikipedia.org/wiki/Self-verifying_theories
Арифметика Пеано (PA) на самом деле очень близко подходит к доказательству своей непротиворечивости. Для любого числа N, в PA можно доказать её ограниченную непротиворечивость, т.е. "В PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где мы подставляем вместо переменной N её значение). Это немного не дотягивает до полноценного утверждения о непротиворечивости "Для любого числа N, в PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где N — переменная, связанная квантором ∀).
Однако, непротиворечивость PA можно доказать, если воспользоваться дополнительной аксиомой о вполне-упорядоченности (well-ordering) многоэтажных многочленов с целыми положительными коэффициентами по скорости роста (которая очень интуитивна, если над ней чуть-учть подумать). Ну, само собой, эту аксиому нельзя доказать в PA, и если она не очевидна, то для её доказательства уже нужна какая-то слабая версия теории множеств с хотя бы счётными ординалами и трансфинитной индукцией.
ЭФ>>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?
N>https://en.wikipedia.org/wiki/Self-verifying_theories
Арифметика Пеано (PA) на самом деле очень близко подходит к доказательству своей непротиворечивости. Для любого числа N, в PA можно доказать её ограниченную непротиворечивость, т.е. "В PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где мы подставляем вместо переменной N её значение). Это немного не дотягивает до полноценного утверждения о непротиворечивости "Для любого числа N, в PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где N — переменная, связанная квантором ∀).
Однако, непротиворечивость PA можно доказать, если воспользоваться дополнительной аксиомой о вполне-упорядоченности (well-ordering) многоэтажных многочленов с целыми положительными коэффициентами по скорости роста (которая очень интуитивна, если над ней чуть-учть подумать). Ну, само собой, эту аксиому нельзя доказать в PA, и если она не очевидна, то для её доказательства уже нужна какая-то слабая версия теории множеств с хотя бы счётными ординалами и трансфинитной индукцией.
Re[2]: Самопроверяющиеся теории
Здравствуйте, nikov, Вы писали:
ЭФ>>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?
N>https://en.wikipedia.org/wiki/Self-verifying_theories
Арифметика Пеано (PA) на самом деле очень близко подходит к доказательству своей непротиворечивости. Для любого числа N, в PA можно доказать её ограниченную непротиворечивость, т.е. "В PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где мы подставляем вместо переменной N её значение). Это немного не дотягивает до полноценного утверждения о непротиворечивости "Для любого числа N, в PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где N — переменная, связанная квантором ∀).
Однако, непротиворечивость PA можно доказать, если воспользоваться дополнительной аксиомой о вполне-упорядоченности (well-ordering) многоэтажных многочленов с целыми положительными коэффициентами по скорости роста (которая очень интуитивна для большинства людей, если над ней чуть-чуть подумать). Ну, само собой, эту аксиому нельзя доказать в PA, и если она не очевидна, то для её доказательства уже нужна какая-то слабая версия теории множеств с хотя бы счётными ординалами и трансфинитной индукцией.
ЭФ>>На странице "Теория доказательств" упомянуты "самопроверяющиеся теории".
ЭФ>>Где бы про это почитать по-подробнее, с увязкой к современным языкам программирования?
N>https://en.wikipedia.org/wiki/Self-verifying_theories
Арифметика Пеано (PA) на самом деле очень близко подходит к доказательству своей непротиворечивости. Для любого числа N, в PA можно доказать её ограниченную непротиворечивость, т.е. "В PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где мы подставляем вместо переменной N её значение). Это немного не дотягивает до полноценного утверждения о непротиворечивости "Для любого числа N, в PA нет доказательства длиной ≤ N, которое приводило бы к противоречию" (где N — переменная, связанная квантором ∀).
Однако, непротиворечивость PA можно доказать, если воспользоваться дополнительной аксиомой о вполне-упорядоченности (well-ordering) многоэтажных многочленов с целыми положительными коэффициентами по скорости роста (которая очень интуитивна для большинства людей, если над ней чуть-чуть подумать). Ну, само собой, эту аксиому нельзя доказать в PA, и если она не очевидна, то для её доказательства уже нужна какая-то слабая версия теории множеств с хотя бы счётными ординалами и трансфинитной индукцией.