Questions tagged [intuitionism]
The intuitionism tag has no usage guidance.
57
questions
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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. ...
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-...
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, \...
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 \...
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 ...
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)) \...
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 ...
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 \...
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)) \...
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 ...
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 $...
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 ...
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 ...
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 ...
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 ...
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 ...
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&...
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 $\...
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 ...
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 ...
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 (...
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 ...
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 ...
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$".
...
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 ...
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\...
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 ...
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; ...
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}...
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 ...
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 ...
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 ...
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\,\...
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.
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 ...
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 \; ...
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 ...
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 ...
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 \...
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 ...
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?
...
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, ...
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 ...
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 ...