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?

Paraconsistent maths workshop begins!

Monday, August 2

9am Introduction - Zach Weber

10 Naive comprehension, circularity and arithmetic in fuzzy
logic- Shunsuke Yatabe

11 TEA

11.30 Groupthink -- Set theory and arithmetic

1 pm. LUNCH

2.30 Paraconsistent Set Theory and Metatheory - Graham Priest

3.30 Relevant Logic and Classical Proofs - Ed Mares

4.30 TEA

5 Paraconsistent arithmetic with binary quantifiers - Sam Butchart

6 DINNER


Tuesday, August 3

9am Coformulas - Greg Restall

10 Church/Turing Thesis - Koji Tanaka

11 TEA

11.30 Co-inductive-like definition in fuzzy truth theory - Shunsuke
Yatabe

1pm LUNCH

2.30 Groupthink -- Proofs and Computation

3.30 Groups, Inconsistency and The Routley Functor - Chris Mortensen

4.30 TEA

5 Conclusion - Open Problems

6.15 Barry Taylor Memorial Lecture (Jon Bigelow)

Interview in "The Reasoner"

This month's issue of "The Reasoner" features me interviewing Greg Restall.

Ever wonder why Greg used to believe in true contradictions, but doesn't now? Find out...

www.thereasoner.org

Paraconsistent Mathematics Workshop

August 2 – 3, 2010
University of Melbourne

To begin our new ARC project, we are hosting a workshop, to present ideas and determine directions for research. Core topics include:

- Set Theories
- Arithmetic
- Recursive Functions and Computability
- “Higher” mathematics – geometry, topology, real analysis, etc.

Questions to discuss include: What logic(s) are appropriate for these theories? How are basic and ubiquitous mathematical notions to be formally expressed? What should we aim to prove, and how will we prove it?

Interested parties are invited to contact me at zweber [at] unimelb.edu.au

Aims and Background

At the turn of the 20th century there was a revolution in logic. New technologies, associated with the names of Frege and Russell, radically changed philosophy, because formal logic lends incredible precision to the asking and answering of old questions. A discipline called foundations of mathematics emerged, casting new light on the nature and meaning of rationality and mathematical truth. In foundational research, philosophical issues and mathematical results develop in tandem, each informing the other. Epochal results came out of early investigations, such as the modern theory of computing as developed by Gödel, Turing and Church.

The goal of the initial foundational project, as articulated by Hilbert (reviving an idea of Leibniz’s), was a method for reliably deciding whether or not a given sentence is true. All approaches to foundations of the last hundred years, from Russell’s to Hilbert’s to Brouwer’s, are beholden to formal consistency. Beset on one side by serious paradoxes, like Russell’s contradiction, and on the other by Gödel’s incompleteness theorems, it is now known that a consistent foundation is impossible to obtain.

Starting in the 1970s, developments in logic produced a novel kind of tool, paraconsistent logic. These logics accommodate inconsistency in a sensible fashion. From the start, many logicians saw the relevance and possible applications of these logics to foundational matters. Techniques have now developed to a level of sophistication where it is possible to renew a serious investigation of foundations. The driving thought here is that one need not founder on the paradoxes that halted older foundational projects. One simply recasts, accepts and even studies some contradictions, controlling any pernicious effects with a paraconsistent logic.

Our project is to construct, for the first time, a fully articulated foundation for mathematics. This will involve the construction of paraconsistent versions of the major pillars of foundational studies:

• Foundations are tested on arithmetic, the basic tool for counting and quantity. The functions that operate over the numbers are the province of recursion theory, which ties into computation.

• The bridge between language and mathematical structures is provided by model theory, which has become an indispensable tool for philosophers and logicians alike. Consistent model theory is not able to take in the full range of what mathematicians express in language. A model theory built on paraconsistent principles will be radically more powerful and illuminating, a major achievement.

• Conducting foundational studies of proof and truth in their natural setting contributes to our understanding of knowledge and beliefs, by providing a simple and credible account of learning.

What will emerge is a wholly new perspective on the nature of mathematical thought and truth, striking results in inconsistent mathematics itself, and a reliable platform for more general theories that no strictly consistent foundation can support.

Formally, we define and describe the objects of mathematics, such as numbers and functions; we prove that there are such objects and that they have the right properties; and we do this in such a way as to allow for some inevitable inconsistencies, using paraconsistency to protect the basic integrity of the theory. Philosophically, we work from that foundation to understand truth, proof and belief in terms of what they are—rational but paradoxical ways that humans navigate through our world.