Интуиционистская пропозициональная логика
Я изучал интуиционистскую логику и то, что называется «негативным фрагментом» интуиционистской пропозициональной логики. Однако мне не удалось найти ни одного ресурса, объясняющего причину, по которой он называется «отрицательным фрагментом».
Любые ссылки/предложения?
Был упомянут Робертом Харпером (см. cs.cmu.edu/~rwh/courses/hott/notes/notes_week1.pdf и cs.cmu.edu/~rwh/courses/hott). Он упоминает об этом ближе к концу лекции 1 и явно не вникает в причину, по которой «отрицательный фрагмент» является названием. Это меня заинтересовало, но я не смог найти вескую причину. Может потом на лекциях объяснит, но чувствовалось, что это что-то общеизвестное.
Ответы 1
Согласно Отрицательные переводы не интуиционистски эквивалентны обычным ,
Образом обычных негативных переводов является (по существу) негативный фрагмент NF, то есть множество всех формул без ∨ и ∃, атомарные формулы которых все отрицается
Если вы посмотрите на правила, приведенные на странице 3 (или здесь), неудивительно, что перевод называется отрицательным. Фрагмент, определенный Харпером, устраняет требование,
атомарные формулы все отрицается
Не могли бы вы указать ссылку, где вы это нашли? Это может помочь нам дать вам более точный ответ.