This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

One logic or many? I say—many. Or rather, I say there is one logic for each way of specifying the class of all possible circumstances, or models, i.e., all ways of interpreting a given language. But because there is no unique way of doing this, I say there is no unique logic except in a relative sense. Indeed, given any two competing logical theories T1 and T2 (in the same language) one could always consider their common core, T, and settle (...) on that theory. So, given any language L, one could settle on the minimal logic T0 corresponding to the common core shared by all competitors. That would be a way of resisting relativism, as long as one is willing to redraw the bounds of logic accordingly. However, such a minimal theory T0 may be empty if the syntax of L contains no special ingredients the interpretation of which is independent of the specification of the relevant L-models. And generally—I argue—this is indeed the case. (shrink)

We document the influence on programming language semantics of the Platonism/formalism divide in the philosophy of mathematics.

This paper investigates the ontological presuppositions of quantifier logic. It is seen that the actual infinite, although present in the usual completeness proofs, is not needed for a proper semantic foundation. Additionally, quantifier logic can be given an adequate formulation in which neither the notion of individual nor that of a predicate appears.

Gödel regarded the Dialectica interpretation as giving constructive content to intuitionism, which otherwise failed to meet reasonable conditions of constructivity. He founded his theory of primitive recursive functions, in which the interpretation is given, on the concept of computable function of finite type. I will (1) criticize this foundation, (2) propose a quite different one, and (3) note that essentially the latter foundation also underlies the Curry-Howard type theory, and hence Heyting's intuitionistic conception of logic. Thus the Dialectica interpretation (in (...) so far as its aim was to give constructive content to intuitionism) is superfluous. (shrink)

Kripke (1982, Wittgenstein on rules and private language. Cambridge, MA: MIT Press) presents a rule-following paradox in terms of what we meant by our past use of “plus”, but the same paradox can be applied to any other term in natural language. Many responses to the paradox concentrate on fixing determinate meaning for “plus”, or for a small class of other natural language terms. This raises a problem: how can these particular responses be generalised to the whole of natural language? (...) In this paper, I propose a solution. I argue that if natural language is computable in a sense defined below, and the Church–Turing thesis is accepted, then this auxiliary problem can be solved. (shrink)

The Lisp programming language is often described as the first functional programming language and also as an important early AI language. In the history of functional programming, however, it occupies a rather anomalous position, as the circumstances of its development do not fit well with the widely accepted view that functional languages have been developed through a theoretically-inspired project of deriving practical programming languages from the lambda calculus. This paper examines the origins of Lisp in the early AI programming work (...) of the mid-to-late 1950s, and in particular in the work of Allen Newell, Cliff Shaw and Herbert Simon. Their 1956 program, the Logic Theory Machine, introduced new ideas about data and program structures that were articulated in response to perceived limitations in existing programming technique. Later writers, notably John Backus, have described these features as constituting a “programming language style” distinct from the traditional style that preceded it. The paper examines the origins of the earlier style in practices of manual computation, analyses the key technical differences between it and the style first manifested in the Logic Theory Machine, and concludes that programming practice and experience play a large and underappreciated role in the development of programming styles and languages. (shrink)

Pure type systems arise as a generalisation of simply typed lambda calculus. The contemporary development of mathematics has renewed the interest in type theories, as they are not just the object of mere historical research, but have an active role in the development of computational science and core mathematics. It is worth exploring some of them in depth, particularly predicative Martin-Löf’s intuitionistic type theory and impredicative Coquand’s calculus of constructions. The logical and philosophical differences and similarities between them will be (...) studied, showing the relationship between these type theories and other fields of logic. (shrink)

