tag:blogger.com,1999:blog-15452141.post8841980972070384049..comments2009-01-12T14:22:18.760-08:00Comments on Words and Other Things: More notes on the SearchShawnhttp://www.blogger.com/profile/15244930958211791213noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-15452141.post-16788516393541414292009-01-10T10:21:00.000-08:002009-01-10T10:21:00.000-08:00Yes, I certainly think the distinction is importan...Yes, I certainly think the distinction is important for logic. For the mathematical proof theorist it may not matter much, but for the philosopher that wants to use proof theory in theorizing I think it is important to at least be aware of the distinctions. <BR/><BR/>The A here is a type (or set, or sort, etc.), but it can be seen in different ways, in particular it can be seen as a proposition -- this is a version of the formulas-as-types interpretation of Curry and Howard. <BR/>As you may know, the notion of judgement plays a fundamental role in constructive type theory, and is one of the features that distinguishes it from most other contemporary systems of logic. In the type theory itself the notion of judgement is taken to be primitive, although it is of course open for philosophical elucidation. The notion of proposition is not primitive but is explained by saying what one must know in order to make the judgement A prop. One can make this judgement if one knows how a canonical proof-object is formed as well as how two equal canonical proof-objects are formed. A canonical proof-object is the canonical element of a type under the Curry-Howard isomorphism. What a canonical element is will therefore depend on the proposition (or type) in question -- it is by specifying these, together with specifying when two canonical elements are equal, that one explains a proposition (or defines a type). I would say, for instance, that a bird's sitting oustide my window would be a canonical proof-object for the proposition that a bird is outside my window.<BR/><BR/>It is perhaps better that I refer to Martin-Löf's book, where these issues are treated in the first few sections. <BR/><BR/>I don't think the method you mention of seeing whether a formula appearing in a natural deduction derivation counts as a theorem catches the right point. Assuming that we already have a notation for signalling theorems, what your method does is rather to distinguish "categorical" from "hypothetical" theorems, where the latter type of theorems are those asserted under an assumption. <BR/>The \vdash in Hilbert-type systems is usually viewed as a theorem-indicator, but in this case, theorem is a metamathematical notion, meaning a formula occurring as the last element of a finite string of formulas possessing certain syntactic <BR/>properties.<BR/>Of course, the judgement-stroke in Frege's ideography is a "theorem-indicator".<BR/><BR/>How is the style of The Search for Mathematical Roots? I have only read one piece by Grattan-Guiness, and that I found terribly dry, it being only a listing of "historical facts" without any interpretation at all...anstenhttp://www.blogger.com/profile/17765855967228534435noreply@blogger.comtag:blogger.com,1999:blog-15452141.post-9207406869289572252009-01-09T14:08:00.000-08:002009-01-09T14:08:00.000-08:00Ansten,That is a good point about the distinctions...Ansten,<BR/>That is a good point about the distinctions in natural deduction. I think it diverges some from the unfortunate overloading in early algebraic logic in the following sense. In the algebraic logic case, there was a shift between types involved in the overloading. In the first example it was between objects and propositions. The rules in natural deduction make sense when applied to theorems, assumptions, and propositions. Some of results of operations in the algebraic case do not have happy propositional interpretations. <BR/><BR/>That being said, there is something I like about the distinction you point to. In the tree formulation we don't have a local indication of a theorem. There would seem to be a global one since we can look to see if there are undischarged assumptions. In Fitch notation, theorems would be marked by the absence of assumption lines to the left of the proposition, although there would still be some ambiguity between assumptions and theorems reiterated within the scope of other assumptions. <BR/><BR/>I've read a little bit on constructive type theory, but I'm still a little shaky as to what is going on in the judgment case there. How does 'A true' function, as opposed to 'A'? Is the latter just barred?Shawnhttp://www.blogger.com/profile/15244930958211791213noreply@blogger.comtag:blogger.com,1999:blog-15452141.post-25266607362082606982009-01-09T11:34:00.000-08:002009-01-09T11:34:00.000-08:00Sundholm (and perhaps others) has remarked that th...Sundholm (and perhaps others) has remarked that the formulas in standard presentations of predicate logic serve (at least) three different roles: as standing for propositions, for propositions assumed, as well as for propositions demonstrated. Consider for instance a proof in a system of natural deduction of A->B and of A (these are proved, say, to get a proof of B). In such a proof, A will typically serve all the three roles: first, as assumption in order to derive A->B, but also as theorem in the derived A, and finally as proposition in the derived A->B. <BR/>I believe signs for assumptions are often marked in natural deduction, but there is no distinciton there between the signs of propositions and of theorems. <BR/>If one believes that the distinctions in questions are theoretically important, proof theory can be accused of an unfortunate overloading of symbols. <BR/>The same confusion of symbols does not arise in constructive type theory, where one distinguishes the judgement A true from the proposition A; it also has a notation for assumption, namely (A true).anstenhttp://www.blogger.com/profile/17765855967228534435noreply@blogger.com