The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

An aside: as relevance arithmetic keeps being dragged  into the pit, merged in a puzzling way with model theory, let us clarify what it shows, and what actual lessons one can draw from studying it. We also seem to have a few other basic misunderstandings regarding model theory itself. I'll address them briefly below, but these are perhaps more obvious to at least some readers of this list than problematic use made of relevance arithmetic in this discussion.

Just to be clear: I think that arithmetic and set theory based on substructural logics  (not only relevance logics) is a very interesting subject, and there is not nearly enough attention devoted to it (still, there are many more references than those quoted so far; a few more are mentioned below). In particular, I believe it has a lot to offer to theorem proving and formalized mathematics.  But sadly, it also has some potential to attract half-baked and overexcited interpretations, particularly  from people with insufficient training. Of course, far be it from me to insinuate we have a case in point here, but I wouldn't like anybody (still) reading this discussion (especially students!) to get wrong ideas, so better safe than sorry.

First and foremost, there are several notions of consistency in relevance logic; as usual with nonclassical logics, one can make distinctions invisible in the classical setting. The consistency notion which corresponds most naturally to the classical one is "negation-consistency". And R# (one should rather write "RA", or even better "MA"...)  is *subject to exactly the same restrictions as PA* here!

It has been stated very clearly by its creator (in the unlikely case it's not obvious anyway):

the impossibility of proving
within R# that R# is negation-consistent is as in the classical case.

http://www.filozof.uni.lodz.pl/bulletin/pdf/05_4_3.pdf

(btw, just to relieve people worried about the name on this paper, Robert K. Meyer has nothing to with James Meyer. The latter is, as correctly mentioned several days ago, a crank. The former was, for all his idiosyncrasies and eccentricities, an eminent logician)

In other words, R# cannot exclude the existence of a sentence A s.t. R# |- A and, at the same time, R# |- ~A (although if there is such a sentence, then PA is screwed as well).

It gets funnier than that: these finitary models of R# where 0 = 1 fails all validate both (0 = 0) and ~(0 = 0) (the latter is not a theorem of R# because it is rejected in various infinite models, including the standard one...). And while they refute (0 = 1), the first of them validates (0 = 2), the next one refutes it, but validates (0 = 3) and so on. One can find more here:

 http://www.jstor.org/stable/227414

Curious as it all is, I doubt that Hilbert would find this satisfying.




*******


This is one sense in which R# is "finitarily consistent". Another, perhaps even more exotic one, is  described by Bob Meyer as follows:

one can prove,
in the natural way, within R# that it is arithmetically consistent, in the
sense that equations which violate the addition or multiplication tables for
+ and \times are trivially undemonstrable.

"Equations which violate the addition or multiplication tables for + and \times" are very weak formulas indeed. Of course, if Peano Arithmetic or Heyting Arithmetic is inconsistent, then in particular such equations are derivable in them, simply because everything is derivable from A & ~A. But, as we have said above, R# may be inconsistent (in the standard sense of being "negation-inconsistent") and still not everything would be derivable. Relevance logic does not obey ex falso quodlibet.

Again, recall that non-derivability of such absurd equations still goes hand-in-hand that many of them actually hold in this or that finitary model of R#. And the situation is even worse for negations of derivable equations, such as ~(0= 0) which hold in all the finitary ones.

Besides, as admitted by Bob Meyer, many cut-free formulations of classical arithmetic have similar consistency properties.


*******

As I said, the family of substructural arithmetic and set theories is not restricted to its relevance species. And the discovery that famous paradoxes and contradictions tend to lose their fangs over substructural propositional base has been made repeatedly. A famous example is Grisin's 1982 consistent naive set theory build without contraction rule (this is, in a sense, the opposite polarity of substructural spectrum to the one investigated by relevance logicians).

(Incidentally, I've read papers in "leading philosophical journals" such as "Mind" published several decades later, which completely ignored this and other substructural developments and presented the realization that Russell's paradox can be "avoided" when contraction is banished as a new and revolutionary discovery...)

The uses of substructural logic in set theory are not limited to playing cat-and-mouse with paradoxes. See, say, Terui's proof that a function on {0,1}-words is provably total in Light Affine Set Theory iff it is computable in polynomial time:

http://www.kurims.kyoto-u.ac.jp/~terui/lastfin.pdf


******

I hope nobody is making the claim that classical model theory as a field leans towards *more* constructive, predicative or relevant approaches than CIC, or that typical publications in the field are agnostic wrt foundations. If anything, the exact opposite seems true. Numerous papers in the field essentially rely not only on ZFC, but on large cardinal axioms; indeed, one obviously needs to assume existence of some inaccessible cardinals to even talk about models of ZFC and similar theories.

Just go tell Shelah, Newelski or Keisler they are supposed to get predicative or avoid classical logic, treat PA with suspicion and perhaps simply base their work on relevant arithmetic.

Indeed, even something as basic as the ultrafilter construction is essentially, fundamentally and irreparably non-constructive.

For this reason, finally, it'd be absolutely surreal to question the axioms of PA, yet talk freely about its nonstandard models. Showing that such models exist requires a bigger and *much* more problematic fragment of ZFC than constructing the standard model of PA in ZF! Ditto for any other metatheory one can think of.


Ciao,
t.

On 04/05/18 05:29, José Manuel Rodriguez Caballero wrote:

Emilio said
So now the question is, can you construct a losing strategy for the
Hydra game? There is such a losing strategy, but you need to take a certain initial segment of non-standard model of first-order Peano arithmetic, this is how Kirby and Paris proved the unprovability of Goodstein theorem in PA (page 291 of Accessible Independence Results for Peano Arithmetic). 

Russell said
I'm about as confident that there is no infinitely long descending chain of ordinal notations in Cantor normal form as I am that there is no infinitely long descending chain of natural numbers.

If you take Nelson's Internal Set Theory in place of ZFC, then you can prove in a trivial way that there exists an "infinitely long" descending chain of ordinal notations in Cantor normal form, where "infinitely long" here means "larger than any standard natural number", i.e. larger than any n : nat. Of course that sequence will be Dedekind-finite, but from a practical point of view, it will be infinite.

To believe that the statement 0 = 1 is false is not the same a to believe in the consistency of PA.  Indeed, the relevant arithmetic R# is consistent and you can prove there that the statement 0 = 1 cannot be deduced. If there is an inconsistency of PA, it will be because of its first-order classical logic and it will be related to the induction principle. 

Many people think that the higher-order logic of Coq is its main advantage, but from the point of view of model theory it is uncomfortable to work with non-standard first-order arithmetic in Coq. Practically, you need to create another software inside Coq in order to do it and from a foundational perspective you need to assume the consistency of Coq in order to prove results which, in some cases, are metamathematically true without assuming any consistency.