Lindenbaum–Tarski algebra

In mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentences of the theory (i.e., the quotient, under the equivalence relation ~ defined such that p ~ q exactly when p and q are provably equivalent in T). That is, two sentences are equivalent if the theory T proves that each implies the other. The Lindenbaum–Tarski algebra is thus the quotient algebra obtained by factoring the algebra of formulas by this congruence relation.

Not to be confused with Jónsson–Tarski algebra.

The algebra is named for logicians Adolf Lindenbaum and Alfred Tarski. It was first introduced by Tarski in 1935[1] as a device to establish correspondence between classical propositional calculus and Boolean algebras. The Lindenbaum–Tarski algebra is considered the origin of the modern algebraic logic.[2]

Operations

The operations in a Lindenbaum–Tarski algebra A are inherited from those in the underlying theory T. These typically include conjunction and disjunction, which are well-defined on the equivalence classes. When negation is also present in T, then A is a Boolean algebra, provided the logic is classical. If the theory T consists of the propositional tautologies, the Lindenbaum–Tarski algebra is the free Boolean algebra generated by the propositional variables.

Heyting algebras and interior algebras are the Lindenbaum–Tarski algebras for intuitionistic logic and the modal logic S4, respectively.

A logic for which Tarski's method is applicable, is called algebraizable. There are however a number of logics where this is not the case, for instance the modal logics S1, S2, or S3, which lack the rule of necessitation (⊢φ implying ⊢□φ), so ~ (defined above) is not a congruence (because ⊢φ→ψ does not imply ⊢□φ→□ψ). Another type of logics where Tarski's method is inapplicable are relevance logics, because given two theorems an implication from one to the other may not itself be a theorem in a relevance logic.[2] The study of the algebraization process (and notion) as topic of interest by itself, not necessarily by Tarski's method, has led to the development of abstract algebraic logic.

gollark: Anyway, I was thinking more along the lines of: the VM automagically™ discovers other listening VMs on the same network, or accepts manual connect commands from the user, and has, say, 16 ports for all the connected things.
gollark: How do you do screen IO/serial/whatever now?
gollark: It haunts my dreams, but otherwise no.
gollark: Interpreters, compilers, same* thing.
gollark: What more do you need?

See also

References
  1. A. Tarski (1983). J. Corcoran (ed.). Logic, Semantics, and Metamathematics — Papers from 1923 to 1938 — Trans. J.H. Woodger (2nd ed.). Hackett Pub. Co.
  2. W.J. Blok, Don Pigozzi (1989). "Algebraizable logics". Memoirs of the AMS. 77 (396).; here: pages 1-2
  • Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.