Adequacy of a logic

[Vaughan Pratt]

Apropos of Neil Tennant's response of Fri, 11 Jun 2021 12:08:27 +0000 to
Patrik Eklund's submission of Friday, June 11, 2021 1:17 AM, I feel Neil
was too kind to characterize Patrik's concerns as merely "orthogonal" to
his own concerns.  The adjective I'd use would be "unreasonable".

As best I could tell, the gist of Patrik's submission seems to be that
category theory is preferable to set theory as a framework in which to
formulate questions of adequacy of formalizations of mathematics.  He
started out seeming to claim that this sort of thing can't even be done in
set theory, then later relaxed it to "Making it precise in set theory is
possible, but indeed, show it to me. Making it precise in category theory
is more elegant. We've done it. And it wasn't all that easy to do it, I can
tell you."

In response to "show it to me", a demonstration that "making it precise"
can be done both elegantly *and* easily in set theory should suffice to
show the unreasonableness of Patrik's several objections scattered through
his submission.  I'll demonstrate this for the following objection.

"We don't keep everything in one and the same bag, and we find it strange
that it is allowed to number everything in that one and the same bag. This
is my objection against Goedel's numbering."

The "bags" Patrik is referring to here would appear to be some or all of
sorts, terms, sentences, entailments, models, axioms, and inference rules.

All of these entities can be written formally and unambiguously as strings
over a fixed finite alphabet S defined independently of the (countably
many) sorts, operations, and variables, using techniques that should be
familiar to any adequately trained student of logic.   The permitted
strings can be defined with a suitable phrase structure grammar (a bit
stronger than context-free, e.g. Knuth's attribute grammars, but with
careful design still easily parsed) generating a language L.  Patrik's
"bags" arise as some of the nonterminals of that grammar.  Yet all these
bags exist as strings of L over the alphabet S, i.e. as members of the
single bag S*.

Every string in every bag has a Goedel number obtained by associating the
i-th terminal in S with the number i, from 0 to s-1 where s = |S|, and
treating the string as a number in radix s.

Yet even though all these strings come from the one bag S* as the set of
all strings over S, the grammar unambiguously determines which logical bag
the string comes from, whether sort, term, sentence, entailment, model,
axiom, inference rule, etc.

For those who've had sufficient practice with this sort of thing, it's easy.

As to whether it's elegant, Einstein's advice would be to ask a tailor,
ideally one in the business of tailoring mathematics to be elegant
regardless of whether its framework is set theory, category theory, or
something else.

Vaughan Pratt
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210611/f434b4ca/attachment.html>