‘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)
basic constructions:
strong axioms
further
(0,1)-category theory: logic, order theory
proset, partially ordered set (directed set, total order, linear order)
distributive lattice, completely distributive lattice, canonical extension
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit type |
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language
</table>
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 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.
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
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 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.
logic symbols?
type theory, logic
basic symbols used in logic
$\phantom{A}$symbol$\phantom{A}$ | $\phantom{A}$meaning$\phantom{A}$ |
---|---|
$\phantom{A}$$\in$ | $\phantom{A}$element relation |
$\phantom{A}$$\,:$ | $\phantom{A}$typing relation |
$\phantom{A}$$=$ | $\phantom{A}$equality |
$\phantom{A}$$\vdash$$\phantom{A}$ | $\phantom{A}$entailment / sequent$\phantom{A}$ |
$\phantom{A}$$\top$$\phantom{A}$ | $\phantom{A}$true / top$\phantom{A}$ |
$\phantom{A}$$\bot$$\phantom{A}$ | $\phantom{A}$false / bottom$\phantom{A}$ |
$\phantom{A}$$\Rightarrow$ | $\phantom{A}$implication |
$\phantom{A}$$\Leftrightarrow$ | $\phantom{A}$logical equivalence |
$\phantom{A}$$\not$ | $\phantom{A}$negation |
$\phantom{A}$$\neq$ | $\phantom{A}$negation of equality / apartness$\phantom{A}$ |
$\phantom{A}$$\notin$ | $\phantom{A}$negation of element relation $\phantom{A}$ |
$\phantom{A}$$\not \not$ | $\phantom{A}$negation of negation$\phantom{A}$ |
$\phantom{A}$$\exists$ | $\phantom{A}$existential quantification$\phantom{A}$ |
$\phantom{A}$$\forall$ | $\phantom{A}$universal quantification$\phantom{A}$ |
$\phantom{A}$$\wedge$ | $\phantom{A}$logical conjunction |
$\phantom{A}$$\vee$ | $\phantom{A}$logical disjunction |
$\phantom{A}$$\otimes$$\phantom{A}$ | $\phantom{A}$multiplicative conjunction$\phantom{A}$ |
$\phantom{A}$$\oplus$$\phantom{A}$ | $\phantom{A}$multiplicative disjunction$\phantom{A}$ |
For centuries, logic was Aristotle's logic of deduction by syllogism. In the 19th century the idea of objective logic as metaphysics was influential
This “old logic” was famously criticized
as opposed to the “new logic” of Peano and Frege, contemporary predicate logic.
The first textbook on mathematical logic is
Modern textbooks on mathematical logic include
William Lawvere, Adjointness in Foundations, Dialectica 23 (1969), 281-296
William LawvereEquality 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)
Pierre Cartier, Logique, catégories et faisceaux, Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p. (numdam)
Lambek, J.; Scott, P.J. (1986), Introduction to Higher Order Categorical Logic, Cambridge University Press.
Jim Lambek, Phil Scott, Reflections on the categorical foundations of mathematics (pdf)
Saunders MacLane, Ieke Moerdijk, Sheaves in Geometry and Logic
Bart Jacobs, Categorical Logic and Type Theory, (1999) Elsevier
Jean-Yves Girard, Lectures on Logic, European Mathematical Society 2011
Jean-Pierre Marquis, Gonzalo Reyes, (2009) The History of Categorical Logic 1963-1977 (pdf)
Last revised on July 3, 2018 at 03:15:07. See the history of this page for a list of all contributions to it.