/sci/ - Science & Math

Here's the intuitionistic section I mentioned:
https://en.wikipedia.org/wiki/Sequent_calculus#Substructural_logics

Also, to enrich this thread with a question that requires less background, how to prove

[math] \left( A\to (B\lor C) \right) \implies \left( A\to B) \lor C) \right) [/math]

now using

[math] (A\to B) = (\neg A \lor B) [/math]

>>8100936
cont.

The secret to when a generic function type has a function is given by the Curry-Howard isomosphism.

Let A,B,C, ... be logical proposition

The proposition
[math]A\to A[/math]
says "A implies A".
It's true.
The trivial prove is:
Given a reason to believe in A, it follows that we have a reason to believe A.
It's represented by

f(x):=x

The proposition
[math](A\land B)\to (B\land A)[/math]
says that if "A and B" is true, then "B and A" is also true. Pretty much part of the deifnition of "and".
The prove is the swap function.

Okay, let's make something slightly less trivial:

The proposition
[math](A\to (B\to C))\to ((A\land B)\to C)[/math]
says "IF from A being true follows that B implies C, then if "A and B" is true, it follows that C is true."
The prove is to juggle with reasons to believe in the propositions again:
Assume we have a reason to believe that [math](A\to (B\to C))[/math] holds. Then given a reason to believe "A and B", we know that "A" hold and also that "B" holds individually. As we've assumed [math](A\to (B\to C))[/math] holds, we know that [math]B\to C[/math] holds, and finally that [math]C[/math] holds. In total, we follows that under the assumption, C is already implied by "A and B".

The formal proof is as follows:
If f is a function variable for a -> (b -> c), so that f(x) is in b->c and f(x)(y) is in c.
Then
g: (a->(b->c)) -> ((a,b) -> c)
g(f)((x,y)):=f(x)(y)

Under the curry howard iso morphism, a generic type having a term corresponds to the corresponding proposition having a proof.

You can't find a term for the type
a
or
Int -> a
You can try, but it's impossible.
The "reason" is that if you could find a term for a, this would mean you could prove any proposition - which is silly.