Relational semantics and a relational proof system for full Lambek calculus

1998 ◽  
Vol 63 (2) ◽  
pp. 623-637 ◽  
Author(s):  
Wendy MacCaull
Keyword(s):  
Proof Theory ◽  
Kripke Semantics ◽  
Substructural Logic ◽  
Lambek Calculus ◽  
Relational Semantics ◽  
Complete Proof ◽  
Proof Search ◽  
Proof Tree ◽  
Relational Logic ◽  
Completeness Theorems

AbstractIn this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style valuation system analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FL is provable if and only if a translation, t(γ1 ● … ● γn ⊃ α)ευu, has a cut-complete fundamental proof tree. This result is constructive: that is, if a cut-complete proof tree for t(γ1 ● … ● γn ⊃ α)ευu is not fundamental, we can use the failed proof search to build a relational countermodel for t(γ1 ● … ● γn ⊃ α)ευu and from this, build a RelKripke countermodel for γ1 ● … ● γn ⊃ α. These results allow us to add FL, the basic substructural logic, to the list of those logics of importance in computer science with a relational proof theory.

scholarly journals A Logic for Vagueness

2010 ◽  
Vol 8 ◽  
Author(s):  
John Slaney
Keyword(s):  
Natural Deduction ◽  
Kripke Semantics ◽  
Substructural Logic ◽  
Relational Semantics ◽  
Deduction System ◽  
First Order ◽  
Natural Deduction System ◽  
Soundness And Completeness ◽  
Propositional System

This paper presents F, substructural logic designed to treat vagueness. Weaker than Lukasiewicz’s infinitely valued logic, it is presented first in a natural deduction system, then given a Kripke semantics in the manner of Routley and Meyer's ternary relational semantics for R and related systems, but in this case, the points are motivated as degrees to which the truth could be stretched. Soundness and completeness are proved, not only for the propositional system, but also for its extension with first-order quantifiers. The first-order models allow not only objects with vague properties, but also objects whose very existence is a matter of degree.

scholarly journals Proof Search and Certificates for Evidential Transactions

2021 ◽  
pp. 234-251
Author(s):  
Vivek Nigam ◽  
Giselle Reis ◽  
Samar Rahmouni ◽  
Harald Ruess
Keyword(s):  
Logic Programming ◽  
Proof Theory ◽  
Knowledge Bases ◽  
Foreign Country ◽  
Proof System ◽  
Complete Proof ◽  
Proof Search ◽  
Logical Data

AbstractAttestation logics have been used for specifying systems with policies involving different principals. Cyberlogic is an attestation logic used for the specification of Evidential Transactions (ETs). In such transactions, evidence has to be provided supporting its validity with respect to given policies. For example, visa applicants may be required to demonstrate that they have sufficient funds to visit a foreign country. Such evidence can be expressed as a Cyberlogic proof, possibly combined with non-logical data (e.g., a digitally signed document). A key issue is how to construct and communicate such evidence/proofs. It turns out that attestation modalities are challenging to use established proof-theoretic methods such as focusing. Our first contribution is the refinement of Cyberlogic proof theory with knowledge operators which can be used to represent knowledge bases local to one or more principals. Our second contribution is the identification of an executable fragment of Cyberlogic, called Cyberlogic programs, enabling the specification of ETs. Our third contribution is a sound and complete proof system for Cyberlogic programs enabling proof search similar to search in logic programming. Our final contribution is a proof certificate format for Cyberlogic programs inspired by Foundational Proof Certificates as a means to communicate evidence and check its validity.

scholarly journals Proof Compression and NP Versus PSPACE II

2020 ◽  
Author(s):  
Lew Gordeev ◽  
Edward Hermann Haeusler
Keyword(s):  
Sequent Calculus ◽  
Total Weight ◽  
Theoretic Approach ◽  
Minimal Logic ◽  
Open Problems ◽  
Complete Proof ◽  
Short Tree ◽  
Proof Tree ◽  
Definition Of ◽  
Subformula Property

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.

MODAL LOGIC WITHOUT CONTRACTION IN A METATHEORY WITHOUT CONTRACTION

2019 ◽  
Vol 12 (4) ◽  
pp. 685-701
Author(s):  
PATRICK GIRARD ◽  
ZACH WEBER
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Kripke Semantics ◽  
Substructural Logic

AbstractStandard reasoning about Kripke semantics for modal logic is almost always based on a background framework of classical logic. Can proofs for familiar definability theorems be carried out using a nonclassical substructural logic as the metatheory? This article presents a semantics for positive substructural modal logic and studies the connection between frame conditions and formulas, via definability theorems. The novelty is that all the proofs are carried out with a noncontractive logic in the background. This sheds light on which modal principles are invariant under changes of metalogic, and provides (further) evidence for the general viability of nonclassical mathematics.

scholarly journals A labelled sequent calculus for BBI: proof theory and proof search

2015 ◽  
Vol 28 (4) ◽  
pp. 809-872
Author(s):  
Zhé Hóu ◽  
Rajeev Goré ◽  
Alwen Tiu
Keyword(s):  
Proof Theory ◽  
Sequent Calculus ◽  
Proof Search ◽  
Labelled Sequent Calculus

scholarly journals Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity

2020 ◽  
Author(s):  
Tiziano Dalmonte ◽  
Björn Lellmann ◽  
Nicola Olivetti ◽  
Elaine Pimentel
Keyword(s):  
Search Strategy ◽  
Cut Elimination ◽  
Relational Semantics ◽  
Optimal Complexity ◽  
Proof Search ◽  
Polynomial Size ◽  
Hypersequent Calculi

Abstract We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.

Sign in / Sign up

Export Citation Format

Share Document