About Logic on Natural Language and the Meaning of σύνεσις

I had in idea about this whilst listening to this interview with Bernhard Schröder and Bernhard Fisseni:

See their Natural language Proof Checking project https://naproche-net.github.io/:

The Naproche system is an implementation of the ideas developed by the Naproche project. It accepts a controlled but rich subset of ordinary mathematical language including TeX-style typeset formulas and transforms them into formal statements. Linguistic techniques are adapted to allow for common grammatical constructs and to extract mathematically relevant implicit information about hypotheses and conclusions. Finally, automated theorem provers are used to prove the correctness of the input text. 

42:20 Listening to this discussion around creating shared facts by locutionary acts it occurred to me that in a sense the idea of frames is partly psycho-linguistic and partly social. So I started to wonder whether there were any ancient Greek words which were to do with the idea of shared knowledge, and it turns out there is one, which is σύνεσις, and these days is taken to mean understanding, wisdom or something like a unification or a confluence, or in a technical linguistic sense of agreement, which is the only one mentioned on the wikipedia page.

But it's so close to σύνθεσις which was the topic of last week's episode that I couldn't help but wonder of there mightn't some reason for this. See About Logic - Analytic and Synthetic Mathematics. 

My comment:

46:58 This sort of to-and-fro exchange was illustrated very well in Imre Lakatos' book Proofs and Refutations. It was supposed to be a representation of the actual historical development of topology, but the dialogue was something which took place over a period of almost a century. See About Logic - Is Mathematics a Story? 

 

[In that I wrote "I sometimes think that Computer scientists look for models in the zoo of mathematical theories, because they feel like this the only possible source of their legitimacy: they say something like "Well, this type system is sound because if it wasn't then ZFC would be inconsistent and you would have much bigger things to worry about than the soundness of my little type system!"  That was actually the case, in particular for Robin Milner's polymorphic types (see https://prooftoys.org/ian-grant/hm/) and others in the ML-style languages, for example MacQueen, Plotkin and Sethi's An Ideal Model for Recursive Polymorphic Types, but after listening to Bob Harper's Course on Principles of Programming Languages and Frank Pfenning's Course on Linear Logic I realise that it's not always the case. Pfenning, following Girard, I suppose, uses deductive systems as models, I think. See Lecture Notes on Resource Semantics: "In this lecture we explore a new presentation of linear logic, one where resources are explicitly tracked in the judgments. It is a new form of semantics, given by intuitionistic means, while generally semantic investigations take a classical point of view even if the studied subject is intuitionistic".]

 

Deniz mentioned Catarina Dutilh Novaes book The Dialogical Roots of Deduction: Historical, Cognitive and Philosophical Perspectives on Reasoning. 

See also A New Kind of Science and Emil Post.

Subscribe to About Logic.