🗄️
math-debrief
  • Math Debrief
  • Math: TIMELINE
  • 100-fundamentals
    • debrief-name: math section-code: 000 section-name: general section-desc: Elementary topics pervasive
      • About Mathematics
      • abstraction-in-math
      • About Math
      • Axiom schema
      • Basic concepts in math
      • Collections
      • Elementary concepts in objects
      • Elements of mathematics
      • math-as-a-language
      • Mathematical structures
      • List of mathematics-based methods
      • Mathematics and Reality
      • Mathematics: General
      • Controversial mathematics
      • the-elements-of-math
      • What is mathematics
    • The foundation of mathematics
      • Mathematical foundations
      • Foundations of Mathematics
      • Axiomatization of mathematics
      • Foundational crisis of mathematics
      • Foundations
      • Hilbert's problems
      • impl-of-math-in-set-theory
      • Gödel's Incompleteness Theorem
      • Theorems in the foundations of mathematics
      • The list of FOM candidates
      • Logicism
    • Philosophy of mathematics
      • Constructive mathematics
      • Constructive mathematics
      • Metamathematics
      • Philosophy of mathematics
      • Schools of mathematics
    • terms
      • Terms
      • Arithmetic
      • Axiom
      • The Axiomatic Method
      • discrete-math
      • 201 Discrete mathematics
      • Euclidean space
      • Formal system
      • Function
      • Generalization
      • Geometry
      • Higher-order
      • Impredicativity
      • Level of measurement
      • Mathematical definition
      • FAQ
      • Mathematical function
      • Mathematical induction
      • Mathematical object
      • Mathematical object
      • Equivalent definitions of mathematical structures
      • Mathematics
      • Mathematical model
      • mathematical-notation
      • Mathematical pages
      • Mathematical terminology
      • Mathematical adjective
      • Numbers
      • plane
      • Primer: Set Theory
      • Mathematical primitive
      • Set
      • Space
      • theory
      • Variable
  • 200 Set and Set theory
    • Sets: Hierarchy
    • set.TERMS
    • SETS › TOPICS
    • 201 Set concepts
      • Mathematical collections
      • The notion of sets
      • Specification of sets
    • Set cardinality
      • Cardinality of the continuum
      • Cardinality
      • Set Cardinality
      • cardinality2
      • Set cardinality
    • Set operations
      • Disjoint sets
      • Overlapping sets
      • Product
      • set-interactions
      • Set qualities
      • Set relations
    • Set properties
      • Basic set properties
      • Set properties
    • Set relations
      • Basic set relations
      • Disjoint sets
      • Inclusion relation
      • Membership Relation
      • Set membership
    • Summary
      • Set FAQ
      • Sets: Summary
    • Set theories
      • Axiomatic set theory
      • Set Theories
      • Naive Set Theory
      • Morse-Kelley set theory
      • von Neumann-Bernays-Gödel Set Theory
      • Quine's New Foundations (NF)
      • Cantor's set theory
      • Zermelo-Fraenkel set theory
    • Axioms of set theory
      • axiom-of-choice
      • The Axiom of Extensionality
      • Axiom of infinity
      • axiom-of-pairing
      • Axiom of powerset
      • Axiom of Regularity
      • Axiom of replacement
      • Axiom of union
      • Axiom of well-ordering
      • axiom-schema-of-comprehension
      • Axiom Schema of Specification
      • Axioms of set theories
      • List of axioms in set theory
      • ZFC Axioms
    • Sets: Terms
      • Bell Number
      • Cardinal number
      • Class (set theory)
      • Closure
      • empty-set
      • Extended set operations
      • Extensions by definitions
      • Family of sets
      • Fundamental sets
      • fundamental-sets2
      • Georg Cantor
      • History of set theory
      • Implementation of mathematics in set theory
      • Indexed family of sets
      • Extensional and intensional definitions
      • Involution
      • list-of-axioms-of-set-theory
      • Implementation of mathematics in set theory
      • Set membership
      • Naive Set Theory
      • Number of relations
      • empty-relation
      • Set Partitioning
      • Powerset
      • Russell's paradox
      • Set-builder notation
      • Set equivalence
      • Set Notation in latex
      • Set notation
      • Set partition
      • Intensional and extensional set specification
      • Set notation
      • Basic concepts in set theory
      • set-theory
      • Set Types
      • set
      • subset
      • Transfinite number
      • Tuples
      • ur-elements
  • Relations
    • basic-concepts
      • algebraic-axioms
      • Elements of a relation
      • Types of Relations
      • Named Relations
      • Relation theory
      • Relations
      • Types of relations
    • Relations
      • Definitions
      • Reflexivity
      • Symmetry
      • Transitivity
    • relation-properties
      • Uniqueness properties of relations
    • Types of relations
      • Transitivity
      • Binary Relation
      • Congruence relation
      • Connex relation
      • axioms-sets-zfc
      • Endorelation
      • Equivalence relation
      • Euclidean
      • Finitary relation
      • Heterogeneous relation
      • Homogeneous relation
      • Transitivity
      • Partial equivalence relation
      • Transitivity
      • Transitivity
      • Reflexive relation
      • Reflexivity
      • Index of relations
      • Serial relation
      • Symmetry
      • Transitivity
      • Ternary relation
      • Trichotomy
      • Universal relation
      • Well-foundedness
    • terms
      • Relations
      • Binary relation
      • Relations
      • _finitary-rel
      • Relations: Overview
      • Relations
      • Index of relations
      • Binary relations
      • Composition of relations
      • Equivalence class
      • Notation
      • Relation
      • Relations
      • Sets: Summary
      • Aggregation: Sets, Relations, Functions
  • Order theory
    • Order theory
    • List of order structures in mathematics
    • List of order theory topics
    • Order theory
      • Hasse diagram
      • Order theory
      • ordered-set
      • Partial order
      • Partially ordered set
      • Total order
  • Function Theory
    • Function Theory: GLOSSARY
    • Function Theory: HIERARCHY
    • Function Theory: LINKS
    • Function Theory: TERMS
    • Function Theory: TOPIC
    • Function Theory: WIKI
    • _articles
      • about-functions
      • Function
      • Formal definition
      • Definition
      • constant
      • Introduction
      • Types of functions
      • Functions: Summary of Notations
      • Functions: Overview
      • Properties of functions
      • Function properties
      • Functions: Summary
      • Function
    • Abjections
      • Bijective function
      • Function (abjections)
      • Injective function
      • Surjective function
    • topics
      • Function: TERMS
      • Codomain
      • Composition of functions
      • Currying
      • Division of functions
      • Domain
      • Function fixed points
      • Function cardinality
      • Function definition
      • Elements of a function
      • Function in mathematics
      • Function notion
      • Function operations
      • Function properties
      • Functional statements
      • Functions in programing languages
      • Image and Preimage
      • Image
      • Inverse function
      • Notion of functions
      • Number and types of functions between two sets
      • Operation
      • Range
      • Successor function
      • Time complexity classes
  • debrief-name: math section-code: 280 section-name: domain-theory section-desc:
    • Domain theory: LINKS
    • Domain theory
  • Logic
    • Logic: CHRONO TERMS
    • Logic: CLUSTERS
    • lo.GLOSSARY
    • Logic: Wiki links
    • 305-basic-concepts
      • Introduction to Logic
      • Argumentation
      • Logic: Basic terminology
      • Logic: Terminology
      • Truth function
      • Truth function
    • README
      • Mathematical Logic
      • Types of Logic
      • BHK interpretation
      • FOL
      • Index of Logic Forms
      • History of logic
      • Logic Indices
      • Interpretation of symbols in logic and math
      • logic-systems
      • Mathematical Logic: People and Events
      • Index of logical fallacies
      • Logical symbols
      • Mathematical conjecture
      • Mathematical induction
      • Mathematical lemma
      • Mathematical Logic
      • Mathematical proof
      • Mathematical theorem
      • Mathematical theory
      • Monotonicity of entailment
      • Satisfiability Modulo Theories
      • Sequent Calculus
      • Sequent
      • Tableaux
      • Truth tables
    • 360-propositional-logic
      • Propositional Logic
      • Propositional Logic
    • 370-predicate-logic
      • Predicate Logic
      • First-order logic
      • Predicate calculus
      • Examples of predicate formulae
    • 380-proof-theory
      • Argument-deduction-proof distinctions
      • Direct proof
      • Mathematical induction
      • Mathematical induction
      • Mathematical proof
      • Natural deduction
      • Natural deduction
      • Proof by induction
      • Proof by induction
      • proof-calculus
      • Proof Theory
      • Structural induction
      • System L
      • Proof theory
    • Logic: Indices
      • Gödel's Incompleteness Theorem
      • The History of Mathematical Logic
      • forallx
      • Logic for CS
      • Lectures in Logic and Set Theory
      • _logicomix
    • Logic
      • Logical connectives
      • Logical equivalence
    • Rules of Inference
      • WIKI
      • Conjunction elimination
      • Conjunction introduction
      • Cut rule
      • Disjunction elimination
      • Disjunction introduction
      • Disjunctive syllogism
      • Exportation
      • implication-elimination
      • implication-introduction
      • Rules of Inference: Index
      • Rules of inference
      • Rules of Inference for Natural Deduction
      • Logical Inference
      • Reiteration
      • Rule of inference
      • Structural rules
      • substitution
    • Logic
      • The principle of bivalence
      • The principle of explosion
      • The Law of Identity (ID)
      • Laws of thought
      • Properties of logic systems
      • List of laws in logic
      • The law of non-contradiction
    • Logic
      • Logic systems: LINKS
      • Logic system
      • logic-systems
      • logic-typ
      • logics-by-purpose
      • _logics
      • Affine logic
      • Algebraic logic
      • Bunched logic
      • Classical logic
      • Traditional first-order logic
      • Hoare logic
      • Linear logic
      • Modal logic
      • Non-monotonic logic
      • Syntax
      • Predicate logic
      • Propositional Logic
      • Relevance logic
      • Separation logic
      • Substructural logics
      • Syllogistic logic
    • Logic: Sections: Elementary
    • Logic: Topics
      • Pages in Logic
      • Logic ❱ Terms ❱ List
      • Logic ❱ Terms ❱ Definitions
      • Absoluteness
      • Assumption
      • Automated theorem proving
      • Canonical normal form
      • Categorical proposition
      • Classical linear logic
      • Consequence
      • Decidability
      • Deduction systems
      • deduction-theorem
      • Deductive reasoning
      • Diagonal lemma
      • Fallacy
      • Fitch notation
      • Formal language
      • formal-system
      • Formalism
      • Formula
      • functionally complete
      • Hilbert system
      • Hoare logic
      • horn-clause
      • Mathematical induction
      • Induction
      • Inductive Reasoning
      • Intuitionistic logic
      • Intuitionistic logic
      • Intuitionistic logic
      • Judgement
      • Judgments
      • Linear logic
      • Logic in computer science
      • Logic
      • Logical connective
      • Logical consequence
      • Logical constant
      • Logical form
      • axioms-sets
      • Logical reasoning
      • Ludics
      • Non-logical symbol
      • Predicate
      • Premise
      • Quantification
      • Realizability
      • Boolean satisfiability problem
      • DPLL algorithm
      • Satisfiability
      • Semantics of logic
      • Skolemization
      • SAT and SMT
      • Syntax
      • Tautology
      • Term
      • Unification
      • Validity
  • 510 Lambda Calculi
    • Lambda Calculus: GLOSSARY
    • Lambda calculi: LINKS
    • Lambda Calculus: OUTLINE
    • Lambda Calculus: Basic concepts
      • Introduction
      • Lambda expressions
      • Free variables
    • Lambda Calculi
      • Lambda calculus: LINKS
      • Lambda calculus combinators in Haskell
      • Lambda calculus: Combinators
      • Combinators
      • combos-all.js
      • combos-bird.js
      • combos-birds-list.js
      • combos-birds.js
      • Fixed-point combinator
      • Fixpoint operator
      • Lambda calculus: Fixpoint
    • combinatory-logic
      • algebraic-structures
      • Combinatory logic
      • Combinatory logic
      • relation-classification
      • 04-definition
    • Lambda calculus encoding schemes
      • bohm-berarducci-encoding
      • Index of Church encodings
      • Church encodings
      • Church Numerals
      • Encoding data structures
      • Encoding schemes in lambda calculi
      • Lambda encoding
      • Mogensen-Scott encoding
      • Parigot encoding
      • encodings
        • Encoding data structures
        • Encoding of Data Types in the λ-calculus
        • church-booleans
        • Church data structures
        • Church encoding
        • Church Numerals: Church encoding of natural numbers
        • Lambda Calculus: Church encoding
        • Lambda Calculus: Church encoding
        • church-numerals
        • Lambda Calculus: Church encoding: Numerals
        • Church pair
        • Pair
        • Lambda Calculus: Church encoding
        • Alternative encodings
        • Encoding schemes
        • Encoding schemes
        • Encodings in Untyped Lambda Calculus
        • Lambda calculus
        • Scott encoding
        • Lambda calculus: Scott encoding
    • lambda-calculus-evaluation
      • Call-by-name
      • Call-by-need
      • Call-by-value
    • lambda-calculus-forms
      • Beta normal form
      • Lambda terms
      • Fixity of lambda-terms
    • lambda-calculus-reductions
      • Alpha conversion
      • Beta reduction
      • Delta reduction
      • Eta conversion
      • Eta conversion
      • Lambda calculus: η-conversion
    • lambda-calculus
      • Alonzo Church
      • Inference rules for lambda calculus
      • Lambda Calculus: Introduction
      • Lambda abstraction
      • Lambda application
      • Lambda Calculus: Definition
      • About λ-calculus
      • Type inference
      • Lambda Calculus
      • Lambda Calculus: Introduction
      • Introduction to λ-calculus
      • Lambda calculus
      • Definition of Lambda Calculus
      • Functions in lambda calculus
      • History of Lambda Calculus
      • Using the Lambda Calculus
      • Name capturing
      • Variable occurrences
      • Variables
    • Lambda Calculus
      • Church-Rosser theorem
      • Curry's paradox
      • De Bruijn index
      • de Bruijn notation
      • Deductive lambda calculus
      • Kleene-Rosser paradox
      • Aspects of the lambda calculus
      • Function Refactoring
      • Lambda lifting
      • Let expression
      • Reduction strategy
      • Substitution
    • typed-lambda-calculi
      • Lambda Cube
      • Simply typed lambda calculus
      • System F
      • Typed lambda calculi
  • Type theory
    • Type Theory: GLOSSARY
    • Type theorists
    • Type Theory: SUMMARY
    • TERMS: Type Theory
      • Types
      • History of type theory
      • History of Type Theory
    • curry-howard-correspondence
      • The Curry-Howard Correspondence in Haskell
      • Curry-Howard correspondence
      • Curry-Howard correspondence
      • Curry-Howard correspondence
      • Curry-Howard-Lambek correspondence - HaskellWiki
    • dependent-types
      • Dependent type
      • Dependent type
    • Hindley-Milner type-system
      • Hindley-Milner type system
      • Monomorphism vs polymorphism
      • Let-polymorphism
      • The Hindley-Milner type system
      • Algorithm W in Haskell
      • Hindley-Milner Type Inference: W Algorithm
      • hindley–milner-type-system
      • Hindley-Milner type system
      • HM inference examples
      • HM in ML
      • Type Inference
    • Homotopy type theory
      • Homotopy type theory
      • Univalent Type theory as the foundations of mathematics
    • Intuitionistic type theory
      • Inductive definition
      • Inductive type
      • Intuitionistic type theory
    • Type Theory
      • TTTools
      • Coinduction
      • Impredicativity
      • Lean
      • Subsumption
    • Type Theory : Topics
      • Type Theory : Terms
      • Recursion types
      • Recursive data type
      • Subtyping
      • Type Class
      • Type Equivalence
      • Type Inference
      • Type rule
      • Type system
      • Variance
    • type-theories
      • Calculus of Constructions
      • Constructive type theory
      • ramified-type-theory
      • simple-type-theory
      • Substructural type systems
    • type-theory-general
      • Linear types
      • History of Type Theory
      • Type Theory
      • Overview
      • Type Theory
  • Abstract Algebra
    • 410-group-theory
      • Abelian group
    • algebras
      • Associative Algebra
      • Field
      • Group-like algebraic structures
      • group
      • Lattice
      • Magma
      • monoid
      • Overview of Algebras
      • Quasigroup
      • Rack and quandle
      • Ring
      • Semigroup
      • Algebra of sets
      • Setoid
    • boolean-algebra
      • Boolean algebra
      • Axioms in Boolean Algebra
      • Boolean algebra
      • Boolean Algebra Laws
      • Boolean Algebra Laws
      • Two-element Boolean algebra
      • Boolean algebra
      • Boolean domain
    • terms
      • Algebra
      • Axioms of abstract algebra
      • Algebraic notation for algebraic data types
      • Algebraic structure
      • Algebraic structure
      • Field of sets
      • Homomorphism
      • Isomorphism
      • Algebraic structures
      • Mathematical structure
      • Polynomials
      • Relation algebra
  • Category Theory
    • CT GLOSSARY
    • Category Theory: OUTLINE
    • CT SUMMARY
    • A First Introduction to Categories (2009)
      • Sets, maps, composition
      • 02-history
      • axioms-logic
      • Bijection of functions
      • Commutative diagram
      • Directed graph
      • CT prerequisites
      • String diagram
      • Transitive closure
    • Category Theory Fundamentals
      • Introduction
      • Interpretation
      • Fundamental concepts
      • Category theory
      • Category
      • Category Theory: Definitions
    • Key concepts
      • Duality
      • Functor
      • Homeset
      • Initial Object
      • Morphism
      • Natural transformation
      • Object
      • Terminal Object
    • Categorical constructions
      • Categorical constructions
      • Coproduct
      • Diagram
      • Product
      • Universal construction
    • Types of categories
      • Concrete category
      • Discrete category
      • Functor category
      • Groupoid
      • Hask
      • Kleisli category
      • Locally small category
      • Monoid
      • monoidal-categories.md
      • Index of named categories
      • Opposite category
      • Ordered category
      • Set category
      • Small category
      • Subcategory
    • Types of Functors
      • Adjoint functor
      • relation-arity
      • Endofunctor
      • Faithful functor
      • Forgetful functor
      • Hom functor
      • Identity functor
      • Inverse functor
      • Monad
      • Powerset functor
    • Types of Morphisms
      • Anamorphism
      • Automorphism
      • Catamorphism
      • Endomorphism
      • Epimorphism
      • Homomorphism
      • Hylomorphism
      • Idempotent morphism
      • Identity morphism
      • Inverse morphism
      • Isomorphism
      • Metamorphism
      • monomorphism
      • Natural isomorphism
      • Split morphism
    • 20-advanced-concepts
      • Coalgebra
      • (Co)Inductive types
      • Recursion Schemes
    • Category Theory
      • Category Theory: TERMS
      • Algebraic Data Types
      • Category Theory
      • Category
      • Coproduct
      • Function type
      • Functoriality
      • Initial Object
      • Limits and Colimits
      • Natural Transformation
      • 5. Products
      • Terminal Object
    • Category Theory :: Contents
      • CT :: Links
      • Category Theory :: Terms
      • Category :: Definition
      • F-Algebra
      • Functor
      • Initial object
      • Monoid
      • Natural Transformation
      • Number of morphisms
      • Terminal object
      • Transitive closure
      • Types of morphisms
      • Categories by cardinality
      • Types of functors
  • Number Theory
    • Invariance and Monovariance Principle
    • 615-arithmetic
      • Addition
      • Aliquot sum
      • Arithmetic function
      • Laws
      • Arithmetic operations
      • Index of arithmetic operations
      • Arithmetic operations
      • Arithmetic
      • Divisibility rules
      • Divisibility
      • division
      • Divisor Function
      • Divisor Summatory Function
      • Divisor
      • Euclidean division
      • Hyperoperations
      • hyperops
      • Modular arithmetic
      • Multiplication
      • Number Theory: primer in numbers
      • Percentage
      • Rules of Divisibility
      • Subtraction
    • The fundamental sets of numbers
      • Algebraic numbers
      • Complex numbers
      • Fractions
      • Fundamental number sets
      • Imaginary numbers
      • Integers
      • Irrational numbers
      • Natural number
      • Rational numbers
      • Real numbers
      • Transcendental numbers
      • Ulam's spiral
      • The whole numbers
    • COUNTING THEORY
      • Counting Theory
      • counting
      • Fundamental Counting Rules
    • 630-combinatorics
      • Combinatorics
      • Combinations
      • Combinatorics
      • Counting theory
      • Counting theory
      • Enumerative combinatorics
      • Partition
      • Pascals triangle
      • Permutations
      • Twelvefold way
    • Probability theory
      • Statistics › Probability theory: Glossary
      • Statistics › Probability theory › Topics
      • Statistics › Probability theory › Wiki Links
      • Conditional Probability
      • Distribution
      • Probability theory
      • Probability
    • Number theory
      • euclids-lemma
      • gcd-lcm
      • Induction
      • Infinity
      • Numbers and numerals with interesting properties
      • Lagrange's four-square theorem
      • Matrix
      • Matrix
      • List of Number Systems
      • Number Theory
      • Number Theory with Glenn Olsen
      • Number
      • Arithmetic
      • Numbers
      • numeral-prefixes
      • Numeral system
      • Numeral
      • Ordinal numbers
      • Parity
      • Peano axioms
      • Polynomial
      • Polynomial
      • Positional notation
      • Probability
      • Symbol
      • Well Ordering Principle
    • topics
      • Coprimality
      • Facorization of composite numbers
      • Fundamental Theorem of Arithmetic
      • Prime factorisation
      • Prime number
      • Prime numbers
  • Theory of computation
    • Theory of computation: Abbreviations
    • Theory of computation: CHRONOLOGICAL TOPICS
    • Theory of computation: GLOSSARY
    • Theory of Computation: HIERARCHY
    • Theory of computation: LINKS
    • Theory of computation: TERMS
    • Theory of computation: TOPICS
    • Theory of computation: WIKI
    • Theory of Computation
      • _toc-more
      • Theory of Computation
    • 610-automata-theory
      • Abstract machine
      • Automata Theory
      • Automaton
      • Edit distance
      • Finite-state Machine
      • Automata Theory: WIKI
    • Formal systems
      • Abstract interpretation
      • Alphabet
      • Binary combinatory logic
      • Chomsky hierarchy
      • Epsilon calculus
      • Formal language
      • Iota and Jot
      • Regular expression
      • Regular Language
      • SKI combinator calculus
    • 621-grammar
      • Backus-Naur Form (BNF)
      • Context-free grammar
      • Context-sensitive grammar
      • Extended Backus–Naur Form (EBNF)
      • Regular Language
      • Terminal and nonterminal symbols
    • 622-syntax
      • Syntax
    • 624-semantics
      • Axiomatic semantics
      • Denotational Semantics: Summary
      • Denotational Semantics
      • Denotational Semantics
      • Denotational semantics
      • Formal semantics
      • Operational semantics
      • Semantics in CS
      • Semantics
    • 630-computability-theory
      • Computability (recursion) theory: TERMS
      • Computability (recursion) theory: TOPICS
      • Effective Computability
      • Church Thesis
      • Church-Turing Thesis
      • Computability theory
      • Computability
      • Computable function
      • Entscheidungsproblem
      • Halting problem
      • Machine that always halts
      • McCarthy Formalism
      • Super-recursive algorithm
      • Recursion theory
    • 632-recursive-function-theory
      • Recursion Theory
      • Ackermann function
      • General recursive function
      • Minimization operator
      • Partial functions
      • Recursion Function Theory
      • Sudan function
    • 634-primitive-recursive-functions
      • Primitive Recursive Function
      • Initial functions
      • The list of primitive recursive functions
      • Primitive combination
      • Primitive composition
      • Primitive recursion
      • Successor function
    • 640-models-of-computation
      • Models of computation: Summaries
      • Model of computation
    • 680-complexity-theory
      • Algorithmic Complexity
      • Complexity Theory
  • debrief-name: math section-code: 900 section-name: aggregations section-desc: Aggregations, indices,
    • Index of closures
    • List of mathematical entities
    • List of mathematical objects
    • Enumeration of mathematical structures
    • Math : Axioms as Formulae
    • 950-math-areas
      • Areas of mathematics
      • Areas of mathematics
    • 970-links
      • check
      • Math: Links
      • Math Debrief: Links
      • Math Primer: LINKS
      • Links
      • Math: LINKS: ncatlab
      • Math: LINKS
      • WIKI
      • WIKI
      • WIKI_ALL
      • Math: Wiki lists
      • Glossary of areas of mathematics
      • WIKI_collections
      • Mathematics for Computer Science
      • Mathematics Classification
      • math
      • Resources
      • Math on YouTubel Video Playlists
      • wiki resources
    • 980-hierarchy
      • HIERAR
      • Math: Hierarchy
      • Math HIERARCHY
      • classification
        • Mathematics
        • https://ncatlab.org/nlab/all_pages https://ncatlab.org/nlab/all_pages/reference https://ncatlab.org/
        • Math Classification and Topical Pages
        • Areas of mathematics
        • Areas of mathematics
        • Math Classification: CCS
        • Math hierarchy
        • Computational mathematics
        • Taxonomy: Mathematics
        • Areas of mathematics
        • Mathematics Subject Classification
        • Math fields
        • math-topics
        • Mathematics Subject Classification – MSC
        • MSC Classification Codes
        • mss-top-levels-filenames
        • MSC classification: Top Levels
        • Math classification
    • 990-appendix
      • Math glossary at ENCYCLOPÆDIA BRITANNICA
      • Bibliography
      • Math: Abbreviations
      • math.GLOSSARY
    • Math : Canon
      • Main branches of mathematics
      • Enumeration: Math paradigms
      • enum-math-symbols
      • List of mathematical theories
      • enum-algebras
        • Group-like algebraic structures
        • Group
        • Groupoid
        • magma
        • Monoid
        • Semigroup
      • enum-axioms-indices
        • 03-variants
        • axioms-relations
        • disjoint-sets
        • ordered-pair
      • enum-axioms
        • Axiom of Extensionality
        • Axioms
          • List of Axioms
          • List of Axioms
          • LINKS
          • Index of axioms
          • Index of axioms
          • List of Axioms
          • List of Axioms in Relations
          • _laws
          • Index of axioms
          • Index of properties
          • Axioms in Boolean Algebra
          • Axioms for the Real Numbers and Integers
          • Axioms for the Real Numbers and Integers
          • ZF Axioms
          • ZFC Axioms
          • Axioms in logic
          • Axioms in set theory
          • List of axioms in set theory
        • Axioms
          • Absorption
          • Annihilation
          • Associativity
          • Cancellation
          • Closure
          • Commutativity
          • Complement laws
          • Distributivity
          • Domination
          • Idempotency
          • identity
          • Invertibility
          • involution
          • Linearity
          • Monotonicity
          • Well-definedness
          • Well-formedness
          • Well-foundedness
          • Well-ordering
      • enum-inference-rules
        • Enumeration: Rules of Inference
        • Enumeration: Rules of Inference for Intuitionistic Natural Deduction
      • Math › Logic formulae
        • Logic formulas concerning functions
        • Logic formulas concerning orders
        • Logic formulas concerning relations
        • Logic formulas concerning sets
      • enum-logic-system-elements
        • Conjecture
      • enum-logic-system-properties
        • Completeness
        • Consistency
        • Decidability
      • enum-topical-hierarchies
        • Outline of category theory
    • Mathematical Lists and Indices
      • Index of algebraic structures
      • Math equations and formulas
      • The fundamental number sets
      • index-of-math-elements
      • Arity
      • List of binary relations
      • Pretty formulae
      • Index of integer sequences
      • List of conjectures
      • Mathematical objects
      • Theorems
      • List of mathematical theories
      • list-of-unsolved-problems
      • Lists of problems in math
      • People
      • list-of-quotes-and-phrases
    • Mathematical elements
      • Mathematical (elements): PAGES
      • Mathematical abstraction
      • Mathematical analysis
      • Mathematical argumentation
      • Mathematical axiom
      • Mathematical concept
      • Mathematical constant
      • Mathematical deduction
      • Mathematical definition
      • Mathematical element
      • Mathematical expression
      • Mathematical formula
      • Mathematical method
      • Mathematical model
      • Mathematical notation
      • Mathematical object
      • Mathematical primitive
      • Mathematical reasoning
      • Mathematical statement
      • Mathematical structure
      • Mathematical symbol
      • Mathematical synthesis
  • debrief-name: math section-code: 800 section-name: misc section-desc: Misc and unclassified mathemat
    • 810-statistics
      • STATISTICS: HIERARCHY
      • STATISTICS: TERMS
      • Statistics › Topics
      • Statistics WIKI LINKS
      • Mathematical Concepts
      • Linear Regression
    • 888-calculus
      • Calculus
      • Math › Calculus › TERMS
