3 ms·
There are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.
by nextos 8mo ago
There are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.
- anon291 7mo agoWeakly typed, but strongly kinded. 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.