Logic
摘要
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.