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?
Philippa Cowderoy@chrisamaphone Intentionally vague counter-question: how much/little does it take to make two theorems different?
@flippac hmm, my conceptual framing here suggests something like “someone with expertise in the domain of proof would consider them different”. so like, interchanging theorem inputs, probably no; rephrasing interprovable props using a completely different intermediate data structure, probably yes?
@chrisamaphone Okay, so "which settings admit this proof?" is a reasonable question even if opinions are likely to vary, and adding "up to encodings of X" even more so?
@chrisamaphone Also, do they become the same again if someone figures out common properties between the intermediate structures and abstracts them out?...
@chrisamaphone (FWIW: I'm entirely okay with an answer where wall-clock time is relevant!)