‘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.’
(Louis Carroll, Through the Looking Glass)
|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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.
The classical subfields of mathematical logic are
By a convergence and unification of concepts that has been named computational trinitarianism, mathematical logic is equivalently incarnated in
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.
See also at categorical model theory.
type theory, logic
This “old logic” was famously criticized
Bart Jacobs, Categorical Logic and Type Theory, (1999) Elsevier