A theorem prover is a dependently typed functional programming language. If you can generate a term with a particular type then the theorem is true. There is no testing involved.
It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed.
Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.
nextos|8 days ago
anon291|4 days ago
It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed.
Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.
cess11|8 days ago
anon291|8 days ago