20
votes
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
20
votes
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
20
votes
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
13
votes
Accepted
About Gödel-Gentzen negative translation
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
13
votes
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
13
votes
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
13
votes
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
12
votes
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
12
votes
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
11
votes
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
11
votes
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 ...
- 9,841
10
votes
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
10
votes
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
10
votes
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
10
votes
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 ...
10
votes
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
10
votes
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
9
votes
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
9
votes
Accepted
Syntactic proof that Peirce's law doesn't hold in simply-typed lambda calculus
You are right in your intuition that proving that a derivation does not exist is somewhat cumbersome. Soundness and completeness of formal proof systems provide us with an interesting duality:
$\vDash ...
- 10.7k
9
votes
Accepted
Type theory and constructivist mathematics with paraconsistent logic?
In general, there are credible early attempts to study aspects of mathematics in the context of paraconsistent calculi (there are many, just look at the ToC of Priest's textbook).
That said, the ...
- 11.9k
9
votes
Accepted
In Homotopy Type Theory, how do the continuous notions of spaces and paths, match the discrete notions of constructible terms and proofs?
I would say there is no mistake in your thinking. Rather, the mistake happened many decades ago when algebraic topologists gradually came to use the word "space" for a discrete object that ...
- 4,844
9
votes
Looking for a simple proof of the independence of the law of excluded middle
The way we always prove that a certain sentence is independent of some axiom system is to find a model which think the sentence is true, and a model which thinks the sentence is false.
For IPL, there ...
- 39.1k
9
votes
Accepted
Is Hilbert's epsilon calculus a conservative extension of intuitionist logic?
It is not a conservative extension to intuitionist logic, and in fact the Law of Excluded Middle succeeds catastrophically: while working over intuitionistic Peano Arithmetic (Heyting Arithmetic, $\sf{...
- 2,784
8
votes
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
8
votes
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
8
votes
Non-constructiveness and finite mathematics
Apologies for the extreme length of this answer, but addressing your question requires a bit of a build-up.
First, I'll briefly discuss why the brute-force proofs of cyclicity for $\mathbb{Z}/p\mathbb{...
- 11.9k
7
votes
Accepted
What is an example of a statment that one can prove in an Intuitionistic approch and cannot prove in the classic approch
There are many systems of constructive mathematics. Some of them are compatible with classical logic in that all the theorems provable in these systems are classically true. Bishop's system has this ...
- 82.6k
7
votes
Accepted
Why $\phi \lor \neg \phi $ is not allowed in intuitionistic logic?
Intuitionistic logic does not consider $\phi\lor\neg\phi$ to be universally valid because that's the way "intuitionistic logic" is defined.
The word "intuitionistic" refers to the intuitionists, a ...
7
votes
Accepted
Prove constructively that $\log_2 3$ is irrational.
$x$ is irrational is defined as "$x$ is not rational", so a proof that shows that from the assumption that $x$ is rational we derive a contradiction is a valid constructive proof for
"$x$ is not ...
- 245k
7
votes
Accepted
Equivalence Between Law of Excluded Middle and Self-Implication
Self-implication is true in intuitionistic logic as well. It really should be: if we assume $P$, we really should be able to derive $P$.
The point is that $P \to Q$ and $\neg P \lor Q$ are not ...
- 13.1k
Only top scored, non community-wiki answers of a minimum length are eligible