# Tagged Questions

**4**

votes

**2**answers

188 views

### What is the status of the extreme value theorem in forms of constructive mathematics, such as Smooth Infinitesimal Analysis?

In certain intuitionistic frameworks the extreme value theorem cannot be proved. Depending on the exact framework, counterexamples can be constructed as well; see for example pp. 294-295 in
...

**0**

votes

**0**answers

94 views

### How to prove a Lefschetzesque principle for relative homology and absolute homology

Here is my conjecture:
If H is some homology theory from some abelian category A to some abelian category B, E is the class of all epimorphism in A, E' is some closed class of epimorphisms in A and ...

**2**

votes

**0**answers

112 views

### Preimages of accessible full subcategories

My question is ultimately about the model theory of $L_{\infty, \omega}$, but it is more convenient to phrase it in terms of category theory. Suppose I have finitely accessible categories ...

**16**

votes

**2**answers

450 views

### Internal logic of the topos of simplicial sets

I am looking for a closed statement (i.e. not depending on any parameter objects) which is true in the internal logic of the topos of simplicial sets, but is not an intuitionistic tautology. Ideally, ...

**3**

votes

**0**answers

142 views

### Equational theories determined by “identities without variables”

How to characterize equational theories $T$ which have the following property: for any two terms $t(x_1,...,x_n)$ and $t'(x_1,...,x_n)$ in the signature of $T$, if for any closed terms (i. e. terms ...

**5**

votes

**1**answer

157 views

### What do algebraic theories with strictly terminal trivial models look like?