This paper addresses a fundamental line of research in neuroscience: the identification of a putative neural processing core of the cerebral cortex, often claimed to be “canonical”. This “canonical” core would be shared by the entire cortex, and would explain why it is so powerful and diversified in tasks and functions, yet so uniform in architecture. The purpose of this paper is to analyze the search for canonical explanations over the past 40 years, discussing the theoretical frameworks informing this research. (...) It will highlight a bias that, in my opinion, has limited the success of this research project, that of overlooking the dimension of cortical development. The earliest explanation of the cerebral cortex as canonical was attempted by David Marr, deriving putative cortical circuits from general mathematical laws, loosely following a deductive-nomological account. Although Marr’s theory turned out to be incorrect, one of its merits was to have put the issue of cortical circuit development at the top of his agenda. This aspect has been largely neglected in much of the research on canonical models that has followed. Models proposed in the 1980s were conceived as mechanistic. They identified a small number of components that interacted as a basic circuit, with each component defined as a function. More recent models have been presented as idealized canonical computations, distinct from mechanistic explanations, due to the lack of identifiable cortical components. Currently, the entire enterprise of coming up with a single canonical explanation has been criticized as being misguided, and the premise of the uniformity of the cortex has been strongly challenged. This debate is analyzed here. The legacy of the canonical circuit concept is reflected in both positive and negative ways in recent large-scale brain projects, such as the Human Brain Project. One positive aspect is that these projects might achieve the aim of producing detailed simulations of cortical electrical activity, a negative one regards whether they will be able to find ways of simulating how circuits actually develop. (shrink)

In this paper we defend structural representations, more specifically neural structural representation. We are not alone in this, many are currently engaged in this endeavor. The direction we take, however, diverges from the main road, a road paved by the mathematical theory of measure that, in the 1970s, established homomorphism as the way to map empirical domains of things in the world to the codomain of numbers. By adopting the mind as codomain, this mapping became a boon for all those (...) convinced that a representation system should bear similarities with what was being represented, but struggled to find a precise account of what such similarities mean. The euforia was brief, however, and soon homomorphism revealed itself to be affected by serious weaknesses, the primary one being that it included systems embarrassingly alien to representations. We find that the defense attempts that have followed, adopt strategies that share a common format: valid structural representations come as “homomorphism plus X”, with various “X”, provided in descriptive format only. Our alternative direction stems from the observation of the overlooked departure from homomorphism as used in the theory of measure and its later use in mental representations. In the former case, the codomain or the realm of numbers, is the most suited for developing theorems detailing the existence and uniqueness of homomorphism for a wide range of empirical domains. In the latter case, the codomain is the realm of the mind, possibly more vague and more ill-defined than the empirical domain itself. The time is ripe for articulating the mapping between represented domains and the mind in formal terms, by exploiting what is currently known about coding mechanisms in the brain. We provide a sketch of a possible development in this direction, one that adopts the theory of neural population coding as codomain. We will show that our framework is not only not in disagreement with the “plus X” proposals, but can lead to natural derivation of several of the “X”. (shrink)

The meaning of 'most' can be described in many ways. We offer a framework for distinguishing semantic descriptions, interpreted as psychological hypotheses that go beyond claims about sentential truth conditions, and an experiment that tells against an attractive idea: 'most' is understood in terms of one-to-one correspondence. Adults evaluated 'Most of the dots are yellow', as true or false, on many trials in which yellow dots and blue dots were displayed for 200 ms. Displays manipulated the ease of using a (...) 'one-to-one with remainder' strategy, and a strategy of using the Approximate Number System to compare of (approximations of) cardinalities. Interpreting such data requires care in thinking about how meaning is related to verification. But the results suggest that 'most' is understood in terms of cardinality comparison, even when counting is impossible. (shrink)

I argue that linguistic meanings are instructions to build monadic concepts that lie between lexicalizable concepts and truth-evaluable judgments. In acquiring words, humans use concepts of various adicities to introduce concepts that can be fetched and systematically combined via certain conjunctive operations, which require monadic inputs. These concepts do not have Tarskian satisfaction conditions. But they provide bases for refinements and elaborations that can yield truth-evaluable judgments. Constructing mental sentences that are true or false requires cognitive work, not just an (...) exercise of basic linguistic capacities. (shrink)

