scholarly journals Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts

2022 ◽  
Author(s):  
Torben Braüner
Keyword(s):  
Natural Deduction ◽  
Hybrid Logic ◽  
Proof Systems ◽  
Sequent Systems ◽  
Tableau Systems

This paper is about non-labelled proof-systems for hybrid logic, that is, proof-systems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that non-labelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.

ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS

2020 ◽  
Vol 54 (3 (253)) ◽  
pp. 127-136
Author(s):  
Anahit A. Chubaryan ◽  
Arsen A. Hambardzumyan
Keyword(s):  
Cut Rule ◽  
Proof Systems ◽  
Nonclassical Logics ◽  
Frege Systems ◽  
Sequent Systems ◽  
Propositional Proof Systems ◽  
Propositional Proof

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for the Frege systems, the sequent systems with cut rule and the systems of natural deductions of classical and nonclassical logics. We show that for these systems there are sequences of tautologies ψn, every one of which has unique minimal tautologies φn such that for each n the minimal proof lines of φn are an order more than the minimal proof lines of ψn.

Gentzen's Proof Systems: Byproducts in a Work of Genius

2012 ◽  
Vol 18 (3) ◽  
pp. 313-367 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Central Component ◽  
Cut Elimination ◽  
Complete Class ◽  
Tree Form ◽  
Proof Systems ◽  
Set Up ◽  
Logical Calculi ◽  
Subformula Property

AbstractGentzen's systems of natural deduction and sequent calculus were byproducts in his program of proving the consistency of arithmetic and analysis. It is suggested that the central component in his results on logical calculi was the use of a tree form for derivations. It allows the composition of derivations and the permutation of the order of application of rules, with a full control over the structure of derivations as a result. Recently found documents shed new light on the discovery of these calculi. In particular, Gentzen set up five different forms of natural calculi and gave a detailed proof of normalization for intuitionistic natural deduction. An early handwritten manuscript of his thesis shows that a direct translation from natural deduction to the axiomatic logic of Hilbert and Ackermann was, in addition to the influence of Paul Hertz, the second component in the discovery of sequent calculus. A system intermediate between the sequent calculus LI and axiomatic logic, denoted LIG in unpublished sources, is implicit in Gentzen's published thesis of 1934–35. The calculus has half rules, half “groundsequents,” and does not allow full cut elimination. Nevertheless, a translation from LI to LIG in the published thesis gives a subformula property for a complete class of derivations in LIG. After the thesis, Gentzen continued to work on variants of sequent calculi for ten more years, in the hope to find a consistency proof for arithmetic within an intuitionistic calculus.

Relational proof system for relevant logics

1992 ◽  
Vol 57 (4) ◽  
pp. 1425-1440 ◽  
Author(s):  
Ewa Orlowska
Keyword(s):  
Natural Deduction ◽  
Proof System ◽  
Algebraic Semantics ◽  
Proof Systems ◽  
Relevant Logics ◽  
Deduction Rules

AbstractA method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.

The relative efficiency of propositional proof systems

1979 ◽  
Vol 44 (1) ◽  
pp. 36-50 ◽  
Author(s):  
Stephen A. Cook ◽  
Robert A. Reckhow
Keyword(s):  
Relative Efficiency ◽  
Natural Deduction ◽  
Type Systems ◽  
Linear Increase ◽  
Proof System ◽  
Proof Systems ◽  
System A ◽  
Frege Systems ◽  
Propositional Proof Systems ◽  
Hilbert Type

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

scholarly journals Another plan for negation

2019 ◽  
Vol 16 (5) ◽  
pp. 159
Author(s):  
Nissim Francez
Keyword(s):  
Paradigm Shift ◽  
Natural Deduction ◽  
Atomic Formula ◽  
Truth Values ◽  
Proof Systems ◽  
Frame Shift ◽  
Main Ideas

The paper  presents a plan for negation, proposing a paradigm shift from the Australian plan for negation,  leading to a family of contra-classical logics. The two main ideas are the following:  Instead of shifting points of evaluation (in a frame), shift the evaluated formula. Introduce an incompatibility set for every atomic formula, extended to any compound formula, and impose the condition on valuations that a formula evaluates to true iff all the formulas in its incompatibility set evaluate to false. Thus, atomic sentences are not independent in their truth-values.  The resulting negation, in addition to excluding the negated formula, provides a positive alternative to the negated formula. I  also present a sound and complete natural deduction proof systems for those logics. In addition, the kind of negation considered in this paper is shown to provide an innovative notion of grounding negation.   

Proof systems for lattice theory

2004 ◽  
Vol 14 (4) ◽  
pp. 507-526 ◽  
Author(s):  
SARA NEGRI ◽  
JAN VON PLATO
Keyword(s):  
Lattice Theory ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Predicate Logic ◽  
Relational Theory ◽  
Predicate Calculus ◽  
Alternative Formulation ◽  
Proof Systems ◽  
Decidable Classes ◽  
Classical Predicate

A formulation of lattice theory as a system of rules added to sequent calculus is given. The analysis of proofs for the contraction-free calculus of classical predicate logic known as G3c extends to derivations with the mathematical rules of lattice theory. It is shown that minimal derivations of quantifier-free sequents enjoy a subterm property: all terms in such derivations are terms in the endsequent.An alternative formulation of lattice theory as a system of rules in natural deduction style is given, both with explicit meet and join constructions and as a relational theory with existence axioms. A subterm property for the latter extends the standard decidable classes of quantificational formulas of pure predicate calculus to lattice theory.

The deduction rule and linear and near-linear proof simulations

1993 ◽  
Vol 58 (2) ◽  
pp. 688-709 ◽  
Author(s):  
Maria Luisa Bonet ◽  
Samuel R. Buss
Keyword(s):  
Propositional Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Upper Bounds ◽  
Proof System ◽  
Proof Systems ◽  
Linear Speedup ◽  
Frege Systems ◽  
Deduction Rule ◽  
Gentzen Sequent Calculus

AbstractWe introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof.A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by “nearly linear” is meant the ratio of proof lengths is O(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O(n . α(n)). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O(n log n) lines and of height O(log n). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O(n log n).

Natural Deduction for Hybrid Logic

2004 ◽  
Vol 14 (3) ◽  
pp. 329-353 ◽  
Author(s):  
T. Brauner
Keyword(s):  
Natural Deduction ◽  
Hybrid Logic
Sign in / Sign up

Export Citation Format

Share Document