nLab logic

‘Contrariwise,’ continued Tweedledee, ‘if it was so, it might be; and if it were so, it would be; but as it isn’t, it ain’t. That’s logic.’

(Lewis Carroll, Through the Looking Glass)

Idea

Traditionally, as a discipline, logic is the study of correct methods of reasoning. Logicians have principally studied deduction, the process of passing from premises to conclusion in such a way that the truth of the former necessitates the truth of the latter. In other words, deductive logic studies what it is for an argument to be valid. A second branch of logic studies induction, reasoning about how to assess the plausibility of general propositions from observations of their instances. This has often been done in terms of probability theory, particularly Bayesian.

Some philosophers, notably Charles Peirce, considered there to be third variety of reasoning for logic to study, namely, abduction. This is a process whereby one reasons to the truth of an explanation from its ability to account for what is observed. It is therefore sometimes also known as inference to the best explanation. At least some aspects of this can also be studied using Bayesian probability.

Deductive logic is the best developed of the branches. For centuries, treatments of the syllogism were at the forefront of the discipline. In the nineteenth century, however, spurred largely by the needs of mathematics, in particular the need to handle relations and quantifiers, a new logic emerged, known today as predicate logic.

As we said above, logic is traditionally concerned with correct methods of reasoning, and philosophers (and others) have had much to say prescriptively about logic. However, one can also study logic descriptively, taking it to be the study of methods of reasoning, without attempting to determine whether these methods are correct. One may study constructive logic, or a substructural logic, without saying that it should be adopted. Also psychologists study how people actually reason rapidly in situations without full information, such as by the fast and frugal approach.

A logic is a specific method of reasoning. There are several ways to formalise a logic as a mathematical object; see at Mathematical Logic below.

Mathematical logic

Mathematical logic or symbolic logic is the study of logic and foundations of mathematics as, or via, formal systems – theories – such as first-order logic or type theory.

Classical subfields

The classical subfields of mathematical logic are

• set theory

• model theory,

• recursion theory

• proof theory

Categorical logic

By a convergence and unification of concepts that has been named computational trinitarianism, mathematical logic is equivalently incarnated in

1. type theory

2. category theory

3. programming theory

The logical theory that is specified by and specifies a given category $\mathcal{C}$ – called its internal logic, see there for more details and also see internal language, syntactic category. – is the one

• whose types are the objects $A$ of $\mathcal{C}$;

• whose contexts are the slice categories $\mathcal{C}_{/A}$;

• whose propositions in context are the (-1)-truncated objects $\phi$ of $\mathcal{C}_{/A}$;

• whose proofs $A \vdash PhiIsTrue : \phi$ are the generalized elements of $\phi$.

Hence pure mathematical logic in the sense of the study of propositions is identified with (0,1)-category theory: where one concentrates only on (-1)-truncated objects. Genuine category theory, which is about 0-truncated objects, is the home for logic and set theory, or rather type theory, the 0-truncated objects being the sets/types/h-sets.

For instance,

• limits and colimits, exponentials, and object classifiers belong to the type theory;

• while their (-1)-truncation, in this order: intersections/(and), unions(or), implications, and subobject classifiers, belong to the logic.

Generally, (∞,1)-category theory, which is about untruncated objects, is the home for logic and types with a constructive notion of equality, the identity types in homotopy type theory.

See also at categorical model theory.

Entries on logic

• axiom of choice

• Boolean algebra

• Boolean algebra with operators

• boolean domain

• boolean function

• boolean-valued function

• classical logic

• constructive mathematics

• context

• dependence logic

• equality

• principle of equivalence

• excluded middle

• geometric logic

• Heyting algebra

• higher-order logic

• internal logic

• intuitionistic logic

• linear logic

• logicality and invariance

• minimal logic

• modal logic

• adjoint logic

  • algebraic models for modal logics
    • closure algebra
    • monadic algebra
    • temporal algebra
  • arrow logic
  • epistemic logic
    • the logic K(m)
    • the logic T(m)
    • the logic S4(m)
    • the logic S5(m)
  • frame (modal logic)
  • geometric models for modal logics
  • modal type theory
  • temporal logic

• negation

• Peirce's law

• predicate

• predicate logic

• predicative mathematics

• propositional logic

• relation

• team logic

• truth value

