34
votes

Accepted

### Alternatives to the law of the excluded middle

No, every consistent propositional logic that extends intuitionistic logic is a sublogic of classical logic. (That’s why consistent superintuitionistic logics are also called intermediate logics.)
To ...

29
votes

### Alternatives to the law of the excluded middle

Your question sounds like you’re thinking mainly about plain propositional logic, and for that, Emil Jeřábek’s excellent answer shows why the answer is “no”. But to supplement it a little, in case ...

24
votes

### How strong is Cantor-Bernstein-Schröder?

I do not know how to answer your questions, but here are some remarks that should make you worried.
First, in the realizability topos over infinite-time Turing machines there is a mono $\mathbb{N}^\...

23
votes

Accepted

### Why would the category of sets be intuitionistic?

You wrote:
Suppose our intuition for the phrase "subset of $X$" comes from the idea of having an effective total function $X \rightarrow \{0,1\}$ that returns an answer in a finite amount ...

21
votes

### Alternatives to the law of the excluded middle

In first-order logic, the sentence
$$\neg\forall x,y(\neg\neg x=y \to x=y)$$
is consistent with intuitionist logic but not with classical logic.
One might call this "the fuzziness of identity&...

17
votes

Accepted

### Why are W-types called "W"?

You write:
Probably "W" means either "wellordered" or "wellfounded". […] But these are notions associated to order theory, whereas W-types don't directly have to do with ...

15
votes

Accepted

### Henkin-style completeness proofs for intuitionistic logic

What you are looking for is a proof of completeness for intuitionistic logic in a constructive metatheory. When one turns constructive, even the notion of completeness varies according to how it is ...

12
votes

### Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

As far as I can tell Martin-Löf's analysis of identity and his formulation of the identity types is the intuitionistic explanation of identity. In terms of BHK it would be an algorithmic version of ...

12
votes

Accepted

### Fibers of the morphism from the free Heyting algebra to the free Boolean algebra

$\let\eq\leftrightarrow$Notice that $\psi(A)=u$ iff $\vdash_\mathrm{CPC}A\eq u$ iff $\vdash_\mathrm{IPC}\neg\neg(A\eq u)$. (I will write just $\vdash$ for $\vdash_\mathrm{IPC}$.) Thus:
$\bot$ has a ...

12
votes

Accepted

### Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?

I would argue that intuitionistic logic is perfectly self-hosting: working in an intuitionistic set theory, one can define a sound semantics of intuitionistic logic relative to models built out of ...

11
votes

Accepted

### Does cut elimination fail here?

