| dc.description.abstract | Jeg viser at man for enhver funksjon f i en delmengde av de Kalmárelementære funksjonene kan konstruere bevis for utsagn på formen N{f(m_1,…m_n)} med høyde lineær i m_1,...,m_n. Delmengden består av de elementære funksjonene, unntatt modifisert subtraksjon og funksjoner hvor modifisert subtraksjon inngår i definisjonen. For enkelhets skyld kaller jeg delmengden av de elementære funksjonene strengt voksende. Uttrykket N{f(m_1,...,m_n)} uttrykker at f er definert for argumentene m_1,...,m_n. De korte utledningene oppnås ved å bruke induktive predikater om funksjonene, introdusert av Jervell og Zhang (2000), som snittformler. Uten snitt har en utledning av N{f(m_1,...,m_n)} minst like stor høyde som tallverdien av f(m_1,...,m_n). Jeg gir en algoritme for å søke etter snitt ut i fra definisjonen av den funksjonen som forekommer i utsagnet man vil bevise. Algoritmen er integrert i en modifisert versjon av den automatiske teorembeviseren PESCA.
Videre viser jeg at hvis det finnes et bevis av N{f(m_1,...,m_n)} med høyde lineær i m_1,...,m_n, så er f elementær. I dette beviset benytter jeg at snitteliminasjonsteoremet gir et elementært bånd på snitteliminasjon, når snittkompleksiteten er kjent.
For å kunne benytte snitteliminasjonsteoremet har jeg definert et
bevissystem for første ordens aritmetikk hvor aksiomer er omskrevet
til ikkelogiske slutningsregler. Metoden, introdusert av Negri og von
Plato (2001), gir systemer som bevarer snitteliminasjon, i motsetning til tradisjonelle aksiomsystemer hvor full snitteliminasjon ikke er mulig. Systemet inneholder ikke induksjonsaksiomet. | nor |