Formalizing a non-linear Henkin quantifier

E. López-Escobar

Displaying similar documents to “Formalizing a non-linear Henkin quantifier”

Normal Form Theorem for Systems of Sequents

Mirjana Borisavljević (2007)

Publications de l'Institut Mathématique

Similarity:

Normalization as a consequence of cut elimination

Mirjana Borisavljević (2009)

Publications de l'Institut Mathématique

Similarity:

On an extremely restricted ω-rule

E. López-Escobar (1976)

Fundamenta Mathematicae

Similarity:

Persistent and invariant formulas for outer extensions

Solomon Feferman (1968)

Compositio Mathematica

Similarity:

Maximum Cuts in Extended Natural Deduction

Mirjana Borisavljević (2010)

Publications de l'Institut Mathématique

Similarity:

Connections between cuts and maximum segments

Mirjana Borisavljević (2010)

Kragujevac Journal of Mathematics

Similarity:

Presentation of Natural Deduction

R. P. Nederpelt (1977)

Zbornik Radova

Similarity:

Rule-Generation Theorem and its Applications

Andrzej Indrzejczak (2018)

Bulletin of the Section of Logic

Similarity:

In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some...

A further restricted ω-rule

G. C. Nelson (1971)

Colloquium Mathematicae

Similarity:

Theorem Provers for Substructural Logics

Mirjana Isaković Ilić (2007)

Publications de l'Institut Mathématique

Similarity:

From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction

Jan von Plato (2017)

Bulletin of the Section of Logic

Similarity:

The way from linearly written derivations in natural deduction, introduced by Jaskowski and often used in textbooks, is a straightforward root-first translation. The other direction, instead, is tricky, because of the partially ordered assumption formulas in a tree that can get closed by the end of a derivation. An algorithm is defined that operates alternatively from the leaves and root of a derivation and solves the problem.