Questions tagged [intuitionism]
The intuitionism tag has no summary.
69 questions
5
votes
0
answers
82
views
Constructive status of the meta-theory of intuitionistic propositional logic
Intuitionistic propositional logic has several kinds of models. Bezhanishvili and Holliday [1] showed that these models form a neat hierarchy:
Kripke
Beth
Topological
Dragalin
Heyting
in the order ...
- 150
5
votes
1
answer
353
views
References on computability and intuitionism
I'm not sure if my question makes sense, but I'm currently studying computability theory, and intuitionistic logic is something that really interests me. My question is, are there any current research ...
- 229
1
vote
0
answers
251
views
Recursive pointfree approach to algebraic topology
$\newcommand\seq[1]{\langle#1\rangle}$A large number of important topological results require simplicial-algebraic machinery (or comparable) to prove. This machinery is ingenious, impressively so even,...
- 1,739
1
vote
0
answers
122
views
Theorem 2 of Esakia's "Topological Kripke Models"
A closure algebra is a Boolean algebra $B$ with a $\vee$-preserving closure operator $\bf C$ that sends $0$ to $0$. A Heyting algebra is a lattice $H$ with a $0$ and a binary operation $\rightarrow$ ...
- 1,979
3
votes
1
answer
244
views
Theorem 1 of Esakia's "Topological Kripke Models"
Preliminaries
A Stone space is defined to be a compact Hausdorff space with a basis consisting of clopen sets. Let $X$ be a Stone space with a binary relation $R$ that is reflexive and transitive. A ...
- 1,979
7
votes
1
answer
324
views
$\mathit{RCA}_0$ without the law of the excluded middle
$\newcommand\name{\mathit}$In Classical Reverse Mathematics, the most famous base theory is $\name{RCA}_0$. I want to work in the area of formal Constructive Reverse Mathematics. I wonder if "$\...
- 1,361
8
votes
2
answers
675
views
Is there a more abstract or unified way to write the modulus condition in constructive definitions of real numbers?
I'm a beginner in constructive mathematics, and while studying different definitions of real numbers, I came across three sources that seem to describe equivalent notions of Cauchy reals:
The first ...
- 83
7
votes
1
answer
388
views
Does a special property hold if the Archimedean property for reals doesn't hold?
Suppose $\mathbb{R}^e=A \cup B$ in which $A \cap B=\varnothing$ and there exist real numbers $a_0$ and $b_0$ such that $a_0 \in A$ and $b_0 \in B$. My question is, can we construct $a \in A$ and $b \...
- 1,361
1
vote
0
answers
118
views
How many constant symbols can a set of intuitionistic formulas have for completeness to hold?
Fitting proves a version of the completeness theorem for intuitionistic FOL in his book on intuitionistic model theory and forcing.
Let $U$ be any set of formulas without parameters (i.e. constant ...
- 169
9
votes
1
answer
464
views
Does the decomposability of $\mathbb{R}$ imply analytic LLPO?
By "BISH" I mean constructive mathematics without axiom of countable choice.
By $\mathbb{R}^f$ I mean real numbers as fundamental sequences of rational numbers and by $\mathbb{R}^d$ I mean ...
- 1,361
3
votes
0
answers
316
views
Intuitionistic set-theoretic geology
Work in ZF, if there are proper class many supercompact cardinals, then all grounds are uniformly definable. Hence under reasonable assumption, we can have choiceless set-theoretic geology.
But can we ...
- 1,523
4
votes
0
answers
257
views
Examples of Grothendieck ($\infty$-)topoi which do / do not satisfy the law of excluded middle
I would like to create a big list of Grothendieck topoi (or Grothendieck $\infty$-topoi) which do / do not satisfy the law of excluded middle. That is, let’s list some examples of topoi whose internal ...
8
votes
2
answers
647
views
Whether the pure implicational fragment of intuitionistic propositional logic is a finitely-many valued logic
Gödel (1932) showed that intuitionistic propositional logic (more precisely, any fragment with implication and disjunction) is not a finitely many-valued logic. What about the pure implicational ...
- 83
0
votes
0
answers
94
views
two different intermediate logics whose intersection is Int
Call a partial order $\mathcal{F}=(F, \leq)$ rooted if there is an element $a \in F$ such that for any $b \in F$, $a\leq b$.
Let $\mathcal{F}_0$ and $\mathcal{F}_1$ be two different finite rooted ...
- 47
6
votes
1
answer
308
views
Electronic copy of Glivenko, ‘Sur quelque points de la logique de M. Brouwer’
Glivenko is cited i.a. in the SEP:
Glivenko, V., 1929, “Sur quelques points de la logique de M. Brouwer,” Académie Royale de Belgique, Bulletins de la classe des sciences, 5 (15): 183–188.
I’m ...
- 111