I was contacted by somebody involved in *The QED Project*. I have given that an $n$Lab page now, linked to from *proof assistant*, cross-linked with *ForMath*. (Maybe we should have a page *formal mathematics* or the like?)

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

]]>Late last night I was reading in *Science of Logic* vol 1, “The objective logic”.

I see that the idea of cohesion is pretty explicit there, not in the first section of the first book (*Determinateness*, which has the discussion of “being and becoming” that Lawvere is alluding to in the Como preface) but in the second section of the first book, “The magnitude”.

There the discussion is all about how the continuous is made up from discrete points with “repulsion” to prevent them from collapsing to a single and with “attraction” that keeps them together nevertheless.

This “attraction” is clearly just the same idea as “cohesion”. One can play this a bit further and match Hegel’s *Raunen* to formal expressions involving the flat modality and the shape modality pretty well. I made some quick notes in the above entry.

On the other hand, that section 1 about being and becoming seems to be more about the underlying type system itself. Notably about the empty type and the unit type, I think

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

Started literature section with several references at forcing.

]]>Recently in an edit of mine Frank Waaldijk found it necessary (here) to replace “intuitionistic” by “constructive”. This alerted me that it would be nice if the distinction were made a bit more transparent in the respective $n$Lab entries. Presently our “constructive logic” simply redirects to “intuitionistic logic”. And while we do have separate entries for “constructive mathematics” and “intuitionistic mathematics”, I find it hard to extract from them their distinction.

I am not going to edit on these matters. This is an alert and a request to the logic experts around here. Maybe if you have some spare energy, it would be worthwhile to improve on this situation of $n$Lab entries a little.

]]>I was involved in some discussion about where the word “intensional” as in “intensional equality” comes from and how it really differs from “intenTional” and what the point is of having such a trap of terms.

Somebody dug out Martin-Löf’s lecture notes “Intuitionistic type theory” from 1980 to check. Having it in front of me and so before I forget, I have now briefly made a note on some aspects at *equality* in the section *Different kinds of equalits* (below the first paragraph which was there before I arrived.)

Anyway, on p. 31 Martin-Löf has

intensional (sameness of meaning)

I have to say that the difference between “sameness of meaning” and “sameness of intenTion”, if that really is the difference one wants to make, is at best subtle.

]]>Foundations of Systems Architecture Design

Using Gödel’s Incompleteness Theorem to ground Systems Theory via Co-recursion based on Special Systems Theory

See https://www.academia.edu/31038671/Foundations_of_Systems_Architecture_Design

I was hoping someone here might be able to help me who would find this approach interesting.

Kent Palmer

http://kdp.me

https://independent.academia.edu/KentPalmer ]]>

When I made *inhabitant* redirect to *term* a few minutes ago, I noticed a bunch of orphaned related entries.

For instance *inhabited type* since long ago redirect to *inhabited set*. I haven’t changed that yet, but I added some cross links and comments to make clear that and how the three

are related. The state of these entries deserves to be improved on, but I won’t do anything further right now.

]]>I have recently created an entry definable set. It is usually defined as an equivalence class of formulas satisfied by the same elements in each structure of the first order language (or model for a theory). But some works recently, like the lectures of David Kazhdan (pdf), take for granted the observation that in fact the relation of equivalence implies that the evaluation of definable sets in a model extends to a functor on the category of models and elementary monomorphismsm, say $\mathcal{M}_{el}$. There are now many other notions in model theory which have ’definable” as a prefix, and they do not fill uniformly in the same pattern. For example, the category of “definable spaces” and “definable continuous maps” is not the same as the functor from $\mathcal{M}_{el}$ to topological spaces and continuous maps, though possibly some examples would probably fit in the latter description. Also some “definable” notions are for a fixed model and not functors on $\mathcal{M}$.

Now, Hrushovski in his 2006 work looked at definable groupoids, about which I just plan to create an entry. Now I was cautious not to say that it is simply an internal groupoid in the category of definable sets, as it is at first defined differently. Besides dealing with internal objects in a large functor category, one should possibly make care about this as well, regarding that we are dealing with a setup where one should be maybe careful about tools like large cardinals (what would be the elegant way to do?).

But in any case, the first problem (that the definition was not given as a functor) can easily be dealt.

So the definition roughly says that one has definable set of objects and of morphisms (just as we wanted), but then the structure maps like target, composition etc. should be definable functions, hence, as relations they are definable subsets of cartesian products, so when presented from $\mathcal{M}_{el}$ as functors into the categories of sets and relations, which are functional in every model. So, now I just checked a very simple fact, specific to the category of sets and functions, that

**Proposition.** Given a small category $\mathcal{M}$ and two functors $F,G:\mathcal{M}\to Set$ the natural transformations $\alpha : F\to G$ are in 1-1 correspondence with
functors $\beta : \mathcal{M}\to Set$ such that $\beta(A) \subset F(A)\times G(A)$ and $\beta(A)$ is a functional relation.

In other words, functoriality of $\beta$ is the same as $\alpha$ being natural. That is new to me.

This immediately implies that the definable groupoid as in Hrushovski arxiv/math.LO/0603413 is (up to the delicacies dealing with functor categories) indeed an internal groupoid in the category of functors $\mathcal{M}_{el}\to Set$ and natural transformations.

]]>Created ZFA, about ZF with atoms. I’ve added it to the foundations side bar under material set theories and a stack of links.

]]>in another entry I want to be able to point to *context extension*, so I created a brief entry

