Logic & Programming

This is a study of certain basic properties of MF (``minimalist foundation’’) of Sambin et Maietti (2009), a formal system consisting of two distinct intuitionistic type theories, mTT, an intensional one, and emTT, an extensional one.

The major result of the paper is the embedding of mTT into emTT, the other direction, the embedding in emTT into mTT, having been shown at the time of introduction of MF using a setoid interpretation.

The embedding of mTT into emTT is proven via two stages, first an embedding of mTT into emTT+propext is given, where propext is the propositional extensionality principle. This principle says that if there exist a proof of equivalence between two propositions, then the two propositions can be considered equal. The second stage is the embedding of emTT+propext into emTT via a notion of canonical isomorphism.

In particular, the embeddings imply the equi-consistency of mTT and emTT for the propositional parts of the two theories: the theories have a sort of propositions distinct from the sort of sets, very much like in the type theories of the Coq proof assistant.

The authors also show, via a double negation translation of the propositional part (but not of the set part) that classical logic can be added to emTT without sacrificing the consistency of emTT. However, classical logic has no implication on the set part, as one cannot, for instance, use a disjunction proposition (even without classical logic) to construct a function of coproduct type.

It would be nice to have the consistency properties between mTT and emTT for the set part as well (an empty set is inhabited in mTT iff it is inhabited in emTT).

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net