REVIEW 2 major objections 4 minor 19 references
Dependent Types Simplified
T0 review · 2 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash
Pith's one-line read Two minimal dependent type systems are proved sound against set-theoretic interpretations, putting their consistency on par with ZFC.
desk verdict A sound, genuinely new semantics-first dependent type system; the abstract oversells Part 2, but the core mathematics is honest and deserves a serious referee. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The machinery is the term language together with its interpretation in the cumulative set hierarchy. Let an assignment of sets to constants and variables be extended so that $\rho R$ is the dependent product $\prod \llbracket R \rrbracket$, $\beta R S$ is the application $\llbracket R \rrbracket(\llbracket S \rrbracket)$, and $\lambda x R S$ is the function sending each $r \in \llbracket R \rrbracket$ to $\llbracket S \rrbracket$ with $x$ valued at $r$; $\alpha$-conversion classes form the statements. The semantic consequence relation $\vDash$ quantifies over all such interpretations, and the syntactic relation $\vdash$ is the smallest sequent closed under the two rules inherited from application and abstraction. The soundness proofs work by showing each inference rule just restates the definition of the corresponding set operation. In the second system the same pattern is carried out with universes $H(\kappa)$ — the family of sets of hereditary cardinality less than $\kappa$ — and product operators typed between them.
What would settle it
Derive a typing statement $t : \bot$ from the empty context in either system using the stated rules and axioms; soundness would force $\llbracket t \rrbracket \in \emptyset$ in every interpretation, which is impossible unless set theory itself is inconsistent. A more local test is to find a finite context $\Gamma$ and statement $X$ such that $\Gamma \vdash X$ by Definition 8.1 or 14.6 but one explicit assignment of sets to constants and variables models $\Gamma$ and fails $X$. For the second system, deriving $u_n : u_n$ for any $n$ would contradict the well-foundedness of membership used in Proposition 11.4.
Extended reading notes
Core claim
The paper's central claim is that dependent type theory can be rebuilt from the ground up with a set-theoretic semantics rather than a categorical or syntactic one. In the first system, terms are strings over six symbols built from constants and variables by dependent products ($\rho$), application ($\beta$), and abstraction ($\lambda$); an interpretation sends each term to a set, and a typing statement $S:P$ is satisfied when the interpretation of $S$ lies in the interpretation of $P$. The inference relation $\vdash$ of Definition 8.1 is generated by just an application rule and an abstraction rule, and Proposition 8.2 proves $\vdash \subseteq \vDash$, soundness. A second system adds a hierarchy of universes $u_n$ and polymorphic product operators $p^m_n$, with reduction and sub-reduction statements, and Proposition 14.7 proves the same soundness. Consequently, if either system proved a statement of the form $t:\bot$, the ambient set theory would already be inconsistent.
Load-bearing premise
The load-bearing premise is that the ambient set-theoretic universe is consistent and well-founded: the paper proves relative consistency, not absolute consistency, so a failure of ZFC would make both type systems inconsistent too.
Editorial extensions
If this is right
- Every derivable typing statement in either system holds in all set-theoretic interpretations, so neither system can derive a contradiction without ZFC being inconsistent.
- For the first system, type inference is decidable: for a finite context and term, the set of derivable predicates is finite, computable, and unique up to alpha-conversion when typed in contexts.
- The canonical interpretations of the second system realize each universe above the bottom one as a model of ZFC minus the power set axiom, using only ZFC background assumptions rather than large cardinals.
- The specification language of the second system pins down structures such as equality, Cartesian products, logical conjunction, and universal quantification up to the intended bijections, via reduction and recursion typing statements.
Reading between the lines
- Beyond the paper: a completeness theorem is the obvious next step and is left open in the paper's final section.
- Beyond the paper: the double-negation truncation for the universal quantifier provides a template for importing classical connectives into a predicative type theory without splitting the language into propositions and types.
- Beyond the paper: a proof assistant built on these systems could treat kernel bugs as ZFC inconsistencies, making consistency arguments auditable by set-theoretic methods.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper develops two dependent type systems with set-theoretic semantics. Part 1 presents a minimal language (constants, variables, ρ, β, λ) and defines an inference relation ⊢ as the smallest sequent satisfying application and abstraction rules; the main result is soundness (⊢⊆⊨) with respect to interpretations in ZFC. It also proves type inference and unique typing for contexts. Part 2 adds a hierarchy of sorts u_n and polymorphic product operators p^n_m, defines canonical interpretations using regular sequences of cardinals and H(κ), and proves a soundness theorem (Prop 14.7) for a sequent calculus with reduction and sub-reduction rules. Several specifications (equality, Cartesian product, conjunction, universal quantifier) are shown semantically complete over canonical models. The paper claims these systems are 'comparable to ZFC' in simplicity and semantics.
Significance. If the soundness results hold, the systems are consistent relative to ZFC, and the semantic approach provides a clear bridge between type theory and set theory. The soundness proofs are detailed and the inference rules are derived from semantic properties rather than postulated. The type-inference result for Part 1 and the completeness proofs for the specifications are substantive. The main limitation is that the systems are not shown to be usable foundations: the paper defers type inference for Part 2, normalisation, semantic completeness, and a complete axiom/specification list for ZFC to future work.
major comments (2)
- [Abstract; §15] The abstract's claim that the two systems are 'comparable to ZFC' is not substantiated by the formal results. The paper proves soundness (Props 8.2, 14.7) and semantic completeness of certain specifications, but §15 explicitly defers type inference for Part 2, normalisation, semantic completeness, and a complete axiom/specification set for ZFC. No theorem shows that the systems have the deductive strength of ZFC or can formalise ZFC. The abstract and introduction should either prove such a result or temper the claim, e.g., to 'comparable to ZFC in simplicity and natural set-theoretic semantics'.
- [§8, after Prop 8.9] The claim that for finite Γ the typing set ⌈S⌉^Γ is finite and computable is stated without proof. The recursive definition of ⌈·⌉^Γ_n does not by itself guarantee that the union over n stabilises; a proof of finiteness (or a precise complexity bound) is needed to support the advertised type-inference property.
minor comments (4)
- [Definition 11.3] The definition of 'regular sequence' does not explicitly require the sequence (κ_n) to be strictly increasing, but the proofs of Props 11.4 and 11.5 use monotonicity (e.g., κ_{m+1} ≤ κ_n for m<n). Please add 'strictly increasing' to the definition or prove it from the condition.
- [Prop 8.6] In the proof of Proposition 8.6, 'Φ, (x : Q)' should be 'Φ, (y : Q)' in the λ-case paragraph.
- [Definition 14.6] The (Ab) rule in Definition 14.6 uses the side condition Γ ⊢ (Q:u_m), which refers to the relation being defined. The soundness proof (Prop 14.7) is only 'immediate' if one spells out the inductive construction of ⊢ as the least fixed point and proves by induction that each stage is contained in ⊨. Please make this explicit.
- [§11] The proof of Prop 11.5 relies on the fact that a regular sequence of cardinals exists in ZFC; the example κ0=ℵ0 and κ_{n+1}=|κ_n^{κ_n}|^+ is given, but the verification that it satisfies the defining inequality is left to the reader. A one-line verification would be helpful.
Circularity Check
No circularity: the soundness proofs in Props 8.2 and 14.7 are self-contained semantic arguments.
full rationale
The paper's central soundness claims (Propositions 8.2 and 14.7) are standard semantic soundness proofs with no circular structure. In Part 1, the semantic consequence relation ⊨ is defined first (Definition 7.1), and the syntactic inference relation ⊢ is then defined as the smallest sequent closed under rules that were independently proved as properties of ⊨ (Propositions 7.5 and 7.6). Proposition 8.2 then follows because every rule preserves ⊨ and ⊨ itself is a sequent; no equation assumes its own conclusion. Part 2 does the same: Definition 14.6 takes rules derived from Propositions 14.2–14.5, and Proposition 14.7 is immediate from those semantic facts. There is no fitting of parameters to data, no quantity is predicted from a subset of itself, and no load-bearing claim is justified by self-citation. The only citations used for substance are standard external texts (Kunen for H(κ) being a model of ZFC−P, Hindley–Seldin for α-conversion properties), and the paper's own canonical-interpretation results (Propositions 11.4–11.6) are used to type product operators, not to assume soundness. The regular-sequence condition in Definition 11.3 is a designed hypothesis, but its consistency is demonstrated by an explicit construction (κ0=ℵ0 and κ_{n+1}=|κ_n^{κ_n}|^+), so it does not smuggle in the target result. The acknowledged lack of a completeness theorem (Section 15) is an honest scope limitation, not a circular step. Accordingly, the derivation chain is self-contained and scores 0.
Assumptions & free parameters
free parameters (1)
- regular sequence (κn) =
any regular sequence; e.g. κ0=ℵ0 and κn+1=|κn^{κn}|^+
assumptions (3)
- domain assumption Background set theory ZFC, including choice and foundation, is consistent and provides the universe for all interpretations.
- standard math H(κ) for uncountable regular κ is a model of ZFC minus power set, and the cardinality facts about H(κ) used in Section 11 are correct.
- standard math Standard alpha-conversion and substitution facts for lambda terms from the literature are correct.
invented entities (2)
-
Sorts u_n for n in omega
independent evidence
-
Polymorphic product operators p^n_m for m,n in omega
independent evidence
Cite this review
Pith. "Pith review of Dependent Types Simplified." pith.science (2026). https://pith.science/paper/IOGPDSCC
@misc{pith2026250704071,
author = {Pith},
title = {Pith review of: Dependent Types Simplified},
year = {2026},
howpublished = {\url{https://pith.science/paper/IOGPDSCC}},
note = {Machine review of arXiv:2507.04071}
}
read the original abstract
We present two logical systems based on dependent types that are comparable to ZFC, both in terms of simplicity and having natural set theoretic interpretations. Our perspective is that of a mathematician trained in classical logic, but nevertheless we hope this paper might go some way to bridging the cultural divide between type theorists coming from computer science.
Reference graph
Works this paper leans on
-
[1]
On relating type theories and set theories
Peter Aczel. On relating type theories and set theories. In Types for proofs and programs. International workshop, TYPES '98. Kloster Irsee, Germany, March 27--31, 1999. Selected papers , pages 1--18. Berlin: Springer, 1999
work page 1999
-
[2]
H. P. Barendregt. Lambda calculi with types. In Handbook of logic in computer science, V ol.\ 2 , volume 2 of Handb. Log. Comput. Sci. , pages 117--309. Oxford Univ. Press, New York, 1992
work page 1992
-
[3]
Mario Carneiro. The type theory of L ean. Master's thesis, Carnegie Mellon University, 2019. URL: https://github.com/digama0/lean-type-theory/releases/tag/v1.0
work page 2019
-
[4]
Lean4lean: Towards a verified typechecker for L ean, in L ean, 2024
Mario Carneiro. Lean4lean: Towards a verified typechecker for L ean, in L ean, 2024. http://arxiv.org/abs/2403.14064 arXiv:2403.14064
arXiv 2024
-
[5]
A. Church. A set of postulates for the foundation of logic. I , II . Ann. Math. (2) , 33:346--366, 1932. http://dx.doi.org/10.2307/1968337 doi:10.2307/1968337
-
[6]
A. Church. An unsolvable problem of elementary number theory. Am. J. Math. , 58:345--363, 1936. http://dx.doi.org/10.2307/2371045 doi:10.2307/2371045
doi:10.2307/2371045 1936
-
[7]
C. C. Chang and H. J. Keisler. Model theory. , volume 73 of Stud. Logic Found. Math. Amsterdam etc.: North-Holland, 3rd rev. ed. edition, 1990
work page 1990
-
[8]
Thierry Coquand. A new paradox in type theory. In Logic, methodology and philosophy of science IX. Proceedings of the ninth international congress of logic, methodology and philosophy of science, Uppsala, Sweden, August 7--14, 1991 , pages 555--570. Amsterdam: North-Holland, 1994
work page 1991
Show all 19 references
-
[9]
Inductively defined types
Thierry Coquand and Christine Paulin. Inductively defined types. Colog-88, Proc . Int . Conf ., Tallinn / USSR 1988, Lect . Not . Comput . Sci . 417, 50-66 (1990)., 1990. URL: https://david.darais.com/assets/Inductively_Defined_Types--Coquand+Paulin.pdf
1990
-
[10]
Roger Hindley and Jonathan P
J. Roger Hindley and Jonathan P. Seldin. Lambda-calculus and combinators, an introduction . Cambridge: Cambridge University Press, 2nd revised and updated ed. edition, 2008
2008
-
[11]
Antonius J. C. Hurkens. A simplification of Girard 's paradox. In Typed lambda calculi and applications. 2nd international conference, TLCA '95, Edinburgh, GB, April 10--12, 1995. Proceedings , pages 266--278. Berlin: Springer-Verlag, 1995
1995
-
[12]
S. C. Kleene and J. B. Rosser. The inconsistency of certain formal logics. Ann. Math. (2) , 36:630--636, 1935. http://dx.doi.org/10.2307/1968646 doi:10.2307/1968646
1935 doi
-
[13]
S. A. Kripke. Semantical analysis of intuitionistic logic. I . Formal Syst . and Recurs . Funct ., Proc . 8th Logic Colloquium , Oxford 1963, 92-130 (1965)., 1965
1965
-
[14]
Set theory
Kenneth Kunen. Set theory. , volume 34 of Stud. Log. (Lond.) . London: College Publications, 2011
2011
-
[15]
The substitutional paradox in R ussell's 1907 letter to H awtrey
Bernard Linsky. The substitutional paradox in R ussell's 1907 letter to H awtrey. Russell: The Journal of Bertrand Russell Studies , 22(1):47--55, 2002
1907
-
[16]
Computation and reasoning
Zhaohui Luo. Computation and reasoning. A type theory for computer science , volume 11 of Int. Ser. Monogr. Comput. Sci. Oxford: Clarendon Press, 1994
1994
-
[17]
Michael W. Mislove. Topology, domain theory and theoretical computer science. Topology Appl. , 89(1-2):3--59, 1998. http://dx.doi.org/10.1016/S0166-8641(97)00222-8 doi:10.1016/S0166-8641(97)00222-8
1998 doi
-
[18]
The not so simple proof-irrelevant model of CC
Alexandre Miquel and Benjamin Werner. The not so simple proof-irrelevant model of CC . In Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24--28, 2002. Selected papers , pages 240--258. Berlin: Springer, 2003. URL: link.sp...
2002
-
[19]
Russell and A
B. Russell and A. N. Whitehead. Principia Mathematica . Vol . I . Cambridge: University Press . xv, 666 S . (1910)., 1910. URL: www.hti.umich.edu/cgi/t/text/text-idx?c=umhistmath;idno=AAT3201
1910
Reviewed August 6, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.