Constructive mathemathics and its dual
post by MrMind · 2013-02-28T17:21:34.629Z · LW · GW · Legacy · 30 commentsContents
30 comments
I have stumbled upon an interesting and, as far as I know, new concept: thinking about the duality between constructive and paraconsistent logics, I've noticed that while the meta-theory of intuitionistic logic (constructive mathematics) is very well understood and studied, the meta-theory of the dual logic is not. If we understand constructive mathematics from an epistemological point of view, as an accretion of truth from an empty base, we ought to be able to think about a sort of destructive mathematics, that starts from the totality of assertions and proceeds by expunging falsity. This seems to have surprising consequences for things like theism, Tegmark universe(s), the Many World Interpretation and so on, but first I need to cover some background informations. This I will do in the present post, while in the next I'll present the concept and some of its applications.
There is a variety of philosophical programs known as constructive mathematics, but their common denominator is to refuse the classic way of conceiving truth and adhere instead to a concept known as verificational existence. That is, for a mathematical formula A to be accepted as true, there must be a construction (a direct proof) of A. On the same level, for a mathematical formula to be denoted false, a constructivist accepts only a proof of (this symbol denotes the negation of A). If neither of such proofs exist, then a constructivist refuse to impose a truth value upon A. This has as consequence the refusal of the general formula
, (
denotes logical disjunction), valid in classical logic, a principle called in Latin tertium non datur (TND), which means "a third is not given". For a constructivist nonetheless the principle
still holds (
denotes logical conjunction), because it is still viewed as impossible that there exists a valid proof of A and of its opposite. This one is called ex contraditione quodlibet (ECQ), which means "anything from a contradiction".
The simple excision of TND from classical logic gives a logical system called intuitionistic logic (because it was developed under the intuitionistic program of constructive mathematics), which has many, many interesting properties.
A logical calculus developed on these fundamental consideration is aimed at preserving justification rather than truth: intuitionistic proofs, instead of carrying from true formulas to other true formulas, only produce justified formulas from other justified formulas.
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.
If then we decide to break the equivalency, it becomes natural to ask: since there's a logic that accepts ECQ but refuses TND (intuitionistic logic), can there be a logic that's a sort of dual, that is it accepts TND but refuses ECQ?
This question, maybe surprisingly, has an affirmative answer, and the resulting plethora of logical systems thus produced are called "paraconsistent logics".
Under this classification, intuitionistic logic can then be said to be a member of the class now known as "paracomplete logics" (although this name is not much used). Paraconsistent logics are a multitude, but one of them is an exact symmetric of intuitionistic logic, known in the literature as dual-intuitionistic logic.
If you reflect on that a little bit, it may seems very strange at first to abandon ECQ. After all, the refusal of contradictions is one of the primary, if not the primary, foundation of rationality. But in formal logic there's also a very cogent and slightly technical reason why contradictions are not allowed: in classical logic, they imply triviality.
A set (possibly infinite) of sentences and formulas in logic is called a theory. It is clear that an empty theory is not very interesting: it literally tells us nothing about the subject at hand. But an equally uninteresting theory is the total theory: the set of all possible sentences and formulas. Since this set makes no distinction on what's true and what's false about the subject of interest, it's as informative as the empty theory. Such a theory is called trivial, and formal systems developed within classical logic strive to avoid contradictions: indeed, from a single formula and its negation you can prove any other formula.
In systems that rely on classical logich then, any contradiction entails triviality, and they are therefore to be avoided.
Paraconsistent logics however depart from this classical setting, and they abandon this principle (sometimes called "principle of explosion").
Be careful though: only the general principle is abandoned. Exactly like in intuitionistic logic, where is abandoned in general, but if you have constructed a proof of (say) A, then for that particular formula
is valid, in dual-intuitionistic logic if you have constructed a proof of (say)
, then
is still valid only for that formula.
What is the meta-theory of dual-intuitionistic logic? How can it be justified and it's at the end somehow useful?
This is where things get interesting, and it's a theme I want to explore in the next post.
Links and references
Over the net, there's more than you could possibly care to learn about constructive mathematics: the usual pointer are Wikipedia's http://en.wikipedia.org/wiki/Constructivism_(mathematics) and http://en.wikipedia.org/wiki/Intuitionistic_logic, while on the SEP side you have http://plato.stanford.edu/entries/mathematics-constructive/ and http://plato.stanford.edu/entries/logic-intuitionistic/.
There is considerable less material on paraconsistent logic, but again you can find http://en.wikipedia.org/wiki/Paraconsistent_logic and http://plato.stanford.edu/entries/logic-paraconsistent/.
30 comments
Comments sorted by top scores.
comment by Kawoomba · 2013-02-28T17:36:43.082Z · LW(p) · GW(p)
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.
Replies from: MrMind↑ comment by MrMind · 2013-02-28T17:46:50.011Z · LW(p) · GW(p)
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!
Replies from: AlexMennen, MrMind, wedrifid↑ comment by AlexMennen · 2013-02-28T20:33:27.023Z · LW(p) · GW(p)
You're trying to make it not boring by ending the post before saying anything interesting?
Replies from: MrMind↑ comment by wedrifid · 2013-02-28T18:17:27.684Z · LW(p) · GW(p)
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!
Replies from: MrMindcomment by [deleted] · 2013-02-28T18:30:47.354Z · LW(p) · GW(p)
The contemporary name for "tertium non datur" is the "Law of excluded middle."
comment by ScottMessick · 2013-03-03T23:11:45.086Z · LW(p) · GW(p)
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.
Replies from: MrMindcomment by passive_fist · 2013-02-28T20:25:36.809Z · LW(p) · GW(p)
Does your new concept have anything to do with dialetheism?
Replies from: MrMind, bryjnar↑ comment by MrMind · 2013-02-28T22:14:53.445Z · LW(p) · GW(p)
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.
Replies from: bogus↑ comment by bogus · 2013-03-01T19:18:29.568Z · LW(p) · GW(p)
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).
↑ comment by bryjnar · 2013-03-01T02:06:02.350Z · LW(p) · GW(p)
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.
comment by Shmi (shminux) · 2013-02-28T18:07:39.194Z · LW(p) · GW(p)
Please add references (at least wiki links) for all the relevant concepts.
Replies from: MrMindcomment by AlexMennen · 2013-02-28T20:25:12.061Z · LW(p) · GW(p)
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.
Replies from: MrMind↑ comment by MrMind · 2013-02-28T22:22:23.209Z · LW(p) · GW(p)
Maybe a better phrasing could have been: if you assume one as an axiom, the other follows as a theorem.
Replies from: AlexMennen↑ comment by AlexMennen · 2013-02-28T23:36:51.577Z · LW(p) · GW(p)
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.
Replies from: Benja↑ comment by Benya (Benja) · 2013-03-01T02:46:12.378Z · LW(p) · GW(p)
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.
Replies from: Pfft, AlexMennen↑ comment by Pfft · 2013-03-01T19:41:41.059Z · LW(p) · GW(p)
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.
↑ comment by AlexMennen · 2013-03-01T03:49:02.023Z · LW(p) · GW(p)
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.
comment by prase · 2013-02-28T19:21:02.125Z · LW(p) · GW(p)
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.
Replies from: shinoteki↑ comment by shinoteki · 2013-02-28T19:47:06.962Z · LW(p) · GW(p)
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.
Replies from: prase↑ comment by prase · 2013-02-28T22:10:59.833Z · LW(p) · GW(p)
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).
comment by whpearson · 2013-02-28T21:16:49.797Z · LW(p) · GW(p)
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.
Replies from: Benja, bryjnar↑ comment by Benya (Benja) · 2013-03-01T03:01:24.287Z · LW(p) · GW(p)
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
?
↑ comment by Benya (Benja) · 2013-03-01T04:27:52.645Z · LW(p) · GW(p)
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.
Replies from: Pfft↑ comment by Pfft · 2013-03-03T23:21:54.301Z · LW(p) · GW(p)
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...
↑ comment by bryjnar · 2013-03-01T02:08:27.203Z · LW(p) · GW(p)
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.