I see, with that mapping your original paragraph makes sense.
Just want to note though that such a mapping is quite weird and I don’t really see a mathematical justification behind it. I only know of the Curry-Howard isomorphism as a way to translate between proof theory and computer science, and it maps programs to proofs, not to axioms.
I see, with that mapping your original paragraph makes sense.
Just want to note though that such a mapping is quite weird and I don’t really see a mathematical justification behind it. I only know of the Curry-Howard isomorphism as a way to translate between proof theory and computer science, and it maps programs to proofs, not to axioms.