516 reputation
419
bio website
location
age
visits member for 3 years, 10 months
seen Sep 16 at 12:01

Dear All,

If you want raw timely information about what is cooking in our lab you can follow the following Google+ and Twitter streams:

Google+ Jekejeke Prolog
Twitter Jekejeke Prolog

We have discontinued our Facebook, Linkedin and XING accounts and are now exclusively posting on Google+ and Twitter.

Have Fun


Mar
18
comment Contradiction Theorem
Mind you, it should read the step from ~~A to A. And my reference is wrong.
Mar
18
comment Contradiction Theorem
You're welcome. (Means: I would be pleased, english for "Bitteschön - Dank erwidernd").
Mar
18
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.
Mar
18
answered Contradiction Theorem
Mar
18
accepted Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say?
Mar
18
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
Mar
18
answered Is there an intuitionistic proof of $\lnot p(a) \rightarrow p(b) \vdash \exists x p(x)$, what would Herbrand's Theorem say?
Mar
15
comment Disjunction in Intuitionistic Logic, what about $((P \to U \lor V) \to Z)$
Just fixed U=1.
Mar
15
revised Disjunction in Intuitionistic Logic, what about $((P \to U \lor V) \to Z)$
edited body
Mar
1
awarded  Yearling
Feb
29
answered First order logic proof question
Jan
19
answered First order logic and higher order logics?
Jan
10
answered Has a Dependent Type always a Type?
Jan
10
revised Has a Dependent Type always a Type?
edited body
Jan
9
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?
Jan
9
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.
Jan
9
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.
Dec
28
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.
Dec
27
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?
Dec
27
revised Has a Dependent Type always a Type?
added 7 characters in body