А вот в классической логике нужно как-то уточнить, что "или" здесь исключающее.
В интуиционизме ничего странного тоже не заявляется. Всего лишь, мы можем доказать ненаселённость опровержения (A | -A) не зависимо от доказательства A и доказательства -A. Это на мой взгляд очень сильное утверждение.
И ещё замечательное свойство интуиционисткого построения доказательства - Either A B всегда "исключающее" - в том смысле, что каждое значение этого типа может содержать только одно из A и B, хотя не отрицается населённость обоих. Поэтому нужно доказать также -(A & -A), то есть, что A и -A не могут быть населены одновременно. Выходит, что -(A & -A) можно доказать с помощью пары -(-A → A) и -(A → -A), а это есть ничто иное как первый и второй закон классики: -A → -A и A → --A.
Таким образом, на пальцах понятно, что Either A (A→⊥) населён, но для consistency мы считаем это недоказанным, пока не будет построено доказательство - т.е. предоставлены конкретные стрелки Left и Right; одна из них будет ⊥→⊥, но чтобы выяснить, какая, нужно доказательство населённости второго.
no subject
В интуиционизме ничего странного тоже не заявляется. Всего лишь, мы можем доказать ненаселённость опровержения (A | -A) не зависимо от доказательства A и доказательства -A. Это на мой взгляд очень сильное утверждение.
И ещё замечательное свойство интуиционисткого построения доказательства - Either A B всегда "исключающее" - в том смысле, что каждое значение этого типа может содержать только одно из A и B, хотя не отрицается населённость обоих. Поэтому нужно доказать также -(A & -A), то есть, что A и -A не могут быть населены одновременно. Выходит, что -(A & -A) можно доказать с помощью пары -(-A → A) и -(A → -A), а это есть ничто иное как первый и второй закон классики: -A → -A и A → --A.
Таким образом, на пальцах понятно, что Either A (A→⊥) населён, но для consistency мы считаем это недоказанным, пока не будет построено доказательство - т.е. предоставлены конкретные стрелки Left и Right; одна из них будет ⊥→⊥, но чтобы выяснить, какая, нужно доказательство населённости второго.