3

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. – user40276 Mar 6 '16 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. – StudentType Mar 23 '16 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) – user40276 Mar 28 '16 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. – StudentType Apr 7 '16 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." – user40276 Apr 8 '16 at 4:13
3

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.

Analytic and Synthetic Judgements in Type Theory, Per Martin-Löf

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? – StudentType Mar 3 '16 at 18:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.