Church's simple theory of types is a system of higher-order logic in which functions are assumed to be total. We present in this paper a version of Church's system called PF in which functions may be partial. The semantics of PF, which is based on Henkin's general-models semantics, allows terms to be nondenoting but requires formulas to always denote a standard truth value. We prove that PF is complete with respect to its semantics. The reasoning mechanism in (...) PF for partial functions corresponds closely to mathematical practice, and the formulation of PF adheres tightly to the framework of Church's system. (shrink)

Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows (...) how the traditional approach to partial functions can be formalized in a range of formalisms that includes first-order logic, simple type theory, and Von-Neumann—Bernays—Gödel set theory. It argues that these new formalisms allow one to directly reason about partial functions; are based on natural, well-understood, familiar principles; and can be effectively implemented in mechanized mathematics systems. (shrink)

Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework (...) directly. We solve this problem by applying recent methods from sorted logics. This paper presents a tableau calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)

Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel set theory (...) for reasoning about sets, proper classes, and partial functions represented as classes of ordered pairs. The underlying logic of the system is a partial first-order logic, so class-valued terms may be nondenoting. Functions can be specified using lambda-notation, and reasoning about the application of functions to arguments is facilitated using sorts similar to those employed in the logic of the IMPS Interactive Mathematical Proof System. The set theory is intended to serve as a foundation for mechanized mathematics systems. (shrink)

Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. (...) We solve this problem by applying recent methods from sorted logics. This paper presents a resolution calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)

Let $\langle\mathscr{T},\leq\rangle$ be the usual structure of the degrees of unsolvability and $\langle\mathscr{D},\leq\rangle$ the structure of the T-degrees of partial functions defined in [7]. We prove that every countable distributive lattice with a least element can be isomorphically embedded as an initial segment of $\langle\mathscr{D},\leq\rangle$ : as a corollary, the first order theory of $\langle\mathscr{D},\leq\rangle$ is recursively isomorphic to that of $\langle\mathscr{T},\leq\rangle$ . We also show that $\langle\mathscr{D},\leq\rangle$ and $\langle\mathscr{T},\leq\rangle$ are not elementarily equivalent.

We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects (...) in the logic, to define an interpreter for such expressions as a function in the logic, and then define quantifiers as "mapping functions." The novelty of our approach lies in the formalization of the interpreter and its interaction with the underlying logic. Our method has several advantages over other formal systems that provide quantifiers and partial functions in a logical setting. The most important advantage is that proofs not involving quantification or partial recursive functions are not complicated by such notions as "capturing," "bottom," or "continuity." Naturally enough, our formalization of the partial functions is nonconstructive. The theorem prover for the logic has been modified to support these new features. We describe the modifications. The system has proved many theorems that could not previously be stated in our logic. Among them are. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion (...) of an interpretation of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of, an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion (...) of an interpretation of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of , an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)

We employ the notions of "sequential function" and "interrogation" (dialogue) in order to define new partial combinatory algebra structures on sets of functions. These structures are analyzed using Longley's preorder-enriched category of partial combinatory algebras and decidable applicative structures. We also investigate total combinatory algebras of partial functions. One of the results is that every realizability topos is a geometric quotient of a realizability topos on a total combinatory algebra.

We describe sets of partial Boolean functions being closed under the operations of superposition. For any class A of total functions we define the set ????(A) consisting of all partial classes which contain precisely the functions of A as total functions. The cardinalities of such sets ????(A) can be finite or infinite. We state some general results on ????(A). In particular, we describe all 30 closed sets of partial Boolean functions which contain (...) all monotone and zero-preserving total Boolean functions. (shrink)

In this work we show that every structure [MATHEMATICAL SCRIPT CAPITAL A] can be expanded to a partial structure [MATHEMATICAL SCRIPT CAPITAL A]* with universal functions for the class of polynomials on [MATHEMATICAL SCRIPT CAPITAL A]*. We can embed [MATHEMATICAL SCRIPT CAPITAL A]* monomorphically in a total structure [MATHEMATICAL SCRIPT CAPITAL A]º that preserves universal functions of [MATHEMATICAL SCRIPT CAPITAL A]* and that is universal among such structures, i.e. [MATHEMATICAL SCRIPT CAPITAL A]º can be homomorphically embedded in (...) every total structure that preserves universal functions of [MATHEMATICAL SCRIPT CAPITAL A]*. Universal functions are the starting point for developing recursion theoretic tools in an [MATHEMATICAL SCRIPT CAPITAL A]* that satisfies some simple additional conditions. (shrink)

