Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
420
questions
1
vote
1
answer
68
views
How can infinitesimals be invertible in SIA?
I read that infinitesimals in SIA can be invertible: https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis
In typical models of smooth infinitesimal analysis, the infinitesimals
are not ...
- 889
2
votes
1
answer
55
views
Do the monotone maps from a poset into a Heyting algebra form a Heyting algebra?
I am interested in generalizing the fact that the up-sets of a poset always form a Heyting algebra.
Let $P$ be a poset and $H$ a Heyting algebra. $\operatorname{Hom}(P,H)$ can be made a bound lattice ...
- 43
0
votes
1
answer
47
views
How to prove $\exists x (x=a)$ in intuitionistic logic
How do you prove $\exists x (x=a)$ intuitionistically, where $a$ is a constant symbol?
Classically, one has
$$ [\neg\exists x (x=a)]^1\vdash \forall x (\neg x=a) \vdash\neg a = a \vdash \bot \vdash^1 \...
- 684
1
vote
0
answers
73
views
Does Dan Willard demonstrate that classical logics with the Law of the Excluded Middle versus those with Double Negation Elimination are distinct?
Context:
Dan Willard's 2020 review paper of his work on Self-Verifying Theories/Self-Justifying Axiom Systems (SJAS) is titled "How the Law of Excluded Middle Pertains to the Second ...
- 61
1
vote
0
answers
49
views
Is intuitionistic logic a subsystem of classical logic?
Joan Moschovakis' Intuitionistic Logic claims:
"Although intuitionistic analysis conflicts with classical analysis, intuitionistic Heyting arithmetic is a subsystem of classical Peano arithmetic....
- 31
5
votes
1
answer
191
views
Type theory vs "Theory On Top of Logic" mantra in Set Theories
I have a question about (especially second part of) following statement following statement from wikipedia emphasizing intrinsical feature in which type theory substantially differs from set theories:
...
- 7,551
2
votes
1
answer
74
views
Identity in Heyting algebras or not
In some computation over a Heyting algebra, I ended up with the following formula:
$$\Big[(x\to y)\to z\Big]\to \Big[\big(x\to(y\vee z)\big)\vee \big((x\to(y\vee z))\to z\big)\Big]$$
I wonder if it is ...
- 1,066
5
votes
2
answers
123
views
Why does countability misbehave in intuitionistic logic
On page 3 of this paper https://arxiv.org/pdf/2404.01256.pdf
I spotted the claim:
Definitions of countability in terms of injection into ℕ misbehave intuitionistically, because a subset of a ...
- 4,223
2
votes
1
answer
107
views
Busy Beaver function in intuitionistic ZF
Let $BB$ denote the Busy Beaver function. Constructively there is no obvious way to prove that the Busy Beaver function is total (e.g. a Turing machine may neither halt nor not halt), and I have heard ...
- 1,311
2
votes
0
answers
100
views
Constructive Proofs in Elementary Real Analysis
In considering the theorem cited here uniform continuity and equivalent sequences , which states that where $f:X \rightarrow \mathbb{R}$ is a function, the following two conditions are equivalent:
(a) ...
- 63
1
vote
1
answer
81
views
False statements in intuitionistic logic
In the explanations of intuitionistic logic I've been reading (1, 2, 3), especially in the explanation of the semantics, I don't understand how a proposition being false influences the situation.
...
- 163
0
votes
1
answer
46
views
Is it decidable whether a classically valid first-order formula is also intuitionistically valid?
Intuitionistic first-order predicate logic is not decidable for arbitrary formulas.
However, suppose that we are given a formula of first-order predicate logic that is classically valid. Is there a ...
- 123
1
vote
1
answer
45
views
What is the correct way to interpret the Intuitionistic rules of Kleene's sequent (Gentzen) system G1 (in sec. 77 of Kleene I.M. 1952)
I'm having difficulty understanding the sequent/Gentzen proof system in section 8 of a paper by Gurevich [G1977], and he defines that system by telling the reader to modify the system G1 from Kleene's ...
- 13
3
votes
0
answers
72
views
Can This Classical-Kleene Combination for Intuitionistic Fragment $\{ \neg, \vee, \wedge \}$ Be Extended to Include $\rightarrow$?
Over a year ago, I worked out a classical-Kleene combination logic that worked to preserve intuitionistic tautologies over the intuitionistic fragment with operators $\{ \neg, \vee, \wedge \}$, which ...
- 209
3
votes
1
answer
93
views
Would the Following Table Strategy Work as an Intuitionistic Decision Procedure?
I had previously sought some insight for handling logical operators in the Rieger-Nishimura lattice and, with assistance here, was able to work out a fairly rigorous way. To the best of my ability, I ...
- 209