/sci/ - Science & Math

>>12399324
Under Curry-Howard, the proof of
[math](p\to q)\to (q\to r \to p\to r)[/math]
is
[math]F=\lambda f. \lambda g. g\circ f\colon (p\to q)\to (q\to r \to p\to r)[/math]
I.e.
[math]\lambda f. \lambda g. g\circ f\colon (p\to q)\to (q\to r \to p\to r)[/math]
And, more specifically, for your question use this with [math]r=\bot[/math].

Let me comment on it. Say you want to prove.
[math](p\to q)\to (q\to r \to p\to r)[/math]
The proof is a procedure F which takes a procedure [math]f\colon (p\to q)[/math] and returns a procedure that takes a procedure [math]g\colon (q\to r)[/math] and returns a procedure of type [math]p\to r[/math].
You can also say function for procedure.
The concatenation does the job.

In words, the proof
[math]\lambda f. \lambda g. g\circ f[/math]
reads
given a reason f to believe that p implies q, then given a reason g to believe that q implies r, you can combine them to see that p implies r.

If you want to use your calculus rules to plug this together in steps, you'll only need the first three rules (since none of the above has to do with "and" or "or" and not even really with "bot", since I generalized your claim).
The example in the bottom of your pic also only concerned implications

>>12164861
That wasn't me. I can invite her back on, but I haven't done anything related to mathematical finance in a while.

>>12164751
Annoying. But this was more fun than expected
https://youtu.be/yo1uj9a-Ig8