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 ...
user avatar
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 ...
user avatar
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}^\...
user avatar
  • 43.4k
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 ...
user avatar
  • 43.4k
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&...
user avatar
  • 16.6k
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 ...
user avatar
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 ...
user avatar
  • 4,647
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 ...
user avatar
  • 43.4k
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 ...
user avatar
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 ...
user avatar
  • 58.9k
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\...
user avatar
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 ...
user avatar
  • 58.9k
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 ...
user avatar
  • 9,422
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 ...
user avatar
  • 9,422
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 43.4k
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 ...
user avatar
  • 2,981
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 "...
user avatar
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 ...
user avatar
  • 6,630
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 ...
user avatar
  • 1,869
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 1,869
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 ...
user avatar
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 ...
user avatar
  • 43.4k
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{...
user avatar
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 ...
user avatar

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