Search Results
Search type | Search syntax |
---|---|
Tags | [tag] |
Exact | "words here" |
Author |
user:1234 user:me (yours) |
Score |
score:3 (3+) score:0 (none) |
Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
Views | views:250 |
Code | code:"if (foo != bar)" |
Sections |
title:apples body:"apples oranges" |
URL | url:"*.example.com" |
Saves | in:saves |
Status |
closed:yes duplicate:no migrated:no wiki:no |
Types |
is:question is:answer |
Exclude |
-[tag] -apples |
For more details on advanced search visit our help page |
Constructive mathematics in the style of Bishop, including its semantics using realizabilty or topological methods.
16
votes
Accepted
Locales as spaces of ideal/imaginary points
I can only answer some of your questions.
Yes, the Zariski locale is extensively studied. It's one of the ways of setting up scheme theory in a constructive context: Don't define schemes as locally r …
13
votes
1
answer
626
views
Constructively correct notion of unique factorization domain
Recall the well-known proof that a unique factorization domain is a GCD domain:
Let $x, y \in R \setminus \{ 0 \}$. Factor $x$ and $y$ into pairwise non-associated irreducible elements: $$\begin{a …
12
votes
Tight apartness relations in toposes
I'm not precisely sure what you're looking for. Here is an example for the external interpretation of an apartness relation:
Recall that the object of Dedekind reals $\mathbb{R}$ in a sheaf topos $\m …
11
votes
Accepted
Constructive proof that a kernel consists of nilpotent elements
This answer provides a scheme how to construct a constructive proof, though I'm still working to actually explicitly extract the constructive proof, so please don't accept the answer just yet. (Update …
9
votes
0
answers
374
views
Reflection principle for intuitionistic Zermelo–Fraenkel?
The well-known reflection principle for classical Zermelo–Fraenkel states:
For any formula $\varphi(x_1,\ldots,x_n)$ of the language of ZFC with free variables $x_1,\ldots,x_n$, ZFC proves
$$ \f …
7
votes
2
answers
1k
views
Explaining the consistency of PRA and ZF from predicative foundations
Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory.
From the point of view of a predicative foundation to …
6
votes
Constructively, is the unit of the “free abelian group” monad on sets injective?
Yes! Here is a proof which is slightly different from both your proof and the proof in Mines–Richman–Ruitenberg.
First define the similarity relation on $\mathrm{List}(R \times X)$ as in Mines–Richma …
5
votes
What does overtness mean for metric spaces?
The spectrum of a commutative ring, defined as the classifying locale of its prime filters, is overt if and only if any element is nilpotent or not nilpotent (Proposition 12.51 in these notes of mine) …
4
votes
constructive Serre classes
Any subclass $\mathcal{C}$ of an abelian category determines a smallest Serre class containing it, by iteratively adding (the zero object and) the object $Y$ for any exact sequence $X \to Y \to Z$ whe …
4
votes
Pure first order logic formulations of Markov's principle
This is not an answer to the question, but rather a comment which benefits from proper formatting.
For me personally, Markov's principle is specifically associated with the natural numbers and not wi …
3
votes
Explaining the consistency of PRA and ZF from predicative foundations
Last week, I learned from Ulrik Buchholtz that there are proof-theoretic reductions from certain impredicative systems to certain predicative ones. While these fall short of predicatively explaining t …