Powered by GitBook
On this page
  • 1900-1927
  • Origin of Russell's theory of types
  • The 1908 "ramified" theory of types[[edit][22]]
  • The axiom of reducibility and the notion of "matrix"[[edit][27]]
  • Truth tables[[edit][31]]
  • Russell's doubts[[edit][39]]
  • Theory of simple types[[edit][47]]
  • 1940s-present[[edit][59]]
  • References[[edit][81]]
  • Sources
  • Further reading

Was this helpful?

  1. Type theory
  2. TERMS: Type Theory

History of type theory

PreviousTypesNextHistory of Type Theory

Last updated 3 years ago

Was this helpful?

The type theory was initially created to avoid paradoxes in a variety of formal logics and rewrite systems. Later, type theory referred to a class of formal systems, some of which can serve as alternatives to naive set theory as a foundation for all mathematics. It has been tied to formal mathematics since Principia Mathematica to today's proof assistants.

1900-1927

Origin of Russell's theory of types

In a letter to (1902), announced his discovery of the paradox in Frege's .[[1]][13] Frege promptly responded, acknowledging the problem and proposing a solution in a technical discussion of "levels". To quote Frege:

Incidentally, it seems to me that the expression "a is predicated of itself" is not exact. A predicate is as a rule a first-level function, and this function requires an object as argument and cannot have itself as argument (subject). Therefore I would prefer to say "a concept is predicated of its own extension".[[2]][15]

