Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics

This paper presents Automath encodings (which are also valid in LF/λP) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.

The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church's higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo's extended calculus of constructions, and Martin-Löf's predicative type theory) and one foundation based on category theory.

The conclusions of this paper are that the simplest system is type theory (the calculus of constructions), but that type theories that know about serious mathematics are not simple at all. In that case the set theories are the simplest. If one looks at the number of concepts needed to explain such a system, then higher order logic is the simplest, with twenty-five concepts. On the other side of the scale, category theory is relatively complex, as is Martin-Löf's type theory.

(The full Automath sources of the contexts described in this paper are one the web at http://www.cs.ru.nl/~freek/zfc-etc/.)     

Direct perception in the intersubjective context

This paper, in opposition to the standard theories of social cognition found in psychology and cognitive science, defends the idea that direct perception plays an important role in social cognition. The two dominant theories, theory theory (TT) and simulation theory (ST), both posit something more than a perceptual element as necessary for our ability to understand others, i.e., to “mindread” or “mentalize.” In contrast, certain phenomenological approaches depend heavily on the concept of perception and the idea that we have a direct perceptual grasp of the other person’s intentions, feelings, etc. This paper explains precisely what the notion of direct perception means, offers evidence from developmental studies, and proposes a non-simulationist interpretation of the neuroscience of mirror systems.     

MizarMode—an integrated proof assistance tool for the Mizar way of formalizing mathematics

The Emacs authoring environment for Mizar (MizarMode) is today the authoring tool of choice for many (probably the majority of) Mizar authors. This article describes the MizarMode and focuses on the proof assistance functions and tools available in it.

We start with the explanation of the design principles behind the Mizar system, and show how these design principles—mainly the concentration on simple and intuitive human-oriented proofs—have helped Mizar in developing and maintaining a very large body of formalized mathematics.

Mizar is a non-programmable and non-tactical verifier: the proofs are developed in the traditional “write—compile—correct” software programming loop. While this method is in the beginning more laborious than the methods employed in tactical and programmable proof assistants, it makes the “proof code” in the long-run more readable, maintainable and reusable. This seems to be a crucial factor for a long-term and large-scale formalization effort.

MizarMode has been designed with the aim to facilitate this kind of proof development by a number of “code-generating”, “code-browsing” and “code-searching” methods, and tools programmed or integrated within it. These methods and tools now include, e.g., the automated generation of proof skeletons, semantic browsing of the articles and abstracts, structured viewing, proof advice using trained machine learning tools like the Mizar Proof Advisor, deductive tools like MoMM, etc. We give an overview of these proof-assistance tools and their integration in the MizarMode, and also discuss some emerging and future extensions such as integration of external theorem proving assistance.     

The four-card problem and the generality of formal reasoning

Three experiments were designed to investigate the failure of intelligent adults to solve an apparently simple problem of formal reasoning devised by Wason. Both the mode of presentation and the type of material reduced the difficulty of the problem, while retaining its essential form. However, success on the original problem remained at a low level, even when subjects had attempted an easier version and had been given an explanation.

These results enable one to reject a “strong” formulation of Piaget's theory of formal reasoning. A “weaker” formulation is suggested as a basis for further research.     

Context-sensitive elemental theory

My theories of associative learning, like those of N. J. Mackintosh and almost all learning theorists, have employed elemental representations of the stimuli involved. We must take notice when two important contributors to elemental theory, J. M. Pearce and W. K. Estes, find sufficient problems with the theory type to cause them to defect from it. I will describe some of the essential problems, concerning the substantial influence of context on learning and retrieval, characterize the different responses of Pearce and Estes, and, then, propose a variation on a recently developed elemental model that was similarly inspired. The resulting elemental theory has a close quantitative relationship to the “product-rule” of Estes and D. L. Medin, and may help us to rationalize how the same formal experimental design can sometimes produce results that favour the configural interpretation of Pearce and at other times the elemental interpretation of R. A. Rescorla and A. R. Wagner, as these have often been pitted against each other.     

Theories and Ordinals in Proof Theory

Astract How do ordinals measure the strength and computational power of formal theories? This paper is concerned with the connection between ordinal representation systems and theories established in ordinal analyses. It focusses on results which explain the nature of this connection in terms of semantical and computational notions from model theory, set theory, and generalized recursion theory.     

Beyond intuition and instinct blindness: toward an evolutionarily rigorous cognitive science

Cognitive psychology has an opportunity to turn itself into a theoretically rigorous discipline in which a powerful set of theories organize observations and suggest focused new hypotheses. This cannot happen, however, as long as intuition and folk psychology continue to set our research agenda. This is because intuition systematically blinds us to the full universe of problems our minds spontaneously solve, restricting our attention instead to a minute class of unrepresentative “high-level” problems. In contrast, evolutionarily rigorous theories of adaptive function are the logical foundation on which to build cognitive theories, because the architecture of the human mind acquired its functional organization through the evolutionary process. Theories of adaptive function specify what problems our cognitive mechanisms were designed by evolution to solve, thereby supplying critical information about what their design features are likely to be. This information can free cognitive scientists from the blinders of intuition and folk psychology, allowing them to construct experiments capable of detecting complex mechanisms they otherwise would not have thought to test for. The choice is not between no-nonsense empiricism and evolutionary theory; it is between folk theory and evolutionary theory.     

What is folk psychology?

Eliminativism has been a major focus of discussion in the philosophy of mind for the last two decades. According to eliminativists, beliefs and other intentional states are the posits of a folk theory of mind standardly called “folk psychology”. That theory, they claim, is radically false and hence beliefs and other intentional states do not exist. We argue that the expression “folk psychology” is ambiguous in an important way. On the one hand, “folk psychology” is used by many philosophers and cognitive scientists to refer to an internally represented theory of human psychology exploited in the prediction of behavior. On the other hand, “folk psychology” is used to refer to the theory of mind implicit in our everyday talk about mental states. We then argue that sorting out the conceptual and terminological confusion surrounding “folk psychology” has major consequences for the eliminativism debate. In particular, if certain models of cognition turn out to be true, then on some readings of “folk psychology” the arguments for eliminativism collapse.     

Relating Quine's NF to Feferman's EM

We show that, if non-uniform impredicative stratified comprehension is assumed, Feferman's theories of explicit mathematics are consistent with a strong power type axiom. This result answers a problem, raised by Jäger. The proof relies upon an interpretation into Quine's set theory NF with urelements.     

On Classification of Scientific Revolutions

The question whether Kuhn's theory of scientific revolutions could be applied to mathematics caused many interesting problems to arise. The aim of this paper is to discuss whether there are different kinds of scientific revolution, and if so, how many. The basic idea of the paper is to discriminate between the formal and the social aspects of the development of science and to compare them. The paper has four parts. In the first introductory part we discuss some of the questions which arose during the debate of the historians of mathematics. In the second part, we introduce the concept of the epistemic framework of a theory. We propose to discriminate three parts of this framework, from which the one called formal frame will be of considerable importance for our approach, as its development is conservative and gradual. In the third part of the paper we define the concept of epistemic rupture as a discontinuity in the formal frame. The conservative and gradual nature of the changes of the formal frame open the possibility to compare different epistemic ruptures. We try to show that there are four different kinds of epistemic rupture, which we call idealisation, re-presentation, objectivisation and re-formulation. In the last part of the paper we derive from the classification of the epistemic ruptures a classification of scientific revolutions. As only the first three kinds of rupture are revolutionary (the re-formulations are rather cumulative), we obtain three kinds of scientific revolution: idealisation, re-presentation, and objectivisation. We discuss the relation of our classification of scientific revolutions to the views of Kuhn, Lakatos, Crowe, and Dauben. This revised version was published online in August 2006 with corrections to the Cover Date.     

The role of associative history in models of associative learning: A selective review and a hybrid model

Associative learning theories strive to capture the processes underlying and driving the change in strength of the associations between representations of stimuli that develop as a result of experience of the predictive relationships between those stimuli. Historically, formal models of associative learning have focused on two potential factors underlying associative change, namely processing of the conditioned stimulus (in terms of changes in associability) and processing of the unconditioned stimulus (in terms of changes in error). This review constitutes an analysis of the proper role of these two factors, specifically with regard to the way in which they are influenced by associative history (the prior training undergone by cues). A novel “hybrid” model of associative learning is proposed and is shown to provide a more satisfactory account of the effects of associative history on subsequent learning than any previous single-process theory.     

Verbal learning: Incremental vs. all-or-none theory

The incremental and all-or-none theories of verbal learning are compared by means of a little-used but methodologically superior variation of the “drop-out” paradigm with paired associates. Earlier experiments purporting to be relevant to the controversy are rejected as failing to offer a conclusive distinction between the two theories. The results presented here are taken to support the incremental theory. It is suggested that irregularities in the results of this and other experiments are caused by several intrusive factors, and a “dual-factor” hypothesis which was put forward to account for these irregularities is questioned on logical and methodological grounds.     

Mental representation of logical connectives

Logical connectives, such as “AND”, “OR”, “IF . . . THEN”, and “IF AND ONLY IF” are ubiquitous in both language and cognition; however, reasoning with logical connectives is error-prone. We argue that some of these errors may stem from people's tendency to minimize the number of possibilities compatible with logical connectives and to construct a “minimalist” one-possibility representation. As a result, connectives denoting a single possibility (e.g., conjunctions) are likely to be represented correctly, whereas connectives denoting multiple possibilities (e.g., disjunctions or conditionals) are likely to be erroneously represented as conjunctions. These predictions were tested and confirmed in three experiments using different paradigms. In Experiment 1, participants were presented with a multiple-choice task and asked to select all and only those possibilities that would indicate that compound verbal propositions were true versus false. In Experiment 2, a somewhat similar task was used, except that participants were asked later to perform a cued recall of verbal propositions. Finally, Experiment 3 used an old/new recognition paradigm to examine participants' ability to accurately recognize different logical connectives. The results of the three experiments are discussed in relation to theories of representation of possibilities and theories of reasoning.     

Mental models and temporal reasoning

We report five experiments investigating reasoning based on temporal relations, such as: “John takes a shower before he drinks coffee”. How individuals make temporal inferences has not been studied hitherto, but we conjectured that they construct mental models of events, and we developed a computer program that reasons in this way.As the program shows, a problem of the form:

1. a before b

2. b before c

3. d while b

4. e while c

What is the relation between d and e?

where a, b, c, etc. refer to everyday events, calls for just one model, whereas a problem in which the second premise is modified to c before b calls for multiple models because a may occur before c, after c, or at the same time as c.

Experiments 1–3 showed that problems requiring one mental model elicited more correct responses than problems requiring multiple models, which in turn elicited more correct answers than multiple model problems with no valid answers. Experiment 4 contrasted the predictions of the model theory with those based on formal rules of inference; its results corroborated the model theory. Experiment 5 confirmed that a premise leading to multiple models took longer to read than the corresponding premise in one-model problems, and that latency to respond correctly was greater for multiple-model problems than for one-model problems. We conclude that the experiments corroborate the mental model theory.     

Children's syllogistic reasoning

Most theories of the development of deductive ability propose that children acquire formal rules of inference. An alternative theory assumes that reasoning consists of constructing a mental model of the situation described in the premises, scanning the model for an informative conclusion, and then searching for alternative models that refute this conclusion. Hence, performance should reflect two principal factors: the difficulty of constructing a model, which depends on the “figure” of the premises, and the number of models that have to be evaluated to respond correctly. In Experiment 1, two groups of children (9- to 10- and 11- to 12-year-olds) drew conclusions from 20 pairs of syllogistic premises. The results confirmed that children are affected both by figure and by number of models. Experiment 2 corroborated these findings for all 64 possible forms of syllogistic premises. The development of reasoning ability may therefore depend on the acquisition, not of formal rules of logic, but of procedures for manipulating models.     

Computationalism

What counts as a computation and how it relates to cognitive function are important questions for scientists interested in understanding how the mind thinks. This paper argues that pragmatic aspects of explanation ultimately determine how we answer those questions by examining what is needed to make rigorous the notion of computation used in the (cognitive) sciences. It (1) outlines the connection between the Church-Turing Thesis and computational theories of physical systems, (2) differentiates merely satisfying a computational function from true computation, and finally (3) relates how we determine a true computation to the functional methodology in cognitive science. All of the discussion will be directed toward showing that the only way to connect formal notions of computation to empirical theory will be in virtue of the pragmatic aspects of explanation.     

Reconnecting interpretation to reasoning through individual differences

Computational theories of mind assume that participants interpret information and then reason from those interpretations. Research on interpretation in deductive reasoning has claimed to show that subjects' interpretation of single syllogistic premises in an “immediate inference” task is radically different from their interpretation of pairs of the same premises in syllogistic reasoning tasks (Newstead, 1989, 1995; Roberts, Newstead, & Griggs, 2001). Narrow appeal to particular Gricean implicatures in this work fails to bridge the gap. Grice's theory taken as a broad framework for credulous discourse processing in which participants construct speakers' “intended models” of discourses can reconcile these results, purchasing continuity of interpretation through variety of logical treatments. We present exploratory experimental data on immediate inference and subsequent syllogistic reasoning. Systematic patterns of interpretation driven by two factors (whether the subject's model of the discourse is credulous, and their degree of reliance on information packaging) are shown to transcend particular quantifier inferences and to drive systematic differences in subjects' subsequent syllogistic reasoning. We conclude that most participants do not understand deductive tasks as experimenters intend, and just as there is no single logical model of reasoning, so there is no reason to expect a single “fundamental human reasoning mechanism”.     

