On the fully rigorous formalization of deductive reasoning in mathematics

[Vaughan Pratt]

It's an interesting question as to whether a rule that is not needed other
than to make an existing proof shorter and/or more understandable should be
granted the same status as rules of reasoning that can't be dispensed with
at all.

Better than many of us, our moderator (MD) may recall the debate among
linguists of the 1950s onward as to whether the English language contained
infinitely many sentences, as proposed by U. Penn professor Zelig Harris
and the first of his six Ph.D. students, Noam Chomsky.

Assuming a finite terminal vocabulary or dictionary, the concern was that
this infinitude of English sentences implied the existence of English
sentences longer than a million words (or for that matter a google).  One
linguist (I forget who) wrote in a linguistics journal paper I read while
still a student in Australia, that while no precise bound on length could
be given it would be on the order of at most hundreds of thousands of
words, with a million being out of the question.

After due consideration Chomsky famously drew a distinction between
competence and performance, with the latter having to do with our human
constraints setting practical limits on the unbounded length implied by our
theoretical competence with the English grammar.

My understanding of Neil's Core Logic is that it doesn't need Cut in the
sense that any theorem provable in it with Cut is also provable without
Cut.  This is not the same thing as "some assembly required" because even
when some assembly is required Cut is not needed for that purpose.

In Harris and Chomsky's understanding of transformational grammar, the
surface structure of an English sentence arises out of how it can be
analyzed as having been transformed from one or more simple or kernel
sentences produced by a straightforward phrase structure grammar (PSG) into
a complex sentence.  The kernel sentences and transformations thereof then
constitute the deep structure giving rise to the final surface structure.
Even if the PSG generates only kernel sentences of some bounded length the
transformations set no limit on how many kernel sentences can be
transformed into one giant sentence, thereby producing infinitely many
surface structures and corresponding sentences.

Neil would be better equipped than I to draw parallels between
transformational grammar and Core Logic.  The process of making a very long
sentence more understandable by breaking it into smaller sentences may be
in some sense dual to making a long cut-free proof more understandable by
using Cut to break it into lemmas.

>From that point of view Core Logic should contain the competence part of
reasoning while Cut would cater for performance.

My thinking being a bit disjointed here, clearly some assembly is required.

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