Skip to main content

Questions tagged [consistency]

A system of formal logic is consistent if false is not deducible in the system. (from nLab).

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
235 views

Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination

Setup Current Understanding I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is ...
idka's user avatar
  • 73
3 votes
1 answer
93 views

Is unguarded fixpoint reduction consistent?

In Coq, there are two restrictions on fixpoints to retain normalization: Recursive calls can only be done on structurally smaller arguments, enforced by a guard condition during type checking; and ...
ionchy's user avatar
  • 1,026
2 votes
1 answer
154 views

Coq: Would adding "inline inductive definition expressions" introduce inconsistency?

Scenario: new ind syntax As far as I know, in Coq, you cannot create new inductive types by only using expressions. You must use commands--namely, the ...
Kyle Lin's user avatar
  • 143