• type

• type theory

Related concepts

• mathematical logic

• logic symbols?

• type theory, logic

• 2-type theory, 2-logic

• (∞,1)-type theory, (∞,1)-logic

• objective and subjective logic

symbol	in propositional logic	Unicode
$:$	typing relation	U+003A
=	propositional equality relation	U+003D
$\neg$	logical negation operator	U+00AC
$\neg \neg$	double negation	U+00AC&U+00AC
$\nLeftarrow$, $\nleftarrow$	negation of converse implication, or negation of converse conditional	U+21CD, U+219A
$\nLeftrightarrow$, $\nleftrightarrow$	negation of logical equivalence, or negation of biconditional	U+21CE, U+21AE
$\nRightarrow$, $\nrightarrow$	negation of implication, or negation of conditional	U+21CF, U+219B
$\Leftarrow$, $\leftarrow$	converse implication, or converse conditional	U+21D0, U+2190
$\Rightarrow$, $\rightarrow$	implication, or conditional	U+21D2, U+2192
$\Leftrightarrow$, $\leftrightarrow$	logical equivalence, or biconditional	U+21D4, U+2192
$\wedge$	logical conjunctionoperator	U+2227
$\vee$	logical dysjunction operator	U+2228
$\neq$	inequality, or apartness relation	U+2260
$\vdash$	syntactic entailment relation	U+22A2
$\vDash$	semantic entailment relation	U+22A8
$\top$	truth value, or top element	U+22A3
$\bot$	false value, or bottom element	U+22A4
$\veebar$, $\oplus$	logical exclusive dysjunction operator	U+22BB, U+2295
$\bar{\wedge}$	logical non-conjunction operator	U+22BC
$\bar{\vee}$	logical non-dysjunction operator	U+22BD

symbol	in first-order logic	Unicode
$\forall$	universal quantifier	U+2200
$\exists$	existential quantifier	U+2203
$\exists!$	uniqueness quantifier	U+2203&U+0021
$\nexists$	negation of existential quantifier	U+2204

symbol	in set theory	Unicode
×	binary Cartesian product, or binary product	U+00D7
$\varnothing$	empty, or uninhabited set	U+2205
$\in$	membership relation	U+2208
$\notin$	negation of membership relation	U+2209
$\ni$	containment relation	U+220B
$\notni$	negation of containment relation	U+220C
$\prod$	n-ary Cartesian product, or product operator	U+220F
$\coprod$	n-ary disjoint union, or coproduct operator	U+2210
$\cap$	binary intersection operator	U+2229
$\cup$	binary union operator	U+222A
$\subset$	subset of relation	U+2282
$\supset$	superset of relation	U+2283
$\nsubset$	negation of subset relation	U+2284
$\nsupset$	negation of superset relation	U+2285
$\subseteq$	inclusion relation, or subset of, or equal to	U+2286
$\supseteq$	converse of inclusion relation, or superset of, or equal to	U+2287
$\sqcup$	binary disjoint union, or binary coproduct operator	U+2294
$\bigcap$	n-ary intersection operator	U+22C2
$\bigcup$	n-ary union operator	U+22C3

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in linear logic$\phantom{-}$
$\phantom{A}$$\top$	$\phantom{A}$additive truth
$\phantom{A}$$\bot$	$\phantom{A}$additive falsehood
$\phantom{A}$$0$	$\phantom{A}$multiplicative falsehood
$\phantom{A}$$1$	$\phantom{A}$multiplicative truth
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$
$\phantom{A}$$^\bot$$\phantom{A}$	$\phantom{A}$negation$\phantom{A}$

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in dependent type theory$\phantom{-}$	$\phantom{-}$propositions as types$\phantom{-}$
$\phantom{A}$$\to$	$\phantom{A}$function type	$\phantom{A}$implication
$\phantom{A}$$\times$	$\phantom{A}$product type	$\phantom{A}$conjunction
$\phantom{A}$$+$	$\phantom{A}$sum type	$\phantom{A}$disjunction
$\phantom{A}$$0$, $\emptyset$	$\phantom{A}$empty type	$\phantom{A}$false
$\phantom{A}$$1$	$\phantom{A}$unit type	$\phantom{A}$true
$\phantom{A}$$=$, $\mathrm{Id}$	$\phantom{A}$identity type	$\phantom{A}$propositional equality
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types	$\phantom{A}$logical equivalence
$\phantom{A}$$\sum$, $\Sigma$, $\times$	$\phantom{A}$dependent sum type	$\phantom{A}$existential quantifier
$\phantom{A}$$\prod$, $\Pi$, $\to$	$\phantom{A}$dependent product type	$\phantom{A}$universal quantifier
$\phantom{A}$$\mathrm{isContr}$	$\phantom{A}$is contractible type	$\phantom{A}$unique proof
$\phantom{A}$$\mathrm{isContr}(A + B)$	$\phantom{A}$sum type is contractible type	$\phantom{A}$exclusive disjunction
$\phantom{A}$$\mathrm{isContr}\left(\sum_{x:A} B(x)\right)$	$\phantom{A}$dependent sum type is contractible type	$\phantom{A}$uniqueness quantifier
$\phantom{A}$$\mathrm{ua}$	$\phantom{A}$univalence axiom	$\phantom{A}$propositional extensionality

