GEB; guesstimation; double-counting proofs
Goedel, Escher, Bach really is excellent. It's a pretty long book, and the logic is not trivial even for me (I just received my Master's in Logic). He talks about Henkin algebras, the Feferman hierarchy, etc... all the while trying to stay close to his goal of making metaphors with cognition and consciousness.
--
I want to write a methodology book titled "A Bayesian's Guide to Guesstimation". The inspiration was when, yesterday, I tried to combine several pieces of information in order to estimate the number of people were on this huge party complex near Ostbahnhof last night. I had:
* seen crowds of young people walking towards
* I roughly knew the size of the complex
* I roughly know Munich's population, and I had heard of this place twice from "random" strangers.
I could have stood and counted the people coming out of the station... and, using common sense priors about what time people tend go out, etc., I could have made a better guesstimate.
How can we combine common sense knowledge, intuitions, etc., before we have a formal model of the relationship between all the different pieces of information that one has? This is probably very relevant to the study of expert decision-making, i.e. "intelligence analysis".
--
some notes on double-counting proofs:
Double-counting proofs have the form:
x 'means' a, y 'means' a.
Therefore, extension of x = extension of y.
For example,
The number of unit squares in an n x n square is n^2 ("n^2 *means*
the number of unit squares")
The number of unit squares in an n x n square is SUM_{i=0 to n}(2i +
1) (L-construction) ("this SUM *means* the number of unit squares")
Therefore, SUM_{i=0 to n}(2i + 1) = n^2
Examples of theorems provable by double-counting:
* 1 + 3 + ... + (2n + 1) = n^2 (the above theorem)
* binomial theorem
* several properties of Pascal's triangle
I would like to formalize such proofs, so that they become less
confusing, and easy to check (both by humans and by machines). What
kind of formal system do we need in order to represent the semantics
used in such proofs?
I want to make a language with a compositional semantics for talking
about combinatorial structures and combinatorial problems.
;;number of ways of ordering a set of k individuals
(defun fact (n)
(if (= n 0) 1
(* n (fact (- n 1)))))
;;number of ways of picking k individuals from a set of n, where order matters
(defun perm (n k)
(/ (fact n) (fact k)))
;;number of ways of picking k individuals from a set of n, order does not matter
(defun comb (n k)
(/ (perm n) (fact (- n k))))
(a) How many couples are possible when there are M males and F females?
(* M F)
(b) How many *maximal* configurations are possible?, (i.e. either all
males have a partner or all females have a partner)
if M < F, then (perm F M) (i.e. we first sort the males, then pick
M females from a set of F, order being important)
(perm n k) can be seen in many ways. It can be:
* the number of ways of taking k individuals out of a set of n with
order being important,.
* the number of ways of making a line of k individuals from a set of n
(the bijection with the above can be easily visualized: just imagine
the individuals forming a line, each one going to the back of the line
as he gets picked).
* the number of maximal couple matchings
Despite the existence of the bijection between the first two, it seems
to me that, intensionally, these are two differents *meanings*. They
denote the same extensional quantity, but this is not known a priori.
I want a compositional language to talk about extensions, but also a
more expressive compositional language for talking about these
intensions.
While we tend to see men and women as similar types, we probably tend
to think about HAVE relations differently: if you phrase the
combinatorial problem as being about matching men with ties, students
will probably think of it differently. Another inherent bias is that
whereas two ties may be thought of as identical, one would be less
likely to think of two women as identical.
An interesting area of cognitive/conceptual research would be to see
how these "idealizations" are made: how do we figure out the intended
mathematical interpretation of a given word problem?
(c) How many configurations are possible?
one solution is to sum for each number lower than the maximal.
For nCouples = 1, the problem reduces to (a).
For nCouples = M, the problem reduces to (b).
(defun poss-config (perm F M nCouples)
if M < F,
M * F + (M - 1) * (F - 1) + ... + (M - nCouples + 1) * (F - nCouples + 1)
I think Mateja Jamnik has done work on this subject.
--
I want to write a methodology book titled "A Bayesian's Guide to Guesstimation". The inspiration was when, yesterday, I tried to combine several pieces of information in order to estimate the number of people were on this huge party complex near Ostbahnhof last night. I had:
* seen crowds of young people walking towards
* I roughly knew the size of the complex
* I roughly know Munich's population, and I had heard of this place twice from "random" strangers.
I could have stood and counted the people coming out of the station... and, using common sense priors about what time people tend go out, etc., I could have made a better guesstimate.
How can we combine common sense knowledge, intuitions, etc., before we have a formal model of the relationship between all the different pieces of information that one has? This is probably very relevant to the study of expert decision-making, i.e. "intelligence analysis".
--
some notes on double-counting proofs:
Double-counting proofs have the form:
x 'means' a, y 'means' a.
Therefore, extension of x = extension of y.
For example,
The number of unit squares in an n x n square is n^2 ("n^2 *means*
the number of unit squares")
The number of unit squares in an n x n square is SUM_{i=0 to n}(2i +
1) (L-construction) ("this SUM *means* the number of unit squares")
Therefore, SUM_{i=0 to n}(2i + 1) = n^2
Examples of theorems provable by double-counting:
* 1 + 3 + ... + (2n + 1) = n^2 (the above theorem)
* binomial theorem
* several properties of Pascal's triangle
I would like to formalize such proofs, so that they become less
confusing, and easy to check (both by humans and by machines). What
kind of formal system do we need in order to represent the semantics
used in such proofs?
I want to make a language with a compositional semantics for talking
about combinatorial structures and combinatorial problems.
;;number of ways of ordering a set of k individuals
(defun fact (n)
(if (= n 0) 1
(* n (fact (- n 1)))))
;;number of ways of picking k individuals from a set of n, where order matters
(defun perm (n k)
(/ (fact n) (fact k)))
;;number of ways of picking k individuals from a set of n, order does not matter
(defun comb (n k)
(/ (perm n) (fact (- n k))))
(a) How many couples are possible when there are M males and F females?
(* M F)
(b) How many *maximal* configurations are possible?, (i.e. either all
males have a partner or all females have a partner)
if M < F, then (perm F M) (i.e. we first sort the males, then pick
M females from a set of F, order being important)
(perm n k) can be seen in many ways. It can be:
* the number of ways of taking k individuals out of a set of n with
order being important,.
* the number of ways of making a line of k individuals from a set of n
(the bijection with the above can be easily visualized: just imagine
the individuals forming a line, each one going to the back of the line
as he gets picked).
* the number of maximal couple matchings
Despite the existence of the bijection between the first two, it seems
to me that, intensionally, these are two differents *meanings*. They
denote the same extensional quantity, but this is not known a priori.
I want a compositional language to talk about extensions, but also a
more expressive compositional language for talking about these
intensions.
While we tend to see men and women as similar types, we probably tend
to think about HAVE relations differently: if you phrase the
combinatorial problem as being about matching men with ties, students
will probably think of it differently. Another inherent bias is that
whereas two ties may be thought of as identical, one would be less
likely to think of two women as identical.
An interesting area of cognitive/conceptual research would be to see
how these "idealizations" are made: how do we figure out the intended
mathematical interpretation of a given word problem?
(c) How many configurations are possible?
one solution is to sum for each number lower than the maximal.
For nCouples = 1, the problem reduces to (a).
For nCouples = M, the problem reduces to (b).
(defun poss-config (perm F M nCouples)
if M < F,
M * F + (M - 1) * (F - 1) + ... + (M - nCouples + 1) * (F - nCouples + 1)
I think Mateja Jamnik has done work on this subject.