chris martensintentionally vague question; please document your assumptions in answers :)
from a (known valid) proof, (when) can you infer what theorem it proves?
(when) can a single proof prove multiple different theorems?
andreasdotorg@chrisamaphone Assuming we live in constructive logic, there's types as propositions. Using that, we can state that:
* By using type inference, we can calculate the type from an expression. Thus, we can calculate the theorem from the proof quite directly.
* Every proof is a proof for exactly one theorem, following from the fact that every expression has well-defined type.
* By using type inference, we can calculate the type from an expression. Thus, we can calculate the theorem from the proof quite directly.
* Every proof is a proof for exactly one theorem, following from the fact that every expression has well-defined type.
@andreasdotorg what type system are you assuming we’re in?