Questions tagged [intuitionism]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
7 votes
2 answers
479 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 ...
sai's user avatar
  • 73
0 votes
0 answers
54 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 ...
4869's user avatar
  • 47
5 votes
1 answer
159 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 ...
wolvercote's user avatar
2 votes
0 answers
174 views

Reference request for a modification of Bi-Intuitionistic Logic

I’ve asked this same question on math.stackexchange.com, but haven’t received any answers. I ask this question in good faith, so I hope it meets this site’s standards. I have been spending the better ...
PW_246's user avatar
  • 184
12 votes
0 answers
156 views

Limits in free cocompletion, constructively

Classically, if a locally small category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits. But all proof I know of that result ...
Simon Henry's user avatar
  • 39.9k
20 votes
4 answers
2k views

Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?

Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He ...
Anon's user avatar
  • 405
6 votes
1 answer
197 views

Preserve validity between the two Kripke frames

The background of our discussion is intuitionistic logic, i.e. the following definitions are intuitionistic Kripke frame. For $n \geq 1$, let $\mathcal{C}_n$ denote the frame which is shown in Fig.1. ...
mahu's user avatar
  • 63
9 votes
0 answers
143 views

Are there good criteria for the topological models where BD-N and BD hold?

A (non-empty/inhabited) subset $S$ of $\mathbb{N}$ is said to be pseudo-bounded if for every sequence $x_n$ in $S$ we have $\lim_{n\to \infty} \frac{x_n}{n} = 0$ Clearly all bounded subsets are pseudo-...
saolof's user avatar
  • 1,823
6 votes
1 answer
161 views

Variable elimination for propositional formulas in Heyting algebras

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, \...
Gro-Tsen's user avatar
  • 29.8k
1 vote
0 answers
73 views

Proof of the Local Deduction Theorem, for one of many logics

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 \...
Martín S's user avatar
  • 421
2 votes
1 answer
455 views

The LNC as a mathematical theorem

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 ...
Kristian Berry's user avatar
7 votes
1 answer
291 views

In CZF (w/ Subset Collection removed) the Powerset axiom Implies Subset Collection

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)) \...
ToucanIan's user avatar
  • 391
4 votes
0 answers
91 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 ...
Beau Madison Mount's user avatar
5 votes
1 answer
163 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 \...
Jordan Mitchell Barrett's user avatar
3 votes
1 answer
295 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)) \...
ToucanIan's user avatar
  • 391
4 votes
0 answers
312 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 ...
ToucanIan's user avatar
  • 391
5 votes
1 answer
435 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 $...
ToucanIan's user avatar
  • 391
10 votes
1 answer
1k 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 ...
user347155's user avatar
2 votes
0 answers
139 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 ...
ToucanIan's user avatar
  • 391
7 votes
3 answers
590 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 ...
ToucanIan's user avatar
  • 391
34 votes
3 answers
4k 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 ...
Colin Tan's user avatar
  • 251
0 votes
0 answers
128 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 ...
Robert Passmann's user avatar
16 votes
3 answers
1k 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&...
ttbo's user avatar
  • 163
7 votes
0 answers
280 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 $\...
მამუკა ჯიბლაძე's user avatar
1 vote
1 answer
155 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 ...
Erik D's user avatar
  • 338
11 votes
1 answer
441 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 ...
Noah Schweber's user avatar
10 votes
1 answer
361 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 (...
Gro-Tsen's user avatar
  • 29.8k
10 votes
2 answers
1k 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 ...
Bruno Bentzen's user avatar
0 votes
1 answer
165 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 ...
user65526's user avatar
  • 629
0 votes
2 answers
208 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$". ...
Zuhair Al-Johar's user avatar
4 votes
1 answer
804 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 ...
Robin Saunders's user avatar
3 votes
1 answer
450 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\...
Thomas Klimpel's user avatar
3 votes
0 answers
132 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 ...
namsap's user avatar
  • 335
6 votes
0 answers
475 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; ...
Robin Saunders's user avatar
3 votes
1 answer
200 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}...
George Cherevichenko's user avatar
2 votes
1 answer
338 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 ...
user65526's user avatar
  • 629
3 votes
2 answers
317 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 ...
user65526's user avatar
  • 629
10 votes
2 answers
794 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 ...
Dmytro Taranovsky's user avatar
6 votes
1 answer
825 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\,\...
George Cherevichenko's user avatar
8 votes
1 answer
344 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.
Erfan Khaniki's user avatar
5 votes
0 answers
379 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 ...
Franka Waaldijk's user avatar
9 votes
3 answers
572 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 \; ...
Bob's user avatar
  • 476
22 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 ...
goblin GONE's user avatar
  • 3,693
10 votes
2 answers
420 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 ...
StudentType's user avatar
7 votes
1 answer
387 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 \...
Matteo's user avatar
  • 71
8 votes
2 answers
935 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 ...
StudentType's user avatar
13 votes
1 answer
661 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? ...
Erfan Khaniki's user avatar
22 votes
6 answers
3k 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, ...
მამუკა ჯიბლაძე's user avatar
8 votes
2 answers
868 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 ...
Thomas Klimpel's user avatar
9 votes
1 answer
1k 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 ...
user40276's user avatar
  • 2,199