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

G. Corsi (2008). The Logic of the Weak Excluded Middle: a Case Study of Proof-Search. MILANO : Springer.

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

#### 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
##### Scheda breve Scheda completa Scheda completa (DC)
2008
Deduction, Computation, Experiment. Exploring the Effectiveness of Proof
95
116
G. Corsi (2008). The Logic of the Weak Excluded Middle: a Case Study of Proof-Search. MILANO : Springer.
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: https://hdl.handle.net/11585/62790
##### Attenzione

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

• ND
• ND
• 0