scholarly journals LOGIC FOR THE THEORY OF CONCEPTS

ARHE ◽  
2021 ◽  
Vol 27 (34) ◽  
pp. 85-102
Author(s):  
JOVANA KOSTIĆ
Keyword(s):  
Classical Logic ◽  
Predicate Calculus ◽  
Logical System ◽  
Logical Basis ◽  
Logical Foundation ◽  
Starting Point ◽  
Partial Predicates ◽  
Classical Predicate

In this paper, we follow Gödel’s remarks on an envisioned theory of concepts to determine which properties should a logical basis of such a theory have. The discussion is organized around the question of suitability of the classical predicate calculus for this role. Some reasons to think that classical logic is not an appropriate basis for the theory of concepts, will be presented. We consider, based on these reasons, which alternative logical system could fare better as a logical foundation of, in Gödel’s opinion, the most important theory in logic yet to be developed. This paper should, in particular, motivate the study of partial predicates in a certain system of three-valued logic, as a promising starting point for the foundation of the theory of concepts.

scholarly journals Towards applied theories based on computability logic

2010 ◽  
Vol 75 (2) ◽  
pp. 565-601 ◽  
Author(s):  
Giorgi Japaridze
Keyword(s):  
Classical Logic ◽  
Formal Theory ◽  
Deductive System ◽  
Predicate Calculus ◽  
Present Contribution ◽  
Algorithmic Solution ◽  
Starting Point ◽  
Soundness And Completeness ◽  
Deductive Power ◽  
Classical Predicate

AbstractComputability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, “truth” means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logicbased Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings—an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems.

Undecidability of modal and intermediate first-order logics with two individual variables

1993 ◽  
Vol 58 (3) ◽  
pp. 800-823 ◽  
Author(s):  
D. M. Gabbay ◽  
V. B. Shehtman
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Calculus ◽  
Single Individual ◽  
First Order ◽  
Short Summary ◽  
Binary Predicate ◽  
Individual Variables ◽  
Image Position ◽  
Classical Predicate

The interest in fragments of predicate logics is motivated by the well-known fact that full classical predicate calculus is undecidable (cf. Church [1936]). So it is desirable to find decidable fragments which are in some sense “maximal”, i.e., which become undecidable if they are “slightly” extended. Or, alternatively, we can look for “minimal” undecidable fragments and try to identify the vague boundary between decidability and undecidability. A great deal of work in this area concerning mainly classical logic has been done since the thirties. We will not give a complete review of decidability and undecidability results in classical logic, referring the reader to existing monographs (cf. Suranyi [1959], Lewis [1979], and Dreben, Goldfarb [1979]). A short summary can also be found in the well-known book Church [1956]. Let us recall only several facts. Herein we will consider only logics without functional symbols, constants, and equality.(C1) The fragment of the classical logic with only monadic predicate letters is decidable (cf. Behmann [1922]).(C2) The fragment of the classical logic with a single binary predicate letter is undecidable. (This is a consequence of Gödel [1933].)(C3) The fragment of the classical logic with a single individual variable is decidable; in fact it is equivalent to Lewis S5 (cf. Wajsberg [1933]).(C4) The fragment of the classical logic with two individual variables is decidable (Segerberg [1973] contains a proof using modal logic; Scott [1962] and Mortimer [1975] give traditional proofs.)(C5) The fragment of the classical logic with three individual variables and binary predicate letters is undecidable (cf. Surańyi [1943]). In fact this paper considers formulas of the following typeφ,ψ being quantifier-free and the set of binary predicate letters which can appear in φ or ψ being fixed and finite.

scholarly journals On an Application of Intermediate Logics

1960 ◽  
Vol 16 ◽  
pp. 119-133
Author(s):  
Toshio Umezawa
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Logical System ◽  
Intermediate Logics ◽  
Individual Variables ◽  
Classical Predicate

In [1] I investigated some logics intermediate between intuitionistic and classical predicate logics. The purpose of this paper is to show the possibility of applying some intermediate logics to mathematics namely, to show that some mathematical theorems which are provable in the classical logic but not provable in the intuitionistic logic are provable in some intermediate logics. Let LZ be the logical system obtained from LJ′ a variant of Gentzen’s LJ [2], by adding as axioms all those sequents which can be obtained from a sequent scheme Z by substitution for propositional, predicate, or individual variables.

APC: The Algorithmic Predicate Calculus

1981 ◽  
Vol 4 (2) ◽  
pp. 343-367
Author(s):  
Wojciech Przyłuski
Keyword(s):  
Time Scale ◽  
Predicate Calculus ◽  
Algorithmic Logic ◽  
Classical Predicate

