🗄️
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
  • Natural deduction
  • Intuitionistic Natural Deduction
  • Rules of Inference for Intuitionistic Natural Deduction
  • Conjunction, Disjunction and Implication
  • Negation
  • Truth
  • Falsehood
  • Universal Quantification
  • Existential Quantification
  • Context
  • Structural Properties of Hypotheses
  • Proof Terms
  • Conjunction

Was this helpful?

  1. Logic
  2. 380-proof-theory

Natural deduction

PreviousMathematical proofNextNatural deduction

Last updated 4 years ago

Was this helpful?

In mathematical logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by the rules of inference.

In natural deduction, a proposition is deduced from a collection of premises by applying inference rules repeatedly.

In natural deduction, a proof is derived through a sequence of steps, each of which is deduced from a set of premises by applying an appropriate rule from the set of inference rules.

Natural deduction, here presented using the Fitch-style diagrams, is a framework for deriving proofs, based on a set of initial premises or on a set of assumptions, using a specific set of inference rules.

The rules of inference dictate the conditions needed for introduction or elimination of logical connectives. Each logical connective in IL, that is, its introduction or elimination, has a corresponding function in Haskell.

is a notational system for constructing formal proofs. A Fitch-style proof arranges the sequence of propositions that make up the proof into numbered rows, with assumptions indented for easier identification.

There are many schematic systems for representing natural deduction proofs, but Fitch's notation seems the most mealable for ASCII presentation.

In a Fitch diagram, a proof is presented as a sequence of steps, with each step justified by stating what rule of inference was applied to which lines.

Natural deduction

from: Automated Theorem Proving by Frank Pfenning, 2004, lecture notes

We explore ways to define logics, or, which comes to the same thing, ways to give meaning to logical connectives. Our fundamental notion is that of a judgment based on evidence. For example, we might make the judgment "It is raining" based on visual evidence. Or we might make the judgment "A -> A is true for any proposition A" based on a derivation.

The use of the notion of a judgment as conceptual prior to the notion of proposition has been advocated by Martin-Lof. Certain forms of judgments frequently recur and have therefore been investigated in their own right, prior to logical considerations.

Two that we will use are hypothetical judgments and parametric judgments, the latter of which sometimes called general judgments or schematic judgments.

A hypothetical judgment has the form B under hypothesis A. We consider this judgment evident if we are prepared to make the judgment B once provided with evidence for A.

Formal evidence for a hypothetical judgment is a hypothetical derivation where we can freely use the hypothesis A in the derivation of B. Note that hypotheses need not be used, and could be used more than once.

  [A]¹
   ⁝
   B
-------
A -> B

A parametric judgment has the form J for any a where a is a parameter which may occur in J. We make this judgment if we are prepared to make the judgment [O/a]J for arbitrary objects O of the right category. Here [O/a]J is the notation for substituting the object O for parameter a in the judgment J.

Formal evidence for a parametric judgment J is a parametric derivation with free occurrences of the parameter a.

In a Hilbert-style axiomatization of logic, we define a judgment 'A is true' without the use of hypothetical judgments. Hilbert-style systems rely on many axioms, while they have a few inference rules. When we make proof structure explicit in such an axiomatization, we arrive at combinatory logic.

A categorical logic arises when the basic judgment is not truth, but entailment, A |- B. Once again, presentations are highly economical and do not need to seek recourse in complex judgment forms. But derivations often require many hypotheses, which means that we need to lean rather heavily on conjunction here. Proofs are realized by morphisms which are an integral part of the machinery of category theory.

While these are interesting and in many ways useful approaches to logic specification, neither of them comes particularly close to capturing the practice of mathematical reasoning. This was Gentzen's point of departure for the design of a system of natural deduction.

From our point of view, this system is based on the simple judgment A is true, but relies critically on hypothetical and parametric judgments. In addition to being extremely elegant, it has the great advantage that one can define all logical connectives without reference to any other connective. This principle of modularity extends to the meta-theoretic study of natural deduction and simplifies considering fragments and extension of logics.

