Читать реферат по математике: "Конструктивная математика" Страница 7
(Назад)
(Cкачать работу)(х)) опровергается, например, для A (x) = E y T (x,x,y), где T (e,x,y) означает, что алгоритм (с кодом) е заканчивает работу над аргументом x за у шагов. Опровергается и закон двойного отрицания х ( В (х) В (х)), например для В (х)= (х) А (х). Приведенное определение связывает конструктивную задачу (поиск реализации) со всяким суждением A, даже если А не содержит , . Предложенный Н.А. Шаниным алгоритм выявления конструктивной задачи не меняет формул без , (нормальных формул) и эквивалентен реализуемости в формальной интуиционистической арифметике с бескванторной индукцией. Произвольные формулы сводятся к почти нормальным, так как основания для почти нормальных формул, содержащих и нетривиальное .
А.А. Марков определяет истинность для почти нормальных формул с помощью выводимости по обычным правилам для рассматриваемых логических связок плюс эффективное -правило: если имеется общий метод, позволяющий для любого n устанавливать выводимость А(n) из суждения К, то х (х) выводимо из К.. Истинность определяется постепенно. Язык Я , состоящий из из формул без ,; язык Яn+1, n 1, включая Яn и формулы, которые можно построить из формул языка Яn одним применением импликации и любым числом применений А, &. Истинность для Я1 – формул – это выводимость по обычным правилам для &, , . Истинность для Я2 -формул определяется через допустимость соответствующего правила. Например, истинность х R (х) y T (y) означает наличие алгоритма такого, что R (n) T ( (n )) для любого числа n. Для Яn+1 – формул при n>1 истинность конъюкций и -формул определяется обычным образом через истинность компонента, а истинность импликации А В означает выводимость В из А по некоторым правилам Sn, о которых уже доказано, что они сохраняют истинность Яn– формул. Системы Sn содержат -правило, а в качестве аксиом – все истинные Яn– формулы. Понятие выводимости в Sn вводится обобщенным индуктивным определением, а для доказательства метатеорем применяется соответствующий принцип индукции. Индукцией по S2 – выводу доказывается допустимость правила х R - А х R . Оно включается в S3и даёт принцип Маркова х R х R.. Системы Sn+3 , n 1, состоят из обычных правил для рассматриваемых связок, включая -правило. Оказывается, что почти нормальная формула А истинна по Маркову тогда и только тогда, когда примитивно рекурсивное дерево Tа поиска вывода формулы А без сечения (но с -правилом и принципом Маркова) является выводом в смысле индуктивного определения. Это эквивалентно (в рамках классической математики) классической истинности А.
В мажоритальной семантике Н.А. Шанина для каждой почти нормальной формулы А определяется трансвинитная иерархия {А } формул простой структуры, причём А А доказуемо в подходящей формальной системе. Формула А называется мажоритарной для А,и А считается истинной формулой ранга , если А верна. Точность аппроксимации растёт с ростом : < ( А А ). Если отвлечься от технических деталей, то формула А строится с помощью - кратного вынесения кванторов, согласно эквивалентности
(В u vC (u, v)) u v (B u vC(u, v) C(u, v)),
и сворачивания цепочек кванторов с помощью алгоритма выявления конструктивной задачи. Это даёт доказуемую в арифметике с транксфинитной
Похожие работы
Интересная статья: Основы написания курсовой работы