The paper presents a logic which is an algorithmic extension of the classical predicate calculus and is based on the ideas given by F. Kröger. The programs and the effects of their execution are the formulas of this logic which are considered at any time scale. There are many interesting properties of the logic which are connected with the notion of time scale. These properties are examined in the paper. Moreover the problem of the formulas normalization is presented. Our logic is compared with the algorithmic logic introduced by A. Salwicki. Next, the usefulness of a new logic in the theory of programs is shown.

Resolution systems and their applications I

1980 ◽  
Vol 3 (2) ◽  
pp. 235-268
Author(s):  
Ewa Orłowska
Keyword(s):  
Theorem Proving ◽  
Sufficient Conditions ◽  
Predicate Calculus ◽  
Resolution Method ◽  
First Order ◽  
Deductive Systems ◽  
Resolution System ◽  
Resolution Principle ◽  
Necessary And Sufficient ◽  
Classical Predicate

The central method employed today for theorem-proving is the resolution method introduced by J. A. Robinson in 1965 for the classical predicate calculus. Since then many improvements of the resolution method have been made. On the other hand, treatment of automated theorem-proving techniques for non-classical logics has been started, in connection with applications of these logics in computer science. In this paper a generalization of a notion of the resolution principle is introduced and discussed. A certain class of first order logics is considered and deductive systems of these logics with a resolution principle as an inference rule are investigated. The necessary and sufficient conditions for the so-called resolution completeness of such systems are given. A generalized Herbrand property for a logic is defined and its connections with the resolution-completeness are presented. A class of binary resolution systems is investigated and a kind of a normal form for derivations in such systems is given. On the ground of the methods developed the resolution system for the classical predicate calculus is described and the resolution systems for some non-classical logics are outlined. A method of program synthesis based on the resolution system for the classical predicate calculus is presented. A notion of a resolution-interpretability of a logic L in another logic L ′ is introduced. The method of resolution-interpretability consists in establishing a relation between formulas of the logic L and some sets of formulas of the logic L ′ with the intention of using the resolution system for L ′ to prove theorems of L. It is shown how the method of resolution-interpretability can be used to prove decidability of sets of unsatisfiable formulas of a given logic.

scholarly journals A Certain Kind of Formal Theories

1965 ◽  
Vol 25 ◽  
pp. 59-86 ◽  
Author(s):  
Katuzi Ono
Keyword(s):  
Classical Logic ◽  
Axiom System ◽  
Logical System ◽  
First Order ◽  
Formal Theories

A common feature of formal theories is that each theory has its own system of axioms described in terms of some symbols for its primitive notions together with logical symbols. Each of these theories is developed by deduction from its axiom system in a certain logical system which is usually the classical logic of the first order.

scholarly journals Elementary-base cirquent calculus II: Choice quantifiers

2020 ◽  
Author(s):  
Giorgi Japaridze
Keyword(s):  
Proof Theory ◽  
Predicate Calculus ◽  
First Order ◽  
Complete Axiomatization ◽  
Calculus I ◽  
Soundness And Completeness ◽  
Classical Predicate

Abstract Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article ‘Elementary-base cirquent calculus I: Parallel and choice connectives’ built the sound and complete axiomatization $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and completeness. The language of $\textbf{CL17}$ augments that of $\textbf{CL16}$ by including choice quantifiers. Unlike classical predicate calculus, $\textbf{CL17}$ turns out to be decidable.

scholarly journals Weak Assertion

2019 ◽  
Vol 69 (277) ◽  
pp. 741-770 ◽  
Author(s):  
Luca Incurvati ◽  
Julian J Schlöder
Keyword(s):  
Classical Logic ◽  
Speech Act ◽  
Modal Operator ◽  
Epistemic Modal ◽  
Logical Constants ◽  
The Core ◽  
Linguistic Evidence ◽  
Starting Point

Abstract We present an inferentialist account of the epistemic modal operator might. Our starting point is the bilateralist programme. A bilateralist explains the operator not in terms of the speech act of rejection; we explain the operator might in terms of weak assertion, a speech act whose existence we argue for on the basis of linguistic evidence. We show that our account of might provides a solution to certain well-known puzzles about the semantics of modal vocabulary whilst retaining classical logic. This demonstrates that an inferentialist approach to meaning can be successfully extended beyond the core logical constants.

Sufficient conditions for the undecidability of intuitionistic theories with applications

1972 ◽  
Vol 37 (2) ◽  
pp. 375-384 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Decision Problem ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
The Other ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Symmetric Relation ◽  
Undecidable Theory ◽  
Classical Models ◽  
Classical Predicate

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC.Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not.Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

A proof-theoretic study of the correspondence of classical logic and modal logic

2003 ◽  
Vol 68 (4) ◽  
pp. 1403-1414 ◽  
Author(s):  
H. Kushida ◽  
M. Okada
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Transformation Method ◽  
Modal Operator ◽  
Theoretic Method ◽  
Barcan Formula ◽  
Theoretic Proof ◽  
Classical Predicate

AbstractIt is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

Sign in / Sign up

Export Citation Format

Share Document