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.

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 =.

The purpose of this paper is to outline an alternative approach to introductory logic courses. Traditional logic courses usually focus on the method of natural deduction or introduce predicate calculus as a system. These approaches complicate the process of learning different techniques for dealing with categorical and hypothetical syllogisms such as alternate notations or alternate forms of analyzing syllogisms. The author's approach takes up observations made by Dijkstrata and assimilates them into a reasoning process based on modified notations. The (...) author's model adopts a notation that addresses the essentials of a problem while remaining easily manipulated to serve other analytic frameworks. The author also discusses the pedagogical benefits of incorporating the model into introductory logic classes for topics ranging from syllogisms to predicate calculus. Since this method emphasizes the development of a clear and manipulable notation, students can worry less about issues of translation, can spend more energy solving problems in the terms in which they are expressed, and are better able to think in abstract terms. (shrink)

I have attempted to show that many attributive adjectives can be dealt with within the framework of first-order predicate calculus 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)

The most basic laws and principles of the Predicate Calculus, also known as Quantification Theory, are stated, as clearly and concisely as possible.

The suppression task challenges classical logic. Classical logic is monotonic. However, in the suppression task, an inference with the form of modus ponendo ponens is inhibited by adding a new premise. Several explanations have been given to account for this fact. The present paper indicates three of them as examples: that of the theory of mental models, that based on logic programming and closed world assumption, and that referring to Carnap's concept of state‐descriptions. Besides, the paper offers one more explanation (...) linked to Carnap's idea of reduction. It proposes sentences akin to a reduction sentence, a pair reduction, and a bilateral reduction sentence. Those sentences are related to the initial conditional in the suppression task. This proposal tries to stay within first‐order predicate logic. (shrink)

Summary We have considered complete consistent systems in the first‐oder predicate calculus with identity, and have studied the set of the models of such a system by means of the maximal consistent condition‐sets associated with the system. The results may be summarized thus: (a) A complete consistent system is no‐categorical (= categorical in the denumerable domain) if and only if for every n, the number of different conditions in n variables is finite (T10). (b) If a complete consistent system (...) has a model M with finite character (i.e. a model M such that every maximal consistent condition‐set satisfied in M has a finite basis), then this model M is uniquely characterized by the property that every other model is an arithmetic extension of M (T 5). (c) Every complete consistent system, which has only a denumerable number of different associated maximal consistent condition‐sets, has a model with finite character (T8). (shrink)

In this paper we define the polyadic Pavelka algebras as algebraic structures for Rational Pavelka predicate calculus . We prove two representation theorems which are the algebraic counterpart of the completness theorem for RPL∀.

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 predicate calculus. 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)

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 predicate calculus. 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 [1932], [1933] and Curry [1930] 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 present a formalization of first-order predicate calculus 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 predicate calculus is shown to be complete in a strong metamathematical sense. (shrink)

We introduce a Gentzen-style sequent calculus axiomatization for Basic Predicate Calculus. 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.

The aim of this paper is to present a strongly complete first order functional predicate calculus generalized to models containing not only ordinary classical total functions but also arbitrary partial functions. The completeness proof follows Henkin’s approach, but instead of using maximally consistent sets, we define saturated deductively closed consistent sets . This provides not only a completeness theorem but a representation theorem: any SDCCS defines a canonical model which determine a unique partial value for every predicate symbol (...) and any function symbol. Any SDCCS can thus be interpreted as an epistemic state. (shrink)

In order to avoid the use of individual variables in predicate calculus, several authors proposed language whose expressions can be interpreted, in general, as denotations of predicates . The present author also proposed a language of this kind [5]. The absence of individual variables makes all these languages rather different from the traditional language of predicate calculus and from the usual language of mathematics. The translation procedures from the ordinary predicate languages into the predicate languages without (...) individual variables and vice versa have a technical character. It is desirable to make possible carrying out such procedures by performing some transformations in a suitable new language which comprises both a sublanguage similar to the ordinary predicate languages and another one not using individual variables. We shall propose now a language of the desired kind. The expressions of this language could be interpreted, in general, as denoting predicates which depend on parameters on a given object domain – this predicate has one argument and depends on one parameter). The proposed language will have the modal features noted in [3] and [5]. It is worthy of mention that the language proposed at the end of [4] although containing expressions interpreted as predicates and expressions with parameters does not allow simultaneous availability of argument places and parameters. (shrink)

Constructs developed for the semantics of artificial languages are often proposed as the proper description of aspects of the semantics of natural languages. Most of us are familiar with the claims that conjunction, disjunction, negation, and material implication in standard versions of propositional calculus describe the meaning of “and”, “or”, “not”, and “if …, then …” in English. The argument for such claims is not only that these constructs account for meanings in English but that they offer the advantage of (...) well-understood formal apparatus for the explication of meaning in natural language. The argument against such claims is that explications based on this apparatus leave important aspects of the meaning of “and”, “or”, “not”, and “if …, then …” unexplicated. It is charged that the advantage of a well-understood formalism is secured at the expense of truth. Many of the most significant issues in philosophic logic are or depend on questions about whether constructs from artificial languages provide adequate semantic descriptions for natural languages. (shrink)

There are at least a few plausible grounds for our use of the term Beta in our title, notwithstanding that there is a key departure, in our framework, from classical Beta Existential Graphs. The situation, in brief, is as follows.The reader accustomed to Peirce’s graphical development of quantificational logic may, if desired, continue to think of formulas being written on a “sheet of assertion.” We retain the “cut” notation for negation and continue to represent conjunction simply by juxtaposition of diagrams. (...) However, on the side of departure, we dispense with the sometimes problematic “lines of identity” of classical Beta and instead represent a quantification by a.. (shrink)