Proving the law of excluded middle (LEM), constructively.

constructive_lem.py

"""
https://en.wikipedia.org/wiki/Modus_ponens
https://en.wikipedia.org/wiki/De_Morgan%27s_laws
https://en.wikipedia.org/wiki/Double-negation_translation
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
https://en.wikipedia.org/wiki/Exponential_object
https://en.wikipedia.org/wiki/Constructive_analysis
"""

def switch(p):
    return (p[1], p[0])

pair = ("this??", "that!")
print(switch(pair))



evaluate = lambda p: p[1](p[0])

print(evaluate(("LEM", len)))
print(evaluate(("subscribe", lambda word: word + "!")))
print(evaluate((5, lambda n: n * n)))
print(evaluate((lambda n: n * n, lambda f: f(3)-f(1))))


"""
switch : ∀S. ∀T. S × T → T × S
switch = λp. <π_R p, π_L p>

mp : ∀C. ∀B. (C × (C → B)) → B
mp = λp. (π_R p)(π_L p)

eat : ∀A. ∀B. ((A → B) × ((A → B) → B)) → B
eat = mp

"I have a reason to believe B if both are the case at once:
'A implies B' and 'A impliying B itself already implies B'"

lem_equivalent : ∀A. ¬(¬A ∧ ¬¬A)
lem_equivalent = mp

Obtained after just using notation ¬A := A → ⊥
"It would be absurd if both are the case at once:
'A is absurd' and 'A being absurd is absurd.'"

¬¬A ∨ ¬¬¬A

Obtained after use of De Morgan's laws (classical rule)

A ∨ ¬A

Obtained after use of double negation elimination (classical rule)
"""