[First time posting here.. please correct me kindly if I have not followed any explicit or implicit rules. And please excuse my question if it’s vague.]

It’s exciting to see that HoTT can prove concrete homotopical results, like $\pi_1(S^1) \simeq \mathbb{Z}$. It seems that to go further into other subfields, we need modality and cohesion in the theory to “buff up” the local structures – be it topological, smooth, or super-smooth..

However, I had a hard time tapping into modality and cohesion. First of, I’ve tried to understand what a cohesive topos means. As a first example of a cohesive topos, I’ve read through geometry+of+physics+–+smooth+sets and found it exciting. However, it remains unclear how to build up a theory with local model “X” from scratch by myself.

To do that, I planned to read Shulman’s proof on Brouwer’s fixed point.. hoping to understand the process by looking at a classical theorem in topology. But it is unfortunately too advanced for me, I’m not even sure where to start asking if there’s someone to help. Not being too familiar with type theory, I reckon there must be something missing.

What would you suggest if I want to quickly tap into these kind of modalic math, understand at least the proof for Brouwer fixed point, and hopefully be able to understand Schreiber’s foundation of geometry and physics?

4th year math PhD student. I’m not afraid of reading formal papers.. as long as it’s as much self-sufficient as possible. In fact, I find there’s “too much” motivation out there.. I hope to get serious, and even start to think/research in this language. Put in another way using an analogy in the world of programming: I regard Def/Thm/Proof as the source code of a program, and a regular math paper as the literate code or the manual/documentation of the source code. Sometimes it’s nice to have docs to read.. but sometimes you’d rather dive into the source code to see what *it is*. My mood is at the latter stage.

I’m willing to provide more details if it’d be helpful. Thank you very much!

]]>I was just wondering why there was so little on “Institution independent Model Theory” or Absrtact Model Theory in the wiki. I found this short entry for Abstract Model Theory, and a link to yet non existing page on institutions.

I am trying to use this to see if this can help me extend the semantic Web semantics to modal logic. The reason is that institutions have been used to show the coherence between the different RDF logics - RDFS, OWL, … and so it seems that it should be helpful to go beyond that.

Some papers on semantic web and institutions are listed below. These are great because the semantic web is quite simple, useful, - and I understand it well - and these show in a practical way how to think about institutions, which would be otherwise much more difficult to get into. Also the basics of Abstract Model theory are quite intuitive

- Lucanu, D., Li, Y. F., & Dong, J. S. (2006). Semantic web languages–towards an institutional perspective. In Algebra, Meaning, and Computation (pp. 99-123). Springer, Berlin, Heidelberg.
- Bao, J., Tao, J., McGuinness, D. L., & Smart, P. (2010). Context representation for the semantic web.

The last one ties rdf to Contexts and to Institutions.

The RDF model is actually really simple btw. See the question and answer “What kind of Categorical object is an RDF Model?”

It is nearly self evident from using it that RDF already contains modal logic (see my short example on semweb mailing list), especially as for RDF1.0 xml syntax one can have relations to RDF/XML literals, whose interpretations are of course sets of models, and in RDF1.1 this is made clearer with the notion of DataSets which are sets of graphs. But they have not given a semantics for it… But self evidence does not make for a proof. (and by the way, RDF/XML is really the ugliest syntax existing. Much better to consider N3 which is Tim Berners-Lee’s neat notation for doing logic on the web.

- Berners-Lee, T., Connolly, D., Kagal, L., Scharf, Y., & Hendler, J. (2008). N3logic: A logical framework for the world wide web. Theory and Practice of Logic Programming, 8(3), 249-269.

Btw, as an extra part the discussion on modal logic in RDF is tied up with the notion of context, which may just be another way of thinking of modal logic (I am working to see if there is a difference)

- Guha, R. V. (1991). Contexts: a formalization and some applications (Vol. 101). Stanford, CA: Stanford University.
- Hayes, P. (1997, November). Contexts in context. In Context in knowledge representation and natural language, AAAI Fall Symposium.
- Bizer, C., Carroll, J. J., Hayes, P., & Stickler, P. (2005). Named Graphs, Provenance and Trust. In Proceedings of the 14th international conference on World Wide Web.
- Hayes, P. (2007). Context Mereology. In AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning (pp. 59-64). This is I thought a really neat paper.
- Bao, J., Tao, J., McGuinness, D. L., & Smart, P. (2010). Context representation for the semantic web.
- Klarman, S. (2013). Reasoning with contexts in description logics.

So because there was little on the wiki on abstract model theory I was wondering if that was not quite thought of as good Category Theory, or if there just had not been time to complete that page. And for Contexts I was wondering if this was the right place to look at. In the book “Institution independent Model Theory” R Diaconescu has a chapter on Kripke frames, but I think we actually need neighborhood semantics, that is not relations between one world and another but between one world and a set of worlds. So that one can represent inconsistent sets of ideas. (which the web really is a big example of)

]]>But are there efforts to create logics with user-defined modal operators, effectively - logics which allow users to define functions (e.g. to act as polyadic modal operators) that can accept sentences (propositions, formulas) as arguments and that allow users to define (and fine tune) non-logical axioms on such user defined functions?

Such feature would be essential for formal semantics of natural language. Of course, the verb BELIEVE(subject, sentence) can be modelled as usual model operator in doxastic logic, but there can be many more shades of belief modality - subject, web tense, degrees of belief strength and so on, so on. Clearly to capture all those possibilties one should move the definition of modal operators from the logical language to the non logical language (where the usual functions reside).

So - are there efforts to define and research such logics?

I am aware of the book https://www.springer.com/gp/book/9783319225562 "Toward Predicate Approaches to Modality" whose opening chapter states, that modality could be modelled as the predicate on the sentence name (sic! - sentence name)! I am still studying this book, maybe it will provide solution for me. ]]>

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

So - one idea is to make ontology of modal logics. One kind of example is http://www.cs.man.ac.uk/~ezolin/ml/ - but it is mostly about complexity of some properties (there are many more of them for modal logics) and there is no list of notable fragments for selected logic as well.

I could see two applications of such ontology (with relevant tooling):

1) one could quickly see where the work is required;

2) one could select the most appropriate modal logic (or combination of them) for application.

The risk of failure for such project could be the fact, that many logics could be not quite uniform.

But anyway - what are thoughts of professional mathematicians about such endeavour and what could be requirements both - for ontology itself and tooling. ]]>