The tag has no wiki summary.

learn more… | top users | synonyms

8
votes
3answers
340 views

“Guarded” negative occurrences in definition of inductive types, always bad?

I know how some negative occurrences can definitively be bad: ...
7
votes
0answers
80 views

Reference for a propositional proof system being equivalent to its soundness?

I am looking for the original reference for the following statement: Let $P$ be a propositional proof system containing $EF$. Then $P$ is equivalent to $EF+Sound(P)$. Background A ...