What is the notion of a proof of a proposition for Martin-Löf?

The notion of proof of a proposition is of the most fundamental notions in Martin-Löf's work on philosophical logic, since it is conceptually prior to the notion of truth - cf "Truth of a proposition, evidence of a judgement, validity of a proof" (p.414). But, as far as I know, he never really gave an explicit philosophical explanation of it.

So what is a proof of a proposition for Martin-Löf? Generally speaking, we can put the question as

• What is a term of a type for Martin-Löf?

(given the Curry-Howard or proposition-as-types correspondence.)

• A proof of a proposition \$A\$ is a proof of the judgment "\$A\$ is true", which is the knowledge about this judgement. Mar 6, 2016 at 18:04
• @user40276 How can you conclude this? I can see that the a proof (or evidence) of the judgment 'A is true' is a proof of a proposition A, though. Mar 23, 2016 at 2:16
• Take a look at this paper pps.univ-paris-diderot.fr/~saurin/Enseignement/LMFI/articles/… . I should mention too that this philosophical definition of proof leads to circularity and is not constructive (actually, not even intuitionistic), however the theory works well (just the philosophical foundations are not suited to the theory) Mar 28, 2016 at 10:32
• @user40276 Sorry, the link is broken. Do you mean On the meanings of the logical constants and justification of the logical laws? If so, I'm relatively familiar with it. So could you please indicate where are exactly the passages you have in mind? I would love to hear how you draw this controversial but interesting conclusion, if could (and had the time to) be more specific. Apr 7, 2016 at 5:16
• This one is not broken for now andrew.cmu.edu/user/ulrikb/80-518-818/MartinLof83.pdf . See page 9-10 of the document (and not of the article). Special interested is in the assertions "A proof is what makes a judgement evident", "to prove = to get to know = to understand, comprehend, grasp, or see." Apr 8, 2016 at 4:13

Martin-Löf has a short article on this.

Kant and Contemporary Epistemology, Volume 54 of the series The University of Western Ontario Series in Philosophy of Science pp 87-99. Analytic and Synthetic Judgements in Type Theory, Per Martin-Löf

He claims

So the usual form of judgement, A is true, is indeed a special case of the existential form of judgement.

He relies thus on the `intuitionist explanation of truth, [...], defined as existence of a proof, or construction, of the proposition.`

And there, he says that the synthetic forms of judgement are the existential forms of judgement.

Since I cannot copy-paste the text, I give a you a picture of the relevant pages.

Another article without the machinery of the types is Truth and Knowability on the Principles C and K of Michael Dummett 1998 He explicitly distinguishes between judgements, propositions, truths and proofs.

all these articles are available on

https://github.com/michaelt/michaelt.github.io/tree/master/martin-lof

• Thanks. I'm familiar with the first paper and that truth is identified with provability for Martin-Löf. What I am interested in, though, is not judgments - but to know what exactly a "proof of a proposition" is supposed to be for him.. would you have any idea in respect to it? Mar 3, 2016 at 18:14