Questions tagged [consistency]
A system of formal logic is consistent if false is not deducible in the system. (from nLab).
4
questions
5
votes
0
answers
206
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 ...
- 73
2
votes
1
answer
145
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 ...
- 143
13
votes
0
answers
331
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-...
3
votes
1
answer
90
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
...
- 1,308