He goes about showing how this might work but seems to pull back from it. As a consequence of what has become known as both Frege and Russell had to quickly amend works that they had at the printers. In an Appendix B that Russell tacked onto his (1903) one finds his "tentative" theory of types. The matter plagued Russell for about five years.[[3]][18]

[[4]][20] presents a historical synopsis of the origin of the theory of types and the "ramified" theory of types: after considering abandoning the theory of types (1905), Russell proposed in turn three theories:

  1. the zigzag theory

  2. theory of limitation of size,

  3. the no-class theory (1905-1906) and then,

  4. readopting the theory of types (1908ff)

Quine observes that Russell's intrduction of the notion of "apparent variable" had the following result:

the distinction between 'all' and 'any': 'all' is expressed by the bound ('apparent') variable of universal quantification, which ranges over a type, and 'any' is expressed by the free ('real') variable which refers schematically to any unspecified thing irrespective of type.

Quine dismisses this notion of "bound variable" as "pointless apart from a certain aspect of the theory of types".[[5]][21]

The 1908 "ramified" theory of types[[edit][22]]

The axiom of reducibility and the notion of "matrix"[[edit][27]]

But because the stipulations of the ramified theory would prove (to quote Quine) "onerous", Russell in his 1908 Mathematical logic as based on the theory of types[[6]][28] also would propose his [axiom of reducibility][29]. By 1910 Whitehead and Russell in their Principia Mathematica would further augment this axiom with the notion of a matrix - a fully extensional specification of a function. From its matrix a function could be derived by the process of "generalization" and vice versa, i.e. the two processes are reversible - (i) generalization from a matrix to a function (by using apparent variables) and (ii) the reverse process of reduction of type by courses-of-values substitution of arguments for the apparent variable. By this method impredicativity could be avoided.[[7]][30]

