4 ms·

Yes, and because of that limitation dependent type theory is an inferior logic for theorem proving.

• guerrilla 4y ago
  That's silly. Whether it's a good or bad metatheory for theorem proving depends entirely on one's goals and preferences. Most mathematicians use a type theory over something else, so it's hard to even take your view seriously. On top of that, you seem very opinionated for someone who was just confused about the topic of this thread. I have no idea why you're waging a holy war over this but maybe take a break.
  • practal 4y ago
    Most mathematicians don't even use formal logic. For sure they don't use type theory! You seem to be the one who is silly/confused here. If you want to lift your confusion, read the [0] link I gave above.
    • deleted 4y ago
      [deleted]