External choice: you (the proof term, or the program) are not "part of the choice", instead, you make the choice
e.g. "I have $50 birthday gift card and I need to decide between buying a keyboard or a mouse, either way I will be happy!"
Internal choice: you (the proof term, or the program) now are "part of the choice", you don’t make the decision, instead, you need to prepare for the decision
E.g. "My parents will buy me a gift worth $50, which could be a keyboard or a mouse and I have no control over their decision, but I will be happy regardless!"
Formally
Propositions
H ::="I am happy"K ::="Keyboard"M ::="Mouse"
Internal Choice (⊕), left rule
To be happy to get K ⊕ M, I must be happy to get either one of them.
If I were happy to get either one of them, I must be happy to get K ⊕ M.
Δ, K ⊢ H Δ, M ⊢ H
-------------------------- Δ, K ⊕ M ⊢ H
This rule is invertible!
External Choice (&), left rule
If I were happy to get M, I must be happy to be able to decide between K & M
If I were happy to get K, I must be happy to be able to decide between K & M
Δ, M ⊢ H Δ, K ⊢ H
---------------------------- Δ, K & M ⊢ H Δ, K & M ⊢ H
These two rules are not invertible!
Internal Choice (⊕), right rule
My parents bought me a K, but they can claim they have prepared me with K ⊕ M
My parents bought me a M, but they can claim they have prepared me with K ⊕ M
Δ ⊢ K Δ ⊢ M
-------------------Δ ⊢ K ⊕ M Δ ⊢ K ⊕ M
These two rules are not invertible!
External Choice (&), right rule
To have the ability to decide between a K & M, I must have enough money to buy either one of them
If I had enough money to buy either one of them, I have the ability to decide between K & M