Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
89
questions with no upvoted or accepted answers
27
votes
0
answers
664
views
How does the internal language of a topos come to be?
There are several books and articles on topos theory which mention the internal language, but I can't manage to see the big picture from any of them. I would like a soft explanation of how the ...
15
votes
0
answers
164
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 ...
6
votes
0
answers
65
views
Disjoint union types in MLTT
In MLTT, by identifying propositions as types (and vice versa), a proposition carries the information regarding how a proof of the proposition is constructed. My question is related to this. Let $P:\...
6
votes
0
answers
63
views
Is Smetanich's logic the second from the top in the lattice of intermediate logics?
Consider the lattice of consistent superintuitionistic logics, also known as intermediate logics. Smetanich's logic is the logic obtained from intuitionistic logic by adding the axiom $((\neg q \...
6
votes
0
answers
90
views
Why are there two sets of rules for set equality in intensional intuitionistic type theory?
In Martin-Löf's "Intuitionistic Type Theory", we can judge two sets are "equal" if the following are true:
$$
membership\ rules:
\frac{a \in A}{a \in B} and \frac{a \in B}{a \in ...
6
votes
0
answers
150
views
Equivariant homotopy theory, topos theory and intuitionistic algebraic topology
This might be a very naive question, but I don't really see what would go wrong, so I'm wondering if this has already been done.
The idea is the following : equivariant homotpy theory as far as I can ...
6
votes
0
answers
123
views
Relationship between intuitionistic logic and infinite dimensional vector spaces.
Some time ago, I've heard that there was a relationship between intuitionistic logic and infinite dimensional vector spaces.
More precisely, the fact that $\neg \neg \phi \to \phi$ may not be "true" ...
6
votes
1
answer
281
views
All translations of classical logic into intuitionistic logic
What are all possible ways of translating classical logic into intuitionistic logic? That is, if $S$ is the collection of sentences of first order logic, what are all the functions $f : S \to S$ such ...
5
votes
0
answers
63
views
Is there an intuitionistic proof of "it is impossible to simulate a die with a guaranteed to terminate process involving coin flips"?
Recently, I happened to be thinking again about the question: "Is it possible to simulate a fair six-sided die using only fair coin flips?" One type of answer which tends to be given is ...
4
votes
0
answers
93
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 ...
4
votes
0
answers
258
views
Learning roadmap for constructive mathematics
I just watched the talk "five stages of accepting constructive mathematics". I am very interested to learn constructive mathematics but have zero knowledge of constructive mathewmatics/logic....
4
votes
0
answers
121
views
Is it not wrong that intuitionistic logic is hard to convey?
As someone who is now mostly working in constructive / intuitionistic logic ($\mathsf{IL}$) I am still wondering about the most concise way to spotlight the relevance to people who so far only know ...
4
votes
0
answers
81
views
Can we rule out candidate single-axiom bases for HI via Curry-Howard?
The motivation for this question begins with an answer elsewhere which references Dolph Ulrich's list of single-axiom bases and unresolved candidate single-axiom bases for implicational intuitionistic ...
4
votes
0
answers
232
views
A complicated, curious tableaux proof rule for Intuitionistic S4
In
Amati and Pirri, A uniform tableau method for intuitionistic modal
logics I (1993)
a tableau method for a variety of intuitionistic modal logics is presented with signed formulas ('$\textbf{T}A$'...
4
votes
0
answers
84
views
Transforming intuitionistic propositional validities into validities of linear logic
A tableaux method for linear logic is briefly discussed in
https://www.academia.edu/6591354/TABLEAU_METHODS_FOR_SUBSTRUCTURAL_LOGICS?auto=download
D'Agostino writes (p.418-9):
''It is ...
3
votes
0
answers
64
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 ...
3
votes
0
answers
152
views
Category of presheaves and logic
Let ${\bf C}$ be a small category. As is well known, the category of presheaves ${\bf Set^C}$ is cartesian closed: it can be a model of intuitionistic propositional logic.
Can it also be a model of ...
3
votes
0
answers
184
views
Intuitionistic logic's book to self study...
I want to study intuitionistic logic by myself?
Can you give some recommendations for the different levels (undergraduate and graduate)?
3
votes
0
answers
79
views
Is intuitionistic first-order logic with no function or relation symbols decidable?
Classical first-order logic with no function or relation symbols is decidable. If I'm not mistaken, this is essentially because any formula (with possible free variables) has truth value uniquely ...
3
votes
0
answers
76
views
Internal frame homomorphisms and sheafification
Let $\mathcal{E}$ be an elementary topos with subobject classifier $\Omega$, and let $j : \Omega \to \Omega$ be a Lawvere-Tierney topology. $\Omega$ is naturally seen as a frame object internal to $\...
3
votes
0
answers
177
views
On a translation of Pfenning and Davies from Lax logic to Intuitionistic S4
Pfenning and Davies present a translation on p.22 of the following reference:
https://www.cs.cmu.edu/~fp/papers/mscs00.pdf [2000]
The translation is from propositional lax logic ($PLL$) into a ...
3
votes
0
answers
163
views
Some modal principles (related to monads) and the deduction theorem (in Propositional Lax Logic)
I have two questions. Suppose we have a Hilbert style axiomatic intuitionistic propositional calculus which we supplement with a modal operator $\bigcirc$ (see the bottom of the question for the ...
2
votes
0
answers
95
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) ...
2
votes
0
answers
119
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 ...
2
votes
0
answers
78
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 ...
2
votes
0
answers
91
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 ...
2
votes
0
answers
74
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 ...
2
votes
0
answers
59
views
Reference to know the history of Superintuitionistic (intermediate) logics
There is any source in books or in the web about the history of development of the study of Superintuitionistic logics? By this concept I refer the wikipedia article called "Intermediate logic&...
2
votes
0
answers
97
views
If $A \to 1$ is an epimorphism in a well-pointed topos, does $A$ have a global element?
In a well-pointed topos, it is simple to show that $A$ is an initial object if, and only if, there are no global elements $1 \to A$.
Now suppose that $A \to 1$ is an epimorphism. Then $A$ cannot be an ...
2
votes
0
answers
62
views
Equivalence of the Classical and Approximate Intermediate Value Theorems in Classical Logic
IVT (Classical) Let $f:\left[a,b\right]\to\mathbb{R}$ be continuous. If $f\left(a\right)<0$ and $f\left(b\right)>0$, then there exists $c\in\left(a,b\right)$ such that $f\left(c\right)=0$.
In ...
2
votes
0
answers
161
views
What does the principle of implosion imply from a truth-value gap?
The principle of implosion (verum ex quodlibet) states that a valid formula follows from anything. It is expressed:
B ⊨ A ∨ ¬A
Consider some paracomplete or intuitionistic logic in which the law of ...
2
votes
0
answers
111
views
Why do intuitionistic connectives preserve open sets in the topological interpretation of IPC?
Is there a deeper significance to the fact that the topological intepretation of the connectives of intuitionistic propositional calculus sends open sets to open sets?
Let $(\varphi)^*$ refer to the ...
2
votes
0
answers
134
views
Literature On Simple Type Theory
I am wondering where I can find literature describing the rules for a simple type theory with just products, sums, function types, unit and the empty type. Robert Harper describes such a theory 3 ...
2
votes
0
answers
108
views
A proof step involving the law of the excluded middle
In the answer provided to the question https://mathoverflow.net/questions/296440/modal-collapse-upon-addition-of-the-law-of-the-excluded-middle-to-an-intuitionis, a proof is given, showing that a ...
2
votes
0
answers
97
views
Curious tableaux rules for a curious logic
In
Avellone, A and Ferrari, M Almost duplication-free tableau calculi for propositional Lax logics (1996): pages 6-7
seemingly ambiguous tableaux rules are formulated. The authors employ a proof ...
2
votes
0
answers
165
views
Strictly positive part
I'm having trouble with the definition of strictly positive part from "Basic Proof Theory" by Troelstra. For instance is the formula
$$\exists x (B\lor C) $$
s.p.p? What about $(A\implies B\lor C )$...
2
votes
1
answer
329
views
How can I show that the Gödel-Dummett logic has the Scroggs' Property?
Gödel-Dummett logic is an extension of the intuitionist logic (IPL) by the following axiom:
$$
(p → q) ∨ (q → p)
$$
A logic has the Scroggs' Property if it isn't characterized by any finite logical ...
2
votes
0
answers
149
views
Is the sublocale determined by the double negation nucleus special among all the Boolean sublocales of a locale?
In pointless topology, for any locale $A$ (a.k.a. complete Heyting algebra) its Heyting negation (a.k.a. pseudocompelement) $\neg : A \to A$ gives rise to a nucleus $\neg\neg: A \to A$. As is also ...
2
votes
0
answers
108
views
Prove $\vdash \neg \neg A \leftrightarrow A$ in intuitionistic logic
I want to prove $\vdash \neg \neg A \leftrightarrow A$ without using $RAA$ and $\bot$ rules. the part that $\vdash A \to \neg \neg A$ is simple but I can't prove the other part. is there any ...
2
votes
0
answers
95
views
Show that the law of the excluded middle does not hold in a BCCC
I want to show that the law of the excluded middle do not hold in a bicartesian closed category (BCCC), interpreted as follows:
In general, there need not be a morphism $1 \to A + 0^A$ for $A \in \...
2
votes
2
answers
914
views
Is it possible to eliminate a contradiction without recourse to the principle of explosion?
I'd like to derive the following inference rule:
$$
\frac{p\lor(q\land\neg q)}{p}\quad\text{[ContradictionElimination]}
$$
I assumed that I could do this minimally somehow, however it turns out I ...
1
vote
0
answers
165
views
“Meet” of Zorn’s Lemma and Law of Excluded Middle
Work in intuitionistic logic (IL), and assume ZF.
The Axiom of Choice (AC) implies both Zorn’s Lemma (ZL) and the law of excluded middle (EM). Furthermore, AC is the “join” of ZL and EM, since we can ...
1
vote
0
answers
133
views
Has this logic already been studied?
I have been spending the better part of a year thinking about the subtleties involved in balancing natural language intuitions for logic with the power and efficacy that Classical Logic and ...
1
vote
0
answers
127
views
Does Curry-Howard correspondence mean that everyone who writes a program is doing intuitionistic mathematics?
As far as I know, the first statement of the correspondence is between two formal theories named simply typed lambda calculus and intuitionistic propositional logic, which maps types to formulas and ...
1
vote
0
answers
44
views
Strategies for proving completeness for an extension of Intuitionistic Logic
Recently I’ve been working on axiomatizing a logic that results from adding a new operator to standard Intuitionistic Logic. I use $\sim$ for standard intuitionistic negation, and $\neg$ for the new “...
1
vote
1
answer
91
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
vote
0
answers
96
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 ...
1
vote
0
answers
78
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 ...
1
vote
0
answers
106
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 ...
1
vote
0
answers
63
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 ...