The duality beween assertion and assumption in logic, which is formally the duality between the two sides of a sequent in the sequent calculus, corresponds to the duality between assertion and denial. When going beyond logic in the narrower sense, by considering also inductive definitions of predicates, that is, the atomic base of logic, we obtain a more general picture with two sorts of negation or denial. The first one is direct whereas the second is related to what in logic programming is called 'negation by failure'. Working out this general situation leads to two sorts of assertion, again a direct one and one that may be called 'assertion by failure'. The talk will sketch the formal system resulting from these considerations.

 

Wagner de Campos Sanz
Cut as a Semantical Principle

 

The eliminability of the Cut rule in the sequent calculus is a cornerstone of proof-theory. It guarantees a series of nice properties of the calculus, like consistency via subformula property, etc. Cut has been usually considered a syntactical rule. We want to defy such an assumption. We see reasons for taking it as a semantical principle. If this thesis is accepted, then as a consequence we obtain a semantics for intuitionistic propositional logic.