1 results
ANALYTICITY AND SYNTHETICITY IN TYPE THEORY REVISITED
- Part of
-
- Journal:
- The Review of Symbolic Logic , First View
- Published online by Cambridge University Press:
- 27 June 2023, pp. 1-27
-
- Article
-
- You have access
- HTML
- Export citation
-
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) \to 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 \> \mathsf {type}$ and 
$A = B \> \mathsf {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.
