# Questions tagged [intuitionistic-logic]

Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.

402 questions
Filter by
Sorted by
Tagged with
1 vote
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 ...
1 vote
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 ...
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 ...
130 views

1 vote
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 “...
85 views

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 ...
1 vote
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 ...
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$ ...