On the fully rigorous formalization of deductive reasoning in mathematics

[Tennant, Neil]

This is a brief reply to Vaughn Pratt's interesting post about a potential analogy with the competence/performance distinction in theoretical linguistics.

"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."

I just want to point out that "theorem provable in it with Cut" means, in the sentence quoted, "theorem provable in Core Logic (from some set of axioms) with Cut". But, as I've just tried to make clear in response to Jo's most recent post, no Core proof ever involves Cut. Core proofs are Cut-free and Thinning-free. That is how (along with subtle tweakings of certain Right and Left rules) they ensure relevance between their premises and their conclusions.

Neil Tennant


________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Vaughan Pratt <pratt at cs.stanford.edu>
Sent: Thursday, June 2, 2022 5:07 PM
To: fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: On the fully rigorous formalization of deductive reasoning in mathematics

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.

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/20220605/9795f561/attachment.html>