This is my first question here, sorry if it turns out to be a duplicate. Mathematical constructivism states that contradicting the non-existence of something won't imply its existence. Does it mean that the tertium non datur does not apply in the question of existence? Is there such a concept, whose non-existence has been proved to be false, yet its existence is still undecided/unproven? Or is the trait of existence of such nature, that is has at least one more state, other than existing or non-existing?
2 Answers
You can see my answer to this post and the relevant quotation from :
- Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 26 :
Classical logic contains the principle of indirect proof: If ¬A leads to a contradiction, A can be inferred. Axiomatically expressed, this principle is contained in the law of double negation, ¬¬A → A. The law of excluded middle, A ∨ ¬A, is a somewhat stronger way of expressing the same principle.
Under the constructive interpretation, the law of excluded middle is not an empty "tautology," but expresses the decidability of proposition A. Similarly, a direct proof of an existential proposition ∃xA consists of a proof of A for some ["witness"] a. Classically, we can prove existence indirectly by assuming that there is no x such that A, then deriving a contradiction, and concluding that such an x exists. Here the classical law of double negation is used for deriving ∃xA from ¬¬∃xA.
Thus, it is correct to say that, from a constructivist point of view, tertium non datur [i.e. excluded middle] does not apply in general.
Its application to existence proofs impies that the existence of a witness of A is undecided/unproven until we are not able to "show it".
answered Sep 12, 2014 at 9:38
As Mauro Allegranza said, in intuitionistic logics the law of excluded middle (and tertium non datur, when the two are distinguished) are not assumed to hold in general. That is, we cannot assume A∨¬A is a tautology for every given A (including, for example, A:=∃xB). It may be true for particular choices of A, just not all of them. It may even happen to be true for all choices of A, but our logic cannot internalize knowledge of that fact (e.g., because the proposition's truth may be contingent rather than necessary, or it may not be uniform in some relevant sense).
More specifically: from ¬¬∃xA we are allowed to conclude ¬∀x¬A, since intuitionistic logic validates the equivalences between ¬∃xA and (∃xA)→⊥, and between (∃xA)→B and ∀x(A→B) (for any A and B where x does not occur free in B). However, going from ¬∀x¬A to ∃x¬¬A is where we run into problems (let alone getting from ∃x¬¬A to ∃xA). In the BHK interpretation of intuitionistic logic, ∃x¬A entails ¬∀xA for any A (because ∃x(A→B) entails (∀xA)→B, more generally); however, the converse does not hold. Just because it's absurd to think every entity has a given property, that doesn't let us fabricate an entity which lacks that property. We can't just suppose some entity exists out there in the aether; we must exhibit a particular entity to witness our claim that one exists.
I note that the above holds for the BHK interpretation of intuitionistic logic because it's not true of all "constructive logics". In particular, the so-called Russian constructivists accept the validity of the generalized Markov's principle (GMP): "¬∀xA entails ∃x¬A for any A". Notably, whenever the domain of x is finitely enumerable, the GMP is perfectly justifiable according to BHK principles: our proof procedure is to exhaustively search through the domain until we come up with a witness. It's even fine for some infinite spaces which admit certain compactness properties; again, because we can exhibit an algorithm for actually constructing a witness to the existential claim. Intuitionists balk at the full power of the GMP because we are unwilling to assume that all domains of quantification admit some such algorithm for constructing witnesses, just as we balk at the full power of LEM because we do not assume all propositions are decidable.
Regarding your second question: intuitionistic logic has three states of "truthiness": A, ¬A, and ¬¬A. (N.B., this does not mean there are three truth values!) As for naming these states of truthiness, some opt for syntactically-oriented names ("positive", "negative", and "double-negative") whereas others prefer semantically-oriented names ("strictly positive", "negative", and "(weakly) positive"). Some authors will say "A is weakly true" to mean ¬¬A is true. Analogously, one could say "there weakly exists some x such that A" to mean ¬¬∃xA is true.
