3
$\begingroup$

In the Stanford Encyclopedia of Philosophy entry "Relevance Logic", the following inference is listed as classically valid:

The moon is made of green cheese. Therefore, it is raining in Ecuador now or it is not.

This inference can be tweaked slightly to make it more mathematical:

The moon is made of green cheese. Therefore, $\mathit{CH}$ or $\lnot\mathit{CH}$ (where $\mathit{CH}$ stands for the continuum hypothesis).

My questions are simply these:

  1. Are the so-called 'paradoxes' of material and strict implication ever actually used as legitimate steps in proofs of theorems in mathematics? (If so, give examples,e.g., proofs of theorems in $\mathit{PA}$, though proofs of this sort in any branch of mathematics would be nice as well.) Also, if a proof of a theorem uses a 'paradox' of material or strict implication, can the proof be rewritten so as to avoid the use of the 'paradox'?

  2. Consider the "variable sharing principle" from the above link, i.e., that "no formula of the form $A\rightarrow B$ can be proven if $A$ and $B$ do not have at least one propositional variable in common in common and that no inference can be shown to be valid if the premises and conclusion do not share at least one propositional variable." Is this idea of relevance logic also part of standard mathematical practice?

  3. If it is helpful to distinguish 'mathematical inference' from 'logical inference', then:

    What sort of relevance logic captures the notion of 'mathematical inference'?

$\endgroup$
11
  • 10
    $\begingroup$ “The moon is made of green cheese. Therefore, $CH$ or $\lnot CH$.”—Sounds like a fine argument to me. Seen that now and then. Not really with cheese and CH, mind you, but with something less conspicuous so that it is easier for the author of the proof not to realize they refer to a premise they do not actually need to use. $\endgroup$ Commented Oct 18, 2016 at 16:24
  • 4
    $\begingroup$ Later on, the relevance logic article makes clear that relevant arithmetic is only a small (and decidable) fragment of arithmetic, so they must be fairly common. $\endgroup$
    – arsmath
    Commented Oct 18, 2016 at 16:33
  • 5
    $\begingroup$ You seem to be asking whether mathematicians ever state theorems with unnecessary hypotheses. We can break this down into the case where there is an intent to state an unnecessary hypothesis and the case where there is not. As to the former, maybe occasionally for some idiosyncratic expositional reason, but by and large people prefer to make their theorems as general as possible. As to the latter, there are a great many papers written to show that some hypothesis in some other paper was unnecessary, so yes, this happens all the time (as I now see @EmilJeřábek has already said). $\endgroup$ Commented Oct 18, 2016 at 16:50
  • 4
    $\begingroup$ I would like to reopen this. Harvey Friedman's research showed that the answer to 1 is yes (eg "for every odd n there is an integer which is not a quadratic residue mod n", which is not provable in relevant arithmetic) and yes (if T is a theorem of PA then "T or not 0=0" is a relevant theorem of PA). $\endgroup$
    – user44143
    Commented Oct 19, 2016 at 0:38
  • 3
    $\begingroup$ For people not familiar with this area, there is a standard philosophical critique of the standard interpretation of implication (known as "material implication"). Logicians have proposed weaker forms of implication, such as "relevant implication". This is all well-explained by the "Relevance Logic" article. Weakened forms of implication are not that unusual anymore -- implication in linear logic is an example. You can ask what theorems of arithmetic are still provable under weaker forms of implication, and there are answers in the literature. $\endgroup$
    – arsmath
    Commented Oct 19, 2016 at 16:35

1 Answer 1

9
$\begingroup$

In answer to 1:

Yes, there are theorems of PA that are not theorems of relevant PA. Harvey Friedman's example is "for every odd $n$ there is an integer which is not a quadratic residue mod $n$", or $\forall x\ \exists y\ \forall z\ \exists a\ \exists b\ (2x+1)a + (y - z^2)b = 1$.

The proof relies on this being a statement with no negation which fails over the complex numbers, and uses Tarski's result on the undefinability of countably infinite sets in that field. See Meyer and Friedman, Whither Relevant Arithmetic, Journal of Symbolic Logic 1992.

And yes, proofs can be rewritten to be relevantly valid. The same paper also proves that if T is a theorem of PA then "T or not 0=0" is a relevant theorem of PA.

In answer to 2:

Apparently some ordinary mathematics does not abide by the rules of relevant logic.

Commenting on 3 without answering it:

I would say that the statement 0=0 is relevant to all arithmetical statements (while the rainfall today in Ecuador might not be relevant to all astronomical statements). So I do not see the value of using relevant logic in the arithmetical context.

$\endgroup$
2
  • $\begingroup$ A question. In "Whither Relevant Arithmetic" (on pg. 829) does the failure of the $QRF$ in $\mathbf R{\sharp}$ relate to the failure of Ackermann's rule $\gamma$ in $\mathbf R{\sharp}$? Also, is the $QRF$ deemed a "classical formula" and is it valid in $\mathbf N$? If so, then by 3.2, the $QRF$ should be a theorem of $\mathbf R{\sharp}{\sharp}$. Note that "$\mathbf R{\sharp}{\sharp}$ has, nonetheless, many of the features of $\mathbf R{\sharp}$ noted in 2.3. For example, proving absolute consistency for $\mathbf R{\sharp}{\sharp}$ is still trivial ([footnote 7]: "And $\endgroup$ Commented Oct 20, 2016 at 7:50
  • $\begingroup$ (cont.) finitary, since mod 2 the $\omega$-rule means inferring (x)$A$(x) from $A0$ and $A1$.")". Also, "$\gamma$ holds for $\mathbf R{\sharp}{\sharp}$". This suggests to me that $PA$ may be made 'relevant' by some system other than $\mathbf R{\sharp}$ (that is, there might be a system of relevant arithmetic which proves all the theorems of $PA$). Also, since the $QRF$ is false in the ring $\mathbb C$, is it an example of a theorem provable in elementary number theory ($PA$) but not provable(?) by the methods of analytic number theory? $\endgroup$ Commented Oct 20, 2016 at 8:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .