The relation between negation and infinity loomed large in the Intuitionist critique of mathematics. But when we come to Intuitionistic logic, it turns out to be all about the conditional. Negation comes in just by means of a definition: ~A =def A β f.
It is in the logicβs realizations that the intimate relation between negation and infinity comes to the fore. Recall from the previous post that the lattice of theories of any distributive logic is a complete Heyting lattice with zero element Cn(π), and
T β Tβ is the weakest (largest) theory X such that T β© X β Tβ;
T β Tβ = β{Tββ: T β© Tββ β Tβ)
The pseudo-complement Β¬T of T, if it exist, must be the weakest element X which is contrary to T, that is, it is such that T β© X β Cn(π). So we instantiate the above: Β¬ T is the weakest element X such that T β© X β Cn(π)), hence:
Β¬ T = T β Cn(π). Equivalently, Β¬ T = β{Tβ: T β© Tβ β Cn(π)}.
So much, so general. How does it happen that the Laws of Excluded Middle and of Double Negation fail in Intuitionistic logic, and their corresponding principles fail in the calculus of systems?
To continue, let L be classical propositional logic, with & and ~ as primitive connectives and let S be the set of all sentences. Thus S = Cn(S) is the unit (top) of the lattice. For brevity, if A is a sentence I will write βCn(A)β for “Cn({A})”.
Note: Contrariety, the condition T β© Tβ β Cn(π), is different from mutually inconsistency. With p, q atomic sentences, Cn(π) is contrary to but consistent with Cn(p), Cn(p) and Cn(~p) are both mutually inconsistent and contrary. But Cn(p & q) and Cn(~p & q) are mutually inconsistent, their join is S, but not contrary for their intersection contains non-theorem q. Contrariety is this:
Theorem 1. T β© Tβ β Cn(π) iff for every non-theorem A in T there is a consistent extension of Tβ that includes ~A.
To prove this we can appeal to the general features of theories in classical logic:
- any consistent theory is part of a maximal consistent theory
- every theory is the intersection of all its maximal consistent extensions
- for all sentences A, if T is a maximal consistent theory then T contains either A or ~A
- if T does not imply A then T has a maximal consistent extension that includes ~A
Proof.
- Let A be any L-non-theorem in T. Suppose that Tβ has no consistent extension that includes ~A. Then A is in all the maximal consistent extensions of Tβ, hence in Tβ, hence in T β© Tβ, which is thererfore not included in Cn(π).
- Suppose that for every L-non-theorem A in T, Tβ has a consistent extension which includes ~A. Then if A is an L-non-theorem in T, A is not in Tβ, and hence not in T β© Tβ. If A is an L-non-theorem that is not in T then it is also not in T β© Tβ. Therefore T β© Tβ contains only L-theorems, and is Cn(π).
Lemma 1. Cn(~A) β Β¬Cn(A)
If E is in Cn(A) there is a sentence B such that E is equivalent to A v B. For each such sentence Cn(~A) has a consistent extension that includes ~(A v B).
- If ~A entails B then it too entails A v B, so then A v ~A entails A v B, hence A v B is an L-theorem.
- If ~A does not entail B then Cn(~A) has a maximal consistent extension that includes ~B, which includes ~A & ~B.
So by Theorem 1, Cn(A) β© Cn(~A) β Cn(π). Hence Cn(~A) β CnA) β Cn(π) = Β¬Cn(A).
Theorem 2. If T is finitely axiomatizable then T Ξ Β¬T = S
Because of the classical conjunction rules, if T is finitely axiomatizable then there is a sentence A such that T = Cn(A). By the lemma, Cn(A) Ξ Cn(~A) β Cn(A) Ξ Β¬Cn(A). But Cn(A) Ξ Cn(~A) = Cn(Cn(A) βͺ Cn(~A)) = S.
It follows then that violations of Excluded Middle can only be by theories that are not finitely axiomatizable.
To pursue this we need to improve on the above lemma.
Lemma 2. T β© Tβ β Cn(π) iff for every non-theorem A in T there is a maximal consistent extension of Tβ that includes ~A.
This follows at once from Theorem 1.
Lemma 3. If T β© Tβ β Cn(π) then Tβ β β© Cn({~A: A is in T})
Suppose T β© Tβ β Cn(π) and that A is an L-non-theorem of T. Let KTβ(A) be the set of all consistent extensions of Tβ that include ~A. So β©KTβ(A) β Cn(~A). Let MTβ be the set of all maximal consistent extensions of T. Then for each L-non-theorem A of T:
Tβ = β©MTβ β β©KTβ(A) β Cn(~A).
Since Tβ has a consistent extension that includes ~A for each L-non-theorem in T it follows that Tβ β β©{Cn(~A): A is an L-non-theorem in T}. From this the lemma follows because if A is an L-theorem then Cn({~A}) = S, which has no effect on the intersection.
Theorem 3. Β¬T = β©({Cn{~A}: A in T}).
First, it is clear that for every L-non-theorem A in T, β©({Cn{~A}: A in T}) has a consistent extension that includes ~A. Therefore β©({Cn{~A}: A in T}) β Β¬T by theorem 1 and definition.
Secondly, T β© Β¬T β Cn(π), so by Lemma 3, Β¬T β β© Cn({~A: A is in T})
Corollaries: Cn({~A}) = Β¬Cn(A), Β¬Cn(π) = S, Β¬S = Cn(π)
This theorem gives us a way to identify the pseudo-complement of theories that are not finitely axiomatizable.
Example. Let AT be the infinite list of atomic sentences p1, β¦, pm , β¦ and T = Cn(AT). Let ATfin be the set of finite conjunctions of atomic sentences. Every member of T is equivalent to a finite conjunction C of atomic sentences disjoined with some other sentence A (e.g. p v q).
So Β¬T = β© Cn({~(C v A): C in ATfin})
As an example, consider the L-non-theorem (p1 & ~p2). Could it belong to Β¬T? It does not belong either to Cn(~p1) or to Cn(~p2). Nor does it belong to Cn(~q) for any q in ATfin other than p1 or p2.
We can generalize this reasoning to cover any L-non-theorem. Since L is classical propositional logic, we can think in terms of truth-table rows or their generalization:
a finite state-description is a consistent conjunction p*1 & β¦& p*m of atomic sentences each of which either has or does not have an appended negation sign.
In classical propositional logic, A is an L-non-theorem if and only if there is a finite state-description B such that BβL~A. For any such B, since B is finite and AT is infinite, there is an atomic sentence q which does not appear in B. But then B is not in Cn(~q), hence not in Β¬T. Therefore there is no derivation of ~A in Β¬T. Hence Β¬T = Cn(π).
This gives us a counterexample to both Excluded Middle and Double Negation, with T = Cn(AT):
T β Β¬T = T and T β S
Β¬ Β¬T = Β¬ Cn(π) = S and S β T
The following analogy strikes me as apt. Remember that Β¬T is also the join of its contraries. There are uncountably many infinite state descriptions, all inconsistent with each other. So we can look to continua for analogies. In a geometric space, the join of a family of subspaces is the least subspace that contains all. Suppose P is a plane, its subspaces are the straight lines through the origin. Take away one such straight line: the join of the remaining ones is still the entire plane.
Bas van Fraassen's philosophy blog 