Lambda the Ultimate

The problem is, if something is not computable then it has no precise definition.

I meant to respond but posted below instead.

I mean, what?

Guessing here, but I think he means that a definition is incomplete if it can't produce an instance of the construction. I'm not sure "precise" is the right word, but I can sort of see it in that proofs of existence via LEM and other non-constructive means might give you some sense of a construction's shape, but they don't give you all the details. Hence, "imprecise".

Mathematical proofs are imprecise because they rely on unspecified domain knowledge and appeals to intuition. All proofs eventually reduce to a "because its obvious" appeal to intuition. The benefit with computable proofs is that there is at least a formal definition of what that minimal system is.

That doesn't seem quite right. Let's not confuse computability with formal proofs. You can have mechanized proofs (that are certainly precise) that use non-computable ideas — using classical logic! See e.g. Isabelle, or even Coq/Agda with extra axioms.

The imprecision you describe can be fixed by more rigorous proofs and more complete axiom systems. Hilbert among others showed that you can write geometric proofs without appeal to intuition, and gave a sufficient list of axioms for geometry (including many that Euclid did not make explicit, because he used intuition instead).

Soon after, he and others made it possible (at least in principle) to write formal proofs.

But computability is used in the metatheory of logic — specifically, in proof theory.
Since classical logic gives definitions to things that you can't touch — even infinities, one might fear problems. That's why proof theory was born: to show that logic "works" using less objectionable techniques, that is finitistic methods. And as far as I understand (which is not enough), finitistic methods restrict to syntactic objects (close enough to ML datatypes) and computable definitions. (Unfortunately, you can't restrict to clearly finitistic methods to prove that, e.g., Peano arithmetic is consistent — you need to go a bit beyond).

(Sorry for the lack of references).

You can have mechanized proofs (that are certainly precise) that use non-computable ideas — using classical logic! See e.g. Isabelle, or even Coq/Agda with extra axioms.

Well, but the extra axioms are computable. They might be right, just as the more traditional, uncontroversial axioms might be right; establishing whether or not they're right isn't a computability issue. To get axioms that are actually non-computable, you'd need an oracle — a handy-dandy peripheral device that you plug into your Turing machine that, when asked a question, gives an answer that it gets by some unknown means that might not be achievable using a mechanical device (perhaps it consults a djinn or deity). By plugging a suitable oracle O into a Turing machine, you can solve the halting problem — for ordinary Turing machines. An O-oracle Turing machine cannot solve the halting problem for O-oracle Turing machines. Likewise, an O-oracle Turing machine, acting as a formal system of logic capable of addressing claims about the behavior of O-oracle Turing machines, cannot escape Gödel's Theorems; it can't be simultaneously consistent and complete; and if it's sufficiently powerful, and can prove itself consistent, then it can also prove itself inconsistent.

There probably is a disagreement about what "computable" means, but in the sense used in Blaisorblade's remark those extra atoms really are not computable.

One way to think of the treatment of axioms in Coq is as free variables: saying at the beginning of a proof of P that you import the excluded-middle axiom is a sort of syntactic sugar to abstract over a variable of type (forall A, A \\/ ~A). You can also directly write a proof of the function type ((forall A, A \\/ ~A) -> P), of the form fun lem -> ..., and that will have (roughly) the same status.

On this basis, when Blaisorblade means that the axiom is not computable, he means that uses of the free variable corresponding to the axiom's abstraction block cut-elimination, that is, computation. There is a canonicity property that says that a closed term of type Nat is either O, or of the form (S n), where n is a closed term of type Nat. No such thing is true, of course, of closed terms of type ((forall A, A \\/ ~A) -> Nat), which may be of the form fun lem -> case lem X of ... for example. By "computable" in this context, people typically mean either:

1. has a corresponding reduction/computation rule
2. has a computation rule that preserves the canonicity property that allows us to know that normal forms are really the expected values of the type

Now there are some axioms for which (1) or (2) may be true, which means that you *can* give them a computational character. For example, proof-irrelevance as defined in Coq (with the separate Prop universe) is computable in the strong sense (2), and excluded-middle can be given a computational meaning in the weaker sense (1). (I'm personally of the opinion that classical logic is constructive in the sense that is has an interesting computational interpretation (1), but some people are only content with sense (2).)

In any case, this is not what Blaisorblade was talking about. The axiom-as-abstraction mechanism blocks computation and are "not computable" in this sense, and this (simple, almost trivial) idea can be applied to any assumption (even inconsistent ones) regardless of whether we know how to make them "computable" in any of those senses.

In other words, you can write perfectly precise proof of P under the axiom A, by just writing a (perfectly precise) intuitionistic (of whatever you prefer) proof of (A -> P), and this works well in practice.

(The other question is whether other people will find the proof of (A -> P) *interesting*, and for this showing that A is computable in sense (1) or (2) definitely helps.)

But in what formal system do you define the axioms? In any logic how are implication, conjunction and disjunction defined? If proofs are not computable (that is the axiom system is encoded on real physical computational hardware, like a Prolog interpreter running on a PC), then the definitions of these terms is in human language, normally English, and subject to all the philosophical problems of meaning (see Wittgenstein's language games). I can't even define what I mean by meaning.

As gasche explained in detail, we are probably using "computable" in different senses. However, I also talked about proof theory. Proof-checking is usually expected to be computable (technically, decidable), even for classical proofs — I guess that's one required result of the proof theory of a logic.

Do we agree that, if for a logic we have decidable proof checking (and we can write a proof checker), we have defined clearly what's a formal proof for that logic and what isn't? I hope so. For practical purposes, I think that can be enough.

We can now debate whether we have defined the meaning of, say, implication in this logic — is it enough to know what's a formal proof of implication? However, now we're firmly in the realm of philosophy. If you answer yes, you are buying what is called "proof-theoretic semantics".
However, this question has a parallel in programming languages.

Some people are happy to know the operational semantics of a language (say, a small-step semantics). But some argue that knowing how a construct behaves (say, reduces) does not tell you whether it has a real meaning, in terms of something other than syntax — according to them, you need a denotational semantics for that!

Historically, the semantics of logics used to be (analogous to) denotational semantics — that's (I guess) why the latter is also called mathematical semantics. However, there's also an analogous of operational semantics — and that's proof-theoretic semantics! See also http://plato.stanford.edu/entries/proof-theoretic-semantics/; the author of that article sits one floor down, though I didn't have enough chance to take advantage of this.

I think we do agree. Even with formal proof checking I would want it done by a machine which is independent of human language.

I would now be happy to define implication in this logic, we define a term and give it a clear and unambiguous interpretation.

I can check your proof if I have an identical machine, and I can understand its meaning by experiment.

...
You build often build different mathematical systems by choosing different axioms, but since the system can be consistent with either an axiom or its negation, it's clear that the axiom isn't constructable from the other axioms.

So all axioms are definable but not constructable.

So this means we can use axioms?

I agree that the perfect optimiser is an impossibility. In some ways predictability of the translation of a language is more important than optimisation. I can reason about access patterns and refactor code to perform better if I am aware of the cost of each operation. It is much harder to finesse the optimisation of code where you are trying to persuade the optimiser to output particular code without the transparency to know what is going on.