Neel이 “제안은 유형”에서 작업하는 경우 와 같이 같은 유형을 결정할 수없는 유형을 쉽게 찾을 수 있습니다 (물론 모든 유형이 동일한 유형을 가질 수 있다고 가정하는 것은 일관됩니다). .N→N

$\mathbb{N} \to \mathbb{N}$

“제안”을보다 제한적인 유형으로 이해한다면 그 대답은 우리가 정확히 무엇을 의미하는지에 달려 있습니다. 당신이 Prop종류 의 건축 미적분학에서 일하고 있다면 , 결정 가능한 제안이 결정 가능한 평등을 가지고 있음을 보여줄 수는 없습니다. 이는 계산 미적분학 Prop에서 증명 관련 유형의 우주와 동일하기 때문에Prop 과 같은 것을 포함 할 수 있기 때문입니다 . 이것은 또한 Coq의 개념에 대한 정리를 증명할 수 없음을 의미합니다 .N→N

$\mathbb{N} \to \mathbb{N}$Prop

그러나 어쨌든 가장 좋은 대답은 homotopy type 이론에서 비롯됩니다. 제안은 를 만족 하는 유형 입니다

즉, 발의안은 최대 한 가지 요소를 갖습니다 (증거와 관련이없는 진실의 가치로 이해되어야하는 것처럼). 이 경우 제안의 정의가 그 평등을 결정할 수 있음을 즉시 암시하기 때문에 대답은 물론 긍정적입니다.P

$P$

$$\forall x, y : P \,.\, x = y.$$

“제안”의 의미가 무엇인지 궁금합니다.

답변