Online research in philosophy

This paper seeks a better understanding of the elements of practical reasoning: premises and conclusion. It argues that the premises of practical reasoning do not normally include statements such as ‘I want to ϕ’; that the reasoning in practical reasoning is the same as in theoretical reasoning and that what makes it practical is, first, that the point of the relevant reasoning is given by the goal that the reasoner seeks to realize by means of that reasoning and the subsequent action; second, that the premises of such reasoning show the goodness of the action to be undertaken; third, that the conclusions of such reasoning may be actions or decisions, that can be accompanied by expressions of intention, either in action, or for the future; and that these are justified, and might be contradicted, in ways that are not only peculiar to them (i.e. in ways that diverge from those found in theoretical reasoning), but are distinctively practical, in that they involve reference to reasons for acting and to expressions of intention, respectively.1.

We discuss the differences between first-order set theory and second-order logic as a foundation for mathematics. We analyse these languages in terms of two levels of formalization. The analysis shows that if second-order logic is understood in its full semantics capable of characterizing categorically central mathematical concepts, it relies entirely on informal reasoning. On the other hand, if it is given a weak semantics, it loses its power in expressing concepts categorically. First-order set theory and second-order logic are not radically different: the latter is a major fragment of the former.

Quasi-equational logic concerns with a completeness theorem, i. e. a list of general syntactical rules such that, being given a set of graded quasi-equations Q, the closure Cl Q = Qeq Fun Q can be derived from by the given rules. Those rules do exist, because our consideration could be embedded into the logic of first order language. But, we look for special (quasi-equational) rules. Suitable rules were already established for the (non-functorial) case of partial algebras in Definition 3.1.2 of [27], p. 108, and [28], p. 102. (For the case of total algebras, see [35].) So, one has to translate these rules to the (functorial) language of partial theories .Surprisingly enough, partial theories can be replaced up to isomorphisms by partial Dale monoids (cf. Section 3), which, in the total case are ordinary monoids.

This paper presents a sound and complete proof system for the first order fragment of Discourse Representation Theory. Since the inferences that human language users draw from the verbal input they receive for the most transcend the capacities of such a system, it can be no more than a basis on which more powerful systems, which are capable of producing those inferences, may then be built. Nevertheless, even within the general setting of first order logic the structure of the formulas of DRS-languages, i.e. of the Discourse Representation Structures suggest for the components of such a system inference rules that differ somewhat from those usually found in proof systems for the first order predicate calculus and which are, we believe, more in keeping with inference patterns that are actually employed in common sense reasoning.This is why we have decided to publish the present exercise, in spite of the fact that it is not one for which a great deal of originality could be claimed. In fact, it could be argued that the problem addressed in this paper was solved when Gödel first established the completeness of the system of Principia Mathematica for first order logic. For the DRS-languages we consider here are straightforwardly intertranslatable with standard formulations of the predicate calculus; in fact the translations are so straightforward that any sound and complete proof system for first order logic can be used as a sound and complete proof system for DRSs: simply translate the DRSs into formulas of predicate logic and then proceed as usual. As a matter of fact, this is how one has chosen to proceed in some implementations of DRT, which involve inferencing as well as semantic representation; an example is the Lex system developed jointly by IBM and the University of Tübingen (see in particular (Guenthner et al. 1986)).

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 theory of ranked partial structures allows a reinterpretation of several of the standard results of model theory and first-order logic and is intended to provide a proof-theoretic method which allows for the intuitions of model theory. A version of the downward Löwenheim-Skolem theorem is central to our development. In this paper we will present the basic theory of ranked partial structures and their logic including an appropriate version of the completeness theorem.

We investigate first order sentences valid in completions of a given partial algebraic structure - a partial model. We give semantic and syntactic description of the set of all sentences valid in every completion of the given partial model - first order theory of this model.

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.

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.

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.