Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Apartness relations between propositions

Zoltan A. Kocsis

Abstract

We classify all apartness relations definable in propositional logics extending intuitionistic logic using Heyting algebra semantics. We show that every Heyting algebra which contains a non-trivial apartness term satisfies the weak law of excluded middle, and every Heyting algebra which contains a tight apartness term is in fact a Boolean algebra. This answers a question of E. Rijke regarding the correct notion of apartness for propositions, and yields a short classification of apartness terms that can occur in a Heyting algebra. We also show that Martin-Löf Type Theory is not able to construct non-trivial apartness relations between propositions.

Apartness relations between propositions

Abstract

We classify all apartness relations definable in propositional logics extending intuitionistic logic using Heyting algebra semantics. We show that every Heyting algebra which contains a non-trivial apartness term satisfies the weak law of excluded middle, and every Heyting algebra which contains a tight apartness term is in fact a Boolean algebra. This answers a question of E. Rijke regarding the correct notion of apartness for propositions, and yields a short classification of apartness terms that can occur in a Heyting algebra. We also show that Martin-Löf Type Theory is not able to construct non-trivial apartness relations between propositions.
Paper Structure (9 sections, 23 theorems, 32 equations, 1 figure)

This paper contains 9 sections, 23 theorems, 32 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Notation and Preliminaries
  3. Heyting algebras
  4. Apartness terms
  5. Possible reducts
  6. Classification
  7. Type Theory
  8. Propositions-as-some-types
  9. Conventions

Key Result

Proposition 2.4

A superintuitionistic logic $L$ has an apartness (resp. tight apartness) relation between its propositions precisely if its Lindenbaum algebra $L'$ (which is a Heyting algebra) has an apartness (resp. tight apartness) term.

Figures (1)

  • Figure 1: Hasse diagram of the Rieger-Nishimura lattice.

Theorems & Definitions (32)

  • Definition 1.1
  • Definition 1.15
  • Definition 1.16
  • Definition 1.17
  • Definition 2.2
  • Proposition 2.4
  • Proposition 2.7
  • Proposition 2.8
  • Definition 3.1
  • Theorem 3.2: Rieger rieger-nishimura-lattice
  • ...and 22 more