Heyting arithmetic

In mathematical logic, Heyting arithmetic (sometimes abbreviated HA) is an axiomatization of arithmetic in accordance with the philosophy of intuitionism (Troelstra 1973:18). It is named after Arend Heyting, who first proposed it.

Introduction

Heyting arithmetic adopts the axioms of Peano arithmetic (PA), but uses intuitionistic logic as its rules of inference. In particular, the law of the excluded middle does not hold in general, though the induction axiom can be used to prove many specific cases. For instance, one can prove that ∀ x, y ∈ N : x = y ∨ x ≠ y is a theorem (any two natural numbers are either equal to each other, or not equal to each other). In fact, since "=" is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula p, ∀ x, y, z, … ∈ N : p ∨ ¬p is a theorem (where x, y, z… are the free variables in p).

History

Kurt Gödel studied the relationship between Heyting arithmetic and Peano arithmetic. He used the Gödel–Gentzen negative translation to prove in 1933 that if HA is consistent, then PA is also consistent.

Heyting algebra

In mathematics, a Heyting algebra is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b of implication such that c ∧ a ≤ b is equivalent to c ≤ a → b. From a logical standpoint, A → B is by this definition the weakest proposition for which modus ponens, the inference rule A → B, A ⊢ B, is sound. Equivalently a Heyting algebra is a residuated lattice whose monoid operation a⋅b is a ∧ b; yet another definition is as a posetal cartesian closed category with all finite sums. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

As lattices, Heyting algebras are distributive. Every Boolean algebra is a Heyting algebra when a → b is defined as usual as ¬a ∨ b, as is every complete distributive lattice satisfying a one-sided infinite distributive law when a → b is taken to be the supremum of the set of all c for which a ∧ c ≤ b. The open sets of a topological space form such a lattice, and therefore a (complete) Heyting algebra. In the finite case every nonempty distributive lattice, in particular every nonempty finite chain, is automatically complete and completely distributive, and hence a Heyting algebra.

Boolean algebra

In mathematics and mathematical logic, Boolean algebra is the branch of algebra in which the values of the variables are the truth values true and false, usually denoted 1 and 0 respectively. Instead of elementary algebra where the values of the variables are numbers, and the main operations are addition and multiplication, the main operations of Boolean algebra are the conjunction and, denoted ∧, the disjunction or, denoted ∨, and the negation not, denoted ¬. It is thus a formalism for describing logical relations in the same way that ordinary algebra describes numeric relations.

Boolean algebra was introduced by George Boole in his first book The Mathematical Analysis of Logic (1847), and set forth more fully in his An Investigation of the Laws of Thought (1854). According to Huntington, the term "Boolean algebra" was first suggested by Sheffer in 1913.

Boolean algebra has been fundamental in the development of digital electronics, and is provided for in all modern programming languages. It is also used in set theory and statistics.