I have a feeling that the two parts of the fundamental theorem of calculus are different in foundational strength. In particular, I believe that the part of the fundamental theorem of calculus which is Stokes's theorem for the interval [0, 1] is equivalent to the law of bounded change. I am aware that the previous assertion is trivial at present, since of these statements are manifestly true (constructively). ]]>

I found the organization at *Zorn’s lemma* a bit rough, so I have tried to smoothen it out a bit

For instance

at one point it had suddenly said “proof of the converse” without a clear statement of the other direction having appeared before. I have created two Theorem-environments and tried to make the statements clearer.

the Idea-section had started out saying that “Zorn’s lemma is a trick”. I think that’s misleading or at least misses the important nature of the thing, so I rewrote that and expanded a bit.

But the foundationalists among you please check!

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

]]>Am trying to get some historical citations straight at *linear type theory*, maybe somebody can help me:

what are the original sources of the idea that linear logic/type theory should generally be that of symmetric monoidal categories (“multiplicative intuitionistic LL”)?

In order of appearance, I am aware of

de Paiva 89 gives one particular example of a non-star-autonomous SMC that deserves to be said to interpret “linear logic” and clearly identifies the general perspective.

Bierman 95 discusses semantics in general SMCs more generally

Barber 97 reviews this and explores a bit more.

What (other) articles would be central to cite for this idea/perspective?

I am aware of more recent reviews such as

but I am looking for the correct “original sources”.

]]>I happened upon our entry *ETCS* again (which is mostly a pointer to further entries and further resources) and found that it could do with a little bit more of an Idea-section, before it leaves the reader alone with the decision whether to follow any one of the many further links offered.

I have expanded a bit, and now it reads as follows. Please feel invited to criticize and change. (And a question: didn’t we have an entry on ETCC, too? Where?)

The **Elementary Theory of the Category of Sets** (Lawvere 65), or *ETCS* for short, is a formulation of set-theoretic foundations in a category-theoretic spirit. As such, it is the prototypical structural set theory.

More in detail, ETCS is a first-order theory axiomatizing elementary toposes and specifically those which are well-pointed, have a natural numbers object and satisfy the axiom of choice. The idea is, first of all, that traditional mathematics naturally takes place “inside” such a topos, and second that by varying the axioms much of mathematics may be done inside more general toposes: for instance omitting the well-pointedness and the axiom of choice but adding the Kock-Lawvere axiom gives a smooth topos inside which synthetic differential geometry takes place.

Modern mathematics with emphasis on concepts of homotopy theory would more directly be founded in this spirit by an axiomatization not just of elementary toposes but by elementary (∞,1)-toposes. This is roughly what univalent homotopy type theory accomplishes, for more on this see at *relation between type theory and category theory – Univalent HoTT and Elementary infinity-toposes*.

Instead of increasing the higher categorical dimension (n,r) in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case $(2,2)$ is the elementary theory of the 2-category of categories (ETCC).

]]>

we were lacking an entry *realizability* that points to all the related entries (and in fact some entries were asking for just “realizability”).

So I started one. Put in the following Idea-paragraph:

]]>The idea of

realizabilityis essentially that of constructivism, intuitionistic mathematics and the propositions as types paradigm: for instance constructively a proof of an existential quantification $\underset{x\in X}{\exists} \phi(x)$ consists of constructing a specific $x \in X$ and a proof of $\phi(x)$, which “realizes” the truth of the statement, whence the name (e.g. Vermeeren 09, section 1).

added to *Kleene’s second algebra* under “Properties” the sentence:

]]>Kleeen’s second algebra is an abstraction of function realizability introduced for the purpose of extracting computational content from proofs in intuitionistic analysis. (e.g. Streicher 07, p. 17)

just in case you are watching the logs and are wondering:

I think we should have another “floating table of contents” for collecting the topic cluster

*Constructivism, Realizability, Computability*

so I am starting one at *constructivism - contents* and am including it into relevant entries.

But right now there is nothing much there yet. This is going to be expanded.

]]>just so that there are (cross-)links to them, I have created brief stub entries on some linear connectives:

and we already talked about

]]>From reading Kock's book "Synthetic differential geometry" and seeing how he introduces axiom after another and seeing the care he takes to inform the reader which axiom he is using in which section, it would seem to me that synthetic differential geometry is a syntactic way of doing geometry. In a later part his book, Kock them introduces models of this geometry. As such, analytic differential geometry appears to be our original semantics of his theory.

The theory of synthetic differential geometry appears to be a Rusellian syntactical crystallization from philosophers of real mathematics, made after careful observation of the manner in which differential geometers create arguments about their original model. ]]>

I felt that we had too many gray links to *metalanguage*, so I gave it a try. But I don’t really have the leisure for it now and not the expertise anyway. Experts please feel invited to take apart what I wrote there and replace with it something better.

Bas Spitters had mentioned the following article on the HoTT list. While I suppose the conclusion has to be taken with several grains of salt, I found this discussion interesting and illuminating, and have added it now to the references at *foundations of mathematics*:

Freek Wiedijk,

*Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics*(pdf)**Abstract**This paper presents Automath encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church’s higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo’s extended calculus of constructions, and Martin-Löf predicative type theory) and one foundation based on category theory. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf’s type theory.