$$
\dfrac{\dfrac{\dfrac{\dfrac{}{A\vdash A}}{A\vdash A\lor(A\to C)}\qquad\dfrac{}{C\vdash C}}{\dfrac{\dfrac{(A\lor(A\to C))\to C,A\vdash C}{(A\lor(A\to C))\to C\vdash A\to C}}{(A\lor(A\to C))\to C\...

11
votes

### Why would the category of sets be intuitionistic?

There are many answers that could be given, but I think the standard "algorithmically oriented" answer is the BHK/Curry-Howard interpretation, according to which a "subset $A$ of $X$" is specified by ...

11
votes

### Forcing is intuitionistic

It seems to me that the "more philosophical" reason why forcing is intuitionistic is that forcing and intuitionistic logic have similar interpretations of the logical connectives and quantifiers. This ...

10
votes

Accepted

### Did Bishop, Heyting or Brouwer take partial functions seriously?

I don't believe that Bishop explicitly assumed all functions are continuous. I think that "no discontinuous function can be proved to be total in Bishop's constructive mathematics" is actually a very ...

9
votes

### Did Bishop, Heyting or Brouwer take partial functions seriously?

The question of how Brouwer perceived partial functions is very interesting and worthy of investigation. I only have two comments about this:
Brouwer and Heyting certainly did consider partial ...

9
votes

### Is there a probability theory developed in intuitionistic logic?

As noted by Andrej Bauer it is good to make a distinction between developing probability theory using intuitionistic logic, and making a new framework for probability compatible with intuitionistic ...

9
votes

### Computability-theoretic results relevant to realizability

Many results of computability theory can be stated synthetically in the effective topos. I have dubbed this idea "synthetic computability" and have tried to develop as much computability ...

9
votes

### Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?

See Palmgren, Constructive Sheaf Semantics for a completeness proof for sheaf semantics within a constructive (and predicative) metatheory. The introduction also mentions several references to earlier ...

8
votes

Accepted

### Forcing in Constructive Set Theories

See
Forcing for IZF in sheaf toposes
Also
Toposes from Forcing for Intuitionistic ZF with Atoms.
Edit:
Maybe more references:
Heyting-valued models for intuitionistic set theory
The book "...

8
votes

### Multiplication of Cauchy and Dedekind real numbers

Whilst the definition of addition of Cauchy or Dedekind real numbers is "obvious", multiplication is rather more tricky. Unfortunately, most accounts, including [RD], leave it as an "exercise for the ...

8
votes

### Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?

Comment environment was acting funny, so I am writing an "answer". Here is a good place to start:
Harry de Swart's PhD from the University of Nijmegen (the Netherlands) was about this kind ...

8
votes

Accepted

### Possible values of "Kripke rank" for formulae in IPL

The finite model property of intuitionistic logic implies that every unprovable formula has finite rank. On the other hand, all positive integers are ranks of some formulas; there are many families of ...

7
votes

Accepted

### Intutionistic Robinson Arithmetic

Both are false. Consider the following Kripke model $M\vDash Q^e$ (in fact, it satisfies the intuitionistic version of $\mathrm{PA}^-$): it consists of two worlds $u,v$ such that $u$ sees $v$; the ...

7
votes

### How strong is Cantor-Bernstein-Schröder?

The Myhill isomorphism theorem is often taken as a computability-theoretic version of the Cantor-Schroder-Bernstein theorem, and this can be interpreted as a version of the result for constructive ...

7
votes

### Is there a completeness proof of intuitionistic predicate calculus using Heyting algebra semantics that is inuitionistically valid?

Harry de Swart's PhD from the University of Nijmegen (the Netherlands) was (explicitly) about this kind of topic. He establishes the completeness of IPC using search trees, in an intuitionistic meta ...

6
votes

### Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

You are right to note that Martin-Löf's treatment of identity as a type is an extension of the BHK-interpretation as originally presented by H(eyting) and K(olmogorov/reisel).
Your guess is also ...

6
votes

### Adding nonconstructive disjunction to intuitionistic logic

$\newcommand{\par}{\mathbin{⅋}}$
$\newcommand{\rz}{\Vdash}$
$\newcommand{\fst}[1]{\mathsf{fst}(#1)}$
$\newcommand{\snd}[1]{\mathsf{snd}(#1)}$
Let me write $r \rz \phi$ when $r$ realizes $\phi$.
If ...

6
votes

### Rice's theorem in type theory

I'll prove the first scheme; you can find a link by using the cite button below this answer.
First, we show that $$\forall x,y : A\,(\phi(x) \lor \lnot\phi(y))\tag{...

5
votes

### Henkin-style completeness proofs for intuitionistic logic

Henkin-style completeness proofs for intuitionistic logic are perfectly possible: instead of maximal consistent sets, you consider, for each formula $A$, maximal sets $\Gamma$ such that $\Gamma\nvdash ...

Only top scored, non community-wiki answers of a minimum length are eligible

#### Related Tags

intuitionism × 48lo.logic × 36

constructive-mathematics × 17

proof-theory × 9

set-theory × 8

reference-request × 6

model-theory × 6

mathematical-philosophy × 5

type-theory × 5

computability-theory × 4

modal-logic × 4

soft-question × 3

ct.category-theory × 2

forcing × 2

lattice-theory × 2

foundations × 2

linear-logic × 2

realizability × 2

pr.probability × 1

real-analysis × 1

gn.general-topology × 1

measure-theory × 1

mp.mathematical-physics × 1

computer-science × 1

order-theory × 1