Since we will consider many fragments and extension, this orthogonality of the logical connectives is a critical consideration. There is another advantage to natural deduction, namely that its proofs are isomorphic to the terms in a λ-calculus via the Curry-Howard isomorphism, which establishes many connections to functional programming.

Finally, we arrive at the sequent calculus (also introduced by Gentzen in his seminal paper) when we split the single judgment of truth into two: A is an assumption and A is true. While we still employ the machinery of parametric and hypothetical judgments, we now need an explicit rule to state that A is an assumption is sufficient evidence for A is a true. The reverse, namely, that if A is true then A may be used as an assumption is the Cut rule which he proved to be redundant in his Hauptsatz.

For Gentzen, the sequent calculus was primarily a technical device to prove consistency of his system of natural deduction, but it exposes many details of the fine structure of proofs in such a clear manner that many logic presentations employ sequent calculi. The laws governing the structure of proofs, however, are more complicated than the CHI for natural deduction might suggest and are still the subject of study. We choose natural deduction as our definitional formalism as the purest and most widely applicable. Later we justify the sequent calculus as a calculus of proof search for natural deduction and explicitly relate the two forms of presentation.

Intuitionistic Natural Deduction

The system of natural deduction we describe is basically Gentzen's system NJ. The calculus of natural deduction was devised by Gentzen in the 1930's out of a dissatisfaction with axiomatic systems in the Hilbert tradition. Instead of a number of axioms and a small set of inference rules, valid deductions are described through inference rules only, which at the same time explain the meaning of the logical quantifiers and connectives in terms of their proof rules.

A language of first-order terms is built up from variables (x,y), function symbols (f,g), each with a unique arity, and parameters (a,b).

terms, t         := vars | params | function symbols
vars             := x, y, z, …
params           := a, b, c, …
function symbols := f(t₁, …, tₙ)
  • A constant c is a nullary function symbol, written c, instead of c()

  • We use t and s to range over terms

The language of propositions is built up from predicate symbols and terms:

proposition, A := predicate symbol | term
                | P(t₁, …, tₙ)
                | A ∧ A
                | A ∨ A
                | A → A
                | ¬A
                | ⟙
                | ⟘
                | ∀x.A
                | ∃x.A

predicate symbol := P, Q, …
  • A propositional constant P is a nullary predicate symbol, written P

  • We use A, B, C to range over propositions

  • the variable x is bound in propositions of the form ∀x.A and ∃x.A

  • (∧) and (∨) bind more tightly than (->)

  • It is convenient to assume that propositions have no free individual variables; we use parameters instead where necessary

The notation for substitution is [t/x]A for the result of substituting the term t for the variable x in A. Because of the restriction on occurrences of free variables, we can assume that t is free of individual variables, and thus capturing cannot occur.

The main judgment of natural deduction is C is true written as C true, from hypotheses A1 true, ..., An true. We'll model this as a hypothetical judgment, which means that certain structural properties of derivations are tacitly assumed, independently of any logical inferences.

  • Hypothesis: If we have a hypothesis A true than we can conclude A true

  • Weakening: Hypotheses need not be used

  • Duplication: Hypotheses can be used more than once

  • Exchange: The order in which hypotheses are introduced is irrelevant

Introduction and elimination inference rules must match in a certain way in order to guarantee that the rules are meaningful and the overall system can be seen as capturing mathematical reasoning.

  1. The first is a local soundness property: if we introduce a connective and then immediately eliminate it, we should be able to erase this detour and find a more direct derivation of the conclusion without using the connective. If this property fails, the elimination rules are too strong - they allow us to conclude more than we should be able to know.

  2. The second is a local completeness property: we can eliminate a connective in a way which retains sufficient information to reconstitute it by an introduction rule. If this property fails, the elimination rules are too weak - they do not allow us to conclude everything we should be able to know.

We provide evidence for local soundness and completeness of the rules by means of local reduction and expansion judgments, which relate proofs of the same proposition.

