Remark 3.1. Martin-Löf (1994) argues that Kant’s analytic judgment a priori and synthetic judgment a priori can be exemplified, in the realm of logic, by ([analytic]) and ([synthetic]) respectively. In the analytic judgment ([analytic]) everything that is needed to make the judgment evident is explicit. For its synthetic version ([synthetic]) a possibly complicated proof construction \(a\) needs to be provided to make it evident. This understanding of analyticity and syntheticity has the surprising consequence that “the logical laws in their usual formulation are all synthetic.” Martin-Löf (1994: 95). His analysis further gives: