nLab disjunctive logic

Idea

Disjunctive logic is the internal logic of pre-lextensive categories. Roughly speaking this means it is cartesian logic, with conjunction and “provably-unique existential quantification”, together with “provably-disjoint disjunction”.

Definition

…

Example

The (coherent) theory of (geometric) fields is obtained from the axioms for the algebraic theory of commutative unital rings by adding the sequents

$$(0=1)\vdash \bot\,\text{ (nontriviality) and }\,\top \vdash_x ((x=0) \vee ((\exists y)(xy=1)))\quad.$$

Since inverse elements in a commutative ring are unique when they exist the second sequent involves a legitimate existential quantification plus a legitimate disjunction (due to the nontriviality) whence the resulting theory is (finitary) disjunctive.

Properties

…

Related entries

• extensive category

• disjoint union

• connected limit

category	functor	internal logic	theory	hyperdoctrine	subobject poset	coverage	classifying topos
finitely complete category	cartesian functor	cartesian logic	essentially algebraic theory
lextensive category		disjunctive logic
regular category	regular functor	regular logic	regular theory	regular hyperdoctrine	infimum-semilattice	regular coverage	regular topos
coherent category	coherent functor	coherent logic	coherent theory	coherent hyperdoctrine	distributive lattice	coherent coverage	coherent topos
geometric category	geometric functor	geometric logic	geometric theory	geometric hyperdoctrine	frame	geometric coverage	Grothendieck topos
Heyting category	Heyting functor	intuitionistic first-order logic	intuitionistic first-order theory	first-order hyperdoctrine	Heyting algebra
De Morgan Heyting category		intuitionistic first-order logic with weak excluded middle			De Morgan Heyting algebra
Boolean category		classical first-order logic	classical first-order theory	Boolean hyperdoctrine	Boolean algebra
star-autonomous category		multiplicative classical linear logic
symmetric monoidal closed category		multiplicative intuitionistic linear logic
cartesian monoidal category		fragment $\{\&, \top\}$ of linear logic
cocartesian monoidal category		fragment $\{\oplus, 0\}$ of linear logic
cartesian closed category		simply typed lambda calculus

Link

• category theory mailing list: discussion on extensive categories

References

The main reference on disjunctive logic is Johnstone (1979) which was inspired by a non-syntactic concept of Yves Diers. The elephant has some additional cursory remarks. Freyd (2002) gives disjunctive logic a short treatment under the name ‘alternating logic’ and discusses the theory of real closed fields as an example. Barr and Wells (1985) discuss the corresponding class of sketches without mentioning the syntactic side.

• Jiří Adámek, Jiří Rosický, Locally presentable and accessible categories, Cambridge UP 1994. (exercise 5f., p.238)

• Michael Barr, Charles Wells, Toposes, Triples and Theories , Springer Heidelberg 1985. (Reprinted as TAC reprint no.12 (2005); section 8.2, pp.292f)

• Peter Freyd, Cartesian Logic , Theor. Comp. Sci. 278 (2002) pp.3-21.

• Peter Johnstone, A Syntactic Approach to Diers’ Localizable Categories , pp.466-478 in Springer LNM 753 Heidelberg 1979.

• Peter Johnstone, Sketches of an Elephant II, Oxford UP 2002. (D1.3.6 p.834, D2.1.2(e) p.863, D2.2.6 p.872, D2.4.8 p.886)