Abstract

I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms $$a : A$$ and $$a = b : A$$ are analytic is unfounded. As I shall show, when $$A$$ evaluates to a dependent function type $$(x : B) \rightarrow C$$, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-Löf's original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic-synthetic distinction reworked here is capable of accommodating judgments of the forms $$A \ \sf type$$ and $$A = B \ \sf type$$ as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-Löf's position on the analytic grounding of synthetic judgments.