Following discussion in some other threads, I thought one should make it explicit and so I created an entry

Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.

The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.

This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.

Thanks for whatever input you might have.

]]>I gave *Sets for Mathematics* a category:reference entry and linked to it from *ETCS* and from *set theory*, to start with.

David Corfield kindly alerts me, which I had missed before, that appendix C.1 there has a clear statement of Lawvere’s proposal from 94 of how to think of categorical logic as formalizing objective and subjective logic (to which enty I have now added the relevant quotes).

]]>created an entry *[[modal type theory]]*; tried to collect pointers I could find to articles which discuss the interpretation of modalities in terms of (co)monads. I was expecting to find much less, but there are a whole lot of articles discussing this. Also cross-linked with *[[monad (in computer science)]]*.

edited [[classifying topos]] and added three bits to it. They are each marked with a comment "check the following".

This is in reaction to a discussion Mike and I are having with Richard Williamson by email.

]]>I started an article about [[Martin-Lof+dependent+type+theory|Martin-Löf dependent type theory]]. I hope there aren't any major mistakes!

One minor point: I overloaded $\mathrm{cases}$ by using it for both finite sum types and dependent sum types. Can anyone think of a better name for the operation for finite sum types?

]]>this MO comment made me realize that we didn’t have an entry *proof assistant*, so I started one

We have several entries that used to mention *Lawvere’s fixed point theorem* without linking to it. I have now created a brief entry with citations and linked to it from relevant entries.

at *complete Boolean algebra* I fixed the missing ${}^{op}$ and then added a pointer to *Set – Properties – Opposite category and Boolean algebras*.

While concentrating on Category Theory as applied to the Web, I have also been following French Philosopher of technology Bernard Stiegler, as he was supportive of the creation of the Philosophy of the Web conference 10 years ago.

Recently he has been looking at the concept of locality which he argues has been repressed mostly after Aristotle, being overtaken since Plato with the notion of the Universal (The world of ideas), transferred into the Philosophers notion of God. Those philosophers who have tried to bring Locality back, such as Heiddegger with his concept of Dasein (being here), or Japanese philosopher Kitaro Nishida concept of place as a departure point, have had problematic relations with the Axis powers during the second world war. Yet Stiegler believes that since Schroedinger’s development in What is Life? of the concept of negative entropy as what fights *locally* entropy, forces us, if we are to take this seriously, to give a central position to locality. In any case the Web and the Internet create tensions between local cultures due to its creating ” a topological space without any distances” (see interview of late Michelle Serres).
I’ll see if I can find a good English paper of Stiegler that makes these connections clearly.

Now the Topos meant place in Ancient Greek (or see also Topoi on Topos: The Development of Aristotle’s Concept of Place). So I was wondering if people here who had deeper intutions about Category Theory than me, can see some insights that Category Theory can bring on these topics. Of course I bring this up here as Topos is also an essential concept in Category Theory which I believe one can summarise as the allowing one to connect logic and topology.

Perhaps modal logic captures this relation to location better. David Corefield in his published Chapter 4 on Modal HoTT writes of adjoint modalities:

]]>Choosing q equal to p, we see that a proposition sits between the images of the two operators (◻︎, p, ◇):

- necessarily true, true, possibly true following the pattern of
- everywhere, here, somewhere.

In “Natural duality, Modality, and Coalgebras”, in his thesis Meaning and Duality - From Categorical Logic to Quantum Physics, and elsewhere Yoshihiro Maruyama talks about $\mathrm{ISP}$, $\mathrm{ISP}$(M), how it is composed of $\mathrm{I}$, $\mathrm{S}$ and $\mathrm{P}$, but I can’t figure out what these stand for.

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

]]>Stub Makkai duality, just recording the most basic references so far; linked from Stone duality.

]]>I have added to the References at *double negation* pointer to Andrej’s exposition:

which is really good. I have also added this to *double negation transformation*, but clearly that entry needs some real references, too.

I take issue with the article on Linear Logic in the nLab. It says:

(In this way, linear logic has a perfect de Morgan duality.) The logical rules for negation can then be proved.

While this is true for *Classical* Linear Logic, for Intuitionistic Linear Logic things are very different and I feel that this whole 'dark side of the moon' is being thrown away for no good reason. There is no reason to decide that Classical Logic is better than Intuitionistic Logic and there is not reason to decide that Classical Linear Logic is better than Intuitionistic Linear Logic. the article should have a discussion of both realms. How do I go about adding this discussion, please?

thanks

Valeria ]]>

added to *pure type system* in the Idea-section the statement

In other words a

pure type systemis

a system of natural deduction

with dependent types

and with the dependent product type formation rule.

and to the *Related concepts*-Section the paragraph

Adding to a pure type sytstem

rules for introduing inductive types

possibly a type of types hierarchy

makes it a

calculus of inductive constructions.

Finally I added to the References-section a pointer to these slides

]]>have expanded the Idea-section at *quantum logic* to now read as follows:

Broadly speaking, *quantum logic* is meant to be a kind of formal logic that is to traditional formal logic as quantum mechanics is to classical mechanics.

The first proposal for such a formalization was (Birkhoff-vonNeumann 1936), which suggested that given a quantum mechanical system with a Hilbert space of states, the logical propositions about the system are to correspond to (the projections to) closed subspaces, with implication given by inclusion of such subspaces, hence that quantum logic is given by the lattice of closed linear subspaces of Hilbert spaces.

This formalization is often understood as being the default meaning of “quantum logic”. But the proposal has later been much criticized, for its lack of key properties that one would demand of a formal logic. For instance in (Girard 11, page xii) it says:

Among the magisterial mistakes of logic, one will first mention quantum logic, whose ridiculousness can only be ascribed to a feeling of superiority of the language – and ideas, even bad, as soon as they take a written form – over the physical world. Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.

and for more criticisms see (Girard 11, section 17).

Therefore later other proposals as to what quantum logic should be have been made, and possibly by “quantum logic” in the general sense one should understand any formal framework which is supposed to be able to *express* the statements whose semantics is the totality of all what is verifiable by measurement in a quantum system.

In particular it can be argued that flavors of *linear logic* and more generally *linear type theory* faithfully capture the essence of quantum mechanics (Abramsky-Duncan 05, Duncan 06, see (Baez-Stay 09) for an introductory exposition) due to its categorical semantics in symmetric monoidal categories such as those used in the desctiption of finite quantum mechanics in terms of dagger-compact categories. In particular the category of (finite dimensional) Hilbert spaces that essentially underlies the Birkhoff-vonNeumann quantum logic interprets linear logic.

Another candidate for quantum logic has been argued to be the internal logic of Bohr toposes .

In quantum computing the quantum analog of classical logic gates are called *quantum logic gates*.

I gave the entry *logical relation* an Idea-section, blindly stolen from a pdf by Ghani that I found on the web. Please improve, I still don’t know what a “logical relation” in this sense actually is.

Also, I cross-linked with *polymorphism*. I hope its right that “parametricity” may redirect there?

I have splitt off from *classifying topos* an entry *classifying topos for the theory of objects* and added the statement about the relation to finitary monads.

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)

]]>I gave *proof by contradiction* a little Idea-section. This came about with writing an Idea-section at *classical logic*, which we are discussing in another thread here.

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

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

added to *modality* a minimum of pointers to the meaning in philosophy (Kant).

added to the list of References at *categorical logic* a pointer to

Created subformula property.

]]>