# Questions tagged [intuitionistic-logic]

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

297 questions
Filter by
Sorted by
Tagged with
10 views

### Modal Heyting Algebras

Is there a standard way to add modal operators over a Heyting algebra -- as it was done e.g. by Johnstone and Tarski for Boolean algebras? Does this provide a semantics to some version of ...
102 views

### There does not exist an even prime greater than two: is there an intuitionistic proof?

My own feeble understanding of intuitionism is that it is constructive and that, by not accepting the law of excluded middle, proofs by contradiction are eschewed. For my background on the topic, see ...
44 views

### What is the algorithm for automated theorem proving in intuitionistic propositional logic?

In classical logic exists law of excluded middle: (a or not a). We can append not a to the knowledge base and show contradiction....
104 views

### Can a proposition be false and its negation be false in Intuitionistic logic?

The principle of non-contradiction say that p and $\neg$ p can not be both true. If you consider the law of excluded middle as relevant, then either p or $\neg$ p is true, and thus the other is false ...
48 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 ...
76 views

### How to prove that $\vdash \neg \neg (p \vee \neg p)$? (Natural Deduction) [closed]

I do know that double negation and LEM are equivalent, but can we prove $$\vdash \neg \neg (p \vee \neg p)$$ without using either of them?
79 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 ...
69 views

39 views

### Showing every state in an intuitionistic model verifies ¬¬p → p

I'm working on a question in the field of intuitionistic logic: In an intuitionistic model, assume p ∨ ¬p is verified at the root state. Give a brief argument showing that every state in the model ...
68 views

91 views

### Converse of $(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$

I have a basic question about the following proposition. $(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$ I can prove it in intuitionistic logic. But I wonder if we have the ...
83 views

45 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 ...
115 views

### Type theory and constructivist mathematics with paraconsistent logic?

Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs ...
66 views

95 views

### Strongly constructive proofs: Proofs that don't make use of decidability?

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic: A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
77 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 ...
62 views

I'm reading about intuitionism, and I've come across an argument put forth by L. E. J. Brouwer that claims to be a counterexample to the statement that $\mbox{The points of the continuum form an ... 0answers 35 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 \...
There exists a superintuitionistic propositional logic where $\neg p \vee \neg \neg p$ is a theorem, but $p \vee \neg p$ is not a theorem. It is called the logic of the weak excluded middle. That ...
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 ...