Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
402
questions
1
vote
1
answer
97
views
LEM and the curry-howard correspondence
The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus ...
- 167
1
vote
0
answers
102
views
How to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic?
I tried to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic.
I used LEM for this proof:
$\lnot(a \neq b)$ :
$a=b$ $\lor$ $a \neq b$
Let $a=b$. Then statement $a \neq b$ is ...
- 527
0
votes
0
answers
49
views
Is there any logic system which ENTIRELY rejects non-contradiction of any kind for any sentence (i.e. all contradictions are true)? Is this possible?
I've recently learned about paraconsistent and intuitionistic logic, and dialetheism.
According to the Stanford Encyclopedia of Philosophy's page on Dialetheism, it states:
Dialetheism is the view ...
- 101
5
votes
2
answers
130
views
Proof that LEM is equivalent to the well-ordering of $\Bbb{N}$
John L. Bell's Intuitionistic Set Theory contains an exceedingly slick demonstration that the law of excluded middle is equivalent to the well-ordering of the natural numbers $\Bbb{N} := \{ 0, 1, 2, .....
- 5,608
0
votes
1
answer
29
views
Proof of contradiction vs refutation by contradiction and what is/isn't allowed in constructive logic?
Here it is stated that constructive logic allows refutation by contradiction:
The proposition to be proved is ¬P.
Assume P.
Derive falsehood.
Conclude ¬P.
But not indirect proof:
The ...
- 167
2
votes
1
answer
49
views
Is Resolution Intuitionistically Valid?
Specifically, is it intuitionistically valid to deduce $Q$ from $P\vee Q$ and $\neg P\vee Q$? The proof I could come up with uses the law of exclusive middle, and I feel that you can probably come up ...
- 1,559
0
votes
1
answer
86
views
Formalizing Real World Sentence In Intuitionistic Logic?
In my local supermarket, there is a notice with a recall, in the end it says:
This warning does not imply that the damage was caused by the producer, manufacturer, importer, or distributor
My first ...
- 3,522
1
vote
0
answers
107
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 ...
- 991
2
votes
1
answer
120
views
Is the fundamental theorem of algebra true for constructive complex numbers?
I wonder whether the fundamental theorem of algebra holds in intuitionistic logic, using constructive complex numbers. (To get around the fact that in general we cannot compute the degree of a ...
- 19.9k
1
vote
1
answer
96
views
What is the nature of the double negated axiom of choice?
Under what circumstances is the principle
$$nnaoc : (\Pi x:A. \lnot \lnot B_x) \implies \lnot \lnot (\Pi x: A. B_x)$$
valid? So the axiom of choice, but using double negation instead of propositional ...
- 13
-1
votes
1
answer
83
views
where can I read the whole proof of impossibility of proving Law of Excluded middle without proof by contradiction in Natural deduction? [duplicate]
Intuitionistic logic can't prove as many sentences as classical logic, for example: Peirce's Law; Reductio Ad Absurdum; Double Negation Elimination; and Tertium Non Datur, which are all equivalent in ...
- 133
2
votes
1
answer
51
views
Find an inhabitant for type $\phi$
I am studying from Sorensen's book (Lectures on the Curry-Howard isomorphism, ed. 2006) and there is a type that is said to be inhabited, but I need to find the inhabitant. However, I can't find it. ...
0
votes
1
answer
72
views
How to prove that a formula is intuitionistically valid using Kripke semantics?
I want to know how to use Kripke semantics so that I can prove that a formula is intuitionistically valid.
I think that all others cases will clear out if I understand the case of implication.
Let's ...
2
votes
1
answer
67
views
Intuitionistic proof of $((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$
I need to prove that the $\psi=((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$ is intuitionistically valid. I tried using the topology of open sets of $\mathbb{R}$ and an arbitrary valuation, ...
0
votes
1
answer
67
views
What meta-theoretic principles are we supposed to adopt when studying formal logic/system?
Also, how do different sets of principles affect the results we can get in our meta-theory?
The more concrete questions that lead me to ask the above two questions are stated below.
If we are studying ...
- 407
2
votes
1
answer
100
views
Intuitionistic well-orderings of uncountable sets
The well-ordering principle has always been considered to be highly unconstructive, as far as I know. However, I think intuitionistic mathematics can be compatible with the existence of a well-...
- 343
1
vote
0
answers
117
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 ...
- 33
2
votes
3
answers
398
views
What are the examples for intuitionistic logic?
I have been curious about intuitionistic logic for some time and I want to know about it and I have a question, the law of the excluded middle and double negation elimination seem completely logical ...
1
vote
2
answers
63
views
Well-Ordering Principle From Recursion Theorem
As far as I understand, in intuitionistic logic we have neither (i) the well-ordering principle nor (ii) the recursion theorem. But can one deduce one from the other? I believe we cannot deduce (ii) ...
- 3,522
1
vote
1
answer
83
views
Is there a simpler Kripke counter-model for this formula?
$\forall x \neg \neg \phi(x) \to \neg \neg \forall x \phi(x)$ is not intuititionistically valid. I can come up with a complicated Kripke counter-model as follows:
Let there be a countably infinite ...
- 991
4
votes
1
answer
403
views
doubly negated intuitionistic formulas
What is an example of some doubly negated statement in intuitionistic logic that is not equivalent to its classical version?
Some background: for every statement $P$ we can find a classically ...
- 343
7
votes
3
answers
2k
views
Why is the Principle of Explosion considered constructive?
I read over this post Why is the principle of explosion accepted in constructive mathematics? and still have some thoughts/questions.
One of the answers mentions that a formula is constructively valid ...
- 991
0
votes
1
answer
102
views
Would a constructive proof that intuitionstic ZF has a nonconstructive model be a problem for the intuitionist?
It is my understanding it is provable in ZFC+zero sharp that intuitionistic ZF has a nonconstructive model.
(Here I am assuming the existence of zero sharp only to guarantee that ZFC has a ...
- 31
2
votes
3
answers
187
views
How to solve $(x-1)(x-2)=0$ constructively?
I want to prove that
$$(x-1)(x-2)=0\Leftrightarrow x=1, 2$$
$\Leftarrow$ is easy. The problem is $\Rightarrow$.
Assuming $x\neq 1, 2$, we can derive $1=0$ by dividing both sides of $(x-1)(x-2)=0$ by $...
- 369
1
vote
0
answers
43
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 “...
- 991
0
votes
0
answers
85
views
Reducing any formal system to intuitionistic or classical logic
Does the following provability hold in intuitionistic logic?
$\vdash a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow a_k)\dots))$ for $0\leq k\leq n$
$a_0\Rightarrow (a_1\Rightarrow(\...
- 4,961
2
votes
1
answer
80
views
Question on Intuitionistic Modal Logic
In the intuitionistic version of the modal logic K (IK), the following is a theorem:
$(\Diamond p \to \Box q) \to \Box( p \to q)$. However, given the definitions for $\Box$ and $\Diamond$, I think I ...
- 991
0
votes
0
answers
70
views
Need Help With First Order Intuitionistic Tableaux
I have a question about semantic tableaux for Intuitionistic FOL. I’ll post a sample tableaux that I’m pretty sure I’m doing wrong, and then I’ll post a sequent calculus approach to show where I get ...
- 991
6
votes
1
answer
412
views
Is intuitionist logic two-valued?
On this page https://en.wikipedia.org/wiki/Principle_of_bivalence :
Intuitionistic logic is a two-valued logic but the law of excluded middle does not hold.
On this page https://en.wikipedia.org/...
- 111
9
votes
1
answer
668
views
How is the “ Axiom of choice is trivial in intuitionistic logic”?
In slide 28 of these slides, the author claims that the “Axiom of choice is trivial in intuitionistic logic” and that classical logic makes it a “ monster from outer space”. How is it trivial when it’...
- 1,119
4
votes
1
answer
90
views
Is there a non-constructive proof-functional logic
I understand that classical logic preserves truth, is bivalent, and contains non-constructive proofs. In contrast, intuitionistic logic preserves justification/verification for a proof, is not ...
- 991
3
votes
1
answer
108
views
Intuitionistic Logic vs Constant Domains
Quantified modal logic is a controversial field, specifically since it forces one to consider what is meant by “world” in Kripke Semantics. For example, the formula $\Box \forall x \varphi \implies \...
- 991
2
votes
2
answers
179
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 (x > y) \vee \neg \neg (y > 0) $.
The Weak Markov's Principle (WMP) is the axiom that every ...
- 639
1
vote
2
answers
144
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
...
2
votes
1
answer
75
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$ ...
- 19.9k
0
votes
1
answer
101
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 \...
- 991
3
votes
1
answer
123
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 ...
- 19.2k
2
votes
1
answer
132
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
117
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 ...
- 135
13
votes
0
answers
127
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 ...
- 131
2
votes
0
answers
67
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 ...
- 19.2k
2
votes
2
answers
52
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 ...
- 19.2k
1
vote
1
answer
76
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,300
1
vote
0
answers
86
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 ...
- 991
3
votes
1
answer
77
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 ...
- 655
1
vote
1
answer
82
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 ...
- 19.2k
3
votes
1
answer
164
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,961
0
votes
1
answer
95
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,998
3
votes
1
answer
217
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 ...
- 3,522
0
votes
0
answers
64
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