Место издания:Русское общество истории и философии науки Москва
Первая страница:247
Последняя страница:251
Аннотация:В работе рассматривается система натурального вывода с зависимостями (линейного типа Леммона), предложенная Аланом Виром для нетранзитивной трехзначной («неоклассической») логики NC3 в рамках разрабатываемого им подхода к анализу парадокса Карри. Характерной чертой NC3 является наличие двух направлений (сохранение истинности сверху вниз и сохранение ложности снизу вверх) при определении отношения логического следования, которые взаимовыводимы в классической логике. Такое определение приводит к тому, что NC3 не обладает стандартным свойством обобщенной транзитивности или сечения, которое является неотъемлемым для классической логики. В духе разрабатываемого автором подхода к поиску натурального вывода для NC3 предложен конечный, непротиворечивый и полный алгоритм поиска вывода, его блоксхема и псевдокод. Отметим, что алгоритм позволяет извлекать контрпример (модель, опровергающую исходную формулу или выводимость) в случае неудачного поиска вывода.
