Follow-up to: Constructive mathematics and its dual

In last post, I've introduced constructive mathmatics, intuitionistic logic (JL) and its dual, uninspiringly called dual-intuitionistic logic (DL).
I've said that JL differs from classical logic about the status of the law of excluded middle, a principle valid in the latter which states that a formula can be meaningfully only asserted or negated. This, in the meta-theory, means you can prove that something is true if you can show that its negation is false.
Constructivists, coming from a philosophical platform that regards mathematics as a construction of the human mind, refuse this principle: their idea is that a formula can be said to be true if and only if there is a direct proof of it. Similarly, a formula can be said to be false if and only if there's a direct proof of its negation. If no proof or refutation exists yet (as is the case today, for example, for the Goldbach conjecture), then nothing can be said about A.
Thus is no more a tautology (although it can still be true for some formula, precisely for those that already have a proof or a refutation).
Intuitionism anyway (the most prominent subset of the constructivist program), thinks that is still always false, and so JL incorporates , a principle called the law of non-contradiction.
Intuitionistic logic has no built-in model of time, but you can picture the mental activity of an adherent in this way: he starts with no (or very little) truths, and incorporates in his theory only those theorems of which he can build a proof of, and the negation of those theorems that he can produce a refutation of.
Mathematics, as an endeavour, is seen as an accumulation of truth from an empty base.

I've also indicated that there's a direct dual of JL, which is part of a wider class of systems collecively known as paraconsistent logics. Compared to the amount of studies dedicate to intuitionistic logic, DL is basically unknown, but you can consult for example this paper and this one.
In this second article, a model is presented for which DL is valid, and we can read the following quote: "[These semantics] reflect the notion that our current knowledge about the falsity of statements can increase. Some statements whose falsity status was previously indeterminate can down the track be established as false. The value false corresponds to firmly established falsity that is preserved with the advancement of knowledge whilst the value true corresponds to 'not false yet'".

My suggestion is to be a lot braver in our epistemology: let's suppose that the natural cognitive state is not one of utter ignorance, but of triviality. Let's then just assume that in the beginning, everything is true.
Our job then, as mathematician, is to discover refutations: the refutation of will expunge A from the set of truth, the refutation of A will remove .
This dual of constructive mathematics just begs to be called destructive mathematics (or destructivism): as a program, it means to start with the maximal possibility and to develop careful collection of falsities.
Be careful though: it doesn't necessarily mean that we accept the existence of actual contradictions. It might be very well the case that in our world (or model of interest) there are no contradictions, we 'just' need to expunge the relevant assertions.
As the dual of constructive mathematics, destructivism regards mathematics as a mental construction, one though that procedes from triviality through confutations.

One major difficulty with destructive mathematics is that, to arrive to a finite set of truths, you need to destroy an infinite amount of falsities (but, on the other side, to arrive to a finite set of falsities in constructive mathematics you need to assert an infinite number of truths).
Usually, we are more interested in truth, so why should we embark in such an effort?
I can see at least two weak and two strong reasons, plus another one that counts as entertainment of which I'll talk about more extensively in the last post.
The first weak reason is that sometimes, we are more interested in falsity rather than truth. Destructivism seems to be a more natural background for the calculus of resolution, although, to my knowledge, this has only been developed in classical setting.
The second weak reason is that destructivism is an interesting choice for coalgebraic methods in computer science: there, co-induction and co-recursion are a method for 'observing' or 'destroying' (potentially) infinite objects. From the Wikipedia entry on coinduction: "As a definition or specification, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects. As a proof technique, it may be used to show that an equation is satisfied by all possible implementations of such a specification."
I whish I could say more, but I don't know much myself: the parallelisms are tempting, but I have to leave the discovery of eventual low-hanging fruits to later times or someone else entirely.

Two instead much more promising fields of application are Tegmark universes and the Many World quantum mechanics.
It's difficult to give a cogent account for why all the mathematical structures should exists, but Tegmark position equates simply a platonist point of view on destructivism.
If all formulas are true, then this means that "somewhere" every model is realized, while on the other side, if all structures are realized, then "on the whole", every formula is true (somewhere).
But the most important reason why one should adopt this framework is that it gives a natural account of quantum mechanics in the Many World flavour (MWI).

Usually, physical laws are seeen as the corrispondence between physically realizable states, and time is the "adjunction" of new states from older ones. Do you recognize anything?
What if, instead, physical laws dictates only those states that ought to be excluded and time is simply the 'destruction' or 'localization' of all those possible states? Well, then you have (almost for free) MWI: every state is realized, but in times you are constrained to just one.
I'm extremely tempted to say that MWI is the dual of the wave function collapse, but of course I cannot (yet) prove it. Or should I just say that I cannot yet disprove it's not like that?
If that's the case, the mystery of why subjective probability follows the Born rule will be 'just' the dual of the non-linear mechanism of collapse. One mystery for a mystery.
I also suspect that destructive mathematics might have implication even for probability theory, but... This framework is still in its infancy, so who knows?

The last interesting motivation for taking seriously destructive mathematics is that it offers a possible coherent account of Chtulhu mythos (!!): what if God, instead of having created only this world from nothing out of pure love, has destructed every world but this one out of pure hate? If you accept the first scenario, then the second scenario is equally plausible / conceivable. I'll explore the theme in the last post: Azathoth hates us all!

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/.