From Formal Systems to HoTT and Topos: Syntax, Foundations, Type-Theoretic Logic, and Internal Truth

This article traces a conceptual path from formal systems to modern structural foundations of mathematics. It begins with the distinction between alphabet, syntax, proof, semantics, and truth. The first claim is that truth is not denied, but truth is not the first raw layer of formalization: before truth-evaluation, there must be symbols, formation rules, and well-formed expressions. The article then distinguishes ordinary mathematical theories from foundations of mathematics. A foundation is a broad formal environment in which mathematical objects, proofs, and theories can be constructed and organized. Set theory is presented as a membership-based foundation, while type theory is presented as a foundation based on judgments, terms, types, contexts, and computation. The central technical part explains how logic is internalized in dependent type theory. Truth corresponds to the unit type, falsehood to the empty type, implication to function type, conjunction to product, disjunction to coproduct, universal quantification to dependent product, existential quantification to dependent sum, and negation to a function into the empty type. A constructive proof is then given of the double negation of excluded middle, showing that ¬¬(P∨¬P) is constructively provable even though P∨¬P is not generally constructively derivable. Finally, Homotopy Type Theory is introduced as the type-theoretic foundation in which identity types acquire a path-like interpretation and univalence expresses structural identity through equivalence. The article concludes by connecting this to category theory and topos theory, where logic is internalized categorically through subobjects and the truth-value object Ω.