Discussion between Christopher King and Andrej Bauer

Feeds

17:49

Q: Which proof assistants implement Church's rule?

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive theories). Note that unlike the axiom CT, Church's rule does not prove any anti-classical result...

Christopher King

@JasonRute if $T$ is classical, than the church rule can't hold because $T$ will be able to show the existence of uncomputable functions. For example, PA proves "for all x there is a y such that y is the xth busy beaver number", in which case $e$ won't exist.

@JasonRute there are no conditions of $\phi$ other than there being a proof of $\forall x.\exists y. \phi(x,y)$. The reason CR can exist is that in constructive proofs can be turned into programs. The program is found by analyzing the proof, not by analyzing the formula $\phi$.

@JasonRute by "implement" I mean an actual piece of software. I am very confident that CR is correct in Agda and Coq. CR is correct in IZF, for example. But I don't know of any software for performing it automatically. (It is always computable for recursively enumerable theories.)

Andrej Bauer

Is $\exists$ allowed te interpreted as $\Sigma$?

Christopher King

@AndrejBauer yeah that's fine. In a system with both, CR using either $\exists$ or $\Sigma$ works.

Andrej Bauer

It was a trick question: From $t : \Pi (x : A) \Sigma (y : B) .\, \phi(x,y)$ we can get a closed term $f = \pi_1 \circ t : A \to B$ and a proof that it works, and we're done.

Christopher King

(Like, the version with $\Sigma$ should probably be referred to as CR! (since the equivalent axiom is called CT!). But I'd also interested in implementations for CR!.)

@AndrejBauer hmm, it's a very subtle issue but I think technically this approach would require $\eta$ to be an interpreter for $T$ terms, which I imagine is impossible to use for Gödelian/Tarskian reasons. $e$ is supposed to part of a discrete data structure, but $f$ is a function. The term underlying $f$ can be represented by a natural number, but turning it back into a function requires an interpreter.

Andrej Bauer

17:49

You can use meta-programming features tu turn f into code (a discrete data structure). And since we're talking about a rule that only applies to sentences, we must go meta-level at some point.

Actually, how is $\eta$ supposed to work? If it's an interpreter for $T$ then there's a problem.

Christopher King

@AndrejBauer $\eta$ could just be an interpreter for Turing machines. That doesn't run into any logical issues (although there are probably more convenient numberings that also avoid logical issues).

Andrej Bauer

It cannot be just that, or else you would introduce partial maps into your type theory.

Christopher King

@AndrejBauer okay so my notation was perhaps a bit misleading. $\eta$ should actually be thought of as a relation, not a function. This formulation of CT is more specific about this (and also applies to CR).

Andrej Bauer

That makes more sense. My observation still stands: it's more productive to implement reflection, quoting and other meta-level techniques, and leave the actual comittment to CT (either as an axiom or as a rule) to people who want it.

OTH, people do care about the fact that every closed term of type $\mathbb{N} \to \mathbb{N}$ denotes a computable map. Even more, proof assistants are very good at computing with them, so it remains questionable what the advantage of CR would be (other than extracting maps from totoal relations, which is a form of choice).

Christopher King

@AndrejBauer yeah I figured it was a bit extravagant (but perhaps there was a tiny proof-of-concept proof assistant that implemented it?). A use case I had in mind: if you have or are in the process of formalizing computability theory in the proof assistant, CR is a convenient way to prove a function of computable, so having it as a built-in tactic is convenient. The requirement that the proof assistant actually produces $e$ is just a preference for the proof assistant being able to compute things (just adding an axiom is obviously easy).

Andrej Bauer

17:49

You should ask a separate question: how to formalize computability theory? The answer is very nice and cannot be done justice in a comment.

last day (15 days later) »

all rooms