On logics intermediate between intuitionistic and classical predicate logic

1959 ◽  
Vol 24 (2) ◽  
pp. 141-153 ◽  
Author(s):  
Toshio Umezawa
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Classical Propositional Logic ◽  
Intermediate Predicate Logics ◽  
Study Inclusion ◽  
Classical Predicate

In [1] and [2] I investigated logics intermediate between intuitionistic and classical propositional logic. In the present paper I shall study inclusion and non-inclusion between certain intermediate predicate logics. All the logics considered result from intuitionistic predicate logic by addition of classically valid axiom schemes.

UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS

2014 ◽  
Vol 7 (3) ◽  
pp. 455-483 ◽  
Author(s):  
MAJID ALIZADEH ◽  
FARZANEH DERAKHSHAN ◽  
HIROAKIRA ONO
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Substructural Logics ◽  
Substructural Logic ◽  
Sequent Calculi ◽  
Structural Rule ◽  
Modal Propositional Logic ◽  
Uniform Interpolation ◽  
Classical Predicate

AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.

scholarly journals Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 115 ◽  
Author(s):  
Joanna Golińska-Pilarek ◽  
Magdalena Welle
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Classical Propositional Logic ◽  
Tableau System ◽  
Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

RELEVANCE LOGIC AND THE CALCULUS OF RELATIONS

2010 ◽  
Vol 3 (1) ◽  
pp. 41-70 ◽  
Author(s):  
ROGER D. MADDUX
Keyword(s):  
Propositional Logic ◽  
Relevance Logic ◽  
Binary Relations ◽  
Classical Propositional Logic

Sound and complete semantics for classical propositional logic can be obtained by interpreting sentences as sets. Replacing sets with commuting dense binary relations produces an interpretation that turns out to be sound but not complete for R. Adding transitivity yields sound and complete semantics for RM, because all normal Sugihara matrices are representable as algebras of binary relations.

scholarly journals The Method of Socratic Proofs Meets Correspondence Analysis

2019 ◽  
Vol 48 (2) ◽  
pp. 99-116
Author(s):  
Dorota Leszczyńska-Jasion ◽  
Yaroslav Petrukhin ◽  
Vasilyi Shangin
Keyword(s):  
Correspondence Analysis ◽  
Boolean Functions ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Sequent Calculi ◽  
Classical Propositional Logic ◽  
Logic Of Questions ◽  
Proof Systems

The goal of this paper is to propose correspondence analysis as a technique for generating the so-called erotetic (i.e. pertaining to the logic of questions) calculi which constitute the method of Socratic proofs by Andrzej Wiśniewski. As we explain in the paper, in order to successfully design an erotetic calculus one needs invertible sequent-calculus-style rules. For this reason, the proposed correspondence analysis resulting in invertible rules can constitute a new foundation for the method of Socratic proofs. Correspondence analysis is Kooi and Tamminga's technique for designing proof systems. In this paper it is used to consider sequent calculi with non-branching (the only exception being the rule of cut), invertible rules for the negation fragment of classical propositional logic and its extensions by binary Boolean functions.

Update Semantics in Communicated Information System

2011 ◽  
Vol 403-408 ◽  
pp. 1460-1465
Author(s):  
Guang Ming Chen ◽  
Xiao Wu Li
Keyword(s):  
Information Systems ◽  
Propositional Logic ◽  
General Purpose ◽  
Main Task ◽  
Information Communication ◽  
Classical Propositional Logic ◽  
Update Semantics ◽  
Essential Form ◽  
Soundness And Completeness ◽  
Multi Agents

An approach, which is called Communicated Information Systems, is introduced to describe the information available in a number of agents and specify the information communication among the agents. The systems are extensions of classical propositional logic in multi-agents context, providing with us a way by which not only the agent’s own information, but the information from other agents may be applied to agent’s reasoning as well. Communication rules, which are defined in the most essential form, can be regarded as the base to characterize some interesting cognitive proporties of agents. Since the corresponding communication rules can be chosen for different applications, the approach is general purpose one. The other main task is that the soundness and completeness of the Communicated Information Systems for the update semantics have been proved in the paper.

Sign in / Sign up

Export Citation Format

Share Document