It seems clear that most everyday human language, and presumably most everyday human thought, is highly metaphorical. Most human statements do not have definite Boolean truth values. Everyday statements have a degree of truth and appropriateness as descriptions of actual events. But while most everyday language is metaphorical, it is also true that some people are capable of doing mathematics — they are capable of working with statements that do have precise truth values. Software engineers in particular must deal with the precise concepts and constructs of formal programming languages. If we are ever going to achieve the singularity it seems likely that we will have to build machines capable of software engineering and hence capable of precise mathematical thought.
How well do we understand mathematical thought? There are many talented mathematicians in the world. But the ability to do mathematics does not imply the ability to create a machine that can do mathematics. Logic is metamathematics — the study of the computational process of dong mathematics. Metamathematics seems more a part of AI than a part of mathematics.
Mathematical thought exhibits various surprising and apparently magical abilities. A software engineer understands the distinction between the implementation and the behavior implemented. Consider a priority queue. It is obvious that if we have two correct implementations of priority queues then we can (or at least should be able to) swap in one for the other in a program that uses a priority queue. This notion that behaviorally identical modules are (or should be) interchangeable in large software systems is one of the magical properties of mathematical thought. How is “identical behavior” understood?
The notion of identical behavior is closely related to the phenomenon of abstraction. Perhaps the most fundamental abstraction is the concept of a cardinal number such as the number seven. I can say I have seven apples and you have two apples and together we have nine apples. The idea that seven plus two is nine abstracts away from the fact that we are talking about apples and seems to involve thought about sets at a more abstract level. We are taking the union of two disjoint sets. The union “behavior” is defined at level of cardinal numbers — the abstraction of a set to its number of elements. Another example of common sense abstraction is the concept of a sequence — the ninth item will be the second item after the seventh item. Yet another example is the concept of a bag of items such as the collection of coins in my pocket which might be three nickels and two quarters. We machine leaning researchers have no trouble understanding that a document can be abstracted to a bag of words. What mental computation underlies this immediate understanding of abstraction? What is abstraction?
It seems clear that abstraction involves the specification of the interface to an object. For example the interface to a priority queue is the set of operations it supports. A bag (multiset) is generally defined as a mapping from a set (such as the set of all words) to a number — the number of times the word occurs in the bag. But this definition misses the point (in my opinion) that any function defines a bag of . For example, a document is a function from ordinal numbers “nth” to words. Any function to words can be abstracted to a bag of words. The amazing thing is that we do not have to be taught this. We just know already. We also know that in passing from a sequence to a bag we are losing information.
Another example is the keys on my key loop. I understand that my two car keys are next to each other on loop even though there is no “first” key among the eight keys on the loop. Somehow I understand that “next to” is part of the “behavior” provided by my key loop while “first” is not.
Lakoff and Nunez argue in the book “Where does Mathematics Come From” that we come to understand numbers through a process of metaphor to physical collections. But I think this is backwards. I think we are able to understand physical collections because we have an innate cognitive architecture which first parses the world into “things” (entities) and assigns them types and groupings. A properly formulated system of logic should include, as a fundamental primitive, a notion of abstraction. The ability to abstract a group to a cardinality, or a sequence to a bag, seems to arise from a general innate capacity for abstraction. Presumably there is some innate cognitive architecture capable of supporting “abstract thought” that distinguishes humans from other animals. A proper formulation of logic — of the foundations of mathematics — will presumably provide insight into the nature of this cognitive architecture.
I will end by shamelessly promoting my paper, Morphoid Type Theory, which I just put on arXiv. The paper describes a new type theoretic foundation of mathematics focusing on abstraction and isomorphism (identity of behavior). Unfortunately the paper is highly technical and is mostly written for professional type theorists and professional mathematicians. Section 2, “inference rules”, should be widely accessible.