Does the finitary proof of the consistency of relevant PA shows that first order PA is irrelevant?

Question

Relevance logic takes a closer look at the implication operation in first-order logic. It suggests that implications such as:

p and not p -> q

cannot hold; in ordinary English, an example of this is:

'Socrates is a man and Socrates is not a man, hence the capital of England is London'.

The conclusion although true, appears to be irrelavnt to the premises under discussion.

Now, Meyer in the 70s, looked at Peanos Axioms (PA) in Relevance Logic, and showed that contra Godel that it was provably consistent.

If the proof of the consistency of PA is important and vital, could not one say that relevant PA is perhaps the correct PA? Or that at least first-order PA is not right PA to look at?

Of course, not all of the theorems of traditional PA holds in relevant PA; but is anything essential lost, say to mainstream number theory or physics, rather that the exotic outer reaches of what is possible in traditional PA?

(Another way to examine this result in the light of Godel, is to consider his theorem that a theory cannot be both complete and consistent; if one desires completeness, one must embrace inconsistency; and in fact relevant logic is paraconsistent).

Answer 1

"Is anything essential lost" or are the shortcomings of Meyer's system in "the exotic outer reaches of what is possible in traditional PA"?

PA proves that formula if p > 2 is prime, then there is a positive integer y which is not a quadratic residue mod p; that is,

∃y ∀z: ¬(y ≡ z^2 (mod p)).

That looks like a pretty unexotic bit of number theory to me. Fails in Meyer's system though. Bad news?

See R. Meyer and H. Friedman, Whither Relevant Arithmetic?, JSL 1992, 824–831.

Answer 2

I recommend the paper: B. Buldt, The Scope of Godel’s First Incompleteness Theorem, Log. Univers. 8 (2014), 499–552 , especially pages 530 - 531.

Answer 3

Now, Meyer in the 70s, looked at Peanos Axioms (PA) in Relevance Logic, and showed that contra Godel that it was provably consistent.

The Australasian Journal of Logic has published recently a special issue devoted to Meyer's work on the Relevant Arithmetic R#. There was published among others, Meyer's paper "The Consistency of Arithmetic" (https://ojs.victoria.ac.nz/ajl/article/view/6906), where had been placed a proof of consistency of Peano Arithmetic, which was (in Meyer's opinion) elementary. One of his arguments was such that Peano Arithmetic was a subsystem of R#. However, in 1992 Harvey Friedman proved that classical Peano Arithmetic was not contained in Relevant Arithmetic R# and this was a failure for Meyer's vision for Relevant Arithmetic R# (see for e.g. Thomas Fergusson's message at FOM discussion list, https://cs.nyu.edu/pipermail/fom/2021-July/022757.html ). Hence, Meyer's proof of consistency of Peano Arithmetic, mentioned above, does not repeal Godel's Second Incompleteness Theorem.

Let me recommend the paper T. J. Stępień, Ł. T. Stępień, „On the Consistency of the Arithmetic System”, Journal of Mathematics and System Science, vol. 7, 43 (2017), arXiv:1803.11072. There was published a proof of consistency of (Peano) Arithmetic System. This proof had been done actually within this System (the abstract related to this paper: T. J. Stepien and L. T. Stepien, "On the consistency of Peano's Arithmetic System" , The Bulletin of Symbolic Logic, vol. 16, No. 1, 132 (2010)).