Truth tables[[edit][31]]

3.331 From this observation we get a further view - into Russell's Theory of Types. Russell's error is shown by the fact that in drawing up his symbolic rules he has to speak of the meanings of his signs.

3.332 No proposition can say anything about itself, because the propositional sign cannot be contained in itself (that is the whole "theory of types").

3.333 A function cannot be its own argument, because the functional sign already contains the prototype of its own argument and it cannot contain itself...

The notion of matrix-as-truth-table appears as late as the 1940-1950s in the work of Tarski, e.g. his 1946 indexes "Matrix, see: Truth table"[[9]][38]

Russell's doubts[[edit][39]]

Russell in his 1920 Introduction to Mathematical Philosophy devotes an entire chapter to "The axiom of Infinity and logical types" wherein he states his concerns: "Now the theory of types emphatically does not belong to the finished and certain part of our subject: much of this theory is still inchoate, confused, and obscure. But the need of some doctrine of types is less doubtful than the precise form the doctrine should take; and in connection with the axiom of infinity it is particularly easy to see the necessity of some such doctrine".[[10]][40]

Russell abandons the axiom of reducibility: In the second edition of Principia Mathematica (1927) he acknowledges Wittgenstein's argument.[[11]][41] At the outset of his Introduction he declares "there can be no doubt ... that there is no need of the distinction between real and apparent variables...".[[12]][42] Now he fully embraces the matrix notion and declares "A function can only appear in a matrix through its values" (but demurs in a footnote: "It takes the place (not quite adequately) of the axiom of reducibility"[[13]][43]). Furthermore, he introduces a new (abbreviated, generalized) notion of "matrix", that of a "logical matrix . . . one that contains no constants. Thus p|q is a logical matrix".[[14]][44] Thus Russell has virtually abandoned the axiom of reducibility,[[15]][45] but in his last paragraphs he states that from "our present primitive propositions" he cannot derive "Dedekindian relations and well-ordered relations" and observes that if there is a new axiom to replace the axiom of reducibility "it remains to be discovered".[[16]][46]

