Constructive mathemathics and its dual
17Kawoomba
3MrMind
4AlexMennen
1MrMind
3MrMind
2wedrifid
2MrMind
14[anonymous]
3ScottMessick
1MrMind
3passive_fist
1MrMind
1bogus
0bryjnar
2Shmi
0MrMind
0AlexMennen
0MrMind
3AlexMennen
2Benya
1Pfft
0AlexMennen
0prase
0shinoteki
0prase
-1[anonymous]
0Benya
6Benya
1Pfft
-1bryjnar
New Comment
It would be helpful to follow along if you at least gave a short sketch of where you're going with this, if only broadly. After all, this isn't a mystery novel with a cliffhanger ending.
Uhm, I'll think about a summary: not an easy task but those who already know constructive mathematics should be pointed in the right direction. As for the cliffhanger, it was admittedly deliberated: it's not the case that a math post has to be boring!
I've now modified the introduction to at least present the briefest sketch of the topic, hoping not to alienate even more people!
not an easy task but those who already know constructive mathematics should be pointed in the right direction.
There is enough of a pointer that thinking through the implications constitutes a free and comparatively safe alternative to tripping on hallucinogens. Thankyou!
Eheh, then for a serious trip wait for the post on destructive theodicy, I'll call it "Azathoth hates us all" :)
The post seems to confuse the law of non-contradiction with the principle of explosion. To understand this point, it helps to know about minimal logic which is like intuitionistic logic but even weaker, as it treats ((false)) the same way as any other primitive predicate. Minimal logic rejects the principle of explosion as well as the law of the excluded middle (LEM, which the main post called TND).
The law of non-contradiction (LNC) is just ). (In the main post this is called ECQ, which I believe is erroneous; ECQ should refer to the principle of explosion (especially the second form).) The principle of explosion is either
%20\to%20Q) or
. These two forms are equivalent in minimal logic (due to the law of non-contradiction). As mentioned above, minimal logic has the law of non-contradiction, but not the principle of explosion, so this shows that they're not equivalent in every circumstance. Rejecting the principle of explosion (especially the second form) is the defining feature of paraconsistent logics (a class into which many logics fall). Some of these still have the validity of the law of non-contradiction. Anti-intuitionistic logic does not, because LNC is dual to LEM, which is invalid intuitionistically.
Ok, so I ended up taking a lot of time researching that nitpick so I could say it correctly. Anyway, I'm curious to see where this is going.
I think it's good to make all these distinctions in the comments, so that the main post is not cluttered but at the same time who wants to have all the details can have them just by reading further.
As far as I know, dialetheism starts from an ontological assertion (there are true contradictions), while this idea of dual constructive mathematics is more of an epistemic framework, so I would say: if they are related, they are only weakly so.
Actually, I think constructive mathematics makes a strong case for dialetheism, or at least for not caring much about logical inconsistency. The problem is that the "constructive mathematics" equivalent to full general recursion is an inconsistent logic. Thus, logical inconsistencies are a lot like non-terminating programs in a Turing-complete programming language. (This can be formally stated in proof theory and type theory; it follows from the properties of progress and preservation, and from the fact that there is no construction of Falsum.) Of course one can limit oneself to only talking about finite, terminating proofs, but since the halting problem is unsolvable, all such limitations are "hacks" which will exclude some interesting constructions.
From a Platonic point of view, it is implausible that the "real" mathematical universe implements one of these ugly hacks; it's much more plausible that "paradoxical" objects actually exist, but we are limited in talking about them by the need to exclude non-terminating proofs (such as "the set of all sets that don't contain themselves is a member of itself, assuming that it isn't a member of itself; but in fact it isn't, assuming that it is; but in fact it is, assuming that it isn't ..." and so on).
Dialethists requires paraconsistent logic, as you have to be able to reason in the presence of contradictions, but paraconsitent logic can be used to model other things than truth. For example, constructive logic is often given the semantics of showing what statements can be proven, rather than what statements are true. There are similar interpretations for paraconsistent logic.
OTOH, if you think that paraconsistent logic is the correct logic for truth, then you probably do have to be a dialethist.
ECQ and TND are both theorems (or axioms) of classical logic. They are in fact equivalent.
Nitpick: any 2 theorems are equivalent to each other, so that's redundant. Perhaps you meant to say that they are in fact intuitively related to each other.
Maybe a better phrasing could have been: if you assume one as an axiom, the other follows as a theorem.
Yes, that's what equivalence means. And if X and Y are both theorems, then if you assume either as an axiom, then the other must follow as a theorem.
It's standard to say that the axiom of choice is equivalent to the well-ordering principle, which means that if you add either to ZF, the other follows and you get ZFC. As I'm reading this, the relevant paragraph in the OP reads,
Notice though: ECQ and TND are both theorems (or axioms) of classical logic. They are in fact equivalent. ECQ is espressed as
, but under the DeMorgan laws, double negation elimination and commutativity of disjunction:
, which is the TND.
So I interpret MrMind as giving the analogous statement with ZF -> (DeMorgan + DNE + commutativity of disjunction + possibly something else?), axiom of choice -> ECQ, well-ordering principle -> TND, and ZFC -> "classical logic" ... which is probably meant to mean classical propositional logic in this context?
I haven't checked this claim, if indeed that was what was intended, though.
The problem is that double negation elimination is already equivalent to classical logic (i.e. adding double negation elimination to minimal logic gives the law of excluded middle as a theorem), so there is no "background theory" like ZF to work in.
Ah, okay. I had been interpreting him as saying that they are equivalent in classical logic. But yeah, they probably are equivalent under a weaker subset of classical logic in which neither is a theorem on its own.
Wouldn't it be still possible for a constructivist to embrace classical logic and the theoremhood of TND? The constructivist would just have to admit that (A or B) could be true even if neither A nor B is true. (A or B) would still not be meaningless, its truth would imply that there is proof for neither (not A) nor (not B), so this reinterpretation of "or" doesn't seem to be a big deal.
Constructively, (not ((not A) and (not B))) is weaker than (A or B). While you could call the former "A or B", you then have to come up with a new name for the latter.
I haven't been suggesting using (A or B) as a name for (not ((not A) and (not B))) in constructive logic where they aren't equivalent. Rather, I have been suggesting using classical logic (where the above sentences are equivalent) with a constructivist interpretation, i.e. not making difference between "true" and "theorem". But since it is possible for (A or B) to be a theorem and simultaneously for both A and B to be non-theorems, logical "or" would not have the same interpretation, namely it wouldn't match the common language "or" (for when we say "A or B is true", we mean that indeed one of them must be true).
I tend to like constructivist maths because it makes sense from a computational point of view. A boolean function may return True or False or it may not return at all (a member of the bottom set in Type theory terms) if it gets stuck in an infinite loop.
So I'm going to look at things from a computational point of view, to see if anything shakes loose. What might ~(A and ~A) represent computationally. The one thing I can think of is if A isn't a pure function, it is an unknown monad of some variety (there is some hidden state). A race condition or memory corruption that means when A is evaluated at different points in time it comes to a different value.
Going by the MWI hint, it also seems to be able to represent questions that aren't meaningful to ask. Did a particle travel through that path or did it not travel that path? Well it travelled through all possible paths, which is neither a yes or a no. You may want a logic that can represent such meaningless questions, because you can't apriori know that a question is meaningless.
So I'm going to look at things from a computational point of view, to see if anything shakes loose. What might ~(A and ~A) represent computationally.
In intuitionistic type theory, if you use the usual definitions that %20:=%20(X\to\bot)) and that
means the set of pairs of elements of
and elements of
, then
) is inhabited because given an element
and a function
, you can apply
to
to get
. This still works if you replace
by some other set which may not be empty (giving the whole thing more computational content but still leaving ECQ trivially true). Perhaps you could come up with an even more different definition of
?
[This comment is no longer endorsed by its author]
Ah, wait. I think it's much simpler -- and "much more dual."
Skimming some things about anti-intuitionistic logic, in "Anti-intuitionism and paraconsistency" by Brunner and Carnielli, I found the following slogan:
This denomination can be understood taking into account that, as far as the intuitionistic philosophic program is committed to constructing truthood, our anti-constructive logics can be seen as committed to eliminating falsehood.
So how about we keep the computational content of intuitionistic logic/type theory exactly, but change our logical interpretation of these constructs? Instead of asking what computational object it would take to prove a given logical statement, let's ask what it would take to disprove this statement.
(A and B), intuitionistic interpretation: To prove this you need a proof of A and a proof of B, so if A and B are types, (A and B) is the type of pairs of elements of A and elements of B.
(A and B), anti-intuitionistic interpretation: To disprove this you need to say that you're going to disprove A and then disprove it, or you need to say that you're going to disprove B and then disprove it, so if A and B are types, (A and B) is the disjoint union of A and B.
(A or B), intuitionistic: To prove this, say you're going to prove A then prove it, or say you're going to prove B then prove it; (A or B) is the disjoint union of A and B.
(A or B), anti-intuitionistic: To disprove this you need to disprove both A and B; elements of (A or B) are pairs of elements of A and elements of B.
(exists x:X. P(x)), intuitionistic: To prove this, tell us an element x of X, then prove P(x). Elements of (exists x:X. P(x)) are pairs where the first element is an element x of X, and the second element is an element of P(x).
(exists x:X. P(x)), anti-intuitionistic: To disprove this, you need to disprove P(x) for every possible element x of X. Elements of (exists x:X. P(x)) are functions taking an element x of X and returning an element of P(x).
(forall x:X. P(x)), intuitionistic: To prove this, you need to prove P(x) for every possible element x of X. Elements of (forall x:X. P(x)) are functions taking an element x of X and returning an element of P(x).
(forall x:X. P(x)), anti-intuitionistic: To disprove this, tell us an element x of X, then disprove P(x). Elements of (forall x:X. P(x)) are pairs where the first element is an element x of X, and the second element is an element of P(x).
(False), intuitionistic: There is no proof of this, so this is the empty type.
(False), anti-intuitionistic: This is trivial to disprove, so this is the unit type.
(True), intuitionistic: This is trivial to prove, so this is the unit type.
(True), anti-intuitionistic: This is impossible to disprove, so this is the empty type.
(A implies B), intuitionistic: To prove this, you need to give a proof of B if you're given a proof of A, so this is the type of functions from A to B.
This time, instead of asking what (A implies B) is in anti-intuitionistic logic (because what you do is that in fact there simply is no implication connective), let's ask: what logical connective should anti-intuitionistically map to the type of functions from A to B? I.e., what connective is such that to disprove it, you need to be able to convert a disproof of A into a disproof of B?
Actually, what we do is to simply invent a new one, "pseudo-difference", or "but not", which corresponds to the classical logic (A and (not B)) in the same way that intuitionistic implication corresponds to the classical ((not A) or B). Thus:
(A but not B) aka (A - B), anti-intuitionistically: To disprove this, you need to give a disproof of A given a disproof of B, so this is the type of functions from B to A.
Finally, (not X) is defined as (True - X), with the same interpretation of "a function from X to the empty type" as in intuitionistic logic.
Hm, maybe we can formulate this using just the intuinistic provability judgement. We associate each formula A with a formula〈A〉which is the type of refutations of A, such that A is disprovable if 〈A〉is (intuinistically) provable. The cases you give for ∧,∨,∃,∀, True and False become
〈A∧B〉= 〈A〉∨〈B〉
〈A∨B〉= 〈A〉∧〈B〉
〈∃ (x:A).B〉= ∀(x:A).〈B〉
〈∀ (x:A).B〉= ∃(x:A).〈B〉
〈True〉= False
〈False〉= True
and we can indeed see that this is "dual" in the sense that 〈〈A〉〉= A.
The domain of the ∀ and ∃ cases is interesting. If we are using just first-order logic it can be omitted, but in higher-order logic and Type Theory we want to say if we are quantifying over individuals, relations, etc. I think the translation of e.g. ∀ (x:A).B makes sense: in order to disprove that we should give a concrete (intuinistically acceptable) construction of an element x that causes it to fail, so we stay in "construct a proof" mode for the A.
But now we have already defined the translation of implication! Using the standard type theory trick to encode A→B as ∀ (x:A).B, where x is a fresh variable not free in B, we get
〈A→B 〉= 〈∀(x:A).B〉=∃ (x:A).〈B〉= A×〈B〉
a pair of a proof of A and a disproof of B. This seems related to your "but not" operator, except here it mixes the logical symbol × and the syntactic operation 〈〉. Similarly the translation of not becomes just
〈not A〉=〈A→False 〉= A × True ~= A
So this basically just the not operator in disguise. The "dualizing translation" in the paper you linked does indeed use a but-not symbol, I guess I should go and read that paper...
Constructivist logic works great if you interpret it as saying which statements can be proven, or computed, but I would say it doesn't hold up when interpreted as showing which statements are true (given your axioms). It's therefore not really appropriate for mathematics, unless you want to look at mathematics in the light of its computational or proof-theoretic properties.