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?
if you’re used to thinking of propositions and types interchangeably, try to wear your logician or mathematician hat for this question rather than leaning on intuitions about type systems. i’m curious whether that might lead to different places.
putting the question another way: imagine your friend looks up a proof of their favorite theorem in a textbook. they cover up the statement of the theorem and send it to you (who is well-versed in the relevant terminology used in the body of the proof, but has never seen this particular proof). can you guess the theorem?
Alley Stoughton@chrisamaphone "Follows by straightforward calculations."
@fullyabstract ha, a list of theorem statements “proven” this way would be fun to see
@chrisamaphone In proof assistants, some proofs using automation can be done with the user having no clue why the theorem holds.
@fullyabstract yeah; this game would be very difficult if the proof you’re handed is “auto.” 😅
David Renshaw
jcreed@david weirdly, I came across this post before I saw @chrisamaphone 's prompt and was like... wtf, I have no idea what theorem this is a proof of, what's going on. but once I knew that my task was guessing the theorem, it was somehow easy
Max S. New ⚜️Well
1. I recognize the book immediately because I did a course on it in college
2. The proof ends with a sequence of equations whose endpoints are the theorem
@maxsnew @david @chrisamaphone oh yeah i agree it's definitely kind of inexcusable that I didn't get it the first time, because of (2). but the meta-knowledge that "someone has told me this *is* a puzzle and therefore ought to be solvable" has an outsized psychological effect on making puzzles seem easier, at least for me
bob@chrisamaphone this is an information retrieval problem, you just need a feature embedding for theorems :)
@chrisamaphone I'd be tempted to try to parse the proofs into things that look like feature structures and index them in an off the shelf search system
@bob so, given this assumption, what are your answers to the original question?
Paul Khuong@chrisamaphone I'm tempted to claim that's necessary for a *good* proof. I think I usually wouldn't be able to recover the theorem from most proofs though :/
Conor Mc Bride@chrisamaphone This is a good question. For type theorists, there's also a key distinction between proof terms as a decidably checkable evidence language and the high level language of proofs, which elaborates (by unspecified amounts of computation) to decidably checkable proof terms, or not if you're unlucky.
Let me chuck in a side-question. To what extent should problem solution documents expose the subproblems which arise in the course of that solution.
OK, I'm massively biased. I want to see the whole problem-solving dialectic appearing in the document, and I do not imagine the document as being written by one human. The document is a collective human-machine effort. We should not conflate the length of the document with the amount of work.
Philippa Cowderoy@pigworker @chrisamaphone Has anybody worked on getting some of this to play nicely with existing eg outlining tools? It's going to get an even messier problem to display as we want to account for the kinds of changes normally relegated to "software engineering", of course - none of these things are really single-dimensional text beyond the representations we're currently stuck using in much anger
@pigworker i am similarly biased! (but trying not to expose that bias too much in collecting answers to this question.)
@chrisamaphone but my own rather poor largely intuitive understanding of Curry-Howard is my only source of intuition about this problem. Which I suppose is I suppose exactly your point here, lol.
My problem is I have a metalogical block that I spent too much time fixated on overcoming, and still to this day I still have no idea what I'm overlooking. Logic has been ingrained in me through programming and the study of mathematics, and I have always been extraordinarily example-efficient when learning logic. The proofs of Godel's theorems makes no sense to me, never have.
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?
@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!)
azul@chrisamaphone Most theorems have universally quantified variables. You could instantiate them at any of those values and get a new theorem with the same proof. This tells me there isn't a unique theorem per proof. But just like type inference, I think one should be able, in many cases, to reason backwards from a proof and come up with a "principal theorem" for this proof, such that any theorem with this same proof follows from the principal theorem.
Boarders@chrisamaphone “by routine induction” “as the reader can verify”
More seriously, I would say there are collections of theorems which all go together (cut elimination, admissibility of substitution, consistency in logic for example), where a proof of one can essentially amount to a proof of any.
@chrisamaphone there are also a bunch of theorems like this in complex analysis where one uses some variant of cauchy’s theorem / the argument principle to prove just about anything
@boarders @chrisamaphone now I just wanna integrate around my logical connectives to find out what their residues are
@jcreed @chrisamaphone no doubt Girard has tried it
@boarders @chrisamaphone When in the business of extracting the theorem from the proof, "it's trivial" won't cut it.
@pigworker @chrisamaphone id really rather it never cut it if I am honest
@boarders @pigworker cutful proofs do seem like they’d be trickier to do this for
julesh@chrisamaphone From a non-formal perspective of proofs-as-prose-communication: a typical proof would usually start with unpacking some consequences of the hypotheses, but usually that's a one-way process and you couldn't always reconstruct the hypotheses of the theorem from their consequences mentioned in the proof, although you could probably make a good educated guess if you knew the topic
Same with conclusions, especially making a qualitative conclusion from quantitative reasoning. A typical undergrad real analysis proof would conclude "this function is continuous" from a more specific bound