Theory of simple types[[edit][47]]

1940s-present[[edit][59]]

Gödel 1944[[edit][60]]

By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: " a has the property φ ", " b bears the relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399).".[[23]][62]

He concluded the (1) theory of simple types and (2) axiomatic set theory, "permit the derivation of modern mathematics and at the same time avoid all known paradoxes" (Gödel 1944:126); furthermore, the theory of simple types "is the system of the first Principia [Principia Mathematica] in an appropriate interpretation. . . . [M]any symptoms show only too clearly, however, that the primitive concepts need further elucidation" (Gödel 1944:126).

Curry-Howard correspondence, 1934-1969[[edit][63]]

de Bruijn's AUTOMATH, 1967-2003[[edit][69]]

Martin-Löf's Intuitionistic type theory, 1971-1984[[edit][72]]

Martin-Löf's theory uses inductive types to represent unbounded data structures, such as natural numbers.

Barendregt's lambda cube, 1991[[edit][77]]

References[[edit][81]]

  1. [^][82] Russell's (1902) Letter to Frege appears, with commentary, in van Heijenoort 1967:124-125.

  2. [^][83] Frege (1902) Letter to Russell appears, with commentary, in van Heijenoort 1967:126-128.

  3. [^][84] cf. Quine's commentary before Russell (1908) Mathematical Logic as based on the theory of types in van Heijenoort 1967:150

  4. ^ [Jump up to: a][87] [b][88] Quine's commentary before Russell (1908) Mathematical logic as based on the theory of types in van Heijenoort 1967:151

  5. [^][89] Russell (1908) Mathematical Logic as based on the theory of types in van Heijenoort 1967:153-182

  6. [^][90] cf. in particular p. 51 in Chapter II The theory of Logical Types and *12 The Hierarchy of Types and the Axiom of Reducibility pp. 162-167. Whitehead and Russell (1910-1913, 1927 2nd edition) Principia Mathematica

  7. [^][91] Post (1921) Introduction to a general theory of elementary propositions in van Heijenoort 1967:264-283

  8. [^][92] Tarski 1946, Introduction to Logic and to the Methodology of Deductive Sciences, Dover republication 1995

  9. [^][93] Russell 1920:135

  10. [^][94] cf. "Introduction" to 2nd edition, Russell 1927:xiv and Appendix C

  11. [^][95] cf. "Introduction" to 2nd edition, Russell 1927:i

  12. [^][96] cf. "Introduction" to 2nd edition, Russell 1927:xxix

  13. [^][97] The vertical bar " | " is the Sheffer stroke; cf. "Introduction" to 2nd edition, Russell 1927:xxxi

  14. [^][98] "The theory of classes is at once simplified in one direction and complicated in another by the assumption that functions only occur through their values and by the abandonment of the axiom of reducibility"; cf. "Introduction" to 2nd edition, Russell 1927:xxxix

  15. [^][99] These quotes from "Introduction" to 2nd edition, Russell 1927:xliv-xlv.

  16. [^][100] L. Chwistek, Antynomje logikiformalnej, Przeglad Filozoficzny 24 (1921) 164-171

  17. [^][101] F. P. Ramsey, The foundations of mathematics, Proceedings of the London Mathematical Society, Series 2 25 (1926) 338-384.

  18. [^][108] A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic 5 (1940) 56-68.

  19. [^][109] J. Collins, A History of the Theory of Types: Developments after the Second Edition of 'Principia Mathematica'. LAP Lambert Academic Publishing (2012). [ISBN][110] [978-3-8473-2963-3][111], esp. chs. 4-6.

