# Questions tagged [intuitionism]

The intuitionism tag has no usage guidance.

45
questions

**3**

votes

**0**answers

57 views

### Negation-quantifier-negation blocks in nonclassical logic: reference request

I'm looking for references to discussion of a certain question in the literature on non-classical first-order logics. I suspect it must have been investigated thoroughly, but I can't seem to find ...

**5**

votes

**1**answer

125 views

### Possible values of "Kripke rank" for formulae in IPL

Fix a (countable) set $\mathcal{P}$ of atomic propositional variables. Recall a Kripke model $\mathcal{K}$ for intuitionistic propositional logic (IPL) consists of:
A preorder $(W,\leq)$
For each $w \...

**3**

votes

**1**answer

205 views

### Subset Collection axiom

In Constructive Set Theory (CZF) the Power Set axiom is replaced with the Subset Collection axiom which I will state here:
$$ \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \...

**3**

votes

**0**answers

167 views

### Is intuitionistic predicate logic (semantically) complete or incomplete?

According to Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (https://archive.org/details/constructivismin0002troe/page/718/mode/2up) it is proven in an intuitionisitc ...

**4**

votes

**1**answer

357 views

### How do working constructivists get by with out the zero product property?

It is stated by Douglas Bridges in Constructive mathematics: a foundation for computable analysis that the following property, which I will call the zero product property:
If $x,y \in \mathbb{R}$ and $...

**9**

votes

**1**answer

822 views

### Why are W-types called "W"?

Why are W-types called "W"?
Probably "W" means either "wellordered" or "wellfounded". (Martin-Löf uses the term "wellorder".) But these are notions ...

**2**

votes

**0**answers

101 views

### In a constructive order/lattice theory are the arbitrary join and the weak suprema the same?

For a poset $X$ we define an upperbound $w \in X$ of a subset $S \subseteq X$ to be a weak-supremum if
$(\forall a \in S (a \leq b)) \implies w \leq b$.
While a supremum is defined more carefully (in ...

**5**

votes

**3**answers

334 views

### Is there a completeness proof of intuitionistic predicate calculus using Heyting algebra semantics that is inuitionistically valid?

According to godelian in Henkin-style completeness proofs for intuitionistic logic there are multiple intuitionstically valid proofs of the completeness of inuitionistic predicate calculus (IPC) via ...

**32**

votes

**3**answers

3k views

### Alternatives to the law of the excluded middle

As a sentential logic, intuitionistic logic plus the law of the excluded middle gives classical logic.
Is there a logical law that is consistent with intuitionistic logic but inconsistent with ...

**0**

votes

**0**answers

95 views

### Where does intuitionistic predicate logic live in the arithmetical hierarchy?

I started reading Plisko's papers on arithmetic complexity on the arithmetic complexity of constructive logic (see for example here or here). In this context, I started wondering about the following ...

**13**

votes

**3**answers

767 views

### Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?

One can study the standard semantics of classical propositional logic within classical logic set theory, so we can say that the semantics of classical logic is meta-theoretically "self-hosting&...

**7**

votes

**0**answers

250 views

### Two simple cases of quantifier elimination for Heyting algebras

This extracts a simple case from a cross-post at cs.SE.
Here is a fact about Intuitionistic Propositional Logic:
A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\...

**1**

vote

**1**answer

125 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 ...

**10**

votes

**1**answer

323 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 ...

**10**

votes

**1**answer

319 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 (...

**8**

votes

**2**answers

686 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

134 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

176 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

610 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 ...

**3**

votes

**1**answer

411 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

115 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 ...

**6**

votes

**1**answer

419 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

180 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

279 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

198 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

677 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

780 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\,\...

**8**

votes

**1**answer

297 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

347 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

424 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

385 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 ...

**7**

votes

**1**answer

332 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

798 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 ...

**13**

votes

**1**answer

579 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

785 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

980 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 ...

**7**

votes

**3**answers

461 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$, ...

**22**

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{...

**12**

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

608 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

367 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

614 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

3k 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 ...