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...

• Type: Conference
• Year: 2000
• Where: FROCOS
• Authors: Paqui Lucio
• Keywords: Control Systems, FROCOS 2000, Intuitionistic Implication, Logical Consequence, Sequent Calculi