Sources

  • Bertrand Russell (1903), The Principles of Mathematics: Vol. 1, Cambridge at the University Press, Cambridge, UK.

  • Bertrand Russell (1920), Introduction to Mathematical Philosophy (second edition), Dover Publishing Inc., New York NY, [ISBN][116] [0-486-27724-0][117] (in particular chapters XIII and XVII).

  • Alfred Tarski (1946), Introduction to Logic and to the Methodology of Deductive Sciences, republished 1995 by Dover Publications, Inc., New York, NY [ISBN][118] [0-486-28462-X][119]

  • Jean van Heijenoort (1967, 3rd printing 1976), From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, Cambridge, MA, [ISBN][120] [0-674-32449-8][121] (pbk)

    • Bertrand Russell (1902), Letter to Frege with commentary by van Heijenoort, pages 124-125. Wherein Russell announces his discovery of a "paradox" in Frege's work.

    • Gottlob Frege (1902), Letter to Russell with commentary by van Heijenoort, pages 126-128.

    • Bertrand Russell (1908), Mathematical logic as based on the theory of types, with commentary by [Willard Quine][122], pages 150-182.

    • Emil Post (1921), Introduction to a general theory of elementary propositions, with commentary by van Heijenoort, pages 264-283.

  • Alfred North Whitehead and Bertrand Russell (1910-1913, 1927 2nd edition reprinted 1962), Principia Mathematica to *56, Cambridge at the University Press, London UK, no ISBN or US card catalog number.

  • Ludwig Wittgenstein (republished 2009), Major Works: Selected Philosophical Writings, HarperCollins, New York. [ISBN][123] [978-0-06-155024-9][124]. Wittgenstein's (1921 in English), Tractatus Logico-Philosophicus, pages 1-82.