One of the important principles of natural deduction is that each connective should be defined only in terms of inference rules without reference to other logical connectives or quantifiers. We refer to this as orthogonality of the connectives. It means that we can understand a logical system as a whole by understanding each connective separately.

Rules of Inference for Intuitionistic Natural Deduction

  • Conjunction

    • introduction, ∧I

    • elimination

      • left, ∧E₁

      • right, ∧E₂

  • Disjunction

    • introduction

      • left, ∨I₁

      • right, ∨I₂

    • elimination, ∨E

  • Implication

    • introduction, →I

    • elimination, →E (MP)

  • Negation

    • introduction, ¬I

    • elimination, ¬E

  • Truth

    • introduction, TI

  • Falsum

    • elimination, ⟘E

  • Universal quantification

    • introduction, ∀I

    • elimination, ∀E

  • Existential quantification

    • introduction, ∃I

    • elimination, ∃E

CONJUNCTION

A true   B true       A ∧ B true       A ∧ B true
--------------- ∧I    ---------- ∧E₁   ---------- ∧E₂
   A ∧ B true           A true           B true


DISJUNCTION
                                               [A]ⁱ true  [B]ʲ true
                                                ⫶           ⫶
  A true           B true          A ∨ B true   C true     C true
---------- ∨I₁   ---------- ∨I₂    ---------------------------------- ∨Eᵢⱼ
A ∨ B true       A ∨ B true                    C true



IMPLICATION

 [A]¹ true
  ⫶
  B true            A true   A → B true
----------- →I¹    --------------------- MP
A → B true                B true



NEGATION

 [A]¹ true
  ⫶
  p true            A true    ¬A true
----------- ¬I¹     ------------------ ¬E
 ¬A true                  C true



TRUTH                        FALSE

                             ⟘ true
-------- ⟙I                 ------- ⟘E
⟙ true                       C true


UNIVERSAL QUANTIFICATION

[a/x]A true               ∀x. A true
------------ ∀Iᵃ          ------------ ∀E
  ∀x.A true               [t/x]A true



EXISTENTIAL QUANTIFICATION

                                       [[a/x]A true]
                                             ⫶
[t/x]A true              ∃x.A true        C true
------------ ∃I          ----------------------------- ∃Eᵃ
  ∃x.A true                        C true

Conjunction, Disjunction and Implication

These 3 have the usual inference rules.

Negation

In order to derive ¬A, we assume A and try to derive a contradiction, ⟘.

Thus, it seems that negation requires falsehood, and, in most literature on constructive logic, ¬A is seen as an abbreviation of A → ⟘.

In order to give a self-contained explanation of negation by an introduction rule, we employ a judgment that is parametric in a propositional parameter p: if we can derive any p from the hypothesis A we conclude ¬A.

The elimination rule follows from this view: if we know ¬A true and A true, then we can conclude any formula C true. This is Ex Falsum Quodlibet or the explosion principle: anything follows from a contradiction (falsum).

EFQ: (A ∧ ¬A) -> C

Truth

There is only the introduction rule for ⟙. Since we put no information into the proof of ⟙, we know nothing new if we have an assumption ⟙ and therefore we have no elimination rule and no local reduction.

It may also be helpful to think of ⟙ as a nullary conjunction: the introduction rule has 0 premisses instead of 2 and we correspondingly have 0 elimination rules instead of 2.

The local expansion allows the replacement of any derivation of ⟙ by ⟙I.

Falsehood

Since we should not be able to derive falsehood, there is no introduction rule for ⟘. Therefore, if we can derive falsehood, we can derive everything.

Note that there is no local reduction rule for ⟘E. It may be helpful to think of ⟘ as a nullary disjunction: we have 0 instead of 2 introduction rules and we correspondingly have to consider 0 cases instead of 2 in the elimination rule.

Even though we postulated that falsehood should not be derivable, falsehood could clearly be a consequence of contradictory assumption. For example, (A ∧ ¬A) -> ⟘ true is derivable.

Universal Quantification

The circumstances in which we consider ∀x.A to be true depend on the domain of quantification.

