1,721,055 research outputs found
2-sequent calculus: intuitionism and natural deduction
No full textThis approach to studying the minimal intuitionistic modal logic is based on a generalization of Gentzen's original sequent calculus introduced and developed by the author in a previous paper [see Ann. Pure Appl. Logic 58 (1992), no. 3, 229--246; MR1191942 (93k:03056)]. The complete proof-theoretic treatment of the calculus is presented, including the cut elimination theorem with some of its consequences. The author considers the corresponding 2-natural deduction system, followed by the normalization theorem, and analyzes its relationship with the 2-sequent calculus. Such an approach to the proof-theoretic analysis of logical systems seems to be very natural, fruitful and applicable to a wide class of logics
2-Sequent calculus: a proof theory of modalities
No full textAbstractMasini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 (1992) 229–246.In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem
On the fine structure of the exponential rule
No full textThe authors investigate fragments of intuitionistic linear logic with the connectives ⊗, →, ! and the constant 1, in which weakening and contraction is not allowed even on modalized formulas. Instead, some rules are retained corresponding to the axioms (K) !(A→B)→(!A→!B), (T) !A→A, and (4) !A→!!A. The formulation in natural deduction style is obtained via the so-called 2-sequent calculus of Masini [Ann. Pure Appl. Logic 58 (1992), no. 3, 229--246; MR1191942 (93k:03056)]. Thus formulas in deductions are indexed by positive integers ("levels''), and the propositional rules preserve the levels; the introduction rule for ! is Aj/!Aj−1 provided j is bigger than any level of any formula occurring in open assumptions. The elimination rule depends on the fragment chosen; for the full KT4 fragment it is !Aj/Ak (k≥j). Via a careful definition of reductions on derivations (which in the exponential case also requires a suitable rewriting of the levels in the contractum) the authors prove a normalization result. By comparison with proof-nets it is maintained, without proof, that strong normalization and confluence hold for the given reduction relation
A natural deduction system for bundled branching time logic
No full textWe introduce a natural deduction system for the until-free subsystem of the branching time logic Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics
Proofs, tests and continuation passing style
No full textThe concept of syntactical duality is central in logic. In particular, the duality defined by classical
negation, or more syntactically by left and right in sequents, has been widely used to relate logic
and computations.
We study the proof/test duality proposed by Girard in his 1999 paper on the meaning of logical
rules. In detail, starting from the notion of “test” proposed by Girard, we develop a notion of test for
intuitionistic logic and we give a complete deductive system whose computational interpretation is
the target language of the call-by-value and call-by-name continuation passing style translations
Proof Nets for Classical Logic
No full textWe propose a new direct presentation of full (propositional) classical logic by means of proof nets, for which strong normalization and confluence hold true. Our proposal is based on the breaking of symmetry between propositional connectives, combined with a principle of focusing/defocusing
A two-dimensional metric temporal logic
No full textWe introduce a two-dimensional metric (interval) temporal logic whose inter- nal and external time flows are dense linear orderings. We provide a suitable semantics and a sequent calculus with axioms for equality and extralogical axioms. Then we prove completeness and a semantic partial cut-elimination theorem down to formulas of a certain type
- …