We introduce a family of rank functions and related notions of total transcendence for Galois types in abstract elementary classes. We focus, in particular, on abstract elementary classes satisfying the condition known as tameness, where the connections between stability and total transcendence are most evident. As a byproduct, we obtain a partial upward stability transfer result for tame abstract elementary classes stable in a cardinal $\lambda$ satisfying $\lambda^{\aleph_{0}}\gt \lambda$, a substantial generalization of a result of Baldwin, Kueker, and (...) VanDieren. (shrink)

The paper studies a domain theoretical notion of primitive recursion over partial sequences in the context of Scott domains. Based on a non-monotone coding of partial sequences, this notion supports a rich concept of parallelism in the sense of Plotkin. The complexity of these functions is analysed by a hierarchy of classes ${\cal E}^{\bot}_n$ similar to the Grzegorczyk classes. The functions considered are characterised by a function algebra ${\cal R}^{\bot}$ generated by continuity preserving operations starting from (...) computable initial functions. Its layers ${\cal R}^{\bot}_n$ are related to those above by showing $\forall n \ge 2.{\cal E}^{\bot}_{n+1} ={\cal R}^{\bot}_n$ , thus generalising results of Schwichtenberg/Müller and Niggl. (shrink)

The use of lateralised cues by predators and fellows may not strongly affect lateralisation. Conservatism of development is a possible source of consistency across vertebrates. Individuals with partial reversal, affecting only one ability, or with varying degree of control of response by one hemisphere do exist. Their incidence may depend on varying selection of behavioural phenotypes such as risk taking.

A type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings). By this and by results in [1] and [2], the Kleene-Kreisel countable functionals and (...) the hereditary effective operations (HEO) are easily characterized. (shrink)

This paper extends earlier work by its authors on formal aspects of the processes of contracting a theory to eliminate a proposition and revising a theory to introduce a proposition. In the course of the earlier work, Gardenfors developed general postulates of a more or less equational nature for such processes, whilst Alchourron and Makinson studied the particular case of contraction functions that are maximal, in the sense of yielding a maximal subset of the theory (or alternatively, of one (...) of its axiomatic bases), that fails to imply the proposition being eliminated. In the present paper, the authors study a broader class, including contraction functions that may be less than maximal. Specifically, they investigate "partial meet contraction functions", which are defined to yield the intersection of some nonempty family of maximal subsets of the theory that fail to imply the proposition being eliminated. Basic properties of these functions are established: it is shown in particular that they satisfy the Gardenfors postulates, and moreover that they are sufficiently general to provide a representation theorem for those postulates. Some special classes of partial meet contraction functions, notably those that are "relational" and "transitively relational", are studied in detail, and their connections with certain "supplementary postulates" of Gardenfors investigated, with a further representation theorem established. (shrink)

This paper examines the ethical conundrum between a hospital's ethos of relieving distress, investigation and treatment, and its concurrent duties under English law to administer tests of decision-making capacity and safeguarding protection where it believes the patient may lack this capacity. Delirium, characterised by a precipitous decline in mental functioning exhibiting the shared symptomology of recoverable depressive disorders and terminal dementia, is not uncommon after emergency admission of elderly patients into acute medical hospital wards. The use of functional capacity testing (...) as a benchmark for decision-making capacity for post-discharge residence has been criticised as outdated, conceptually floored, subjective, lacking central guidance, transparent process, and accountability. A study of patient experience demonstrates the potential for hospital misuse of capacity testing, the failure of functional testing to differentiate decision making capacity from the disability of partial cognitive impairment, and how hospital capacity processes can interact and amplify patient pathology thereby decreasing recovery prospects. Prioritisation of mental capacity obligations above thorough investigation of emergent mental pathology and relief of patient anguish, results in extended detention in medical wards lacking bespoke facilities. Further understanding of patient experience is needed to inform policy with interventions tailored to avoid harm and increase wellbeing. (shrink)

We develop a bottom-up approach to truth-value semantics for classical logic of partial terms based on equality and apply it to prove the conservativity of the addition of partial description and selection functions, independently of any strictness assumption.

This article will study a class of deduction systems that allow for a limited use of the modus ponens method of deduction. We will show that it is possible to devise axiom systems α that can recognize their consistency under a deduction system D provided that: (1) α treats multiplication as a 3-way relation (rather than as a total function), and that (2) D does not allow for the use of a modus ponens methodology above essentially the levels of Π1 (...) and Σ1 formulae. Part of what will make this boundary-case exception to the Second Incompleteness Theorem interesting is that we will also characterize generalizations of the Second Incompleteness Theorem that take force when we only slightly weaken the assumptions of our boundary-case exceptions in any of several further directions. (shrink)

The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established.