Para sistemas como Coq, que se basan en la teoría de tipos, esta pregunta es más difícil de responder de lo que cabría esperar.
En primer lugar, ¿qué hace falta para "conocer" la fuerza de consistencia de algún sistema? Clásicamente, los sistemas lógicos más estudiados se basan en la lógica de primer orden, utilizando el lenguaje de la aritmética elemental o el de la teoría de conjuntos. Así que si se puede decir: "El sistema X es equiconsistente con ZF" (o con PA, o PRA, o ZFC + infinitos inaccesibles, etc.), entonces la mayoría de la gente sentirá que "conoce" la fuerza de consistencia de X, porque lo ha calibrado contra una jerarquía familiar de sistemas.
Sin embargo, Coq se basa en algo llamado Cálculo de Construcciones Inductivas (CIC). Sin entrar en una explicación detallada de lo que es, permítanme mencionar que el núcleo de CIC no tiene ningún axioma, pero normalmente la gente añade axiomas según sea necesario. Por ejemplo, si quieres una lógica clásica, entonces puedes añadir la ley del medio excluido como axioma. Para conseguir más potencia se pueden añadir más axiomas (aunque hay que tener cuidado porque se sabe que ciertas combinaciones de axiomas son inconsistentes). Pero intentar alinear los distintos sistemas que se pueden obtener de esta manera con sistemas aritméticos o de teoría de conjuntos más conocidos es una tarea complicada. Normalmente, no podemos esperar una calibración exacta, pero podemos interpretar varios fragmentos de la teoría de conjuntos en la teoría de tipos y viceversa, mostrando que la consistencia de la CIC más ciertos axiomas se encuentra entre dos sistemas diferentes en el lado de la teoría de conjuntos. Si quieres profundizar en los detalles, te recomiendo el artículo Sets en Coq, Coq en Sets de Bruno Barras como punto de partida.
