Non-triviality and Coherence

It has been an open problem whether the logic I used in "Transfinite Numbers in Paraconsistent Set Theory" (which does seem to be getting read by people, according to Review of Symbolic Logic site...) is non-trivial for a naive comprehension scheme. The system seems pretty strong; it can prove the axiom of choice, after all. Can it prove everything? That would be bad.

Ross Brady has proved that logics very-much-like it are safe -- there are models satisfying all the theorems of the set theory, in which some (absurd) sentences are not satisfied. But I needed the additional counterexample principle:

A, ~B; therefore ~(A --> B)

and it was unclear whether this could fit into Brady's construction. For the proof in his 2006 book "Universal Logic," the counterexample principle definitely does not fit. (Indeed, there's a counterexample.) So, TFNPST could have been fated to be a much-less-famous Fregean Grundgesetze.

Very happily, we noticed last week that one of Brady's older papers, "The Non-Triviality of Dialectical Set Theory" in Paraconsistent Logic: Essays on the Inconsistent (1989) proves non-triviality for a much stronger logic. That logic turns out to contain (in rule form) both the above counterexample principle, and its contrapose:

(A --> B); therefore ~A or B.

So unless ZF and similar systems are themselves inconsistent (...hmm...) it follows that the work in TFNPST is demonstrably coherent.

=======================================================
Speaking of coherence, Greg Restall recently wrote a paper to appear in Analysis, where he argues that non-classical logicians should stay away from using two little connectives: t, the conjunction of all truths, and u, the disjunction of all untruths. Having these little letters around allows us to define the following connective:

A > B := A&t --> B v u

where --> is an arrow that obeys modus ponens and a few other sensible properties. Restall shows that the new arrow > can make a lot of trouble, in the form of Curry paradoxes, strengthened liars, and general malaise.

So Jc Beall, Graham Priest and I wrote a reply. We claim, as dialetheists, that the disjunction of all untruths, little u, is itself true. After all, some of the conjuncts of little t are false; they have true negations. And this defuses most of that trouble and general malaise. (We also claim that a truth value gapper can say something analogous about little t.) Dave Ripley and I noticed that it boils down to this derivation:

1. u
2. t --> u (from 1, by t-introduction)
3. A&t --> u (from 2, antecedent strengthening)
4. u --> u v B (or-introduction)
5. A&t --> u v B (3, 4, conjunctive syllogism)
6. A > B (definition of >)

Line 6 is completely general, any A and B at all. So this means that the arrow > really isn't an arrow at all. It certainly shouldn't obey modus ponens, contra Restall. And so the world is (doubly) safe for paraconsistency once again.

Or so the claim goes. It all depends on how to understand little u, and whether or not logical space can be partitioned in particular ways. What are the untruths? What work is "un" doing here?