[FOM] relevant logic and paraconsistent logic

[Harvey Friedman]

On 3/17/06 1:37 PM, "Katalin Bimbo" <kbimbo at indiana.edu> wrote:

> R. Brady (ed.), Relevant Logics and their Rivals, vol. II,
> (A continuation of the work of R. Sylvan, R. Meyer, V.
> Plumwood and R. Brady), Burlington (VT), Ashgate, 2003.
> 
> G. Restall, Relevant and substructural logics, in Handbook
> of the History of Logic, vol. 6, D. M. Gabbay and J. Woods
> (eds.), Amsterdam, Elsevier, 2006.
> 
> N. C. A. da Costa, D. Krause and O. Bueno, Paraconsistent
> logics and paraconsistency, in Handbook of the Philosophy
> of Logic, D. Jacquette (ed.), Amsterdam, Elsevier
> (North-Holland), 2006.
> 
> (And a bit of self-ad:)
> K. Bimbo, Relevance logics, in Handbook of the Philosophy
> of Logic, D. Jacquette (ed.), Amsterdam, Elsevier
> (North-Holland), 2006, pp. 723--789.

What role does relevance play in the conduct of elementary mathematics?
E.g., baby combinatorics, baby number theory, baby real analysis.

1. How much of it as normally done satisfies relevance criteria?

2. How much of it can be fixed to satisfy relevance criteria, so as to stay
nice and readable, and in particular without significant blowup in the size
of the proofs?

3. How much of it can be fixed, theoretically, to satisfy relevance
criteria?

4. To what extent are the answers to 1,2,3 dependent on the choice of
relevance criteria? What are the main choices of relevance criteria that
that diverge on 1,2,3?

We have a clear, but far from perfect, understanding of the analogous issues
with regard to "constructive proofs".

I don't think our understanding of 1,2,3 is very good with regard to "cut
free proofs". One of the main difficulties is that real baby mathematics is
conducted in an environment with plenty of facilities for abbreviations. My
entirely superficial impression is that perhaps the theory of cut
elimination may have to be rethought for formalisms directly supporting
abbreviations.    

Harvey Friedman