Transitive Primal Infon Logic: the Propositional Case

Primal (propositional) logic PL is the ∧,→ fragment of intuitionistic logic, and primal (propositional) infon logic PIL is a conservative extension of PL with the quotation construct psaid. Logic PIL was introduced by Gurevich and Neeman in 2009 in connection with the DKAL project. The derivation problem for PIL (and therefore for PL) is solvable in linear time, and yet PIL allows one to express many common access control scenarios.

The most obvious limitation on the expressivity of logic PL is the failure of the transitivity rule

(trans0) producing x → z from x → y, y → z.

Similarly, the most obvious limitation on the expressivity of logic PIL is the failure of the transitivity rule

(trans) producing (pref (x → z)) from (pref (x → y)), (pref (y → z))

where pref ranges over quotation prefixes.

Here we investigate the extension T of PL with an axiom x → x and the inference rule (trans0) as well as the extension qT of PIL with an axiom (pref x → x) and the inference rule (trans).

• [Subformula property] T has the subformula property: if Γ yields y then there is a derivation of y from Γ comprising only subformulas of Γ ∪ y. qT has a similar locality property.
• [Complexity] The derivation problems for T and qT are solvable in quadratic time.
• [Soundness and completeness] We define Kripke models for qT (resp. T) and show that the semantics is sound and complete.
• [Small models] T has the one-element-model property: if Γ does not yield y then there is a one-element counterexample. Similarly small (though not one-element) counterexamples exist for qT.