# Tag Info

Accepted

### How Do Heyting Algebras Relate To Logic?

As Noah Schweber says, this is a generalization of how Boolean algebras relate to logic, so it would be good to get a handle on that case first. A Boolean algebra $B$ is a set equipped with two ...
• 441k
Accepted

### How is the “ Axiom of choice is trivial in intuitionistic logic”?

The right text to look at for more details is Andrej Bauer's text "Propositions as [Types]". You may also look at the paragraph "In Type Theory" of this nLab article, which ...
• 4,350

### Why is the Principle of Explosion considered constructive?

NB I start by talking about type theory in this first section, but the second section contains comments about usual first-order logic and Heyting arithmetic that also make sense on their own. When we ...
• 11.9k
Accepted

Does it mean that if $\varphi$ is true in intuitionistic logic, $\varphi^N$ is not necessarily intuitionistically true? First, let's get the meaning of "a sentence $\varphi$ may not imply its ...
• 11.9k

### Looking for a simple proof of the independence of the law of excluded middle

The others answers give simple semantic proofs showing that LEM is independent of intuitionistic logic. However, you don't always need to construct a model to show non-derivability. There are simple, ...
• 11.9k

### Why do intuitionists think that proving $\neg \neg P$ merely constitutes a proof of the inexistence of a proof for $\neg P$?

Intuitionists agree that if you prove $\neg Q$, you are proving that $Q$ is false. For an elaboration on this idea, see my answer here. This is true in the special case of $Q = \neg P$. If I'm not ...
• 32.3k
Accepted

### Is intuitionist logic two-valued?

First, give us a definition of what it means for a logic to be $n$-valued; then, we'll be able to tell whether intuitionistic logic is 2-valued or not. Since there is no standard, widely-accepted ...
• 11.9k
Accepted

### Why is it called linear logic?

Girard himself, in his native language (cf. Girard, Cours de Logique I, Hermann, 2006, Section 1.B.2), writes: "La logique linéaire est issue d'une prise en compte systématique de l'interprétation ...
• 1,288
Accepted

### Looking for a simple proof of the independence of the law of excluded middle

Every Heyting algebra is a model of IPL. Some Heyting algebras (the Boolean algebras) satisfy LEM, and some do not. Therefore, LEM is independent of IPL. For explicit examples: The simplest non-...
• 80.1k

### Relation between Heyting algebras and Intuitionistic logic

You certainly will not always get intuitionistic logic. For instance, if $H$ is actually a (nontrivial) Boolean algebra, then you get Boolean logic. And if $H$ is the trivial (1-element) algebra you ...
• 335k

### Why is the Principle of Explosion considered constructive?

There are other excellent answers, but here is another piece of the story I find helpful: the comparison with disjunction. First think about just disjunction for a moment, $A_1 \vee A_2$. It ...

### Which theorems of classical mathematics cannot be proved without using the law of excluded middle?

Just to clarify: the intuitionists' rejection of Excluded Middle does not mean embracing $\lnot (A \lor \lnot A)$ for all $A$! Some instances of Excluded Middle are acceptable, namely those for which ...
• 624
Accepted

### Semantics for minimal logic

Yes, tweaking Kripke semantics based on that for intuitionistic logic does the trick. If I recall right, there are slightly different ways of doing this. Here's a version for minimal logic and some ...
• 55.6k
Accepted

### What is the intuitive meaning of the Heyting algebra?

Gödel showed (in effect) that no finite Heyting algebra is complete. The term model or Lindenbaum algebra of intuitionistic propositional logic (IPL) is a countable Heyting algebra that is complete ...
• 49.6k
Accepted

### Can we prove $1\neq 2$ using intuitionistic methods?

Assume $S(0)=S(S(0))$. One of the Peano axioms say that $S(x)=S(y) \to x=y$, so we immediately conclude $0=S(0)$. But this contradicts the axiom $\forall x(0\ne S(x))$. Thus $S(0)\ne S(S(0))$. This ...

### Does double negation distribute over implication intuitionistically?

Somewhat surprisingly, the identity does hold in intuitionistic logic. We give three arguments: an informal natural deduction-style proof, a formal proof in the Agda proof assistant, and a formal ...
• 11.9k

### Is there a reverse double-negation translation?

Based on an analysis of computational complexity, we should not expect any such $f$ to be computable in polynomial time. It is well-known that the problem of determining whether $\vdash \phi$ ...
• 32.3k

### Triple negation in intuitionistic logic?

In addition to the two very nice formal answers, let me give an informal proof that $\neg\neg\neg A \Rightarrow \neg A$. Recall that, by definition, $\neg B$ is an abbreviation for $B \Rightarrow \bot$...
• 3,220
Accepted

• 2,784
Accepted

### Independence of connectives in intuitionistic logic

No three intuitionistic connectives can be used to define the fourth one. McKinsey [1] showed this using nigh-trivial semantic proofs: in modern terminology, we would say that he constructs Heyting ...
• 11.9k
Accepted

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

There's no intuitionism/constructivism issue going on here at all. First of all, as a general matter of practice you need to keep separate the notions of proof by contradiction and proof by negation. ...
• 251k