Traces the development of recursive functions from their origins in the late nineteenth century to the mid-1930s, with particular emphasis on the work and influence of Kurt Gödel.

The topics of structural proof theory and logic programming have influenced each other for more than three decades. Proof theory has contributed the notion of sequent calculus, linear logic, and higher-order quantification. Logic programming has introduced new normal forms of proofs and forced the examination of logic-based approaches to the treatment of bindings. As a result, proof theory has responded by developing an approach to proof search based on focused proof systems in which introduction rules are organized into two alternating (...) phases of rule application. Since the logic programming community can generate many examples and many design goals, the close connections with proof theory have helped to keep proof theory relevant to the general topic of computational logic. (shrink)

Leon Henkin (1921–2006) was not only an extraordinary logician, but also an excellent teacher, a dedicated professor and an exceptional person. The first two sections of this paper are biographical, discussing both his personal and academic life. In the last section we present three aspects of Henkin’s work. First we comment part of his work fruit of his emphasis on teaching. In a personal communication he affirms that On mathematical induction, published in 1969, was the favourite among his articles with (...) a somewhat panoramic nature and not meant exclusively to specialists. This subject is covered in the first subsection. Needless to say that we also analyse Henkin’s better known contribution: his completeness method. His renowned results on completeness for both type theory and first order logic were part of his thesis, The Completeness of Formal Systems, presented at Princeton in 1947 under the advise of Alonzo Church. It is interesting to note that he obtained the proof of completeness for first order logic readapting the argument for the theory of types. The last subsection is devoted to philosophy. The work most directly related to philosophy is an article entitled: Some Notes on Nominalism which appeared in the Journal of Symbolic Logic in 1953. Unfortunately, we are not covering his contribution to the field of cylindric algebras. As a matter of fact, Henkin spent many years investigating algebraic structures with Alfred Tarski and Donald Monk, among others. (shrink)

There are three different degrees to which we may allow a systematic theory of the world to embrace the idea of relatedness—supposing realism about non-symmetric relations as a background requirement. (First Degree) There are multiple ways in which a non-symmetric relation may apply to the things it relates—for the binary case, aRb ≠ bRa. (Second Degree) Every such relation has a distinct converse—for every R such that aRb there is another relation R* such that bR*a. (Third Degree) Each one of (...) them applies in an order to the things it relates—with regard to the state that results from R's applying to a and b, either R applies to a first and b second, or it applies to b first and a second. Whereas the first degree is near-indubitable, embracing the second or third generates unwholesome consequences. The second degree embodies a commitment to the existence of a superfluity of distinct converses and states to which such relations give rise. The third degree embodies commitment to recherché facts of the matter about how the states that arise from the application of one non-symmetric relation compare to any other. It is argued that accounts that purport to offer an analysis of the first degree generate unwelcome second or third degree consequences. This speaks in favour of our adopting an account of the application of relations that's not an analysis at all, an account that takes the first degree as primitive. (shrink)

This paper is dedicated to Alonzo Church, who died in August 1995 after a long life devoted to logic. To Church we owe lambda calculus, the thesis bearing his name and the solution to the Entscheidungsproblem.His well-known book Introduction to Mathematical LogicI, defined the subject matter of mathematical logic, the approach to be taken and the basic topics addressed. Church was the creator of the Journal of Symbolic Logicthe best-known journal of the area, which he edited for several decades This (...) paper is in three sections. The first is written in journalistic style:the story of the life of AlonzoChurch is told, including some of the many anecdotes I have collected from different sources. The secondpart is devoted to his work, but is far from being exhaustive. The last part is more original; in it I attempto show that Church’s great discovery was lambda calculus and that his remaining contributions weremainly inspired afterthoughts in the sense that most of his contributions as well as some of his pupils derivefrom that initial achievement. Included are Kleene’s Recursion Theory and the completeness proof ofHenkin. I have added an appendix in which is presented the typed lambda calculus and a proof of theundecidability of first-order logic. (shrink)

