Skip to main content

Questions tagged [decidable]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
2 answers
369 views

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
Municipal-Chinook-7's user avatar
-1 votes
1 answer
104 views

Implementability of proof assistants for Infinitary logics with finite many terms

Infinitary logic is a natural consequence of extending the length of proofs of first-order logic to a infinite ordinal level. By definition, since proof lengths are infinitely long, one should not ...
Ember Edison's user avatar