logic for answering combinatorics questions / double-counting proofs

[gusl]

I have this recurring idea that I once wrote about ~1 year ago. Last night, I wrote about it here.

The idea is that we should use multiple kinds of representations for formalizing proofs (and for making automatic reasoners). In combinatorics, this is obvious, if you've ever wanted to formalize your proofs in a natural way. Formal proofs tend to be written in a "syntactic" (algebraic) style, and are unnecessarily long, since there is often an easy "semantic" proof, which is unfortunately hard to make formal.

This is the heart of my post from a year ago:

The formal concept '''perm(n,k)'''(n! / (n-k)!) can be seen in many ways. It can be:
* (1) the number of ways of picking k individuals out of a set of n with order being important.
* (2) the number of ways of making a line of k individuals from a set of n (bijection with (1): just imagine the picked individuals forming a line, each one going to the back of the line as he gets picked. All lines correspond to a picking, and all pickings correspond to a line.).
* (3) the number of maximal couple matchings with n men and k women ("maximal" means all women are matched) (bijection with (1): imagine the k women have been put in a line (no choice about the order of women), and now they must each choose exactly one man. Each matching here corresponds to a picking in (1). Bijection with (2): each matching corresponds to a line of k men and vice-versa.)

Despite the existence of the bijections between these first three concepts, it seems to me that, intensionally, they all have different *meanings*. They denote the same extensional quantity, but this is not known a priori.

In a formal system, the concept of perm(n,k) is enough to prove everything you need to prove. But the intuitive counterparts of this concept, despite their redundancy, may be crucial if we want to capture human intuitions in these kinds of problems. ("Who wants to build computers using only nand gates?" is something Kerber might say)

Readers, please comment on the above. I'd like to know how much of a kook I am for caring so much about this.


Also, can Twelf prove the equivalence of the two ways of counting the number of Full-Houses (as in my pseudo-Prolog code)?

Comments

[ikeepaleopard]

You could do it in twelf by establishing a correspondance between proofs in the first style and proofs in the second and showing that your correspondance establishes a bijection.

[gustavolacerda.livejournal.com]

uhm, I'm talking about a regular object-level proof, I think.

[ikeepaleopard]

Oh weird. I guess you could do that. I feel like formalizing a bunch of arithmetic probably isn't much fun.

[gustavolacerda.livejournal.com]

But it would be interesting if the Twelf proof would capture the proof idea naturally, since the proof idea uses the concept of "number of full houses".

The only proof I have is informal (namely, the "number of full houses" can be broken down into two different expressions, which therefore must be equivalent).

[fancybred.livejournal.com]

Really? What I think aleffert means is that first you declare the four type families two-pair, three-of-kind, full-house1, and full-house2...something like so:

two_pair : num -> num -> card -> card -> card -> card -> type.
three_of_a_kind : num -> card -> card -> card -> type.
full_house1 : hand -> type.
full_house2 : hand -> type.

%mode two_pair +N1 +N2 +C1 +C2 +C3 +C4.
%mode three_of_a_kind +N1 +C1 +C2 +C3.
%mode full_house1 +H.
%mode full_house2 +H.

and write clauses corresponding to the prolog program, e.g.

pf_two_pair : two_pair N1 N2 C1 C2
<- card_number N1 C1
<- card_number N1 C2
<- card_number N2 C3
<- card_number N2 C4.

pf_three_of_a_kind : ...
pf_full_house1 : ...
pf_full_house2 : ...


Then you declare a mapping fh1fh2, again as a type family:

fh1fh2 : (full_house1 H) -> (full_house2 H) -> type.
%mode fh1fh2 +D -E.

and give the clauses of the translation carrying derivations D of full_house1 H to derivations E of full_house2 H. Finally, you prove it is a bijection, i.e. something like the following:

surjective : {D:full_house1 H} fh1fh2 D E -> type.
injective : {D1:full_house1 H} {D2:full_house1 H} {E:full_house2 H} fh1fh2 D1 E -> fh1fh2 D2 E -> eq D1 D2 -> type.

%mode surjective +D -E.
%mode injective +D1 +D2 +E -R.

you write the clauses for surjective and injective, and finally, finally, give a meta-level proof that these relations are total, by calling the termination checker.

[gustavolacerda.livejournal.com]

Thank you. This Curry-Howard thing can be so confusing.

So a derivation of full_house1 is a constructive proof that a hand is a member of it?

How long would it take you to write up this proof in Twelf, if you had to estimate it?

[fancybred.livejournal.com]

> So a derivation of full_house1 is a constructive proof that a hand is a member of it?

Almost: full_house1 is a type family, i.e. for any hand H, full_house1 H is a type. A derivation of full_house1 H (i.e. an object of type full_house1 H) is a constructive proof that H has a full house.

> How long would it take you to write up this proof in Twelf, if you had to estimate it?

Well I don't know how the paper proof is supposed to work, and I'm not really a twelf hacker...but...my guess is that this kind of twelf proof would be about as burdensome as a rigorous set-theoretic argument.

[combinator.livejournal.com]

Your sameness seems to be equivalent to "seems the same" which means "the brain finds their equivalence trivial".

You need to establish a computational model for the human brain, then, establish that the bijections are not trivial on this model.

[selfishgene.livejournal.com]

I find it a lot easier to understand a proof if I can visualize a human scale example thereof. Formal mathematics is a great tool for avoiding mistakes. It sucks for human communication and insight.
Multiple proofs, even if mathematically equivalent, may spark different follow-up ideas. The multiple ways the laws of thermodynamics are stated can each be useful in particular contexts.

[gustavolacerda.livejournal.com]

Formal mathematics is a great tool for avoiding mistakes. It sucks for human communication and insight.

This is an interesting issue. I have argued that formality is the best protocol in the worst case. But in all realistic cases, you're better off relying on the other person having the same intuitions and background knowledge as yourself.

I think one of the holy grails of MKM is to have a system so that we are no longer forced to compromise between formality and high-level communication.

[selfishgene.livejournal.com]

Nice trick if you can do it.