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 have tried to brush-up *existential quantifier* a little more. But not really happy with it yet.

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 have expanded Lawvere-Tierney topology, also reorganized it in the process

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

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

]]>some bare minimum at *cut rule*

I have given *necessity* and *possibility* (which used to redirect to *S4-modal logc*) an entry of their own.

The entry presently

first recalls the usual axioms;

then complains that these are arguably necessary but not sufficient to characterize the idea of necessity/possibility;

and then points out that if one passes from propositional logic to first-order logic (hyperdoctrines) and/or to dependent type theory, then there is a way to axiomatize modalities that actually have the correct interpretation, namely by forming the reflection (co)monads of $\exists$ and $\forall$, respectively.

You may possibly complain, but not necessarily. Give it a thought. I was upset about the state of affairs of the insufficient axiomatics considered in modal logic for a long time, and this is my attempt to make my peace with it.

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

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

stub for *deduction theorem*

I noticed that all the paradox-related articles were happily pointing to *paradox*, which however was less than a stub. So I tried to promote it at least to stub-status.

created a stub for *no-cloning theorem*.

For the moment what I wanted to highlight is that under the identification of linear logic as quantum logic it is this theorem which is the “linearity” of the logic.

]]>I keep feeling the need to point to an entry named *formal logic*. None of the existing entries seems to quite deserve to be where this link should be redirecting to. So I created a page *formal logic* with just some pointers to pages that the reader *might* expect behind this term.

Just so that I can use that link for the time being.

]]>Hi, all.

I am trying to understand the proof of proposition 7.6 in Shulman’s paper https://arxiv.org/pdf/1808.05204.pdf . I am interested in understanding it for applying it within SEAR to obtain interesting constructions (or ETCS, I say SEAR here because it comes with a collection axiom). One point that confuses me is that I am not yet familiar to the notion of stacks. As the claim is that the proof of 7.6 can be carried our within SEAR for each particular case, I think it would be ideal if I can see how the proof of 7.6 expands on particular examples to obtain a proof within SEAR. (Note: I do not think I am confused by how to apply the principle of replacement, I am confused by how its proof works for these particular examples. Say, from the context we can obtain from collection, how can we derive the existence of the context we want by manipulation within these examples without directly appeal to the replacement schema.)

For the simplest example I can think of, consider we want to build the well-ordered set N without explicitly defining the order “$lt$”. I think we may obtain an isomorphic copy of the well-ordered set N using replacement.

Let U be N, u be a natural number n in N, we can prove for each n there exists a set A and a relation R on A, such that R is a well order on A. That is, the context $\Theta$ is $[A,R:A\looparrowright A]$, and it can be proved that consider the formula $\phi$ such that $\phi(N,n,A,R:A\looparrowright A)$ is true iff $A$ has cardinality $n$ and $R$ is a well-order on $A$, then there would be a context over a cover $p:V \to N$ which descents to a context over $N$, and the resultant context should consist of a set $\tilde{A}$ and a relation on $\tilde{A}$, where $\tilde{A}$ has a map to $N$, call it $q$. I think then $q^{-1}(n)$ will be the well-ordered set contains $n$ elements, and the whole $\tilde{A}$ is the disjoint union of $A_0,\cdots,A_n,\cdots$. where $A_n$ is the well-ordered set containing $n$ elements. Then we can collect the maximal elements in each such set and obtain a copy of $N$ with the order $\lt$.

This example above is due to myself and I am not sure if I have got it correct, but the following example from Mike Shulman must be correct. It is a bit complicated and let me expand the story in details below.

For an ordinal $\alpha$, there is a notion of the $\alpha$-th Beth number, denoted as $\beth_\alpha$. This **number** itself is a **set**, so you may think of associate each ordinal with a set.

