Questions tagged [intuitionism]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3
votes
0answers
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
1answer
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
1answer
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
0answers
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
1answer
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
1answer
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
0answers
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
3answers
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
3answers
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
0answers
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
3answers
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
0answers
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
1answer
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
1answer
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
1answer
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
2answers
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
1answer
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
2answers
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
1answer
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
1answer
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
0answers
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
1answer
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
1answer
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
1answer
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
1answer
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
2answers
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
1answer
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
1answer
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
0answers
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
2answers
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
3answers
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
2answers
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
1answer
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
2answers
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
1answer
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
6answers
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
2answers
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
1answer
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
3answers
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
3answers
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
6answers
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
1answer
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
1answer
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
3answers
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
4answers
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 ...