this MO comment made me realize that we didn’t have an entry proof assistant, so I started one
]]>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)]].
]]>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.
]]>at complete Boolean algebra I fixed the missing ${}^{op}$ and then added a pointer to Set – Properties – Opposite category and Boolean algebras.
]]>added to pure type system in the Idea-section the statement
In other words a pure type system is
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.
]]>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 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
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.
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)
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)
]]>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.
]]>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 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.
]]>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.
]]>Made a stub for admissible rule with a few examples, after seeing the discussion about negation here
]]>[new thread since “irreflexive relation” was not found among the LatestChanges threads]
A few day ago I added a standout box to irreflexive relation suggesting clarifying a notation.
I did this since there seems to be something to be clarified, but there is, as far as I can tell, nothing more to do than replace $x\nsim x$ with $\neg\, (x\sim x)$, and
Since this appears not to have worked out, this message.
Again, it seems that $\nsim$ is nothing else than an abbreviation, definitionally-equal to $\neg\, (x\sim x)$. It seems to be that this should be spelled out, the $\nsim$ not being defined anywhere (definitely not on the page itself, and I looked around a bit), and it is at this point most probably not meant to denote an apartness-relation, distinct from the relation $\sim$, i.e., $\nsim$ is not a relation symbol, in other words, not part of the syntax, rather part of a meta-syntax.
]]>In the following,
“cats” is used informally, to have a useful monosyllabic umbrella for ‘anything categorical’
“syntactic” and “semantic” are used informally.
Roughly speaking, the categorical logic developed in the last fifty years connected cats with logic, having cats appear on the semantic side.
Recent developments in mathematics seem to call more and more for technology which routinely handles cats on the syntactic side, too.
In the existent categorical logic, by and large, the “forms” one can handle, in particular—that one can apply the Mod-functor to— remain essentially 1-dimensional things.
Remarks.
More precisely, “multidimensional” seems a better modifier than “higher-dimensional” which in turn seems better than “higher”, for reasons of descriptiveness, neutrality, brevity, etc.
The meaning of the phrase “higher model theory” as it appears in the book edited by Barwise and Feferman is different and one can ignore it (for the purposes of this question, I mean.)
This idea is very much in the air these days, and bits and pieces of it appear all over the place. Just think of all the research on “higher-dimensional syntax” or usages like “a signature is a set of allowed moves” (the latter seems to be used around the Oxford computing lab, having to do with their constructing proof assistants helping to deal with multidimensional syntax). This thread is meant to focus on more technical and localized questions, though, in particular,
Essentially this is the probem of models for higher cats.
To ground the discussion, let me propose an easy test-problem, concerning two “almost equal” sets of multidimensional formulae:
Note: the set of axioms $\mathbb{A}_{\square}$ appears the more common one nowadays, maybe without any compelling reason.
Questions:
for this problem?
Remarks:
I do not expect there to be something essentially new here, but am asking out of curiosity. The possibility of doing apparently trivial modification to a set of formulas of course existed in one-dimensional model theory too, and the usual answer in traditional model theory is that the two sets of models of the two theories so obtained are exactly equal. Still, differences of degree can sometimes turn into something of a difference of kind. There are, intuitively, more possibilities to make seemingly inconsequential changes to a set of diagrammatically-expressed axioms.
The main issue besetting this question seems this: if you opt for some “class of all models” definition of Mod(), together equality of the respective classes, you have to commit to some “ontology” for the models; if on the other hand you opt for some more “constructive”/”algorithmic”/”it’s what you make of it” - definition of Mod(), then the slight difference in the shape of axioms on either side becomes an issue: it will “give the constructor ideas”/”give the algorithm ideas”/”give you ideas”, so that perhaps “what you make of it” comes out different on either side.
Type-theory has probably much to say on the question of how to define Mod, and this lightning overview provides a useful entry point to relevant modern developments.
I have cross-linked the entries forcing and classifying topos just a tad more by
adding a half-sentence at the end of the paragraph in the Idea-section at “forcing” which mentions the word “classifying topos”
adding to “classifying topos” the references (grabbed from “forcing”) on the relation between the two: here.
I imagine any categorical logician who would write a pedagogical exposition at forcing on how this concept appears from the point of view of topos theory could have some effect on the community. The issue keeps coming up in discussions I see, and so if we had a point to send people to really learn about the relation (instead of just being bluntly old that there is one) that might have an effect.
]]>At vector bundle all the way back from rev 1 there is a request for an entry “sheaf semantics”, at the bottom, where it says
sheaf semantics (Kripke-Joyal semantics)
Should we just make “sheaf semantics” redirect to Kripke-Joyal semantics?
]]>