Concept

Disjunction property

The property of a logic that whenever it proves A or B, it proves A or it proves B. The constructive system has it and classical logic does not, since it proves p or not-p without proving either half.

Named by 2 essays across one field — each of them below, with the objects they name alongside it.

Gluing two countermodels: p ∨ ¬p. Two small Kripke models, each refuting one half of a disjunction, and the model made by placing both above a new first stage, at which neither half is forced.

A proof that says which half

Classical logic proves p ∨ ¬p without any idea which half is true. The constructive system never does that: whenever it proves a disjunction, it proves one of the two halves. The reason is a picture — two countermodels placed side by side above a new first stage that forces neither — and the logics between the two lose the property exactly when their pictures are not allowed to be glued.

logic · Non classical logic

Which chains of truth values validate Gödel's disjunctions. A grid of Gödel's pigeonhole formulas in m letters against chains of n truth values, marking which chains validate which formula, forming a staircase where m exceeds n.

No table of truth values is enough

Two truth values decide classical logic. Gödel asked in 1932 whether some longer list of values could decide the constructive system, and answered with a pigeonhole: with n values, some two of n + 1 statements must share one, so a formula saying exactly that holds in every n-valued table and is not a theorem. The chains of truth values then descend forever, and what they share is a logic of its own — the logic of the real interval.

logic · Non classical logic

Named alongside it

The objects these essays reach for when they reach for this one.

Heyting algebra Intuitionistic logic Chain Constructive proof Excluded middle Exhaustive search Kripke model Many valued logic Pigeonhole principle Truth table

All concepts