Algorithmic chemistries are often based on a fixed formalism which limits the fragment of chemistry expressible in the domain of the models. This results in limited applicability of the models in contemporary mathematical chemistry and is due to the poor fit between the logic used for model construction and the system being modeled. In this paper, I propose a system-oriented methodology which selects a formalism through a mapping of chemical transformation rules to proof-theoretic structural rules. Using a formal specification framework (...) from the field of artificial chemistry, expressive adequacy is ensured by the choice of logic being based on the system properties to be modeled. To illustrate the methodology, a case study is provided that shows how the proposed approach selects linear logic for modeling resource sensitivity and the proof-theoretic interpretation facilitates translation to a programming language. Since the method results in a plurality of models, I conclude with a discussion on how the proposal contributes to multi-model paradigms in computational pharmacology. (shrink)

This paper proposes an Interface Transparency Thesis concerning how linguistic meanings are related to the cognitive systems that are used to evaluate sentences for truth/falsity: a declarative sentence S is semantically associated with a canonical procedure for determining whether S is true; while this procedure need not be used as a verification strategy, competent speakers are biased towards strategies that directly reflect canonical specifications of truth conditions. Evidence in favor of this hypothesis comes from a psycholinguistic experiment examining adult judgments (...) concerning ‘Most of the dots are blue’. This sentence is true if and only if the number of blue dots exceeds the number of nonblue dots. But this leaves unsettled, e.g., how the second cardinality is specified for purposes of understanding and/or verification: via the nonblue things, given a restriction to the dots, as in ‘|{x: Dot(x) & ~Blue(x)}|’; via the blue things, given the same restriction, and subtraction from the number of dots, as in ‘|{x: Dot(x)}| – |{x: Dot(x) & Blue(x)}|’; or in some other way. Psycholinguistic evidence and psychophysical modeling support the second hypothesis. (shrink)

Scientific knowledge develops in an increasingly fragmentary way.A multitude of scientific disciplines branch out. Curiosity for thisdevelopment leads into quests for a unifying understanding. To a certain extent, foundational studies provide such unification. There is a tendency, however, also of a fragmentary growth of foundational studies, like in a multitude of disciplinaryfoundations. We suggest to look at the foundational problem, not primarily as a search for foundations for one discipline in another, as in some reductionist approach, but as a steady (...) revelation ofpresuppositions for individual scientific theories – which are boundto meet, sooner or later, in a common language. A decisive point hereis our holistic conception of language, as a whole of description-interpretation processes which are entangled(complementary) in the language itself. For every language there is alinguistic complementarity. We suggest this unique form ofentanglement as a unifying presupposition, ultimately foundational forall communicable knowledge. Involved is a linguistic realism, in terms ofwhich we critically examine ``language-world'' problems, as exposed byWittgenstein, and Russell, about a foundational interdependence of language andreality (world). Throughout, we attach to the developmentof foundational studies of mathematics, logics, and the naturalsciences. In particular, we study the interpretation problem foraxioms of infinity in some detail. We emphasize that the holistic concept of language contradicts Carnap's semiotic fragmentation thesis (thus, no clean cutbetween syntax, semantics, pragmatics). (shrink)

