Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
371
questions
1
vote
0
answers
31
views
Is there a sheaf model where the Weak Markov's principle fails?
We define a real number $x$ to be pseudopositive if $\forall y \in \mathbb{R}$ we have $ \neg \neg (y < x) \vee \neg \neg (y > 0) $.
The Weak Markov's Principle (WMP) is the axiom that every ...
- 567
1
vote
2
answers
116
views
In what sense are proofs that rely on the Law of the Excluded Middle really proofs?
As a non-mathematician, it seems to me that the Law of Excluded Middle is merely an axiom when it comes to proofs that employ it.
Can we really rely on such proofs? In what sense are they valid?
EDIT
...
1
vote
1
answer
56
views
In intuitionistic FOL, does $\forall x \forall y (P(x) \lor Q(y))$ imply $(\forall x, P(x)) \lor (\forall y, Q(y))$?
Of course, in classical logic, if you have $\forall x \forall y (P(x) \lor Q(y))$, then you can conclude $(\forall x, P(x)) \lor (\forall y, Q(y))$: if you didn't have that, then there would be $x$ ...
- 17.5k
0
votes
1
answer
65
views
Question about an extension of Intuitionistic Logic
Kurt Gödel introduced a mapping from Intuitionism to Classical S4 Modal Logic as follows:
$A’=\Box A$ where $A$ is a positive atomic formula.
$(\sim A)’=\Box \sim (A’)$
$(A \land B)’=A’ \land B’$
$(A \...
- 427
3
votes
1
answer
105
views
What subclass of topological spaces validate the theorems of classical logic?
I know that there is a topological semantics for intuitionistic logic. But that raises the question, precisely what subclass of topological spaces corresponds to classical logic? Basically, I am ...
- 16.8k
2
votes
1
answer
83
views
Completeness of intuitionistic propositional logic
I want to study the semantics of intuitionistic propositional logic.
Fix a topological space $X$, let $\Gamma\models^X A$ denote that $A$ is valid under $\Gamma$ in the algebra of all open sets of $X$....
- 61
2
votes
0
answers
114
views
Does "Every set of $\mathbb{R}$ is Lebesgue measurable" imply some weakened LEM?
I would like to know if the Reverse Mathematics has a conclusion for this axiom ($\text{LM}$:Every set of $\mathbb{R}$ is Lebesgue measurable).
I have tried to translate this axiom into a halting ...
- 35
10
votes
0
answers
111
views
Is it known whether there are atoms in the complete lattice of intermediate logics?
By "intermediate logic" I mean a (non-trivial) propositional logic at least as strong as intuitionistic logic whose set of theorems is closed under modus ponens and closed under substitution ...
- 101
2
votes
0
answers
52
views
What if the metatheory is itself intuitionistic?
Usually, even in intuitionistic logic, the metatheory is classical. That is, to give just one example, either something is a theorem of intuitionistic logic, or it is not. That is an example of a ...
- 16.8k
2
votes
2
answers
40
views
Is this formula provable in intuitionistic first-order logic?
I know that in classical first-order logic, the formula $(\exists x)( \exists y) x \neq y \rightarrow (\forall x)(\exists y) x \neq y$ is a theorem. Is it also a theorem of intuitionistic first-order ...
- 16.8k
1
vote
1
answer
60
views
How many fragments of second-order (classical/intuitionistic) logic are there using only $\exists$/$\forall$?
Question: How many fragments of second-order (classical/intuitionistic) logic are there using only the quantifiers $\exists$/$\forall$?
Specifically only those "fragments of second order (...
- 1,144
1
vote
0
answers
66
views
Question on the translation from Intuitionism to S4 Modal Logic
Below is the standard translation from Intuitionistic Propositional Logic to Classical S4 Modal Logic:
P:▢P
PvQ:PvQ
P&Q:P&Q
~P:▢~P
P->Q:▢(P->Q).
My question is thus: if the semantics for ...
- 427
3
votes
1
answer
55
views
Using Heyting algebras outside of Intuitionistic Propositional Calculus.
I am looking for examples of proofs or constructions that rely on a Heyting algebra. Furthermore, said examples must use the fact that Heyting algebras can be considered semantics for IPC, but be ...
- 533
1
vote
1
answer
50
views
How to prove rigorously that neither the universal nor the existential quantifier can define the other in intuitionistic logic?
I know that in classical first-order logic, each of the universal and existential quantifier can be used to define the other, and I suspect that in intuitionistic first-order logic, neither can define ...
- 16.8k
3
votes
1
answer
117
views
Does the intuitionistic logic contain classical (in a sense)?
Is it true that for every finite set of axioms $a_0$, ..., $a_n$, if a statement $t$ follows from these axioms in the classical first-order predicate logic, then in intuitionistic first-order ...
- 4,893
0
votes
1
answer
69
views
is the NNO in a sheaf topos a model of classical PA?
In their book Models for Smooth Infinitesimal Analysis Moerdijk and Reyes claim that the natural number object in any Grothendieck topos is a model of all classical provable statements of first order ...
- 3,031
3
votes
1
answer
169
views
Curry-Howard Isomorphism For Classical Logic
I wonder if there is some direct proof of how $\lambda$-$\mu$-calculus maps to classical logic via the Curry-Howard correspondence. Just like one can verify a valid sentence in propositional logic by ...
- 2,948
0
votes
0
answers
53
views
How to efficiently enumerate all valid propositional formulas from implicational fragment of intuitionistic logic?
A set of valid Propositional logic formulas is decidable. A set of implicational propositional formulas is a subset of this set. If we limit Axiom schemas by removing Axiom schema 3 (Peirce's law) we ...
- 415
-3
votes
1
answer
152
views
Why do intuitionists think that proving $\neg \neg P$ merely constitutes a proof of the inexistence of a proof for $\neg P$?
In every case of $\neg \neg P$ that I've come across, the statement $\neg P$ has been disproven. Never has such a proof merely been proof for the inexistence of a proof for $\neg P$.
Take the ...
- 976
0
votes
0
answers
50
views
Measure and Integration theory based on intuitionism
Measure and integration theory uses the axiom of choice extensively, for example the idea behind σ-algebra is that there are non-measurable sets (in the sense of lebesgue) like Vitali set, but on the ...
- 123
5
votes
4
answers
273
views
What is the reasoning behind the negation definition in Intuitionistic Logic Forcing and Set Theory Forcing?
In Kunen page 96 - of 10th impression 2006:
(p $\Vdash^* \neg A) \iff $ $\forall q \leq p \; \neg \; (q \Vdash^* A)$
Similarly in https://www.logicmatters.net/resources/pdfs/LogicStudyGuide.pdf on ...
user239186
4
votes
3
answers
394
views
The simplication of left implication rule in intuitionistic sequent calculus
The original left implication rule in sequent calculus for intuitionistic logic is
$$
\dfrac{\Gamma, A \supset B \vdash A \quad \Gamma,A \supset B, B \vdash C}{\Gamma, A \supset B \vdash C}
$$
There ...
- 367
0
votes
1
answer
91
views
Model theory of intuistionistic logic
The Tarskian interpretation of first order logic, $I=I_{S,\alpha}$, where $S$ is a first order structure w.r.t. the signature $\Sigma$, and $\alpha$ is a variable assignment, assign either $T$ or $F$ ...
- 11k
4
votes
1
answer
275
views
Is there a reverse double-negation translation?
There are many double-negation translations $f$, each with the property that $\vdash\varphi$ classically iff $\vdash f(\varphi)$ intuitionistically. Is there a translation the other way? ...
- 193
1
vote
0
answers
83
views
Do we have a translation from intuitionistic logic to classical logic which can translate all formulas with their precise meaning?(not only theorems)
I want to know if there is a translation from intuitionistic propositional logic formulas to classical propositional logic formulas satisfying the properties I'm looking for.
Actually first part of my ...
- 15
4
votes
1
answer
111
views
Is (Hausdorff $\implies$ Unique Limits) intuitionistic?
It's well known that in Hausdorff topological spaces, limits of convergent sequences are unique and essentially the only proof I know (which appears very natural) is:
Suppose $(x_i)$ is a convergent ...
- 2,681
4
votes
3
answers
246
views
is proof by contradiction essential for proving the Pigeonhole Principle? [duplicate]
The standard way to prove the Pigeonhole Principle that, putting $n+1$ pigeons into $n$ pigeonholes necessitates the existence of at least one pigeonhole with at least 2 pigeons is by contradiction. ...
user630227
1
vote
1
answer
61
views
Constructive Proof that Intuitionistic Higher-Order Logic is Conservative over Constructive First-Order Logic
In the classical setting, we know that higher-order logic is conservative over first-order logic.
More precisely, consider a classical first-order many-sorted theory $T$, and consider some sentence $\...
- 29.2k
4
votes
2
answers
183
views
Can a formula with only unique variables be an intuitionistic tautology?
Consider intuitionistic propositional formulae, using only the connective "$\rightarrow$" and absurdity .
Can there exist a formula such that it is a theorem/tautology and every pair of ...
- 533
0
votes
1
answer
77
views
Why is this infinite series _intuitionistically_ Cauchy?
I'm currently writing a short paper on Intuitionism for uni. The subject of this paper is the decay of the intermediate value theorem under intuitionism. I have found a proof for this but I have a ...
- 259
2
votes
0
answers
70
views
Examples of Intuitionistic Proof
For uni I need to write a paper and give a presentation on intuitionism, and I am looking for nice examples of theorems or other results to prove or disprove intuitionistically. One example I found ...
- 259
1
vote
2
answers
144
views
Intuitionistic logic, tree-like Kripke model
There is a tree-like Kripke model in which the set of worlds $\mathfrak{W}$ is ordered as a tree:
(a) there is a smallest world $W_0$
(b) for any $W_i \ne W_0$ there is a unique preceding world $W_k: ...
- 11
2
votes
0
answers
56
views
Is Kleene's realizability recursive?
Kleene introduced realizability as a practical semantical interpretation of Heyting Arithmetic (see link for definition). The key result he proved is that provability of $\varphi$ in HA implies the ...
- 21
4
votes
2
answers
152
views
distribution of disjunction and conjunction over each other in intuitionistic logic
I can't find any references as to whether or not the usual properties of disjunction and conjunction distributing over each other hold in intuitionistic logic. Consider:
$$(1) \ \ (p \vee (q \& r))...
- 607
0
votes
0
answers
21
views
Proof of the Local Deduction Theorem, for one of many logics
(I also asked this in MathOverflow)
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 \bigcup \{\phi\} \models \psi$ iff for ...
- 149
0
votes
1
answer
27
views
An exercise in fuzzy logics built from a t-norm
(I also asked this in MathOverflow)
Consider the following t-norm:
$
a * b = \begin{cases}
\text{$2ab,$} &\quad\text{if $a, b$}\le1/2\\
\text{$min\{a, b\}$} &\quad\text{...
- 149
0
votes
2
answers
107
views
Intuitionistic logic: double negation and LOEM removed?
Why are double negation and the law of excluded middle excluded from the theory vs one of classical logic?
I see that the law of the excluded middle $\lnot(p \land \lnot p)$ requires double negation ...
- 1,021
0
votes
0
answers
33
views
What Are the Smallest Totally Ordered Set and the Conditional Valuation Rule Needed for Intuitionistic Countermodels for Propositions in IPC?
According to the Wikipedia article on Heyting algebras:
Every totally ordered set that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice). In this case p→q ...
- 103
0
votes
0
answers
30
views
Filter on Heyting algebra
Consider the first order intuitionistic logic.
Let $H$ be an Heyting algebra, let $F$ be a filter on $H$ and let $V:\text{Frm} \rightarrow H$ be an evaluation function.
Suppose that $b \rightarrow V^{[...
- 165
3
votes
1
answer
64
views
Is a Hetying algebra with coexponetials Boolean?
Suppose we have a Heyting algebra $\mathcal A$ with coexponentials. Specifically, for every $a, b : \mathcal A$ we have an object $b \backslash a$ with the properties that $b \le a \lor (b \backslash ...
- 2,165
0
votes
1
answer
61
views
$ \bigcap _{i \in I} (A\cup S_i) \subset A\cup \bigcap _{i \in I} S_i $ on the intutionistic logic
I want to prove below for nonempty I on the intuitionistic logic.
$$
\bigcap_{i\in I} (A\cup S_i) \subset A \cup\bigcap_{i \in I} S_i
$$
This is equivalent to next.
$$
(\forall x)(\phi\lor\psi_x)\...
- 51
1
vote
1
answer
76
views
Help calculating relative pseudo-complements in a Heyting algebra/lattice
I'm trying to work some examples of relative pseudo-complements in lattices, to make sure I understand them. I wonder if anybody could check my examples, and tell me if I'm correct or if I've ...
- 93
5
votes
1
answer
245
views
Existence elimination in Lean 3
Lean 3 is a theorem prover that implements the calculus of inductive constructions. Differently than Coq, Lean 3s kernel works proof irrelevant. This means that in the kernel of Lean all proofs of the ...
- 3,031
1
vote
0
answers
53
views
Prove that propositional Aczel slash is closed under deduction
I have already proved that
$ \Gamma |\phi \Rightarrow \Gamma \vdash_{IPC} \phi $.
On the other hand, I have tried to prove the other side. I used induction on the length of the proof.(I used natural ...
1
vote
0
answers
56
views
Strange pattern in numbers why is the series of absolute differences always 0? [duplicate]
Put any four numbers in a row, say,
77 73 29 179.
Under the first number write the difference between it and the second number. Under the second number put the difference ...
- 83
3
votes
1
answer
76
views
Upper bound for size of topology needed to falsify a non-tautology in IPC
I was attempting to answer this question with an algorithm based on an answer I gave as an exercise posed by Z.A.K here.
I think it is easy to show the decidability of IPC by converting to S4 and then ...
- 9,246
13
votes
3
answers
1k
views
Can we make intuitionistic logic "intuitive"?
This is something I am wondering about, because all the formulations I've seen of the logic seem fairly difficult to grasp, e.g. lists of abstract axioms that have a few missing versus classical logic....
- 18.6k
4
votes
0
answers
87
views
Prove in $NI$ that $\neg\neg\exists x\forall y[P(y) \to P(x)]$
I have been tasked to prove a slightly different version of the Drinker's paradox:
$\vdash_{NI} \neg\neg\exists x\forall y[P(y) \to P(x)]$
Where ${NI}$ stands for natural deduction in intuitionistic ...
- 180
6
votes
2
answers
195
views
Is there a decision procedure for *monadic* intuitionist first-order logic?
In Ch. 19 of the 4th edition of Methods of Logic, Quine gives a decision procedure for classical monadic first order logic (technically it's a decision procedure for what he calls "Boolean ...
- 63
1
vote
1
answer
80
views
What does this typed lambda-calculus notation mean?
In Definition 3.2 (page 12) of Gallier's 'Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi' he sets out the rules for his typed $\lambda^{\to, +, \times, \perp}$-...
- 904