Sciweavers

Share
FROCOS
2000
Springer

Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic

9 years 1 months ago
Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic
We define a sound and complete logic, called FO , which extends classical first-order predicate logic with intuitionistic implication. As expected, to allow the interpretation of intuitionistic implication, the semantics of FO is based on structures over a partially ordered set of worlds. In these structures, classical quantifiers and connectives (in particular, implication) are interpreted within one (involved) world. Consequently, the forcing relation between worlds and formulas, becomes non-monotonic with respect to the ordering on worlds. We study the effect of this lack of monotonicity in order to define the satisfaction relation and the logical consequence relation which it induces. With regard to proof systems for FO , we follow Gentzen's approach of sequent calculi (cf. [8]). However, to deal with the two different implications simultaneously, the sequent notion needs to be more structured than the traditional one. Specifically, in our approach, the antecedent is structure...
Paqui Lucio
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where FROCOS
Authors Paqui Lucio
Comments (0)
books