References

General

For centuries, logic was Aristotle's logic of deduction by syllogism. In the 19th century the idea of objective logic as metaphysics was influential

• Hegel, Wissenschaft der Logik ( Science of Logic )

This “old logic” was famously criticized

• Bertrand Russell, Logic as the Essence of Philosophy, 1914

as opposed to the “new logic” of Peano and Frege, contemporary predicate logic.

Textbooks on mathematical logic:

• David Hilbert, Wilhelm Ackermann, Grundzüge der Theoretischen Logik, 4th ed. Springer Heidelberg 1959 [1928]

• Clarence I. Lewis, Cooper H. Langford, Symbolic Logic (1932), Dover (2000) [App. II pdf]

  (giving the first modern formalizations of modal logic)

• John Lane Bell, M. Machover, A Course in Mathematical Logic, North-Holland Amsterdam 1977. (ch. 10,§5) (ISBN:9780720428445)

• Jean-Yves Girard (translated and with appendiced by Paul Taylor and Yves Lafont), Proofs and Types, Cambridge University Press (1989) [ISBN:978-0-521-37181-0, webpage, pdf]

• Open Logic Project, The open logic text (pdf)

On categorical logic

• William Lawvere, Adjointness in Foundations, Dialectica 23 (1969), 281-296

• William Lawvere, Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, ed., Proc. New York Symp. on Applications of Categorical Algebra, pp. 1–14. AMS, 1970. (pdf)

• Michael Makkai and Gonzalo Reyes, First Order Categorical Logic: Model-theoretical methods in the theory of topoi and related categories, Lecture Notes in Math. 611, Springer-Verlag, 1977. re-written by Francisco Marmolejo in 2018 (web announcement, pdf)

• Pierre Cartier, Logique, catégories et faisceaux, Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p. (numdam)

• Joachim Lambek, Philip J. Scott, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7 (1986) [ISBN: 0-521-24665-2, pdf]

• Jim Lambek, Phil Scott, Reflections on the categorical foundations of mathematics (pdf)

• Saunders MacLane, Ieke Moerdijk, Sheaves in Geometry and Logic (1992)

• Bart Jacobs, Categorical Logic and Type Theory, (1999) Elsevier

• John Bell, The development of categorical logic (pdf)

• Jean-Pierre Marquis, Gonzalo Reyes, (2009) The History of Categorical Logic 1963-1977 (pdf, pdf)

• Samson Abramsky, Nikos Tzevelekos: Introduction to Categories and Categorical Logic, in New Structures for Physics, Lecture Notes in Physics 813, Springer (2011) 3–94 [doi:10.1007/978-3-642-12821-9_1, arXiv:1102.1313]

• Jean-Yves Girard, Lectures on Logic, European Mathematical Society (2011)

• Jacob Lurie, Categorical Logic, Lecture notes 2018 (web)

• Steve Awodey, Andrej Bauer: Introduction to categorical logic, lecture notes for a course at Carnegie Mellon University (January-April 2024) [web, 0:pdf, 1:pdf, 2:pdf, 3:pdf, 4:pdf]

Logic in natural languages

• Pieter A. M. Seuren, The logic of language, vol. II of Language from within; (vol. I: Language in cognition) Oxford University Press 2010

category: logic