less info
reputation
419
bio website location age member for 3 years, 10 months seen Sep 16 at 12:01 profile views 354

Dear All,

 Mar18 comment Contradiction Theorem Mind you, it should read the step from ~~A to A. And my reference is wrong. Mar18 comment Contradiction Theorem You're welcome. (Means: I would be pleased, english for "Bitteschön - Dank erwidernd"). Mar18 comment Contradiction Theorem I know, but I ALWAYS use ASCII art. And damned, this stack exchange is too stupid to change it automatically into what they prefer. Mar18 answered Contradiction Theorem Mar18 accepted Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say? Mar18 revised Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say? added 37 characters in body Mar18 answered Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say? Mar15 comment Disjunction in Intuitionistic Logic, what about $((P \to U \lor V) \to Z)$ Just fixed U=1. Mar15 revised Disjunction in Intuitionistic Logic, what about $((P \to U \lor V) \to Z)$ edited body Mar1 awarded Yearling Feb29 answered First order logic proof question Jan19 answered First order logic and higher order logics? Jan10 answered Has a Dependent Type always a Type? Jan10 revised Has a Dependent Type always a Type? edited body Jan9 comment Has a Dependent Type always a Type? The rules for sort judgements in calculus of construction are Prop:Type(0), Set:Type(0) and Type(i):Type(i+1), and i is infered. How do you get a dependency of the quality of D, x : A |- B : s2(x) from this? Either semantically or syntactically? Is convertibility needed? Jan9 comment Has a Dependent Type always a Type? The SIG rule looks to me like a lambda-rule à la Barendregt and not like a p-rule à la Barendregt. Similar to the last rule you show for the calculus of construction and the first rule you show for ML. In the full formulation à la Barendregt some additional judgements are necessary, but it is seen that even if there were some dependency on s2, since the s2 drops out in the conclusion, there is no problem with scope in a lambda-rule (page 136). The problem is only there for p-rules. Jan9 comment Has a Dependent Type always a Type? Calculus of construction as you show it is an instance of a generalized type system where (s1,s2,s3) = (_,S,S). But you also write S does not contain x, so we do not have the dependence here that I would be interested in. Dec28 comment Has a Dependent Type always a Type? Just reading: Jan-Willem Roorda, Pure Type Systems for Functional Programming, is (PI) rule would not work when x in t. Dec27 comment Has a Dependent Type always a Type? Thanks for the link, I didn't know about this terminological distinction. Do pure type systems work with a modified p-rule? Can we find a p for this p-rule? Dec27 revised Has a Dependent Type always a Type? added 7 characters in body