Further reading

  • W. Farmer, "The seven virtues of simple type theory", Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267-286.

Quine explains the ramified theory as follows: "It has been so called because the type of a function depends both on the types of its arguments and on the types of the apparent variables contained in it (or in its expression), in case these exceed the types of the arguments".[[5]][23] in his 1952 Introduction to Metamathematics describes the ramified theory of types this way:

The primary objects or individuals (i.e. the given things not being subjected to logical analysis) are assigned to one type (say type 0), the properties of individuals to type 1, properties of properties of individuals to type 2, etc.; and no properties are admitted which do not fall into one of these logical types (e.g. this puts the properties 'predicable' and 'impredicable' ... outside the pale of logic). A more detailed account would describe the admitted types for other objects as relations and classes. Then to exclude definitions within a type, the types above type 0 are further separated into orders. Thus for type 1, properties defined without mentioning any totality belong to order 0, and properties defined using the totality of properties of a given order belong to the next higher order. ... But this separation into orders makes it impossible to construct the familiar analysis, which we saw above contains impredicative definitions. To escape this outcome, Russell postulated his , which asserts that to any property belonging to an order above the lowest, there is a coextensive property (i.e. one possessed by exactly the same objects) of order 0. If only definable properties are considered to exist, then the axiom means that to every impredicative definition within a given type there is an equivalent predicative one (Kleene 1952:44-45).

