# Questions tagged [intuitionism]

The intuitionism tag has no usage guidance.

33
questions

**1**

vote

**1**answer

105 views

### Markov's principle from constant domain logic

I am looking for a proof of and/or a reference for the result that Markov's principle can be proved in the framework of constant domain logic. By constant domain logic, I mean intuitionistic logic ...

**9**

votes

**1**answer

283 views

### Computability-theoretic results relevant to realizability

This may be a very naive question which only reflects my failure at literature search, but:
Although realizability (in its original form at least) is grounded in computability, the details of ...

**9**

votes

**1**answer

294 views

### Fibers of the morphism from the free Heyting algebra to the free Boolean algebra

For $k\in\mathbb{N}$, let $H_k$ be the free Heyting algebra on $k$ variables $p_1,\ldots,p_k$ and $B_k$ be the free Boolean algebra on the same $k$ variables. Thus, $B_k$ has $2^{2^k}$ elements (...

**5**

votes

**2**answers

417 views

### Henkin-style completeness proofs for intuitionistic logic

Henkin-style completeness proofs are founded on a few basic presuppositions, such as the assumptions that the language of a logical theory must be enumerable (or at least that the axiom of choice ...

**0**

votes

**1**answer

106 views

### Superintuitionistic logics which are not hereditary/monotonic: impossible or possible?

An intuitionistic Kripke model is a triple $\langle W,\leq, \Vdash \rangle$, where $\langle W,\leq \rangle$ is a preordered Kripke frame, and
$\Vdash$ satisfies the following condition of ...

**0**

votes

**2**answers

154 views

### Are Regularity schema and $\in$-induction schema equivalent in intuitionistic logic?

In posting "Does Regularity schema imply $\in$-induction when added to first order Zermelo set theor?"
the answer was that they are equivalent in classical first order logic with membership "$\in$".
...

**3**

votes

**1**answer

528 views

### Going beyond the strength of Peano arithmetic “without sets”

First-order arithmetic is fairly weak, as measured for example by its consistency strength. When a stronger theory is desired, it is common to work with (fragments of) second-order arithmetic or set ...

**2**

votes

**1**answer

392 views

### Does cut elimination fail here?

Proving $\lnot\lnot(A\lor\lnot A)$ in intuitionistic sequent calculus with cut seems to be easy:
We use cut to prove $\lnot(A\lor\lnot A)\vdash \bot$ from $\lnot(A\lor\lnot A)\vdash \lnot A \land\lnot\...

**3**

votes

**0**answers

99 views

### A conservativity result of intuitionistic set theory over arithmetic

In their 1985 paper "Arithmetic Transfinite Induction and Recursive Well-Orderings", Friedman and Ščedrov prove that the theory $\mathbf{ZFI}$ is conservative over $\mathbf{HA}^*$ (see here, Theorem ...

**5**

votes

**1**answer

384 views

### Infinite-time Turing machines and the formal Church's thesis

Infinite-time Turing machines are known to either halt or loop in countable time.
In the spirit of double-negation translation, is there a statement which is: classically equivalent to this; ...

**3**

votes

**1**answer

171 views

### Fixed-point property and $T_0$ separation property

Each topological space $A$ with fixed-point property is $T_0$ space. Proof: suppose, two different points $a_1$ and $a_2$ belong to the same open subsets of $A$. Then the function
$$f(a)=
\begin{cases}...

**2**

votes

**1**answer

212 views

### Can we avoid the modal collapse in a certain Intuitionistic modal logic by abandoning ¬◯⊥ but retaining the law of the excluded middle?

Consider Propositional Lax Logic ($PLL$)
https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf
The Hilbert system of $PLL$ takes as axiom ...

**2**

votes

**1**answer

156 views

### Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic

Consider Propositional Lax Logic ($PLL$)
https://www.uni-bamberg.de/fileadmin/uni/fakultaeten/wiai_professuren/grundlagen_informatik/papersMM/pll.pdf
The Hilbert system of $PLL$ takes as axiom ...

**10**

votes

**2**answers

620 views

### Adding nonconstructive disjunction to intuitionistic logic

In constructive mathematics, under realizability interpretations, we can define nonconstructive disjunction $A⅋B$ as follows:
A witness for $A⅋B$ gives a candidate witness for $A$ and a candidate ...

**6**

votes

**1**answer

757 views

### Rice's theorem in type theory

From the formula
$$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$
we can get the scheme
$$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\...

**6**

votes

**1**answer

263 views

### Forcing in Constructive Set Theories

I searched on the internet, but I could not find anything useful about applications of forcing in constructive set theories.
Are there any developments of forcing in CZF or IZF?
Thanks in advance.

**5**

votes

**0**answers

334 views

### Did Kleene constructively prove Brouwer's axioms?

Harvey Friedman's request on the FoM-forum for an overview of current intuitionistic foundations revived the following question, which I have been meaning to ask for five years. (I'm no expert on ...

**9**

votes

**2**answers

391 views

### Admissibility of Harrop's rule, computationally

It is obvious that the following formula is not a theorem of
intuitionistic propositional calculus (IPC).
$$
(\neg A \; \to \; B \vee C) \;\; \to \;\;
((\neg A \; \to \; B) \vee (\neg A \; \to \; ...

**19**

votes

**3**answers

2k views

### Why would the category of sets be intuitionistic?

This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order ...

**10**

votes

**2**answers

363 views

### Why is the notion of algorithm a primitive one in Brouwer's intuitionism?

I've seen several times people mentioning that the notion of an algorithm / a computation is taken as a primitive notion in L. E. J. Brouwer's intuitionism. For instance, in Varieties of Constructive ...

**6**

votes

**1**answer

283 views

### Pure first order logic formulations of Markov's principle

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate:
$\neg \neg \exists x P \to \...

**7**

votes

**2**answers

715 views

### Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

In the opening passage of Martin-Löf's (1975) he famously says that
"the theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic ...

**12**

votes

**1**answer

543 views

### Intutionistic Robinson Arithmetic

By Friedman translation $HA$ and $PA$ prove the same $\Pi_2$ formulas.
Is it true for Intutionistic Robinson arithmetic(Robinson axioms with intutionistic logic) and classic Robinson arithmetic?
...

**21**

votes

**6**answers

2k views

### How strong is Cantor-Bernstein-Schröder?

There are several questions here on MO about the Cantor-Bernstein-Schröder ((C)BS) theorem, but I could not find answers to what arose to me recently.
Although I don't think I need to recall it here, ...

**8**

votes

**2**answers

743 views

### Did Bishop, Heyting or Brouwer take partial functions seriously?

The partial μ-recursive functions which may or may not be provably total seem to have some direct relation to the initial motivations for intuitionistic mathematics. (Following Kronecker, one ...

**8**

votes

**1**answer

852 views

### Forcing is intuitionistic

The main idea of why it´s necessary a generic filter $G$ to extend a countable transitive $\epsilon$-interpretation (not necessarily a model) $M$ is given by the condition (for which $G$ being a ...

**6**

votes

**3**answers

434 views

### Models of intuitionistic linear logic that reflect the resource interpretation

I am interested in models of intuitionistic linear logic, that is, the logic that you get if you take classical linear logic and restrict the set of operators to $\otimes$, $1$, $\multimap$, $\times$, ...

**18**

votes

**3**answers

2k views

### Is there a probability theory developed in intuitionistic logic?

Since Boole it is known that probability theory is closely related to logic.
According to the axioms of Kolmogorov, probability theory is formulated with a (normalized)
probability measure $\mbox{...

**10**

votes

**6**answers

2k 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

**1**answer

573 views

### Multiplication of Cauchy and Dedekind real numbers

In Michael Dummett's book "Elements of Intuitionism", the product of real numbers is defined as follow:
$x\cdot y= \{ \langle r_n\rangle \cdot \langle s_n\rangle$ | $\langle r_n\rangle\in x , \langle ...

**0**

votes

**1**answer

356 views

### A question on intuitionistic propositional logic [closed]

One week ago, I asked a question on math.stackexchange.com (https://math.stackexchange.com/questions/209120/a-question-on-intuitionistc-propositional-logic). But nobody answered my question. So I ...

**4**

votes

**3**answers

574 views

### What is the proper name for “compact closed” multiplicative intuitionistic linear logic?

Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed ...

**11**

votes

**4**answers

2k views

### intuitionistic interpretation of classical logic

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic ...