Kripke models for classical logic