The paper is Part III of the large research, dedicated to both the revision of the system of basic logical categories and the generalization of modern predicate logic to functional logic. We determinate and contrapose modern Fregean logistics and proposed by the author ultra-Fregean logistics, next we describe values and arguments of functions, arguments of relations, relations themselves, sets (classes), and subsets (subclasses) as derivative categories (concepts) of ultrafregean logistics. Logistics is a part of metalogic, independent of semantics. Fregean logictics (...) is a metalogical theory, based on the quadruple <particular (individual), predicate, equality, sequence>; it generates predicate logic. Ultrafregean logictics is based on the quadruple <particular, function, representation, sequence>, where the notion of a function is a generalization of the notion of a predicate and the notion of representation is a generalization of the notion of equality; this logictics generates functional logic. For the completely correct denotation of the functional values, we need the Churchian symbolics with parenthesis. Predicates are usually identified with relations. A relation is the derived and even definable category of ultra-Fregean logictics. Namely, relations are representations by functions (of one of their arguments). We show that Frege could really establish this definition and the notion (category) of representation but, unfortunately, rejected this course of thought. Next, we show that every n-ary relation can be resolved for some of its arguments via some (n-1)-ary function. A set, or class, is a derived and not definable category of ultra-Fregean logistics. The universal way to introduce the sets is Frege’s abstraction principle. We formulate this principle for functional logic and show that the notion of a set is quantified, so there is the dual existential notion of a nonempty subset, involved by the same abstraction principle. (shrink)

A sentence like every circle is blue might be understood in terms of individuals and their properties or in terms of a relation between groups. Relatedly, theorists can specify the contents of universally quantified sentences in first-order or second-order terms. We offer new evidence that this logical first-order vs. second-order distinction corresponds to a psychologically robust individual vs. group distinction that has behavioral repercussions. Participants were shown displays of dots and asked to evaluate sentences with each, every, or all combined (...) with a predicate. We find that participants are better at estimating how many things the predicate applied to after evaluating sentences in which universal quantification is indicated with every or all, as opposed to each. We argue that every and all are understood in second-order terms that encourage group representation, while each is understood in first-order terms that encourage individual representation. Since the sentences that participants evaluate are truth-conditionally equivalent, our results also bear on questions concerning how meanings are related to truth-conditions. (shrink)

This paper discusses certain problems arising within the treatment of the senses of functions in Alonzo Church's Logic of Sense and Denotation. Church understands such senses themselves to be "sense-functions," functions from sense to sense. However, the conditions he lays out under which a sense-function is to be regarded as a sense presenting another function as denotation allow for certain undesirable results given certain unusual or "deviant" sense-functions. Certain absurdities result, e.g., an argument can be found for equating any two (...) senses of the same type. An alternative treatment of the senses of functions is discussed, and is thought to do better justice to Frege's original theory. (shrink)

It is well known that the circumflex notation used by Russell and Whitehead to form complex function names in Principia Mathematica played a role in inspiring Alonzo Church's “lambda calculus” for functional logic developed in the 1920s and 1930s. Interestingly, earlier unpublished manuscripts written by Russell between 1903–1905—surely unknown to Church—contain a more extensive anticipation of the essential details of the lambda calculus. Russell also anticipated Schönfinkel's combinatory logic approach of treating multiargument functions as functions having other functions as value. (...) Russell’s work in this regard seems to have been largely inspired by Frege’s theory of functions and “value-ranges”. This system was discarded by Russell due to his abandonment of propositional functions as genuine entities as part of a new tack for solving Russell’s paradox. In this article, I explore the genesis and demise of Russell’s early anticipation of the lambda calculus. (shrink)

This essay considers arguments for and against syntactical constraints on the proper formalization of definitions, originally owing to Alfred Tarski. It discusses and refutes an application of the constraints generalized to include a prohibition against not only object-place but also predicate-place variables in higher-order logic in a criticism of a recent effort to define the concept of heterologicality in a strengthened derivation of Grelling's paradox within type theory requirements. If the objections were correct, they would offer a more general moral (...) for the proper formal definition of terms in philosophical logic. The criticism nevertheless seems mistaken both in the substance and specific application with respect to legitimate synctactical constraints on definitions of key concepts in the case of Grelling's paradox. As such, the critique provides no justification for overturning previous conclusions concerning the possibility of resurrecting a type-observant version of Grelling's heterologicality paradox. (shrink)

