Thank you. I downloaded this paper a month ago to read it eventually. Your comment made me read it yesterday and i have a question. By using the type system wo

Thank you. I downloaded this paper a month ago to read it eventually. Your comment made me read it yesterday and i have a question. By using the type system would we exlude potentially consistent theories? Is it similar to how limitimg ourselves to a decidable language instead of a turing complete one would prevent us from writing potentially never halting programms that could still halt?