Things I've been meaning to write:

[gusl]

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.

Comments

[jcreed.livejournal.com]

Hey I just got your email with the same stuff in it --- interesting thoughts, but formalizing the geometric intuitions that go into the "L-shape" reasoning, or even the "Little Gauss" theorem about 1+2+...+n (which you can get by visualizing two copies of the triangle that fit together to make an n*(n-1) rectangle) seems like it would be kind of hard to do in a natural way. What is going on in these proofs isn't just the interplay between intension and extension of sets, but facts about the preservation of cardinality under rotation/flipping and rather visually-oriented conclusions about having bijectively filled up some shape with smaller subshapes.

To formalize the proof that even the union of the L-shapes makes a square seems like a lot more work than the instantaneous recognition that we do visually.

[gustavolacerda.livejournal.com]

facts about the preservation of cardinality under rotation/flipping and rather visually-oriented conclusions about having bijectively filled up some shape with smaller subshapes.

Great! You've already come up with some axioms. :-)

If what people do when they do these reasonings is serial (no weird parallel neural processing going on at this level), then I believe it should be "easy" to formalize these reasonings. This is my general position on formalizations.

My general philosophical position is:
* Scientists have logical thoughts.
* It would be a most excellent thing to have an electronic library of the formal correspondants of these thoughts (assumptions, concepts, arguments), i.e. axioms, definitions, theorems.
You could say that I wish to formalize all academic discourse (or to begin with, all "well-known" stuff: undergraduate curricula, etc). I see no reason why this would be impossible. In fact, I think the amount of work involved is on the order of magnitude of the CYC project.

[gustavolacerda.livejournal.com]

from http://www.cl.cam.ac.uk/~mj201/book/foreword.html:

What is novel about Mateja Jamnik's work is that she has found an explanation of at least part of the mystery of how humans are able to ``see'' the truth of certain mathematical propositions merely by contemplating appropriate diagrams and constructions. This ability to ``see'' is one of the really fundamental components of the human mathematical cognitive repertoire. As the late great mathematician G. H. Hardy put it: in the last analysis there is no such thing as ``proof'' - all a mathematician really does is observe what is there. To convince others of what he observes to be the case all he can do is point and say: do you see? Mateja Jamnik's program ``sees'', for example, as we do, that a 5 by 5 array of dots is also a nest of 5 ``ells'' containing respectively 1, 3, 5, 7, and 9 dots, and that there is nothing special about this special case. It and we can see that the case of 5 is but one instance of the general pattern whereby, for any n, an n by n array of dots is also a nest of n ``ells'' containing respectively 1, 3, 5, 7, ..., 2n-1 dots. In this way it and we can directly see, as a kind of mathematical sense datum, the truth of the mathematical theorem that the number n2 is the sum of the first n odd numbers. This act of seeing is analyzed in the program as a set of alternative decompositions of a given square array; we can see it either as a row of columns: or as a column of rows, or as a nest of frames, or as a nest of ells, or as an array of subsquares, and so on and on. Each of these perceptions is the same as seeing the truth of a corresponding mathematical theorem.

[jcreed.livejournal.com]

I like that Hardy comment; I've tried to think now and then about the fundamental cognitive processes that get used when I check proofs, and a really important one (at least in the kind of proofs that I do most often) is observing that two symbols are the same. This is a foundational task whenever you have variable names at all: to substitute something for this x, I have to recognize those xs over there as being the same as it, and all the other variables as different from it. This seems connected to me somehow to the task of recognizing this L-shape over here as being isomorphic to that L-shape over there (modified by a rotation as well as a translation)

Which brings up the fact that we do in fact consider symbols "up to isomorphism" in more cases than we realize; an x set in a smaller font in the superscript of some symbol is the same x, and it's not even (if you're using TeX) exactly the same image as the bigger x scaled down, for TeX does optical font scaling, changing the proportions of letters at various font sizes to make them more legible.

So at the very low level, I think there is very little hope of formalizing what's going on, because it depends too finely on what our brains are actually doing — but this hasn't hindered formalization of symbolic proofs, nor should it hinder formalization of diagrammatic proofs. For we succeeded in finding various good sets of middle-level primitives, (for instance, first-order logic, as you mentioned in your other reply) and I suppose then that there is hope for finding good sets of diagrammatic primitives. Maybe Jamnik already has — I should go read her stuff.

[gustavolacerda.livejournal.com]

I mean:

"The fact is that [the heuristic approach] has been severely hampered by a shortage of insights into mathematical cognition and ratiocination. Professor Alan Bundy's group at the University of Edinburgh has for some time now been patiently and insightfully seeking to remedy this shortage."

which reminds me of this previous post of mine, in which I quoted
Manfred Kerber, Martin Polleti - On the Design of Mathematical Concepts

That foundational systems like first-order logic or set theory can be used to construct large parts of existing mathematics and formal reasoning is one of the deep mathematical insights. Unfortunately it has been used in the field of automated theorem proving as an argument to disregard the need for a diverse variety of representations. While design issues play a major rôle in the formation of mathematical concepts, the theorem proving community has largely neglected them. In this paper we argue that this leads not only to problems at the human computer interaction end, but that it causes severe problems at the core of the systems, namely at their representation and reasoning capabilities.

i.e. people in the ATP community are using their hammer on too many things, because in fact it works to some extent. But not everything is a nail... which is why using representations that mirror the concepts (and logics?) used by human mathematicians (e.g. visual concepts) can improve ATP at its core.

--

But actually, I don't see why diagrammatic reasoning would be inherently more "heuristic" than sentential reasoning.

[gustavolacerda.livejournal.com]

For we succeeded in finding various good sets of middle-level primitives

I guess my point is that if you can put your reasoning into a few words, or think about it in a conscious / "serial" way, that means that this formalism is already implemented inside the very restricted machine in which conscious thought happens. As a consequence, these "middle-level primitives" can also be implemented on a computer. My main premise is the simplicity of human consciousness.

But from the standpoint of a general intelligence, what you call "middle-level primitives" are actually very low-level (low Kolmogorov Complexity). For a human mind, logic may in fact be high level, but this is only because the brain is a terribly inefficient machine in which logic is implemented on top of neural networks (imagine that!!).

[gustavolacerda.livejournal.com]

Excuses for all the deleted and reposted comments. I wish LJ were more wiki-like.

believing is seeing

[gustavolacerda.livejournal.com]

It and we can see that the case of 5 is but one instance of the general pattern whereby, for any n, an n by n array of dots is also a nest of n ``ells'' containing respectively 1, 3, 5, 7, ..., 2n-1 dots. In this way it and we can directly see, as a kind of mathematical sense datum, the truth of the mathematical theorem that the number n2 is the sum of the first n odd numbers.

We only sense this "mathematical sense datum" because we believe in induction.