Kripke Models for Classical Logic

Danko Ilik (PPS; Gyesik Lee (ROSAEC); Hugo Herbelin (PPS; INRIA Paris - Rocquencourt; INRIA Paris - Rocquencourt); LIX)

arxiv: 0904.0071 · v5 · pith:3NY5E3IAnew · submitted 2009-04-01 · 🧮 math.LO · cs.LO

Kripke Models for Classical Logic

Danko Ilik (PPS , INRIA Paris - Rocquencourt , LIX) , Gyesik Lee (ROSAEC) , Hugo Herbelin (PPS , INRIA Paris - Rocquencourt) This is my paper

classification 🧮 math.LO cs.LO

keywords classicalkripkelogicnotionapplicationscompletenessconstructivelycut-free

0 comments

read the original abstract

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.

This paper has not been read by Pith yet.

Kripke Models for Classical Logic

discussion (0)