Questions tagged [intuitionism]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
5 votes
1 answer
101 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, \...
  • 23.7k
1 vote
0 answers
66 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 \...
  • 401
0 votes
1 answer
355 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 ...
7 votes
1 answer
281 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)) \...
  • 371
4 votes
0 answers
77 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
146 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
237 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)) \...
  • 371
4 votes
0 answers
228 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 ...
  • 371
4 votes
1 answer
377 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 $...
  • 371
10 votes
1 answer
945 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
116 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 ...
  • 371
6 votes
3 answers
398 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 ...
  • 371
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 ...
  • 507
0 votes
0 answers
108 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 ...
15 votes
3 answers
893 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&...
  • 153
7 votes
0 answers
269 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
139 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 ...
  • 338
10 votes
1 answer
396 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
336 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 (...
  • 23.7k
10 votes
2 answers
847 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
146 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 ...
  • 619
0 votes
2 answers
190 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
657 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
427 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
126 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 ...
  • 335
6 votes
1 answer
445 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
296 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 ...
  • 619
3 votes
2 answers
273 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 ...
  • 619
10 votes
2 answers
709 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
797 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
317 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
354 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
474 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 \; ...
  • 413
21 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 ...
  • 3,523
10 votes
2 answers
402 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
349 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 \...
  • 71
7 votes
2 answers
843 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
621 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
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, ...
8 votes
2 answers
803 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 ...
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 ...
  • 2,129
8 votes
3 answers
511 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$, ...
23 votes
3 answers
3k 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{...
  • 447
13 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 ...
  • 12.5k
8 votes
1 answer
664 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 ...
  • 81
0 votes
1 answer
374 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 ...
  • 11
4 votes
3 answers
636 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 ...
  • 1,480
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 ...
user avatar