I’m currently wrestling with the ideas in the following two pages:

Here are the specifics: In [1] the Grothendieck construction is described as the (strict) pullback of the universal Cat-bundle $\operatorname{Cat}_{\ast,\ell}\to\operatorname{Cat}$. In [2], under the section “$n$-subobject classifiers” is the statement:

$E_{pt}\operatorname{Cat}\to\operatorname{Cat}$ is $\operatorname{Cat}_*\to\operatorname{Cat}$. Pullback of this gives the Grothendieck construction.

Of course, the categories $\operatorname{Cat}_*$ and $\operatorname{Cat}_{\ast,\ell}$ are slightly different, only in the morphisms. My question is: can the category $\operatorname{Cat}_{\ast,\ell}$ be described as some variation of the pullback:

$E_{pt}\operatorname{Cat} = \lim([I,\operatorname{Cat}]\to\operatorname{Cat}\leftarrow pt) = \operatorname{Cat}_*?$ ]]>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 by 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?

I would like to add that it is very important that everyone at this time come up with some advice or suggestion, idea. Now the economic crisis is starting again and it is very important to finalize the achievement of artificial intelligence and streamline them into industry exactly now. Only the increase of the supply side productivity (by the artificial intelligence) can save the us from the coming crisis.

]]>http://cstheory.stackexchange.com/questions/18716/good-reference-about-approximate-methods-for-solving-logic-problems

I also have found several papers about it. E.g. undecidability of modalo logics can be overcome by limiting depth of nesting of modal operators. While this is not mathematically pure solution, it is very good approximation to the human reasoning that is not quite capable of self-reflection.

Are there chances that heuristic methods - e.g. genetic algorithms or neural networks can overome undecidability problem - e.g. by discovering theorems and proofs that can not be discovered by algorithmic methods?

I see big prospects for categorical logic to become the universal logic that unifies all sorts of reasoning types (human agent modelling, creativity modelling, mathematical reasoninig, legal reasoning are all types of reasoning that requires different different methods but the application borders are smooth and therefore unification is necessary) but the application will be impossible if there is no methods for handling undecidable cases. Therefore one should be able to overcome undecidability. ]]>

I'm one of the founders of Arbital, a website for crowdsourced, intuitive math explanations. We are currently doing a collaborative project to explain the Universal Property concept in Category Theory. If you'd like to check it out, take a look here: https://arbital.com/project/

Once we are done, I'll post a link here so people can read the explanation. :) ]]>

I have added to universal covering space a discussion of the “fiber of $X\to \Pi_1(X)$” definition in terms of little toposes rather than big ones.

I find this definition of the universal cover extremely appealing. It seems that this sort of thing must have been on the tip of Grothendieck’s tongue, and likewise of all the other people who have studied fundamental groups and groupoids of a topos, but it all becomes so much clearer (I think) when you state it in the language of higher toposes. In this case, merely (2,1)-toposes are enough, so no one can argue that the categorical technology wasn’t there – so why didn’t people see this way of stating it until recently? Or did they?

]]>I was reading MacLane (like a good student) and when I saw the diagram for a universal arrow, it made me think of natural transformations.

It looked like we could describe a comma category $(d\downarrow F)$ as a natural transformation $\tau:\Delta d\to F$, where $\Delta d:C\to D$ is a constant functor.

If so, then the universal arrow, i.e. initial object of the comma category, would be like the “initial component” of a natural transformation.

Does that make any sense?

]]>