4
votes
2answers
201 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
0answers
95 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
0answers
113 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
2answers
461 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
0answers
143 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
1answer
158 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
1answer
245 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
3answers
589 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
3answers
426 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
1answer
305 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
0answers
151 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
0answers
228 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
1answer
179 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
1answer
525 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
1answer
251 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
2answers
236 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 ...
10
votes
3answers
1k 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
0answers
160 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
1answer
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
1answer
675 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
4answers
685 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
6answers
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
2answers
916 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
3answers
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
2answers
804 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
1answer
175 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
2answers
373 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
2answers
137 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
1answer
190 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 ...
15
votes
0answers
405 views

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

EDIT: I'm bumping this, because I'm still curious, and because I have a relative consistency result over the theory of a well-pointed topos with NNO, and I am wondering how much baggage I save by not ...
9
votes
1answer
510 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
2answers
293 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
1answer
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
2answers
247 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
0answers
314 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
1answer
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
2answers
563 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
4answers
882 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
1answer
355 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
0answers
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
1answer
524 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
4answers
590 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
2answers
411 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
0answers
152 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
2answers
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
2answers
273 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
1answer
676 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
0answers
265 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
2answers
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
3answers
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 ...