Skip to main content

Questions tagged [foundations]

Use this tag for questions about mathematical or logical foundations of proof assistants. Questions should be related in some way to proof assistants. Possible topics might include mathematical modelling, consistency and computability, universes, etc.

4 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
13 votes
0 answers
363 views

Unintentionally proven false theorem with type-in-type outside logic and foundations?

We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
user21820's user avatar
  • 484
5 votes
0 answers
224 views

Proof-theoretic strength of HOL compared to predicative dependent types

By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($\varepsilon$ operator). By predicative dependent types, I am thinking of MLTT + W-...
Ilk's user avatar
  • 547
3 votes
0 answers
123 views

Uniform notions of pattern matching at dependent types with impredicative proof strength

I am looking for axioms/inference rules that satisfy the following 3 conditions: can be added to predicative intensional Martin-Löf type theory, so $\Pi$, $\Sigma$, equality type, with W-types, ...
Ilk's user avatar
  • 547
0 votes
0 answers
117 views

MLTT with first-order reasoning and equality-reasoning information preservation

Terms in Extensional MLTT don't contain equality-reasoning information (implicit transports), effectively meaning data is lost, which is bad. But at the same time, higher-order reasoning (reasoning ...
Russoul's user avatar
  • 345