We give a Kripke style semantics for an intuitionistic logic for pragmatics ILP, with consists of the Horn fragment of relevant logic to express causal relations between (elementary formulas for) assertions and obligations in the framework of propositional intuitionistic logic as a logic of assertions. In order to prove the completeness theorem we give a decision procedure that given an ILP sequent S either returns a cut-free derivation of S or constructs a finite counter-model, if S is not provable. As a corollary we have the finite model property for ILP and also a new proof that the cut rule is eliminable in ILP.
A Kripke-style Semantics for the Intuitionistic Logic of Pragmatics ILP
BELLIN, Gianluigi;
2003-01-01
Abstract
We give a Kripke style semantics for an intuitionistic logic for pragmatics ILP, with consists of the Horn fragment of relevant logic to express causal relations between (elementary formulas for) assertions and obligations in the framework of propositional intuitionistic logic as a logic of assertions. In order to prove the completeness theorem we give a decision procedure that given an ILP sequent S either returns a cut-free derivation of S or constructs a finite counter-model, if S is not provable. As a corollary we have the finite model property for ILP and also a new proof that the cut rule is eliminable in ILP.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
J Logic Computation-2003-Bellin-755-75.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
2.48 MB
Formato
Adobe PDF
|
2.48 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.