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.

]]>Does anyone of any connections that have been made between the notions of cybernetics, autopoeitic systems, or even George Spencer Browns Laws of Form, and homotopy theory or category theory?

I suppose right now such connections might be somewhat tenuous, as the latter is pretty philosophical, and the former is pretty formal, but it seems that there are perhaps connections to be made. Especially, with the notion of the distinctions in space that Spencer-Brown talks about, ideas of homology and homotopy occur to me. Also, possible connections with David Spivak’s ontology logs and various ideas about categorical database type things. I’m also wondering if there are any connections between the aforementioned more philosophical topics and internal logic of topoi, or even topological semantics.

Any references or ideas on this would be really appreciated, it’s just kind of a shot in the dark. Perhaps the question is not well formed.

Best, Jon Beardsley

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

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.

]]>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 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 question comes to me because I am interested in organising ETCS in a formal language. I found this material called FOLDS https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf and it is claimed that topos axioms can be stated in FOLDS as in the style of the axioms on page 19. However, when we have both an initial object 0 and a terminal object 1, the sort of arrows from 1 to 0 is empty, but it does not seem to me that FOLDS allows empty sort.

On page 20 of the above link, it is written:

When X is a sort, and x:X, that is, x=〈2,X,a〉 for some a, x is called a variable of sort X

And later it is written that we can use the natural numbers to serve as the “a”. Therefore, once we have a sort, we can form infinitely many variables.

If we require every sort to be non-empty then we have soundness issue here: it can be easily proved that there does not exist any arrow 0 -> 1, otherwise we will have $0\cong 1$.

So is it my misunderstand? How do we treat empty sort in FOLDS?

]]>I have expanded Lawvere-Tierney topology, also reorganized it in the process

]]>Even as recently as this year, work is published attempting to deal with the logic of imperatives. I’ve not found a treatment of the logic of imperatives in HoTT. I’m curious whether such treatment exists or is possible.

Working through some examples, it’s not clear to me whether the available tools in HoTT are able to capture the logic of imperatives without some modification. Although it would be possible to convert imperative statements to declarative ones, Ross’s paradox (see part 6 here) seems to remain unsolved. However, I have an (unsubstantiated) hunch that HoTT may be closer to the solution due to the existence of typed function calls over which inference can be made. Consider a variation over the (unfortunately rather punitive) Donkey sentence:

“If you are a farmer and own a donkey, beat it”

Although HoTT provides an elegant way to construct the dependent product that formalizes the original declarative sentence, the imperative form seems to imply, rather, that the invocation of the dependent product is required. If we take $f:\equiv\Pi_{z:{\Sigma_{x:Donkey}(Owns(John, x))}} Beats(John, p1(z))$, then it seems that what is desired is the invocation $f(z)$ for all $z$ within the context.

Let’s consider a follow on imperative:

“If you beat your donkey, console it.”

There is an obvious inference here but I’m struggling to see how it can be made from from the respective declarative HoTT types. It seems as though what is missing is a type which represents the act of executing an action on some elements (for example, $f(z)$). An element of this type would be a warrant that a specific action was executed. The imperative sentence then is satisfied when such a warrant exists.

I’m fairly new to HoTT so I don’t know if that makes sense at all, but I’d appreciate a nudge or hint in the right direction.

]]>It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

I think the statement of strong induction to prove is as the following.

For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

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

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

I am reading the following document about Lawvere’s ETCS:

http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf

My question is about Theorem 6 in this document. The aim is to prove an equivalence relation is an equalizer. On page 29, the author says:

Finally we can assert our theorem (I think the $a_0q = a_1g$ in the link is a typo.) $a_0q = a_1q$ iff $a_0 \equiv a_1$.

And finished the proof.

That is, the author proves for every element $\langle a_0,a_1\rangle$ from the terminal object $1$, we have the split via the map which we want to prove to be an equalizer. But to prove the equalizer result, we need that we still have the factorization when $1$ is replaced by any arbitrary object. I know that $1$ is the generator in ETCS, and have trouble working out the proof that the existence of factorization for $1$ implies the existence of factorization for any $T$. I tried taking the elements of $T$, and unable to construct a factorization from $T$ from the factorization for its elements.

Any help, please? Thank you!

Note: If someone is reading the link above, then please note that the composition is written as: if $f: A \to B,g: B\to C$, then the author will write $fg$ to denote the composition of $f$ of $g$, rather than $g \circ f$.

]]>stub for *Hilbert’s sixth problem*

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

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

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