Are there efforts to automatically discover new logics? Logics are simple structures - they have formal language, deduction rules, semantics and certain properties that are proved or discarded for every new logic. In fact, each logic can be put into framework of institutions (by Diaconescu et al).

So - is it possible to automatically learn/discover new logics?

E.g. type logical grammars (development of (abstract) categorial grammars) map natural language sentences into lambda expressions (some logics into language in lambda expressions). It can appear, that resulting expressions can not be built due to low expressibility of the logic. So - new, more expressive, more adaptable logics should be discovered. Can the process be automated by using criterion of "optimally highest level of understanding" (i.e. whether the machine can understand and operate with the formalized text or not) - e.g. if machine can not understand the valid natural language text, then machine is obliged to discover new logic into which the text can be translated and understood.

There is formalization of the notion of "understanding" https://link.springer.com/chapter/10.1007/978-3-319-41649-6_11 and this understanding can be optimized for the discovery of new logics.

So - are there trends to do this?

I am aware of inductive logic programming which discover rules in some logic, but I am aiming for the discovery of the logic itself. So - there is also inductive metalogic programming but I have managed to find only two articles about this (one in Japanese) and they seem to be not about new logics.

I have also heard about framework of ludics of Girard, but it is very, very bounded work on linear logic, more general setting is required and ludics seem to be not generalizible enough.

  • 1
    $\begingroup$ I'm not sure to understand your idea but "Logics are simple structures - they have formal language, deduction rules, semantics" Unfortunately, it's not that easy... That's a way to see a logical system but logic is way more than that. It's quite clear that we need ideas. Do you think we can invent new kinds of lambda calculi automatically ? See the difference between System F, simply typed λ-calculus, λμ-calculus... Moreover, Linear Logic is actually quite general : it can encode classical and intuitionistic logic and is more than some formal rules (see proof nets, GoI, polarity, ...) $\endgroup$ – Boris Dec 20 '17 at 22:53
  • $\begingroup$ Certainly, we should not discover new lambda calculus - it is just language in which each logical expression (of some logic) can be written down (okmij.org/ftp/gengo/applicative-symantics/AACG.pdf for example, mentions, that FOL can be expressed in lambda calculus). Of course, logics are not simple, but they form the category in the institution theory approach, there is certain path what each new logic should go. $\endgroup$ – TomR Dec 20 '17 at 22:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.