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

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

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

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

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