The question whether qualities are metaphysically more fundamental than or mere limiting cases of relations can be addressed in an applied symbolic logic. There exists a logical equivalence between qualitative and relational predications, in which qualities are represented as one-argument-place property predicates, and relations as more-than-one-argument-place predicates. An interpretation is first considered, according to which the logical equivalence of qualitative and relational predications logically permits us ontically to eliminate qualities in favor of relations, or relations in favor of qualities. If (...) metaphysics is understood at least in part as an exercise in ontic economy, then we may be encouraged to adopt a property ontology of qualities without quality-irreducible relations, or relations without relation-irreducible qualities. If either strategy is followed, the choice of reducing qualities to relations or relations to qualities will need to be justified on extra-logical grounds. These might include a perceived greater intuitiveness, explanatory fecundity, compatibility with cognitive ontogeny or developmental psychology, expressive or explanatory elegance or cumbersomeness, and an open-ended list of philosophical motivations that could reasonably favor the ontic prioritization of qualities over relations or relations over qualities. Despite its intuitive appeal, the thesis that logical equivalence together with extra-logical preferences justifies unidirectional ontic reduction of relations to qualities or qualities to relations is rejected in light of the more defensible proposition that the logical equivalence of qualitative and relational predications actually supports the opposite conclusion, that both qualities and relations are logically indispensable to a complete ontology of properties. The logical equivalence of qualitative and relational predications, insofar as we continue to observe the distinction, makes it logically necessary ontically for both qualities and relations to exist whenever either one exists. That logically equivalent qualitative and relational predications have as their truth-makers the exemplification by objects of both qualities and relations as equi-foundational properties further suggests that there is no deeper logical distinction between qualities and relations, but only two convenient lexical-grammatical designations for property predications involving one- versus more-than-one-argument-place. (shrink)

This essay examines an argument of perennial importance against naive Leibnizian absolute identity theory, originating with Ruth Barcan in 1947 (Barcan, R. 1947. ?The identity of individuals in a strict functional 3 calculus of second order?, Journal of Symbolic Logic, 12, 12?15), and developed by Arthur Prior in 1962 (Prior, A.N. 1962. Formal Logic. Oxford: The Clarendon Press), presented here in the form offered by Nicholas Griffin in his 1977 book, Relative Identity (Griffin, N. 1977. Relative Identity. Oxford: The Clarendon (...) Press). The objection considers the property of being necessarily identical to a specific object a as a counterexample to Leibnizian identity conditions, and more particularly to the indiscernibility of identicals, when it is only contingently true that a=b. The inquiry eliminates necessity and reference to a specifically designated object as responsible for the counterexample, leaving only identity. The requirements for an exact reinterpretation of Leibniz's Law in light of counterexamples involving converse intentional properties and the family of properties suggested by the property of being necessarily identical to a where a=b (or an equivalent definite descriptor variation) is only logically contingently true, are formalized in a more powerful, counterexample-resistant version of Leibniz's Law that does not succumb to relative identity as a necessary alternative motivated by desperation over the failure of the absolute identity principle. (shrink)

An argument against multiply instantiable universals is considered in neglected essays by Stanislaw Lesniewski and I.M. Bochenski. Bochenski further applies Lesniewski's refutation of universals by maintaining that identity principles for individuals must be different than property identity principles. Lesniewski's argument is formalized for purposes of exact criticism and shown to involve both a hidden vicious circularity in the form of impredicative definitions and explicit self-defeating consequences. Syntactical restrictions on Leibnizian indiscernibility of identicals are recommended to forestall Lesniewski's paradox.