In 1921, would develop a theory of "truth functions" and their truth tables, which replace the notion of apparent versus real variables. From his "Introduction" (1921): "Whereas the complete theory [of Whitehead and Russell (1910, 1912, 1913)] requires for the enunciation of its propositions real and apparent variables, which represent both individuals and of different kinds, and as a result necessitates the cumbersome theory of types, this subtheory uses only real variables, and these real variables represent but one kind of entity, which the authors have chosen to call elementary propositions".[[8]][34]

At about the same time developed similar ideas in his 1922 work [Tractatus Logico-Philosophicus][36]:

Wittgenstein proposed the truth-table method as well. In his 4.3 through 5.101, Wittgenstein adopts an unbounded as his fundamental logical entity and then lists all 16 functions of two variables (5.101).

In the 1920s, [[17]][49] and [[18]][51] noticed that, if one is willing to give up the , the hierarchy of levels of types in the "ramified theory of types" can be collapsed.

The resulting restricted logic is called the theory of simple types[[19]][53] or, perhaps more commonly, simple type theory.[[20]][54] Detailed formulations of simple type theory were published in the late 1920s and early 1930s by R. Carnap, F. Ramsey, W.V.O. Quine, and A. Tarski. In 1940 (re)formulated it as .[[21]][57] and examined by Gödel in 1944. A survey of these developments is found in Collins (2012).[[22]][58]

in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote:

The is the interpretation of proofs-as-programs and formulae-as-types. The idea starting in 1934 with and finalized in 1969 with . It connected the "computational component" of many type theories to the derivations in logics.

Howard showed that the typed lambda calculus corresponded to intuitionistic (that is, natural deduction without the ). The connection between types and logic lead to a lot of subsequent research to find new type theories for existing logics and new logics for existing type theories.

created the type theory as a mathematical foundation for the Automath system, which could verify the correctness of proofs. The system developed and added features over time as type theory developed.

found a type theory that corresponded to by introducing , which became known as or Martin-Löf type theory.

The was not a new type theory but a categorization of existing type theories. The eight corners of the cube included some existing theories with at the lowest corner and the at the highest.

[^][85] cf. commentary by before Russell's (1908) Mathematical logic as based on the theory of types in van Hiejenoort 1967:150-153

[^][102] Gödel 1944, pages 126 and 136-138, footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938-1974, Oxford University Press, New York NY, [ISBN][103] [978-0-19-514721-6].

[^][105] This does not mean the theory is "simple", it means that the theory is restricted: types of different orders are not to be mixed: "Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded." Gödel 1944, pages 127, footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938-1974, Oxford University Press, New York NY, [ISBN][106] [978-0-19-514721-6].

[^][112] Gödel 1944:126 footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938-1974, Oxford University Press, New York NY, [ISBN][113] [978-0-19-514721-6].

Gottlob Frege
Bertrand Russell
Begriffsschrift
predicate
Russell's paradox
The Principles of Mathematics
Willard Quine
Stephen Kleene
impredicative
axiom of reducibility
Emil Post
propositional functions
Ludwig Wittgenstein
Sheffer stroke
Leon Chwistek
Frank P. Ramsey
vicious circle principle
Alonzo Church
simply typed lambda calculus
Kurt Gödel
Curry-Howard correspondence
Haskell Curry
William Alvin Howard
natural deduction
Law of excluded middle
Nicolaas Govert de Bruijn
Automath
Per Martin-Löf
predicate logic
dependent types
intuitionistic type theory
lambda cube
simply typed lambda calculus
calculus of constructions
W. V. O. Quine
104
107
114