Challenging epistemology: Interactive proofs and zero knowledge

This essay explores what (if anything) research on interactive zero knowledge proofs has to teach philosophers about the epistemology of mathematics and theoretical computer science. Though such proof systems initially appear ‘revolutionary’ and are a nonstandard conception of ‘proof’, I will argue that they do not have much philosophical import. Possible lessons from this work for the epistemology of mathematics—our models of mathematical proof should incorporate interaction, our theories of mathematical evidence must account for probabilistic evidence, our valuation of a mathematical proof should solely focus on its persuasive power—are either misguided or old hat. And while the differences between interactive and mathematical proofs suggest the need to develop a separate epistemology of theoretical computer science (or at least complexity theory) that differs from our theory of mathematical knowledge, a casual look at the actual practice of complexity theory indicates that such a distinct epistemology may not be necessary.     

Abductive inference in defeasible reasoning: a model for research programmes

Abduction is regarded as the inference process that goes from observations to explanations within a more general context or theoretical framework. There are good characterizations of abduction of surprising observations in monotonic theories. Also, in normal logic programs there are a tight relation among SLDNF and the abduction of negative literals. However, a problem that faces abduction is the explanation of anomalous observations, i.e., observations that are contradictory with respect to the current theory. For this reason, in this work we will consider the problem of embedding abduction of surprising and anomalous observations in defeasible (nonmonotonic) theories. We discuss some issues arising the pragmatic acceptance of abductive inferences in defeasible theories, and how to accommodate anomalous observations and characterize all the possible outcomes that a defeasible theory may face when confronted with new evidence. We explore the use of partial structures approach as a semantic foundation for our system. Finally, we discuss an application of our system as a formal device for representing the methodology of scientific research programmes. In this representation, a programme is regarded as a defeasible theory that draws predictions. When confronted with surprising or anomalous observations, the programme protects itself by means of heuristic procedures, which are represented in our system as abductive inference procedures.