For example, if x ranges over ℕ, then we can conclude ∀x.A, if we can prove that the proposition A holds for all ℕ, [0/x]A, [1/x]A, [2/x]A, etc. With infinitely many premisses, such a rule would not be effective; thus, one usually retreats to rules such as induction.

However, in a general treatment of predicate logic we would like to prove statements which are true for all domains of quantification. Therefore, we can only say that ∀x.A is provable if [a/x]A is provable, for a new parameter a about which we can make no assumption; we instantiate ∀x.A with an new parameter, an object a, [a/x]A. The label a on the ∀-introduction rule is a reminder the parameter a must be fresh, that is, it may not occur in any undischarged assumption in the proof of [a/x]A or in ∀x.A itself. In other words, the derivation of the premis must be parametric in a.

Conversely, if we know ∀x.A, we know that [t/x]A for any term t. That is, if a proposition A holds for all terms x, then it surely holds for a term t.

Existential Quantification

We conclude that ∃x.A is true when there is a term t such that [t/x]A is true.

When we have an assumption ∃x.A we do not know for which t it is the case that [t/x]A holds. We can only assume that [a/x]A holds for some parameter a about which we know nothing else. Thus the elimination rule resembles the one for disjunction.

Context

Contexts Γ := · | Γ,u:A

  • · represents the empty context

  • Γ,u:A means adding the hypothesis A true, labelled u, to Γ

  • each label must occurs at most once in a context to avoid ambiguities

The main judgment can then be written as Γ |- A which can be expanded to a conjunction of hypothesis, u:B, v:C, ... |- A.

With these additional definitions, we get the familiar version of the rules of inference with contexts, such as Γ, Δ, etc.

We also have a new rule for hypotheses which was an implicit property of the hypothetical judgments before.

-------------- u
Γ,u:A, Δ |- A

Structural Properties of Hypotheses

The following properties hold for intuitionistic natural deduction:

Γ¹,u:A,  Γ²,v:B,  Γ³   |- C
----------------------------- EXCHANGE
Γ¹,v:B,  Γ²,u:A,  Γ³   |- C


Γ¹,     Γ²   |- C
----------------------------- WEAKENING
Γ¹,u:A, Γ²   |- C


Γ¹,u₁:A, Γ²,u₂:A, Γ³   |- C
----------------------------- CONTRACTION
Γ¹,u:A,  Γ²,      Γ³   |- C


Γ¹,u:A, Γ² |- C     Γ¹ |- A
----------------------------- SUBSTITUTION
Γ¹, Γ²     |- C

Proof Terms

The basic judgment of the system of natural deduction is the derivability of a formula A, written as |- A.

As has been noted by Howard (CHI), there is a strong correspondence between intuitionistic derivations and λ-terms. The formulas A then act as types classifying λ-terms. In the propositional case, this correspondence is an isomorphism: formulas are isomorphic to types and derivations are isomorphic to simply-typed λ-terms. These isomorphisms are also called programs-as-proofs and propositions-as-types.

The notation for derivations in natural deduction system: for example, if M represents a proof of A and N represents a proof of B, then the pair (M,N) represents the proof of A ∧ B by ∧I. We write Γ |- M : A to express that the judgment M is a proof term for A under hypotheses Γ.

We also repeat the local reductions and expansions from the previous section in the new notation. For local expansion we state the proposition whose truth must established by the proof term on the left-hand side. This expresses restrictions on the application of the expansion rules.

Conjunction

The proof term for a conjunction is the pair of proofs of the premises.

Γ |- M : A     Γ |- N : B
------------------------- ∧I
    Γ |- (M,N) : A ∧ B

Γ |- M : A     Δ |- N : B
-------------------------- ∧I
  Γ,Δ |- (M,N) : A ∧ B



Γ |- M : A ∧ B
----------------------- ∧Eʟ
Γ |- fst M : A


Γ |- M : A ∧ B
----------------------- ∧Eʀ
Γ |- snd M : B
https://en.wikipedia.org/wiki/Natural_deduction
Fitch diagrams