2
votes
0answers
102 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
382 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
127 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
143 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
227 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 – ...
11
votes
3answers
554 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
378 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
276 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
148 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
214 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
175 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 ...
13
votes
1answer
487 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
240 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
180 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 ...
6
votes
3answers
861 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
153 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
320 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
603 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 ...
8
votes
4answers
660 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 ...
7
votes
2answers
765 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 ...
10
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
746 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
160 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
352 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
112 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
185 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 ...
13
votes
0answers
344 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
1answer
503 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
248 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
224 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?
2
votes
0answers
295 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
239 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
551 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
852 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
342 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
247 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
504 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
587 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
394 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
149 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 ...
20
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
270 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
643 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
258 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
386 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
275 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 ...
4
votes
5answers
612 views

Union of a object (a set) in the Elementary Theory of the Category of Sets

I see the Todd Trimble article "Elementary Theory of the Category of Sets" on catlab. I ask: how make (in the categorical setting) the usual union of a set $\cup X=${$y |\exists x\in X: y\in x$}? ...
5
votes
2answers
465 views

Forcing the nonexistence of a certain set

I have a certain set-theoretic axiom (WISC) which follows from Choice (this is a nuking a fly BTW), but which I suspect is independent of ZF. To show this I need to show that a certain set does not ...