<abstract xmlns="http://www.w3.org/1999/xhtml"><p>We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads to derivability of every valid formula. We build a tree of consistent and complete PNPs which is used to construct the model.</p></abstract>

We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads to derivability of every valid formula. We build a tree of consistent and complete PNPs which is used to construct the model.

Weak Completeness Theorem for Propositional Linear Time Temporal Logic

Department of Logic, Informatics and Philosophy of Science, University of Białystok, Plac Uniwersytecki 1, 15-420 Białystok, Poland

Formalized Mathematics

{"article-title":"Weak Completeness Theorem for Propositional Linear Time Temporal Logic"}

We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator....

Weak Completeness Theorem for Propositional Linear Time Temporal Logic

Publié en ligne: 02 févr. 2013

Pages: 227 - 234

DOI: https://doi.org/10.2478/v10037-012-0027-8

This content is open access.