Kripke Models for Classical Logic

Danko Ilik (1, 2, 3) , Gyesik Lee (4) , Hugo Herbelin (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
4 ROSAEC - Research On Software Analysis for Error-free Computing

We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.

Mots clés: Kripke model; classical logic; sequent calculus; lambda mu calculus; classical realizability; normalization by evaluation

Domaines: Logique [math.LO]; Logique en informatique [cs.LO]

Danko Ilik, Gyesik Lee, Hugo Herbelin. Kripke Models for Classical Logic. Annals of Pure and Applied Logic, 2010, Special Issue: Classical Logic and Computation (2008), 161 (11), pp.1367-1378. ⟨10.1016/j.apal.2010.04.007⟩. ⟨inria-00371959v4⟩