에서 프로그래밍 언어에 대한 실무 기초 , 로버트 하퍼는 말한다
제안이 참되다는 증거가 있다는 의미라면, 그 제안이 거짓이라는 것은 무엇을 의미합니까? 그것은 우리가 그것을 반박 하여 증명할 수 없음을 보여줍니다. 즉, 그것이 사실이라는 증거가 알려진 사실과 모순된다는 것을 보여줄 수 있다면 제안은 거짓입니다.
그러나 이것은 건설적 / 직관적 논리에 모순 이 무엇인가라는 질문을 제기한다 .
이것은 어떻게 든 파생의 의미 입니까? 합리적인 방법으로 이런 일이 어떻게 일어날까요? 양식 대한 판단을 도입해야합니까?( A ⊃ ⊥ true )
(⊥ true)(A⊃⊥ true)
대안으로, 독자가 재량에 따라 모순적으로 무언가를 비공식적으로 표시한다는 의미일까요? 예를 들어, 및 를 충돌하는 제안으로 해석 .a ≠ b
a=ba≠b
답변
우리가이 상황에서 건설적 논리 나 고전적 논리에 관해 말하는 것은 중요하지 않습니다. 질문을 다시 읽으면 두 종류에 모두 해당되는 것을 볼 수 있습니다. 우리의 통지를 취할 필요가 유일한 차이점은의 표현입니다 부정 . 그것은 고전적으로 여러 가지 방법으로 제시 될 수 있지만, 직관적으로 (Bob Harper가 인용 한 단락에서 암시 하는 것)의 약어로 사용하는 것이 가장 좋습니다 . 그러나 부정과 모순을 혼동하지 마십시오.A ⇒ ⊥
¬AA⇒⊥
두 경우 모두 모순은 우리가 허위 을 증명 한 상황입니다
⊥. 합리적인 방법으로 을 어떻게 도출 할 수 있을까요? 일관성이없는 일련의 가설들로부터, 그것은 그것을 할 수있는 합리적인 방법입니다.
⊥모순을 “선언”할 재량 은 없습니다 . 을 도출하여 주어진 가설 세트가 모순됨을 증명 해야합니다 . 예를 들어, 및 경우 가 의 약어이며 modus ponens에 의해 결론을 사용할 수 있습니다.a = b ¬ ( a = b ) ¬ ( a = b ) ( a = b ) ⇒ ⊥ ⊥
⊥a=b
¬(a=b)
¬(a=b)
(a=b)⇒⊥
⊥
답변
모순은 일반적으로 됩니다. 직관적 인 논리에서 를 으로 정의하는 것이 일반적입니다 . 에서 을 파생시킬 수 있습니다 . 궁극적으로 모순은 정의가 암시 하는 것처럼 의 가상 유도 일 것이다 . 그렇지 않으면 논리가 일치하지 않기 때문에 가상이됩니다.¬ A A ⇒ ⊥ ⊥ A ∧ ¬ A ⊥ ¬
A∧¬A¬A
A⇒⊥
⊥
A∧¬A
⊥
¬
하퍼하게되는 점은 뭔가을 증명하는 것입니다 있는 증거와 반박 뭔가에를하는 것입니다 있는 이 암시하는 증거 . 그러나, 당신은 쉽게 당신이 (메타가-논리적으로) 할 수있는 상황이 될 수 증명 당신이 제공 할 수없는 것을 하나 증명하거나 반박을. 그러한 상황에서 제안은 건설적으로 사실도 거짓도 아닙니다.
⊥
고전적인 논리를 이해하고 위에 대비하기위한 방법은 다음 (기본적으로 콜 모고 로프의 이중 부정의 해석)입니다 : 우리는 제안을 받았다고 거짓 이 모순을 의미하는 경우, 즉 그것이 의미 . 명제는 사실 우리가이 모순 될 수 없음을 증명 우리가 모순 거짓 리드입니다 가정 보여줄 수있는, 즉 할 수 있습니다. 기호에서 는이 의미에서 평소와 같이 인 경우 거짓입니다 . 이 의미에서 는 , 즉A A ⇒ ⊥ A ¬ A ⇒ ⊥ ¬ ¬ A ¬ ¬ ( ¬ ¬ A ∨ ¬ A ) ¬ ¬ ¬ A ⇒ ¬ A
⊥A
A⇒⊥
A
¬A⇒⊥
¬¬A
증명할 수 있습니다. 이러한 의미에서 “참”과 “거짓”을 해석하면 제외 된 중간의 법칙이 건설적으로 유지됨을 보여줄 수 있습니다. 즉, 건설적으로 보유하고 있음을 증명할 수 있습니다 . 보다 간결하게, 표시 할 수 있습니다 . 이 “참”과 “거짓”의 개념으로, 우리는 반박이 존재하지 않음을 증명할 수 있다면 제안이 참이라고 말할 수 있습니다. 반대로, 시스템 내에서 반박이 존재하지 않는다는 것을 입증 할 수 있더라도 건설적으로 건의안은 건설적으로 참이 될 수 없습니다.
¬¬(¬¬A∨¬A)¬¬¬A⇒¬A