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 p said. 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 limitations on the expressivity of logics PL and PIL are the failures of the transitivity rules x→ y y → z (trans0) x→ z pref x→ y pref y → z (trans) pref x→ z respectively where pref ranges over quotation prefixes p said q said . . .. 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 Γ ` 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 Γ 6` y then there is a one-element counterexample. Similarly small (though not one-element) counterexamples exist for qT.