Classical Fictions

It seems there is a fundamental tension between exploiting the full power of a constructive type theory and upholding the fictions of classical mathematics.

—Noam Zeilberger

The desire not to be anti-classical puzzles me, because in my opinion the law of the excluded middle isn't just unprovable in automated proof assistants, it is really wrong; The statement (in Agda syntax):

∀ {p : Set} → p ⊎ (¬ p)

is usually read "for all statements p, p is true or p is false" but a more faithful translation (to the way the language actually behaves) would be "There exists a program, that, when given any statement, either proves that it is true or proves that it is false." Such a program is famously impossible.

But more than that, even if we could invoke the hand of God and introduce such a program as a postulate, we would still have an impossibility, since Gödel showed that there must be statements that can neither be proven true nor false -- in other words, the constructed law of the excluded middle is impossible even to God. Such a postulate isn't just wrong, it is one of the most widely known wrong things in math.

So it seems to me, that any language that is not anticlassical must be missing the benefit of a few assumptions. I would like to see

¬ (∀ {p : Set} → p ⊎ (¬ p))

to be provable, translated as "If you show me a program and claim it can prove or disprove any statement, I will analyze that program and find a case on which it fails."

The implementation of the above may involve pattern matching on functions (ie, inspecting to see what parts it is built of (lambda, application, constructor, ...)), which would violate extentionality, which I have no problem with because I think extentionality is also obviously untrue. Sure, you may define a

data ExtentionallyEqual {A B : Set} (f : A → B) (g : A → B) : Set where
    ext-equal : (pf : ∀ {a} → f a ≡ g a) → ExtentionallyEqual f g

and reason about it (as you may construct a classical theory within an anticlassical language), but there's no need for all terms in the language to conform, especially when there exist extentionally equal terms with wildly different performance characteristics.

Plus, if you could pattern match on functions, then the compiler could be written as an ordinary function in the source language, in the same execution environment; there would be no need to treat compilation as a "magical" task that happens outside of the main program. And much of the distinction between macros and functions disappears, as all terms are open for inspection. Of course, the inspections would need to respect whatever level of equality the language generally aims to support, and I am thinking but I haven't thought about it too deeply that in Agda that would mean that all pattern matching on functions must only see closed normal forms (which is not unlike how pattern matching already behaves in Agda).