If the classical notion of knowledge-independent truth is replaced by the constructive one of possessing a construction or proof, then logic must be explained differently. On the so-called Proof Interpretation, implication for example is now explained as a method that, whenever I have a proof of the antecedent, can be used to transform it into a proof of the consequent. The Principle of the Excluded Middle is rejected, as, given an arbitrary proposition, one is not always in a position to prove it or its negation. One might suspect that this rejection implies that propositions possess a “third” truth value, yet we present a theorem by Glivenko demonstrating that intuitionistic logic is not three-valued. We also show that while proof by contradiction is useful for establishing negative facts, it is, in general, powerless to establish positive ones.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Logic

  • Dirk van Dalen,
  • Mark van Atten,
  • Craig Smoryński

摘要

If the classical notion of knowledge-independent truth is replaced by the constructive one of possessing a construction or proof, then logic must be explained differently. On the so-called Proof Interpretation, implication for example is now explained as a method that, whenever I have a proof of the antecedent, can be used to transform it into a proof of the consequent. The Principle of the Excluded Middle is rejected, as, given an arbitrary proposition, one is not always in a position to prove it or its negation. One might suspect that this rejection implies that propositions possess a “third” truth value, yet we present a theorem by Glivenko demonstrating that intuitionistic logic is not three-valued. We also show that while proof by contradiction is useful for establishing negative facts, it is, in general, powerless to establish positive ones.