I have attempted to show that many attributive adjectives can be dealt with within the framework of first-order predicatecalculus by the method suggested in this paper. I've also supplied independent reasons for the claim that attributive adjectives that are not responsive to this method require a formal treatment different from the one that the adjectives successfully dealt with by that method require. Thus, if the method I've argued for is sound, then the scope of first-order predicate (...)calculus was shown to be wider than assumed by several logicians. This I take to be of interest from a logical point of view. (shrink)
Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicatecalculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. (...) Both translations are closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church ,  and Curry  to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)
We introduce a Gentzen-style sequent calculus axiomatization for Basic PredicateCalculus. Our new axiomatization is an improvement of the previous axiomatizations, in the sense that it has the subformula property. In this system the cut rule is eliminated.
Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicatecalculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not (...) translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of $\lambda$ -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)
A programme to construct an extension of predicatecalculus is proposed in which predicates and constants are indexed and interpreted with respect to different (mini-)vorlds reffered to by indices. From another perspective the proposed system is an extension of the idea of indexing noun phrases in syntactic representations in generative grammar. Some applications are given, bx particular, it is applied to the description of ambiguities in intensional contexts, and a comparison is made with a description recently given by (...) Saarinen. (shrink)
We present a formalization of first-order predicatecalculus with equality which, unlike traditional systems with axiom schemata or substitution rules, is finitely axiomatized in the sense that each step in a formal proof admits only finitely many choices. This formalization is primarily based on the inference rule of condensed detachment of Meredith. The usual primitive notions of free variable and proper substitution are absent, making it easy to verify proofs in a machine-oriented application. Completeness results are presented. The (...) example of Zermelo-Fraenkel set theory is shown to be finitely axiomatized under the formalization. The relationship with resolution-based theorem provers is briefly discussed. A closely related axiomatization of traditional predicatecalculus is shown to be complete in a strong metamathematical sense. (shrink)
Two subject-predicate calculi with equality,SP = and its extensionUSP =, are presented as systems of natural deduction. Both the calculi are systems of free logic. Their presentation is preceded by an intuitive motivation.It is shown that Aristotle's syllogistics without the laws of identitySaP andSiP is definable withinSP =, and that the first-order predicate logic is definable withinUSP =.
We establish a completeness theorem for first-order basic predicate logic BQC, a proper subsystem of intuitionistic predicate logic IQC, using Kripke models with transitive underlying frames. We develop the notion of functional well-formed theory as the right notion of theory over BQC for which strong completeness theorems are possible. We also derive the undecidability of basic arithmetic, the basic logic equivalent of intuitionistic Heyting Arithmetic and classical Peano Arithmetic.
The syllogism and the predicatecalculus cannot account for an ontological argument in Descartes' Fifth Meditation and related texts. Descartes' notion of god relies on the analytic-synthetic distinction, which Descartes had identified before Leibniz and Kant did. I describe how the syllogism and the predicatecalculus cannot explain Descartes' ontological argument; then I apply the analytic-synthetic distinction to Descartes’ idea of god.
This approach does not define a probability measure by syntactical structures. It reveals a link between modal logic and mathematical probability theory. This is shown (1) by adding an operator (and two further connectives and constants) to a system of lower predicatecalculus and (2) regarding the models of that extended system. These models are models of the modal system S₅ (without the Barcan formula), where a usual probability measure is defined on their set of possible worlds. Mathematical (...) probability models can be seen as models of S₅. (shrink)