A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in Martin-Löf's style, and conjectured the equivalence. The equivalence has been left an open question since 2011. This paper shows that CLKID-omega and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKID-omega, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.

EXPLICIT INDUCTION IS NOT EQUIVALENT TO CYCLIC PROOFS FOR CLASSICAL LOGIC WITH INDUCTIVE DEFINITIONS

Berardi Stefano
2019-01-01

Abstract

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in Martin-Löf's style, and conjectured the equivalence. The equivalence has been left an open question since 2011. This paper shows that CLKID-omega and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKID-omega, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.
2019
15
3
1
25
https://lmcs.episciences.org/5661/pdf
proof theory, inductive definitions, Brotherston-Simpson conjecture, cyclic proof,Martin-Lof’s system of inductive definitions, Henkin models
Berardi Stefano
File in questo prodotto:
File Dimensione Formato  
document.pdf

Accesso aperto

Descrizione: versione open access
Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 449.7 kB
Formato Adobe PDF
449.7 kB Adobe PDF Visualizza/Apri
main.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 431.45 kB
Formato Adobe PDF
431.45 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/2318/1779613
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 2
social impact