All Questions

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...

HoTT provides a foundation of math that remains mysterious for many mathematicians including me. Hence this question. There are several implementations of math based on ZFC, an example being MetaMath. ...

The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...