Basic Models for Positive and Negative Introspection

Basic models handle justification logics whose postulates are conditions on justification operations, such as J, J4, J45, etc. For such models justification term evaluation conditions can be expressed as closure conditions, and then any propositional atom valuation and any justification term valuation can be extended inductively to all formulas.

Recall, J4 is J with an additional “proof checking” axiomin the

extended language of J with a new unary operation ! on justifications. We begin with the empty constant specification, and then full generality is immediate. We remind the reader of Definitions 3.5 and 3.10.

Theorem 3.14 BM(J4(0)) is the class of basic models for J₀ with the follow­ing closure condition for !

Corollary 3.15 Let CS be an arbitrary constant specification. Basic models for J4(CS), that is BM(J4(CS)), are the basic CS-models for J4. J4(CS) is sound and complete with respect to BM(J4(CS)).

The justification logic J45 is J4 with an additional “negative proof check­ing” axiom

in the extension of the language of J4 with a new unary operation ? on justifi­cations.

Theorem 3.16 BM(J45(0)) is the class of basic models for J4(0) with the ?-condition

Corollary 3.17 Let CS be an arbitrary constant specification. Basic mod­els for J45(CS), BM(J45(CS)), are the basic CS-models for J45. J45(CS) is sound and complete with respect to BM(J45(CS)).

3.4