In a multiagent and multi-cultural world, the fine-grained analysis of agents’ dynamic behaviour, i.e. of their activities, is essential. Dynamic activities are actions that are characterized by an agent who executes the action and by other participants of the action. Wh-questions on the participants of the actions pose a difficult particular challenge because the variability of the types of possible answers to such questions is huge. To deal with the problem, we propose the analysis and classification of Wh-questions apt for (...) agents’ communication in a multiagent system (MAS). Our proposal of such a system consists of agents who communicate with their fellow agents by messaging so that each autonomous agent, though resource-bounded, can make less or more rational decisions to meet its own and collective goals. In addition, by communicating with other fellow agents and their environment, agents can learn new concepts and enrich their ontology so that their behaviour is dynamic. We aim to make a general proposal of the system so that the ‘envelope’ of agents’ messages can be formalized in any MAS standard, be it The Foundation for Intelligent Physical Agents - Agent Communication Language (FIPA-ACL) or Knowledge Query and Manipulation Language (KQML). Yet, the content of messages is encoded in a formalized natural language. To this end, we apply Transparent Intensional Logic (TIL) with its procedural semantics which is particularly apt for a fine-grained analysis in which all the semantically salient features of natural language can be plausibly formalized. In this paper, we concentrate on analysing the content of query messages, particularly the content of those that encode Wh-questions and the answers to them. We also summarize TIL deduction system that makes it possible to answer such questions in an intelligent way. Linguists distinguish several subtypes of Wh-questions. Though the linguistic classification is helpful, it is not always suitable for agents’ communication and reasoning. We need the classification based on a logical analysis of Wh-questions so that the agents can infer possible answers to such questions rather than only looking for them by keywords. This paper aims to apply an appropriate classification of the logical types of Wh-questions and the analysis of such questions; we concentrate in particular on questions concerning the participants of activities. The application of these results to the analysis of processes and events based on verb valency frames is another novelty of the paper. (shrink)

The issue of whether formal reasoning or a computing-intensive approach is the most efficient manner to address scientific questions is the subject of some considerable debate and pertains not only to the nature of the phenomena and processes investigated by scientists, but also the nature of the equation and algorithm objects they use. Although algorithms and equations both rely on a common background of mathematical language and logic, they nevertheless possess some critical differences. They do not refer to the same (...) level of symbolization, as equations are based on integrated concepts in a denotational manner, while algorithms specifically break down a complex problem into more elementary operations, in an operational manner. They may therefore be considered as suited to the representation of different phenomena. Specifically, algorithms are by nature sufficient to represent weak emergent phenomena, but not strong emergent patterns, while equations can do both. Finally, the choice between equations and algorithms are by nature sufficient to represent weak emergent phenomena, but not strong emergent patterns, while equations behave conversely. We propose a simplified classification of scientific issues for which both equation- and/or algorithm-based approaches can be envisaged, and discuss their respective pros and cons. We further discuss the complementary and sometimes conflicting uses of equations and algorithms in a context of ecological theory of metapopulation dynamics. We finally propose both conceptual and practical guidelines for choosing between the alternative approaches. (shrink)

Questions of definedness are ubiquitous in mathematics. Informally, these involve reasoning about expressions which may or may not have a value. This paper surveys work on logics in which such reasoning can be carried out directly, especially in computational contexts. It begins with a general logic of partial terms, continues with partial combinatory and lambda calculi, and concludes with an expressively rich theory of partial functions and polymorphic types, where termination of functional programs can be established in a natural way.

The problem of representing the spatial structure of images, which arises in visual object processing, is commonly described using terminology borrowed from propositional theories of cognition, notably, the concept of compositionality. The classical propositional stance mandates representations composed of symbols, which stand for atomic or composite entities and enter into arbitrarily nested relationships. We argue that the main desiderata of a representational system — productivity and systematicity — can (indeed, for a number of reasons, should) be achieved without recourse to (...) the classical, proposition-like compositionality. We show how this can be done, by describing a systematic and productive model of the representation of visual structure, which relies on static rather than dynamic binding and uses coarsely coded rather than atomic shape primitives. (shrink)

