# Questions tagged [intuitionism]

The intuitionism tag has no usage guidance.

The intuitionism tag has no usage guidance.

49
questions

5
votes

1
answer

101
views

By an (intuitionistic) propositional formula $\varphi(x_1,\ldots,x_n)$ I mean a formula built up from a (finite) number of variables $x_1,\ldots,x_n$ using connectors $\top, \bot, \land, \lor, \...

1
vote

0
answers

66
views

I'm looking for a proof of the Local Deduction Theorem for any one of many logics. That is, a proof of the statement:
$\Sigma \cup \{\phi\} \models \psi$ iff for some positive $n,$ $\Sigma \models \...

0
votes

1
answer

355
views

One of the most intriguing things I've read about over the last few years is Diaconescu's theorem, which says that, in some forms of constructivist/intuitionistic set theory, even if the law of the ...

7
votes

1
answer

281
views

The Subset Collection axiom:
$$ \forall a \forall b \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longrightarrow \exists d \in c (\forall x \in a \exists y \in d (\psi(x,y,u)) \...

4
votes

0
answers

77
views

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

146
views

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

237
views

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)) \...

4
votes

0
answers

228
views

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

377
views

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

10
votes

1
answer

945
views

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

116
views

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

6
votes

3
answers

398
views

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

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

108
views

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

15
votes

3
answers

893
views

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

269
views

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

139
views

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

396
views

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

336
views

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

10
votes

2
answers

847
views

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

146
views

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

190
views

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

657
views

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

427
views

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

126
views

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

445
views

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

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

296
views

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

3
votes

2
answers

273
views

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

709
views

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

797
views

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

317
views

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

354
views

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

474
views

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 \; ...

21
votes

3
answers

2k
views

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

402
views

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

349
views

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

843
views

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

621
views

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

3k
views

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

803
views

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

9
votes

1
answer

1k
views

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

8
votes

3
answers

511
views

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

23
votes

3
answers

3k
views

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

13
votes

6
answers

2k
views

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

664
views

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

374
views

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

636
views

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

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