Hiro Uchida, Post Doc Cognitive Science
Hiro Uchida, Post Doc Cognitive Science
Humans can at least apparently conduct deductive reasoning. Various logical inference systems such as classical first-order logic have been developed in order to characterize such human reasoning. The strength of such a properly logical analysis of human reasoning lies in its productivity and predictive power; it enables the theorist to define precisely which data-space the theory covers and then mathematically prove that the theory covers the intended data-space sound and complete. However, as a demerit of a properly logical approach to human reasoning, it is not clear how humans have developed the ability to deal with the knowledge representations that such an analysis indicates. The structure of the logical language representations, which includes abstract elements such as quantifiers and disjunction operators, deviates greatly from the structure of the representations that the other cognitive mechanisms (such as vision and auditory perception) deal with. Thus, a properly logical analysis of human reasoning implies a larger evolutionary gap in the development of this cognitive ability. Moreover, the presence of quantifiers and other propositional operators in the logical language representation makes it harder to ground logical inferences in perception, since perceptual representations do not seem to include corresponding elements. The larger discrepancy between the logical and non-logical representations as above also poses a problem for the computational theory of human-level intelligence. Such a computational theory typically uses both logical and non-logical methods depending on the task, and each of these computational methods uses a different kind of representational structure. In order to improve the efficiency of the spontaneous data-exchange between the logical and non-logical computation methods, it is better to make the knowledge representation that the logical method uses structurally closer to the representations that non-logical methods use, such as topological space for visual computation and some sort of spectrogram-based data-structure for auditory information processing.
Enabling general reasoning in terms of simulations conducted with perceptual mechanisms can solve the above problems, since the language representation that perceptual simulations use does not include abstract elements such as quantifiers and negative and disjunctive operators. The crucial question is how well such an approach can maintain the productivity and predictive power of a properly logical approach. My Issues paper in 2011 has shown that our simulation language can be at least as expressive as classic first-order logic. However, since the paper did not provide the precise inference rules and their intended interpretations in some well-defined semantic structure, such as a finitely axiomatizable algebra, it is not clear if the theory of reasoning using our simulation language is as predictive as the one using a proof theoretically well-behaved logical inference system, such as the sequent calculus for FOL. Admittedly, analyzing the deductive reasoning that humans conduct in terms of perceptual simulations indicates that the deductive reasoning needs not be enabled in terms of a properly logical inference system with its expected properties such as consistency, decidability and completeness. However, giving up these proof theoretic properties means that the resultant theory of human reasoning cannot strictly predict either its precise intended data coverage or whether the theory can actually achieve the intended data coverage in a complete manner. This is because the inference patterns that humans' deductive reasoning covers is potentially infinite and at least apparently, humans seem to be achieving this data coverage by way of a finite number of inference rules.
Based on these considerations, this talk gives the first stab at this problem of axiomatizing the inference rules using our simulation language, as well as speculating what intended semantic structure this inference system would be sound and complete to. Since this is just an initial attempt, I do this by comparing our putative proof theory with the sequent calculus for classic first-order logic, which arguably has the best proof theoretical properties among its established competitors.