Интуиционистская пропозициональная логика

Я изучал интуиционистскую логику и то, что называется отрицательным фрагментом интуиционистской пропозициональной логики. Однако мне не удалось найти ни одного ресурса, объясняющего причину, по которой он называется отрицательным фрагментом.

Любые ссылки/предложения?


logic dependent-type type-theory
person geguze    schedule 20.12.2020    source источник
comment
Не могли бы вы указать ссылку, где вы это нашли? Это может помочь нам дать вам более точный ответ.   -  person lemontree    schedule 21.12.2020
comment
Был упомянут Робертом Харпером (см. cs.cmu.edu/ ~rwh/courses/hott/notes/notes_week1.pdf и cs .cmu.edu/~rwh/courses/hott). Он упоминает об этом ближе к концу лекции 1 и явно не вникает в причину, по которой отрицательный фрагмент является именем. Это меня заинтересовало, но я не смог найти вескую причину. Может быть, позже на лекциях он объяснит, но чувствовалось, что это что-то общеизвестное.   -  person geguze    schedule 21.12.2020

Ответы (1)


arrow_upward
1
arrow_downward

Согласно отрицательные переводы интуитивно не эквивалентны обычным,

Образ обычных отрицательных переводов - это (по существу) отрицательный фрагмент NF, то есть множество всех формул без ∨ и ∃, чьи атомарные формулы все отрицаются.

Если вы посмотрите на правила, приведенные на странице 3 (или здесь), неудивительно, что перевод называется отрицательным. Фрагмент, определенный Харпером, устраняет требование,

все атомарные формулы отрицаются

person Alexey Romanov    schedule 21.12.2020