The Coq mailing list

[FloDo <florian-dold AT online.de>]

Hi!
As I'm fairly new to Coq I have a question regarding it's underlying theory.
Namely, what is provable in CoC? If CoC's strong normalization property is
not provable within CoC
itself, where is the border between provable and not provable? Can it prove
all propositions provable in higher-order-logic? If so, in which system can
strong normalization be proved?


With best regards,
Florian Dold.
-- 
View this message in context: 
http://www.nabble.com/What-is-provable-in-Coq--tp22897613p22897613.html
Sent from the Coq mailing list archive at Nabble.com.