6 ms·
I don't agree that a-priori truths are limited to axioms—it's a much larger category of "necessary" truths. A theorem which has been proved is an a-priori truth
by howardcurry 7y ago
I don't agree that a-priori truths are limited to axioms—it's a much larger category of "necessary" truths. A theorem which has been proved is an a-priori truth.
Sure, programs are proofs in the context of Curry-Howard. But not necessarily proofs of what you want them to prove.
- ukj 7y agoA theorem is a consequence of a set of axioms. By definition. It may be an a-priori truth in the context of the particular proof you are working on, but a-priori your theorem there is always an axiom. Wanting to prove that X is a theorem of a-priori truth Y is the same thing as writing the algorithm for f: Y -> X
- joycian 7y agoIf it has been proven from your axioms (really down from the axioms!) then you can add it to a library of statements you 'know' (or in the case of your axioms, assume) to be true.
- ukj 7y agoMore succinctly: The thing you want proven is a proposition. A proposition is a type. Writing the algorithm which implements the type is the same as proving it. https://ncatlab.org/nlab/show/propositions+as+types https://ncatlab.org/nlab/show/propositions+as+types