This paper deals with two issues. First, it identifies structured propositions with logical procedures. Second, it considers various rigorous definitions of the granularity of procedures, hence also of structured propositions, and comes out in favour of one of them. As for the first point, structured propositions are explicated as algorithmically structured procedures. I show that these procedures are structured wholes that are assigned to expressions as their meanings, and their constituents are sub-procedures occurring in executed mode. Moreover, procedures are not (...) mere aggregates of their parts; rather, procedural constituents mutually interact. As for the second point, there is no universal criterion of the structural isomorphism of meanings, hence of co-hyperintensionality, hence of synonymy for every kind of language. The positive result I present is an ordered set of rigorously defined criteria of fine-grained individuation in terms of the structure of procedures. Hence procedural semantics provides a solution to the problem of the granularity of co-hyperintensionality. (shrink)

The classical theory of semantic information (ESI), as formulated by Bar-Hillel and Carnap in 1952, does not give a satisfactory account of the problem of what information, if any, analytically and/or logically true sentences have to offer. According to ESI, analytically true sentences lack informational content, and any two analytically equivalent sentences convey the same piece of information. This problem is connected with Cohen and Nagel's paradox of inference: Since the conclusion of a valid argument is contained in the premises, (...) it fails to provide any novel information. Again, ESI does not give a satisfactory account of the paradox. In this paper I propose a solution based on the distinction between empirical information and analytic information. Declarative sentences are informative due to their meanings. I construe meanings as structured hyperintensions, modelled in Transparent Intensional Logic as so-called constructions. These are abstract, algorithmically structured procedures whose constituents are sub-procedures. My main thesis is that constructions are the vehicles of information. Hence, although analytically true sentences provide no empirical information about the state of the world, they convey analytic information, in the shape of constructions prescribing how to arrive at the truths in question. Moreover, even though analytically equivalent sentences have equal empirical content, their analytic content may be different. Finally, though the empirical content of the conclusion of a valid argument is contained in the premises, its analytic content may be different from the analytic content of the premises and thus convey a new piece of information. (shrink)

What is the meaning of language expressions and how to compute or calculate it? In this paper, we give an answer to this question by analysing the meanings of aspects and tenses in natural languages inside the formal model of an grammar of applicative, cognitive and enunciative operations , using the applicative formalism, functional types of categorial grammars and combinatory logic . In the enunciative theory and following , an utterance can be decomposed into two components: a modus and a (...) dictum . In GRACE, the modus is a complex operator applied to a proposition and is generated from more elementary operators of the categories of tense, aspect, and modality. The dictum is a proposition generated by a predicative relation. In this way, we can attribute a semantic meaning to different grammatical aspecto-temporal operators. The applicative expressions of CL can be easily translated into a functional programming language such as HASKELL or CAML. (shrink)

We constructively prove completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable in iFOL if and only if it is uniformly valid in intuitionistic evidence semantics as defined in intuitionistic type theory extended with an intersection operator.Our completeness proof provides an effective procedure that converts any uniform evidence into a formal iFOL proof. Uniform evidence can involve arbitrary concepts from type theory such as ordinals, topological structures, algebras and so forth. We have implemented that procedure in the (...) Nuprl proof assistant.Our result demonstrates the value of uniform validity as a semantic notion for studying logical theories, and it provides new techniques for showing that formulas are not intuitionistically provable. Here we demonstrate its value for minimal and intuitionistic first-order logic. (shrink)

In the early thirties, Church developed predicate calculus within a system based on lambda calculus. Rosser and Kleene developed Arithmetic within this system, but using a Godelization technique showed the system to be inconsistent.Alternative systems to that of Church have been developed, but so far more complex definitions of the natural numbers have had to be used. The present paper based on a system of illative combinatory logic developed previously by the author, does allow the use of the Church numerals. (...) Given a new definition of equality all the Peano-type axioms of Mendelson except one can be derived. A rather weak extra axiom allows the proof of the remaining Peano axiom. Note. The illative combinatory logic used in this paper is similar to the logic employed in computer languages such as ML. (shrink)