Minimal Logic. Preliminary Remarks

We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight (= total number of symbols) and time complexity of the provability involved are both polynomial in the weight of ρ. As in [3], we use proof theoretic approach. Recall that in [3] we considered any valid ρ in question that had (by the definition of validity) a "short" tree-like proof π in the Hudelmaier-style cutfree sequent calculus for minimal logic. The "shortness" means that the height of π and the total weight of different formulas occurring in it are both polynomial in the weight of ρ. However, the size (= total number of nodes), and hence also the weight, of π could be exponential in that of ρ. To overcome this trouble we embedded π into Prawitz's proof system of natural deductions containing single formulas, instead of sequents. As in π, the height and the total weight of different formulas of the resulting tree-like natural deduction ∂1 were polynomial, although the size of ∂1 still could be exponential, in the weight of ρ. In our next, crucial move, ∂1 was deterministically compressed into a "small", although multipremise, dag-like deduction ∂ whose horizontal levels contained only mutually different formulas, which made the whole weight polynomial in that of ρ. However, ∂ required a more complicated verification of the underlying provability of ρ. In this paper we present a nondeterministic compression of ∂ into a desired standard dag-like deduction ∂0 that deterministically proves ρ in time and space polynomial in the weight of ρ. Together with [3] this completes the proof of NP = PSPACE. Natural deductions are essential for our proof. Tree-to-dag horizontal compression of π merging equal sequents, instead of formulas, is (possible but) not sufficient, since the total number of different sequents in π might be exponential in the weight of ρ − even assuming that all formulas occurring in sequents are subformulas of ρ. On the other hand, we need Hudelmaier's cutfree sequent calculus in order to control both the height and total weight of different formulas of the initial tree-like proof π, since standard Prawitz's normalization although providing natural deductions with the subformula property does not preserve polynomial heights. It is not clear yet if we can omit references to π even in the proof of the weaker result NP = coNP.

Download Full-text

Semantics of the Minimal Logic of Quantum Mechanics

The Logico-Algebraic Approach to Quantum Mechanics ◽

10.1007/978-94-009-9351-8_2 ◽

1979 ◽

pp. 17-29

Author(s):

H. Dishkant

Keyword(s):

Quantum Mechanics ◽

Minimal Logic

Download Full-text

A Remark on the Intersection of Tow Logics

Nagoya Mathematical Journal ◽

10.1017/s0027763000011715 ◽

1966 ◽

Vol 26 ◽

pp. 167-171 ◽

Cited By ~ 17

Author(s):

Satoshi Miura

Keyword(s):

Intuitionistic Logic ◽

General Feature ◽

Minimal Logic ◽

Axiom Scheme

The intuitionistic logic LJ and Curry’s LD (cf. [1], [2]) are logics stronger than Johansson’s minimal logic LM (cf. [3]) by the axiom schemes ⋏→x and y ∨ (y→⋏), respectively. However, LM can not be taken literally as the intersection of these two logics LJ and LD, which is stronger than LM by the axiom scheme (⋏ → x) VyV (y→⋏). In pointing out this situation, Prof. K. Ono suggested me to investigate the general feature of the intersection of any pair of logics. In this paper, I will show that the same situation occurs in general. I wish to express my thanks to Prof. K. Ono for his kind guidance.

Download Full-text

A Kotas-Style Characterisation of Minimal Discussive Logic

Axioms ◽

10.3390/axioms8040108 ◽

2019 ◽

Vol 8 (4) ◽

pp. 108 ◽

Cited By ~ 1

Author(s):

Krystyna Mruczek-Nasieniewska ◽

Marek Nasieniewski

Keyword(s):

Deductive System ◽

Modal Logics ◽

Original Model ◽

Accessibility Relation ◽

Minimal Logic ◽

One To One

In this paper, we discuss a version of discussive logic determined by a certain variant of Jaśkowski’s original model of discussion. The obtained system can be treated as the minimal discussive logic. It is determined by frames with serial accessibility relation. As the smallest one, this logic can be treated as a basis which could be extended to richer discussive logics that are obtained by varying accessibility relation and resulting in a lattice of discussive logics. One has to remember that while formulating discussive logics there is no one-to-one determination of discussive logics by modal logics. For example, it is proved that Jaśkowski’s logic D 2 can be expressed by other than S 5 modal logics. In this paper we consider a deductive system for the sketchily described minimal logic. While formulating the deductive system, we apply a method of Kotas that was used to axiomatize D 2 . The obtained system determines a logic D 0 as a set of theses that is contained in D 2 . Moreover, any discussive logic that would be expressed by means of the provided model of discussion would contain D 0 , so it is the smallest discussive logic.

Download Full-text

Interpolation and Definability in Extensions of the Minimal Logic

Algebra and Logic ◽

10.1007/s10469-005-0038-4 ◽

2005 ◽

Vol 44 (6) ◽

pp. 407-421 ◽

Cited By ~ 17

Author(s):

L. L. Maksimova

Keyword(s):

Minimal Logic

Download Full-text

Semantics of the minimal logic of quantum mechanics

Studia Logica ◽

10.1007/bf02120818 ◽

1972 ◽

Vol 30 (1) ◽

pp. 23-30 ◽

Cited By ~ 32

Author(s):

H. Dishkant

Keyword(s):

Quantum Mechanics ◽

Minimal Logic

Download Full-text

A theory of properties

Journal of Symbolic Logic ◽

10.2307/2274394 ◽

1987 ◽

Vol 52 (2) ◽

pp. 455-472 ◽

Cited By ~ 42

Author(s):

Ray Turner

Keyword(s):

Recent Work ◽

Set Theory ◽

Semantic Theory ◽

Truth Predicate ◽

Minimal Logic ◽

History Of ◽

Concept Of Truth ◽

Almost All ◽

The Liar ◽

Self Reference

Frege's attempts to formulate a theory of properties to serve as a foundation for logic, mathematics and semantics all dissolved under the weight of the logicial paradoxes. The language of Frege's theory permitted the representation of the property which holds of everything which does not hold of itself. Minimal logic, plus Frege's principle of abstraction, leads immediately to a contradiction. The subsequent history of foundational studies was dominated by attempts to formulate theories of properties and sets which would not succumb to the Russell argument. Among such are Russell's simple theory of types and the development of various iterative conceptions of set. All of these theories ban, in one way or another, the self-reference responsible for the paradoxes; in this sense they are all “typed” theories. The semantical paradoxes, involving the concept of truth, induced similar nightmares among philosophers and logicians involved in semantic theory. The early work of Tarski demonstrated that no language that contained enough formal machinery to respresent the various versions of the Liar could contain a truth-predicate satisfying all the Tarski biconditionals. However, recent work in both disciplines has led to a re-evaluation of the limitations imposed by the paradoxes.In the foundations of set theory, the work of Gilmore [1974], Feferman [1975], [1979], [1984], and Aczel [1980] has clearly demonstrated that elegant and useful type-free theories of classes are feasible. Work on the semantic paradoxes was given new life by Kripke's contribution (Kripke [1975]). This inspired the recent work of Gupta [1982] and Herzberger [1982]. These papers demonstrate that much room is available for the development of theories of truth which meet almost all of Tarski's desiderata.

Download Full-text