I am searching for all the possible features of reasoning (all of them can be expressed in logic), so far I have found the following features:
- non-monotonicity, defeasible reasoning (expressed by special features of consequence relation)
- probabilistic reasoning (expressed by assignment of probabilities to the predicates and by the operations on the probabilities to the connectives and modal operators)
- higher order logic (expressed by allowing the predicated to take other predicates and formulas as arguments)
- modal operators (expressed by the unary operators acting on the predicates and formules)
- special connectives (expressed by special connectives that can arise in linear/substructural setting)
My question is this - are there any other features beside those 5, features that can improve the expresiveness of the logic.
I am trying to combine all those features in one logic and initially I would be happy to know that the set of those 5 features is exhaustive and so - when I come up with the language that can express all those 5 features then there is no more general language than that. Of course, I am thinking about templates, i.e., I will leave open the final set of modal operators and connectives (and the interactions among them), because different concrete logics can arise in each concrete choice of those. My aim is to create reasoner (forward chaining engine) that could be used for such templates and that works modulo concrete set of modal operators and connectives.
Of course, I will have to find common proofs for each of the logic but I plan to automate this task by formalizing each concrete logic in Coq or Isabelle/HOL as it has already be done for linear logics. Then (semi)automatic proof search can lead to the proofs of rejections of soundness and completeness theorems and other theorems for each logic. I am even thinking about combination of genetic search (for the operators/connectives/their sequence rules) with automatic theorem proving (for the theorems about concrete logic) (possibly - with deep learning inspired) for (semi)automatic discovery and development of logics. But to guide all this process, to predict the most general grammar for the possible logics, I should be sure that there is nothing beyond those 5 features. (Neural methods have stuck in deadlock, as can be seen from delayed introduction of autonomous vehicles, that is why strong boost of symbolic methods is necessary and automation of the discovery and research of the logics is the key process for the adoption of symbolic methods in industrial setting).
After that I will have to find semantics, but I am sure that set semantics (with probability distributions and set operations and relations (for modalities and substructural connectives)) is sufficient for all those 5 features, because everything in math can be expressed by (ZFC) set theory and that is why any other possible (sophisticated) semantics can be expressed via sets anyway.
Of course, I am aware of the efforts by Logica Universalis community, but the Florian Rabe, but the community of categorical logics and institution theory. But I am having hard time to find the logic that already encompass those 5 features and also I can not find definite answer that those 5 features are exhaustive or am I missing something?