By algebraic theory I mean one in the sense of Lawvere, i.e. a collection of finitary operations, including projections, together with a multi-composition satisfying the obvious axioms. (I believe ...

**2**

votes

**1**answer

241 views

### Expressive power of first-order category theory

Given the signature $\lbrace \mathsf{dom}, \mathsf{cod}, \mathsf{id},\circ \rbrace$ and the axioms of category theory – which are expressible in the signature's first-order (FO) language – ...

**12**

votes

**3**answers

580 views

### The interplay between certain aspects of interpretability, model theory and category theory

I have some questions about the interplay of interpretability, model theory and category theory. Since I had difficulties in finding literature or other helpful information about this topic, it would ...

**1**

vote

**3**answers

421 views

### Another adjoint pair: Definable sets and set-builder formulas

I see adjointness between the two concepts of "being a definable set" and "being a set-builder formula":
A set $X$ is definable when there is a formula $\phi(x)$ such that $X = \lbrace x : ...

**8**

votes

**1**answer

298 views

### Categorical Semantics for Second-Order Logics

I am currently doing some work using a categorical semantics of first-order logic. The specific semantics I am using is due to Andrew Pitts, as described in:
Categorical Logic, Andrew M. Pitts, ...

**1**

vote

**0**answers

149 views

### A question on definable categories

One way to define a category set-theoretically might be to give four $\in$-formulas (not sets!)
$$\begin{array}{rl}
\mathsf{O}(X)&\text{(“$X$ is an object”)}\\
\mathsf{M}(X,Y,z)&\text{(“$z$ ...

**6**

votes

**0**answers

226 views

### Is there Ultracoproduct-like construction for topological spaces in general?

In
http://arxiv.org/pdf/math/9704205.pdf
they define the ultracoproduct of a sequence of compact Hausdorff spaces, $\sum_\mathcal{U}X_i$ along an ultrafilter $\mathcal{U}$ as the Wallman-Frink ...

**5**

votes

**1**answer

178 views

### Adjoining an arrow to a CCC

I just started reading Lambek and Scott's book "Introduction to higher-order categorical logic".
Right now I am reading Part I, section 5 (Polynomial categories). They explain two ways of adjoining ...

**14**

votes

**1**answer

518 views

### On Joyal's completeness theorem for first order logic

In 1978, in a series of unpublished conferences in Montréal, A. Joyal announced a remarkable theorem that unified several completeness theorems for fragments of first order logic, as well as first ...

**1**

vote

**1**answer

249 views

### What is the analogue for the category of presheafs for complement toposes?

Complement Toposes are dual in a sense to (elementary) Toposes and are expected to have typed higher paraconsistent logic as its internal language (as dual intuitionistic logic is paraconsistent).
...

**2**

votes

**2**answers

225 views

### Further relation between monads and theories

This question want to be a follow up of the following question.
In that thread I was interested in understanding relation between various presentation of algebraic theories. In particular in Eduardo ...

**8**

votes

**3**answers

936 views

### Is there a categorical proof of Gödel's incompleteness theorem?

A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new ...

**3**

votes

**0**answers

158 views

### Is there a useful Galois connection between Languages and Grammars?

I've just beginning to learn logic and proof theory - and the following rather vague and perhaps ill-formed question occurred to me.
Given an alphabet it's straightforward to construct the Language, ...

**4**

votes

**1**answer

332 views

### Is there a nice characterisation of topoi with nice meta-logical properties?

First-order order classical logic with standard semantics has a proof theory: it is complete, sound and effective.
In higher order logic with standard semantics one cannot obtain a proof theory - ...

**14**

votes

**1**answer

660 views

### Lawvere's fixed point theorem and the Recursion Theorem

Building off of Qiaochu's comment on my answer to a previous mathoverflow question, I would like to know: can the Recursion Theorem, $$\forall e\exists k[\Phi_e\text{ is total }\implies ...

**9**

votes

**4**answers

680 views

### On the large cardinals foundations of categories

(This question was posted on math.SE over two weeks ago, but received no answer. I am therefore posting it here as well.)
It is well-known that there are difficulties in developing basic category ...

**8**

votes

**6**answers

1k views

### Intuitionistic logic as quantization of classical logic?

A classically trained mathematician is more likely to be familiar (at least anecdotally) with an area of mathematical physics such as deformation quantization than with Intuitionistic logic. It is ...

**8**

votes

**2**answers

830 views

### Categories of recursive functions

I have a couple of conjectures on recursive functions, that I feel must have been proved or refuted by someone else, but I don't know where to look. In short:
1. The primitive recursive functions ...

**11**

votes

**3**answers

2k views

### A “mother of all groups”? What kind of structures have “mother of all”s?

For ordered fields, we have a “mother of all ordered fields”, the surreal numbers $\mathbf{No}$, a proper-class “field” which includes (an isomorphic copy of) every other ordered field as a subfield. ...

**18**

votes

**2**answers

794 views

### What can be expressed in and proved with the internal logic of a topos?

The title of this post expresses what I really want, which is to learn how to wield the internal logic of a topos more effectively. However, to bring it down to earth, I'll ask a few basic questions ...

**0**

votes

**1**answer

174 views

### Poset axioms of Boolean algebra [closed]

I found in Awodey's "Theory Category", second edition p34, a set of poset axioms to define Boolean algebras, whereas I don't see how they can be sufficient.
Here are the axioms:
A Boolean algebra ...

**2**

votes

**2**answers

372 views

### Are exponentials in categorical models of linear logic harmful?

Categorical models for linear logic with $\otimes$, $1$, $\&$, $\top$, $\oplus$, $0$, and $\multimap$ are typically symmetric monoidal closed categories (for modeling $\otimes$, $1$, and ...

**2**

votes

**2**answers

117 views

### Adjoint of Pushout as Modal Operators in Internal Logic

Regarding the internalization of mathematics to a particular category as in the nLab article: Internal Logic, there is a peculiar table mentioned in the section on Categorical Semantics in which there ...

**3**

votes

**1**answer

188 views

### Completeness of a Theory from the Categorical Viewpoint

I am interested in a more specific reference or explanation of "the categorical view" explained in the article http://ncatlab.org/nlab/show/theory#CategoricalView. In particular, I am interested in ...

**14**

votes

**0**answers

352 views

### Relative consistency of ETCS over the theory of a well-pointed topos with NNO

Gödel's well-known proof of the implication $Con(ZF) \Rightarrow Con(ZFC)$ used the construction of the inner model $L$ in $ZF$ to get a model of $ZFC$ (and in fact much more). However such a ...

**9**

votes

**1**answer

509 views

### Finite order arithmetic and ETCS

I'm looking for a reference to the statement that Lawvere's Elementary Theory of the Category of Sets (ETCS) is equal in proof-theoretic strength to finite order arithmetic. The person who informed ...

**6**

votes

**2**answers

250 views

### A continuous notion of realizability

I have been interested in non-classical logics, off and on, for quite a while. This question is probably very basic, and I hope it is not too low-level for MO. My question stems from an attempt to ...

**2**

votes

**1**answer

165 views

### A categorical framework for Freiman s-morphisms

Let $\mathfrak A_i$ be groups ($i = 1, 2$), written multiplicatively, and $s$ a non-negative integer (here, as usual, I am abusing notation and denoting the operations of $\mathfrak A_1$ and ...

**3**

votes

**2**answers

244 views

### What categories correspond to the typed lambda calculus with parametric types?

the unadorned typed lambda calculus correspond to the closed cartesian categories, but if we add in dependent or parametric types how are they then characterised?

**3**

votes

**0**answers

313 views

### Groupoid interpretation of type theory

Hello,
I read the paper on groupoid interpretation of type theory by Hofmann and Streicher and I have a question. According to the authors $Tm([[\text{Set}\:[\Gamma]\: ]])$ is the same as ...

**7**

votes

**1**answer

246 views

### Monomorphisms from natural numbers objects into products.

Let $A$ and $B$ be objects in a topos $\mathcal{E}$ with natural numbers object $\mathbb{N}$. If there is a monomorphism $m: \mathbb{N}\rightarrow A\times B$, is it necessarily the case that there is ...

**9**

votes

**2**answers

562 views

### Category of Judgements?

I have been able to find a lot of information on the category of contexts -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar ...

**18**

votes

**4**answers

874 views

### There are two slightly different notions of ultraproduct. Why is one said to be better than the other?

Let $I$ be a set and $\mathcal{U}$ an ultrafilter on $I$. Let $(X_i)_{i \in I}$ be an $I$-indexed family of sets. The ultraproduct of the family $(X_i)$ with respect to $\mathcal{U}$ is, everyone ...

**5**

votes

**1**answer

348 views

### Resources-Aware Combinatorial Game Theory

First of all, I preemptively apologize if my question happens to be naive, I am no expert of CGT (or general game theory, for that matter).
Now the question:
**is there such a thing as the study of ...

**6**

votes

**0**answers

250 views

### Free CCC or topos on a cartesian category

$\def\sC{\mathcal{C}}\def\sD{\mathcal{D}}\def\Set{\mathbf{\mathrm{Set}}}\DeclareMathOperator{\Sub}{Sub}\def\op{\circ}$I have a Cartesian category $\sC$. I would like to embed $\sC$ into a cartesian ...

**5**

votes

**1**answer

521 views

### Topos Without point, from the point of view of logic.

Hello !
I am a little troubled by the following "paradox" :
Let $X$ be a non trivial (Grothendieck) Topos without point.
We want to look this situation from the point of view of logic, $X$ ...

**8**

votes

**4**answers

589 views

### Set-Theoretic Issues/Categories

It is a major bummer that one cannot strictly speaking talk about the category of all categories without saying "it is not really a category, since the morphisms between objects may form a class" and ...

**3**

votes

**2**answers

410 views

### NNO = (first order) PA

Recall the definition of a Natural Numbers Object in a topos, and the first order axioms for Peano Arithmetic. I am more familiar with the first definition than the second, so I cannot tell from the ...

**5**

votes

**0**answers

151 views

### What propositions about sets can be transfered to propositions about a presheaf category?

When I work with various presheaf categories, and I need some lemma, I often am able to prove the lemma by proving the analogous lemma for sets. As a simple example, let $f_i :X_i\hookrightarrow Y$ be ...

**21**

votes

**2**answers

1k views

### What is the theory of local rings and local ring homomorphisms?

It is well-known that the category of local rings and ring homomorphisms admits an axiomatisation in coherent logic. Explicitly, it is the coherent theory over the signature $0, 1, -, +, \times$ with ...

**6**

votes

**2**answers

272 views

### Why no morphisms from the contradictory proposition to the inconsistent context?

Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this question applies to ...

**1**

vote

**1**answer

670 views

### About logical axioms of propositional logic.

I see in th P . Johnstone little (but dense) book "Notes on logic and Sety theory" that propositional logical calculus as the follow three axioms:
1) $(p\Rightarrow (q\Rightarrow p)$
2) ...

**6**

votes

**0**answers

263 views

### What are these sets in Freyd's model?

Recall Freyd's model of $ZF +\neg AC$ (as recounted in MacLane and Moerdijk's book Sheaves in Geometry and Logic): it arises as the Fourman interpretation of the topos of sheaves on a particular ...

**8**

votes

**2**answers

389 views

### Categorical Brouwer-Heyting-Kolmogorov interpretation

Let $\mathcal{L}$ be the language of intuitionistic propositional logic generated by some atomic propositions $t_1, t_2, \ldots$. The Lindenbaum–Tarski algebra of $\mathcal{L}$ can be regarded as a ...

**2**

votes

**3**answers

277 views

### Can the 'linkages' between equivalent extensions of modules of an algebraic group be taken to have bounded length?

I have a conjecture concerning how "tightly" two equivalent $n$-fold extensions of modules over an algebraic group over a field might
be "linked". I suspect that the
question has been already ...