30
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
I think we can assume MLTT is a formal system of the usual kind. Therefore, in formal arithmetic using Gödel numbering we can formulate the arithemetic statement con(MLTT), stating the consistency of ...
- 309
29
votes
Accepted
Formalizations of the idea that something is a function of something else?
First of all, it seems to me as though the real question here is "what is a variable quantity?" Most of the definitions you quote from pre-20th century mathematicians assume that the notion of "...
- 66.7k
25
votes
Applications of Categorical Logic to Logic
There are plenty of applications of categorical logic to understanding of logic itself, including some which provide unexpected connections and insights. It is just not true that no real theory has ...
- 5,902
23
votes
Two interpretations of implication in categorical logic?
There are two concepts here, which are tightly connected. Logically, this corresponds to the distinction between $\vdash$ and $\Rightarrow$.
(A) Morphisms $t : \Gamma \to A$ represent (well-formed, ...
- 10.6k
21
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
There is a generalization of Gödel's incompleteness theorem that is more naturally applicable to MLTT: Löb's theorem says that to prove $P$, it suffices to prove that $P$ is true whenever $P$ is ...
- 695
21
votes
Accepted
Precise relationship between elementary and Grothendieck toposes?
There are known statements that are true in any Grothendieck topos, but not in every elementary topos with NNO. For instance:
Freyd's theorem that a complete small category is a preorder is not ...
- 66.7k
17
votes
Internal logic of the topos of simplicial sets
I will augment François Dorais’s answer with an exact identification of the propositional logic.
Let $D_n$ be the free distributive lattice with a top, considered as a finite Heyting algebra. ...
- 47.1k
17
votes
Accepted
Does foundation/regularity have any categorical/structural consequences, in ZF?
Yes, the axiom of foundation has structuralist consequences.
Let $\phi$ be the assertion, "if every well-founded set is well-orderable, then every set is well-orderable."
This statement, I claim, ...
- 236k
16
votes
Accepted
What does the topos of (light) condensed sets classify?
The topos of light condensed sets is generated by the Cantor set $\Delta = \prod_{\mathbb N} \{0,1\}$. So it classifies "Cantor space objects". Here is what this gives, essentially ...
- 21.3k
15
votes
Accepted
Proof assistant for working in weaker foundations?
One possibility that's worth thinking about is to use a "meta-proof-assistant" like Twelf, which implements a meta-theoretic logical framework inside of which you can specify any "object language" you ...
- 66.7k
14
votes
Applications of Categorical Logic to Logic
I hesitated a lot before writing this answer, because I feel that the current question ("Is there any hard logic conjecture that has been proven by using categories?") hinges on how one ...
- 756
13
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
Maria Emilia Maietti starts her http://www.sciencedirect.com/science/article/pii/S1571066104805693 by saying that "André Joyal constructed arithmetic universes to provide a categorical proof of ...
- 179
12
votes
Formalizations of the idea that something is a function of something else?
The situation here seems very analogous to that in probability, where there is also a state space $\Omega$ (which is the underlying set of a probability space $(\Omega, {\mathcal B}, {\bf P})$) which ...
- 114k
11
votes
Accepted
Free models of finitely presented essentially algebraic theories in elementary toposes?
If you are willing to accept internal argument instead of purely categorical (external) one, a very good reference for this is Palmgren and Vickers' paper: " Partial Horn Logic and cartesian ...
- 42.4k
11
votes
Accepted
Brouwer's Theorem in the free topos?
To summarize, the Lambek and Scott book actually says that functions on the reals in the free topos represent continuous functions. The nLab previously made the stronger claim that Brouwer's Theorem ...
11
votes
Accepted
Images of complemented subobjects in toposes
No, not even if $E=S$, $f$ is the identity morphism, and $x=1$. In that special case, your question asks whether $\forall z\in s\,\big((z\in u)\lor \neg(z\in u)\big)$ (in the internal language of $S$) ...
- 73.1k
11
votes
Accepted
Equivalence between geometric theories and frames internal to the free topos
Simon essentially answered the question already, but I will expand some of the parts that may not be clear to the experts. Sketches of an elephant is a good reference for everything I am going to say.
...
- 9,111
11
votes
Accepted
Ultracategories with one object
$\newcommand{\cat}{\mathrm}
\newcommand{\St}{\cat{Stone}^\cat{fr}}
\newcommand{\Cat}{\cat{Cat}}
\newcommand{\Cart}{\cat{Cart}}
\newcommand{\Fun}{\cat{Fun}}
\newcommand{\Mon}{\cat{Mon}}
\newcommand{\...
- 15.8k
10
votes
Equivalence between geometric theories and frames internal to the free topos
When you think about it the right way the idea is fairly simple :
Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one ...
- 42.4k
10
votes
Accepted
Are flat functors out of a finite category necessarily finite?
A positive answer to your first question can be seen as a consequence of Lemma 2.5 of On continuity of accessible functors.
Following the notation of the Lemma, you should take $\beta$ to be the ...
- 499
9
votes
How do we construct the Gödel’s sentence in Martin-Löf type theory?
I am a little bit rusty on the subject so I hope whatever I am going to say is correct (otherwise someone else will possibly correct me and I'll learn something :) ).
Before I start allow me to ...
- 3,349
9
votes
Two interpretations of implication in categorical logic?
The answers of varkor and Dmitri explain that in a given category, entailment corresponds to external homsets while implication corresponds to internal-homs. However, there's another thing going on ...
- 66.7k
9
votes
Accepted
Universal property of the codomain fibration
First a note about terminology: older literature sometimes uses the term "cofibration" for a functor $p:E\to B$ such that $p^{\rm op} : E^{\rm op} \to B^{\rm op}$ is a fibration, but it's ...
- 66.7k
8
votes
Accepted
Set-theoretical multiverses and their representation as functors? Why *the* multiverse?
Of course we have been investigating a wide variety of
multiverse concepts, and in this sense, yes, we have not just one,
but many, multiverses.
But to be sure, much of this multiverse analysis has ...
- 236k
8
votes
Does foundation/regularity have any categorical/structural consequences, in ZF?
The following provides an "engine" for generating many structural statements provable in ZF but not in ZF without foundation:
Theorem. Let $S$ be any structural equivalent of the axiom of ...
- 17.7k
8
votes
Grothendieck toposes and logic
Barr's classical result (that a Grothendieck topos admits a surjective morphism from the topos of sheaves on a Boolean algebra), besides helping in the proof of Deligne's theorem as mentioned in the ...
- 5,902
7
votes
Accepted
Diagrams in an Elementary Topos
If $E$ is small complete, then $[I, E]$ is an elementary topos, by the following argument.
If $I_0$ is the discrete category of objects of $I$, then $[I_0, E]$ is just an $I_0$-indexed product of ...
- 53.3k
7
votes
Brouwer's Theorem in the free topos?
Dear All: you must be precise on what you mean by Brouwer's theorem. The free topos is closed under many rules, but unlike the realizability topos, it is seldom closed under the internal implicative ...
- 71
7
votes
Precise relationship between elementary and Grothendieck toposes?
Regarding the bullet point list of questions at the end, I believe that every true $\Pi^0_1$-sentence holds in the internal logic of any Grothendieck topos, so in that case $T_{\mathbf{GrTop}}$ is ...
- 4,378
7
votes
Two interpretations of implication in categorical logic?
Morphisms A→B form a set (typically denoted by C(A,B) or hom(A,B)), whereas the internal hom Hom(A,B) is an object in the same category C.
A morphism A→B corresponds to the entailment A⊢B,
whereas the ...
- 37.8k
Only top scored, non community-wiki answers of a minimum length are eligible