If $\alpha \lt \omega$, means that $\alpha$ is a finite ordinal, that is, a natural number, then the $\alpha$-th Beth number is the power set That is, , $P^\alpha(\mathbb N\beth_0 =\mathbb N\beth_1= PN$, $\beth_2 = PPN$ and $\beth_3 =PPPN$, etc.

Now consider the notion of the $\omega$-th Beth number, $\beth_\omega$ is defined to be the minimal set such that for every natural number $n$, the set $\beth_n$ injects to it. We are going construct $\beth_\omega$, and its construction relies on schema of replacement.

Regarding how to apply the replacement schema (credit to Mike Shulman):

The way to use replacement of contexts here is something like the following. For simplicity consider the natural numbers N. For x in N, consider the context consisting of a set X, a function p : X -> N, a relation R from X to X, and a function z : N -> X. Depending on x and on this context, consider the statement that the image of p is {y | y <= x}, that z is an isomorphism onto the fiber p^{-1}(0), and that R is the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x. One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic. Therefore, by replacement of contexts, there is a universal such context over N, which in particular has a function p : X -> N x N. Pulling this back along the diagonal map of N, we obtain an N-indexed family of sets that is the sequence of iterated powersets starting with N, and thus its total space is beth_omega.

Recall the statement of replacement of contexts (from Shulman’s paper):

for any formula $\phi(U, u :\in U, \Theta)$, for any $U$, if for every $u :\in U$ there is an extension $\Theta$ of $(U, u)$ such that $\phi(U, u, \Theta)$, and moreover this extension $\Theta$ is unique up to a unique isomorphism of contexts $\Phi_\Theta$, then there is an extension $\Theta_0$ of $(U ^* U,\Delta U )$ in $Set/U$ such that $\phi(U, u , u ^ * \Theta_0 )$ for all $u :\in U$.

Here the $\phi$ is the “statement” in ” consider the statement that the image of p”. This statement is on the following parameters: 1. The fixed natural number $x$, as in “For x in N, consider…”. 2. the function $p:X\to N$, 3. the relation $R:X\looparrowright X$, which is “the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x”. (Union of relations are given by consider a relation from $X$ to $Y$ as a subset of the power set ${\cal P} (X\times Y)$). 4. the funcion $z:N\to X$, which injects $N$ to $X$.

Intuitively, this relation says that $X$ is a set which is fibred over $N$ via the projection map $p:X\to N$, such that the fibre of $0$ is $N$, and for each number $m\lt n$ the fiber of its successor $m+1$ is the power set of the fiber of $m$. (*) Therefore, $\beth_n$ is the fiber of $n$.

Call the predicate by $Upow(n,p:X\to N,R:X\looparrowright,z:{N}\to X)$, we apply replacement of contexts on $Upow$. Here $U$ is $N$, $u\in U$, is $n\in N$, $\Theta$ is the list $[X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]$. As suggested by

One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic.

By induction on $n\in N$, we prove there exists a context $[X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]$ up to unique isomorphism such that $Upow(n,p:X\to N,R:X\looparrowright X,z:{ N}\to X)$. Therefore we can apply replacement. It gives a context $\Theta_0:=[X_0(\to N),p_0:X_0\to { N}\times { N}, R_0:X_0\looparrowright X_0,z_0:{\Bbb N}\times {N}\to X_0]$ where the maps $p_0,z_0$ and the relation $z_0$ are in the slice category. In particular, the fibre of the map $p_0:X_0\to { N}\times { N}$ on the point $(n,n)$ is the greatest fiber, i.e., the fiber of $n$ as in (*) above, of a context satisfying $Upow(n,p:X\to N,R:X\looparrowright,z:{ N}\to X)$. Therefore, pulling back along the diagonal map just means take out all these sets $\beth_1,...,\beth_n,\beth_{n+1},...$ (infinitely many). All these sets are contained as a subset of $X_0$, so we can take union of them.

Could someone please explain the proof of 7.6 in Shulman’s paper, in terms of some examples such as the two above, to illustrate how the proofs work? It does not have to be convoluted. I am most confused by the step which uses “Set is a stack of its regular topology”.

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

created a stub (in category: reference) for *Principia Mathematica*, in order to mention its idea of “ramified types”. Added a pointer to this to the lists of references at *type theory* (also at *foundations of mathematics*).

I’d like some kind of comment like “This is the earliest proposal of a type theory.” Or “This is the earliest substantial/formal/sensible/substantive/influential proposal…” or the like. What’s the right thing to say?

Thanks to David Roberts for highlighting this in discussion. Ultimately I’d find it fun to get a historical impression of Russell’s road from the “revolt against idealism” to type theory.

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

I have added the following paragraph to *calculus of constructions*, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:

]]>More in detail, the

Calculus of (co)Inductive Constructionsis

a system of natural deduction with dependent types;

with the natural-deduction rules for dependent product types specified;

and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.

and with a type of types (hierarchy).

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

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?

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.

]]>Hi, all.

I would like to understand hoe does SEAR Axiom 5 works, that is Axiom of collection in SEAR.There is a section on “Application of Collection” and a sentence “(more detail to be added here…)”. My question is basically “what is intended to be there” in short.

According to my current understanding the example in this incomplete section, which aims to construct the ghost of $\{P^n(N)\mid n\in N\}$ should work as follows: we have a predicate taking a natural number $n$ and a set $Pn$, such predicate holds if $Pn \cong P^n(N)$ (here $\cong$ means bijection, cannot use equality here because the nlab page claims that there is no equality between sets.). And by axiom 5, we have a set $B$, a function $p:B\to N$. and a $B$-indexed family of sets $M:B\looparrowright Y$ such that for any $b\in B$, $M_b \cong P^{p(b)}( N)$ and for any $n\in N$, there exists a member of$b$ which is mapped to $n$. (because $P^n(N)$ exists for every $n$).

Does this sound correct?

If so, then it seems to me that the application of Axiom 5 only gives $Y$ contains $\coprod_{n\in N}P^n(N)$. As the nlab page claims that the collection axioms plays a similar role as replacement. How can I demonstrate that the thing I have obtained here is useful enough to be an analogue of the set $\{P^n( N)\mid n\in N\}$ as in ZF?

Other examples on SEAR Axiom 5 would also be nice! Thank you!

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

]]>