The logic of the weak excluded middle, known also as Jankov's logic, is an extension of the intuitionistic logic obtained by adding the schema "not A or not not A". This logic offers a good case study for some metatheoretical properties: Is there a cut-free calculus for this logic? Is it analytic? Is there a proof-search procedure that answers the question whether a formula is a theorem or not, and if not, does it give us a strategy to build a countermodel? We answer these quetsions by presenting a calculus, SJC, with the following metatheoretical properties: 1. Proof.search is performed by a single tree. 2. proof.search always terminates since never enters into loops, thanks to the a fortiori rule. 3. there is no need of back-tracking thanks to the rules push and pop. 4. SJC-proofs satisfy the sub-formula property 5. SJC-proofs are cut free. 6. If proof search in SJC fails we get a kripke countermodel based on a ocnvergent frame

The Logic of the Weak Excluded Middle: a Case Study of Proof-Search

CORSI, GIOVANNA
2008

Abstract

The logic of the weak excluded middle, known also as Jankov's logic, is an extension of the intuitionistic logic obtained by adding the schema "not A or not not A". This logic offers a good case study for some metatheoretical properties: Is there a cut-free calculus for this logic? Is it analytic? Is there a proof-search procedure that answers the question whether a formula is a theorem or not, and if not, does it give us a strategy to build a countermodel? We answer these quetsions by presenting a calculus, SJC, with the following metatheoretical properties: 1. Proof.search is performed by a single tree. 2. proof.search always terminates since never enters into loops, thanks to the a fortiori rule. 3. there is no need of back-tracking thanks to the rules push and pop. 4. SJC-proofs satisfy the sub-formula property 5. SJC-proofs are cut free. 6. If proof search in SJC fails we get a kripke countermodel based on a ocnvergent frame
Deduction, Computation, Experiment. Exploring the Effectiveness of Proof
95
116
G. Corsi
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11585/62790
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact