![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslI 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:
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)?
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)?