3 ms·
A-priori truths are called axioms. In the context of the Curry-Howard isomorphism you don't "prove things about programs". Programs ARE proofs. Not all progra
by ukj 7y ago
A-priori truths are called axioms.
In the context of the Curry-Howard isomorphism you don't "prove things about programs".
Programs ARE proofs. Not all programs, mind you. You need to be using a dependently-typed language like Agda, Coq or Idris.
The link in my post to the UniMath project is a bunch of codified proofs to various theorems in Category theory, Topology, Combinatorics etc.
- howardcurry 7y agoI 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