(no subject)

[gusl]

To summarize my recents philosophical thoughts about formal mathematics & intuition:

(see http://www.livejournal.com/users/gustavolacerda/156135.html?nc=7 and http://www.livejournal.com/users/gustavolacerda/155299.html?nc=7)


* If we have tools, why not use them?

For the same reason that a mathematician wouldn't want to find a *constructive* proof of the Fundamental Theorem of Algebra, I wouldn't want to find a proof of the Jordan Curve Theorem (a visually "obvious", but hard-to-prove theorem).
(Freek interestingly likes the idea of the first project, but not the second one)


* While minimality is nice, "expressivity" is more important:

If in order to express my simple thoughts I need to write complex code, then I consider this language to not be "expressive" enough. The Jordan Curve Theorem is a good example of this: the standard mathematical foundation is not "expressive" enough: it takes a lot of work to prove that which we can see intuitively. Of course, this is a criticism of standard mathematical practice in general, not of any specific formalization programs. Grounding the JCT into foundations (i.e. proving it follows from the foundations) is necessary to maintain the minimality of the axioms, and thereby the "elegance" of the system.


WAYS IN WHICH FORMAL MATHEMATICS DOESN'T CORRESPOND TO REAL HUMAN MATHEMATICS

There are many languages for formal mathematics, but they often don't correspond to mathematicians' cognitive structures.

This is for the following reasons:

* These proofs are currently too low-level (proof plans, proof sketches are possible solutions to this)

* They don't model multiple representations, or semantics (while humans integrate symbolic & visual reasoning)

* They work from absolute mathematical foundations. As we know, real mathematics existed way before it was given good foundations. Human mathematicians work with relative foundations, and (sometimes) try to ground them later.


My vision: tag formal proofs with "chunks" / high-level concepts, analogous to the way texts are semantically tagged.
Create multiple, parallel formal proofs using different foundations, and hook them into each other (I suspect we will need something like Logical Frameworks to accomodate different foundations in a standard form. I think "faithful interpretations" may have a role to play here).

Comments

[triple-entendre.livejournal.com]

Interesting... like chess strategy vs. the way one would _explain_ one's chess strategy vs. the way one would _prove_ one's chess strategy

[gustavolacerda.livejournal.com]

I don't understand your analogy. Would you care explain?

[triple-entendre.livejournal.com]

I didn't really add anything that interesting to the discussion -- or maybe I'm just too sleepy to elaborate on my analogy. But I will do so at a future time if you insist.

I really like your vision of a semantic framework tying together different formal mathematics.

[jcreed.livejournal.com]

I would be more inclined to apply the "if we have tools, why not use them?" idea to the very notion of formalism. Yes, mathematicians used to do proofs rooted in rather high-level intuitions, but now we have the tools to justify and ground in lower-level axioms those intuitions, and to certify with extremely high confidence the proofs that used to rest on those high-level intuitions.

As for constructivism, the axiom of choice or the law of excluded middle is a "tool" to some people and a simple falsehood to others. Viewing it from the other way around, the ability to discriminate between the proofs that correspond to computations and the ones that don't (or, if you prefer the essentially equivalent but more honest formulation, discriminating between programs that are allowed to use side-effects such as a call-with-current-continuation primitive) is a "tool" that the constructivists don't want to cast aside by saying, "hrmph! everybody knows that classical logic is actually true"

[gustavolacerda.livejournal.com]

Viewing it from the other way around, the ability to discriminate between the proofs that correspond to computations and the ones that don't (or, if you prefer the essentially equivalent but more honest formulation, discriminating between programs that are allowed to use side-effects such as a call-with-current-continuation primitive) is a "tool" that the constructivists don't want to cast aside by saying, "hrmph! everybody knows that classical logic is actually true"
can you parse this for me? Is this the core of the paragraph: "The ability to discriminate is a "tool" that the constructivists don't want to cast aside." ?


Btw, here's an interesting way of looking at intuitionism:

from Johan van Benthem - Argument and Procedure

A semantic viewpoint may also help understand
these proof­-theoretic distinctions. Intuitionistic logic is the logic of trees of
`information stages'. These reflect its origin as a description of constructive
mathematics, oriented towards acquiring knowledge. Classical logic is only about
the final stages where all the evidence is in.

I'm not sure I understand what he's saying, but it seems to be related to the provability interpretation.

for comparison, the first line of Geuvers, Jojgov - Open Proofs and Open Terms: A Basis for Interactive Logic

Logic is about finished proofs and not about the process of finding a proof.

I guess they must be talking about classical logic.


Btw, what is different about programs that use call-with-current-continuation? It would seem that both kinds of programs are constructible (duh!).

[jcreed.livejournal.com]

can you parse this for me? Is this the core of the paragraph: "The ability to discriminate is a "tool" that the constructivists don't want to cast aside." ?

Yeah, sorry for writing such dense sentences :) You got the core right, yes. I'm trying to claim that actually there's no easy way to tell whether constructive or nonconstructive logic is more "right" by applying the principle "let's use all the tools we can". This is because a constructivist can tell you the ability to discriminate between things that are true constructively and things that are true only nonconstructively is a "tool", and a classicist will tell you the extra axioms are "tools".

Then it comes down to a sort of question of whether it's mathematics' job to prove fewer things, or more things. In the extreme, it's neither. We don't want to include all of our axioms A in every statement, publishing long-titled papers like, "if you assume the axioms of blah, bloo, blee, and so forth, then 1 = 1". We also don't want to include so many axioms that we derive false statements --- but now we're back arguing whether excluded middle and AC are "true".

It seems very reminiscent to me of arguments between languages with very strict typing disciplines, and languages with "lots of language features", I'm thinking in particular objects, aspects, macros, etc., things that let you do "more things" to existing programs. The people that advocate the former are interested in being able to write fewer wrong programs, and the people that advocate the latter are interested in being able to write more programs.

Ideally we want to write more, and more correct programs, and write more, and more certain proofs, but I'm not sure how to do this.

[gustavolacerda.livejournal.com]

I'm trying to claim that actually there's no easy way to tell whether constructive or nonconstructive logic is more "right" by applying the principle "let's use all the tools we can". This is because a constructivist can tell you the ability to discriminate between things that are true constructively and things that are true only nonconstructively is a "tool", and a classicist will tell you the extra axioms are "tools".

Which is why we need Logical Frameworks :-) Since neither classical logic nor intuitionistic logic will give you all the information, it may become necessary to look at it from the meta-level.

[jcreed.livejournal.com]

I'll split this up further since you've given me so much to reply to :)

I'm not sure I understand what he's saying, but it seems to be related to the provability interpretation.

Yes, it is, and I think you can actually nail down the relationship formally, though I forget how it goes.

It's something like, well, a proof of an implication "A implies B" is really a program that can transform proofs of A into proofs of B. Therefore, if at some future time a proof of A appears, then at that time I can apply my A-to-B machine to get a proof of B. The Kripke axioms for a lots-of-possible-worlds-through-time model of intuitionistic logic specifically says that intuititonist implies must work at any future world like this.

[jcreed.livejournal.com]

I guess they must be talking about classical logic.

I haven't read the paper, but I think they might just be referring to proof theory as opposed to the rest of mathematics, since proof theory (classical or intuitionistic) actually takes finished proofs as objects and does stuff with them. Although when we prove metalogical theorems in logic, then the same concerns about how we come up with proofs as in the rest of mathematics appear, i.e., how we guess and check and use human intuition and try to apply common proof techniques etc.

[jcreed.livejournal.com]

Btw, what is different about programs that use call-with-current-continuation? It would seem that both kinds of programs are constructible (duh!).

Well, when you say intuitionistic logic is about writing programs that embody proofs, it only works if you don't have callcc. Proofs of implications are functions from proofs to proofs, proofs of conjunctions are pairs of proofs, proofs of disjunctions are tagged injections into a sum type of proofs, and the "and so on" is the celebrated Curry-Howard Correspondence.

Then if you can write a program of type P, you've written an intuitionistic proof of P', where P' is P with all the function arrows turned into implications, etc. You can't write programs of "type" ¬¬A ⊃ A or A ∨ ¬A or ((A ⊃ B) ⊃ A) ⊃ A or any of the other standard classically-but-not-intuitionistically true sentences.

But if you put callcc into your language, then you can: in fact, depending on how you set it up, the callcc primitive itself has the type ¬¬A ⊃ A or ((A ⊃ B) ⊃ A) ⊃ A. Then A ∨ ¬A in particular is easily provable/programmable.

So does this mean that intuitionistic ≠ constructive after all? This seemed to be what you were hinting at, and it's a valid objection. We know what callcc is, it has a perfectly well-defined meaning, and we can use it in our programs. So we can write 'constructions' of A ∨ ¬A. However, there's something unsatisfying about these proofs, still. A finished piece of data of type --- a value of type A ∨ ¬A --- ought to be a value of type A or a value of type ¬A. This was true before we introduced callcc, and now it's not. In fact, there was a true statment of this form for every type before we introduced callcc. There is a lovely Value Inversion Theorem that tells us that if no further computation can be performed on a piece of data, its syntactic shape is very highly constrained by its type. Introducing callcc breaks this. This doesn't mean that even the most religious adherents of constructivist logic don't ever use callcc! My advisor is probably one of them, and he happily teaches callcc in his courses, and writes thread libraries using it, and even describes it as a way to give constructive meaning to classical logic. But there's still a reluctance to accept it as part of the basic language, to put it on the same footing with functions and tuples and so on, to give up the ability to imagine what the language looks like without it.

[gustavolacerda.livejournal.com]

So we can write 'constructions' of A ∨ ¬A.

what do they look like?

[jcreed.livejournal.com]

callcc(fn (x : A ∨¬ A cont) => inr(fn (y : A) => throw (inl y) to x))

you can see http://www-2.cs.cmu.edu/~fp/courses/312/handouts/08-aggregate.pdf for more details about what I mean by inr and inl.

The general idea is that I claim to have something of type A ∨ ¬A. You ask me, ok, well, is it derived from something of type A, or derived from something of type ¬A? It has to be one or the other! I claim it's ¬A (because I'm doing an inr into the sum type) but not before saving the current continuation. Now if you actually try to use the promised fact that &lnot;A is true --- i.e. that A is a contradiction --- that means you will try to combine the proof of &lnot;A that I promised you and some proof of A that you came up with, in order to disprove me. But since I have callcc, I can snatch the A-proof away from you and take it with me in my time-machine, back to where I told you that &lnot;A was true. Instead, now, I can tell you that A is true. Look, here's a proof! (It's actually the proof I took from you)

So I get away with promising &lnot;A, and force you to refute me. If you do, callcc lets me change my story. If you don't, then there can be no contradiction and either I guessed right, or else you can't prove that I didn't.

[jcreed.livejournal.com]

As a footnote, I consider looking for either a constructive proof of the FToA or a formal proof of the Jordan theorem as both valuable projects, assuming at least that we have good reason to believe the FToA to be true constructively. (I don't have enough intuition to see why it would or wouldn't be, necessarily)

Both would produce better proofs than we currently have. Maybe the "obviousness" of Jordan is enough for you, but it's not enough for my tastes (and I admit it's a matter of taste). A nonconstructive proof of FToA might feel like satisfying enough to me, but a constructive proof would be more satisfying.

[gustavolacerda.livejournal.com]

A constructive proof of FTA has already been formalized in Coq, and in fact its PX was a notorious failure (the first approximation took a few hours, and was a "0"... the second approximation took even more hours and was "0" to a greater precision... and that was the last iteration it reached).

Then this might be incredibly satisfying then: a constructive proof of FTA without using the rationals.

[jcreed.livejournal.com]

Oh, wow! These look really cool. Thanks for the links.