Index

Overview

Below is an outline of the topics covered in my personal wiki. The aim is not for completeness, on all topics, but rather to provide the definitions that serve my research. As such some topics, such as Algebra, are only lightly covered, while topics closer to my research area, in type theory, should be covered more thoroughly, although still expect many notes to be stubs, rather than full encyclopedia entries.

Mathematical Meta-Frameworks

• Mathematics: Broadest domain of study.
• Foundations of Mathematics: Study of the axiomatic bases of mathematics.
• Philosophy of Mathematics: Investigation of mathematical ontology and epistemology.

Structural Frameworks

• Category Theory: Structural backbone for relating disparate mathematical domains.
  • Topos: Categories with internal logical structure.
  • Infinity-Topos: Higher-dimensional generalization for homotopy theory.
• Set Theory: Classical membership-based foundation.
• Algebra: Study of operations on sets (Group, Ring, Field).
  • Heyting Algebra: Algebraic structure of intuitionistic logic.
  • Boolean Algebra: Algebraic structure of classical logic.

Logic and Proof Systems

• Logic: Syntax and semantics of formal languages.
  • Propositional Logic: Zero-order logic of connectives.
  • Predicate Logic: Logic with quantification ($\forall$, $\exists$).
• Proof Theory: Study of the structure of formal proofs.
  • Natural Deduction: Introduction and elimination rule framework.
  • Curry-Howard Correspondence: Isomorphism between proofs and programs.
• Constructive Mathematics: Mathematics without the law of excluded middle.
  • BHK Interpretation: Constructive semantics.

Type Theory

• Type Theory: Foundational system using types as the primary objects.
  • Martin-Löf Type Theory: Predicative constructive framework.
    • Type Theory: Judgmental equality is restricted.
    • Extensional Type Theory: Equality reflection enabled.
  • Homotopy Type Theory: Merging type theory with homotopy theory.
    • Univalent Foundations: Foundations based on the Univalence Axiom.
    • Cubical Type Theory: Constructive, computational univalence.
    • Higher Inductive Type: Types with path constructors.

Geometric and Spatial Structures

• Topology: Study of continuous deformation.
  • Topological Space: Set-theoretic definition of continuity.
• Homotopy Theory: Identification of spaces via continuous paths.
  • Homotopy Group: Algebraic invariants of spaces.
  • Weak Infinity Groupoid: Categorical model for homotopy types.

Computational Theory

• Computer Science: Theory of information and computation.
  • Lambda Calculus: Formal basis for functional computation.
  • Programming Language Semantics: Meaning of formal languages.
  • Automata Theory: Theory of abstract machines.