Forskningsagendaer, forespørsler og svar i konstruktiv typeteori.

Abstract

Konstruktiv typeteori ble introdusert av Per Martin-Löf i 1984. Bakgrunnen var å unngå skillet mellom form og mening. Konstruktiv type- teori ble dannet på bakgrunn av Brouwers intuisjonisme fra begynnelsen av 1900-tallet. Senere, i 2006, publiserer Olsson en artikkel hvor han implementerer forskningsagendaer og spørsmål i AGM-teorien. Relasjonen mellom AGM-teorien og konstruktiv typeteori ble utviklet av Primiero. Det er denne teorien jeg skal ta utgangspunkt i her. Mitt prosjekt er å forklare hvordan man kan forstå forskningsagendaer og spørsmål i kon- struktiv typeteori. En forskningsagenda består av spørsmål som må besvares. Disse spørs- målene representeres som eksklusive disjunksjoner. Jeg skal beholde den- ne definisjonen av spørsmål her, men skille dem fra det spørrende as- pektet ved å stille et spørsmål. Dette aspektet introduseres ved hjelp av en forespørselsoperator. En forespørsel krever svar. Jeg skal introduse- re en svaroperator som angir om en forespørsel er lukket eller ikke. Vi har tre varianter av denne forespørselsoperatoren, en for typedeklarasjo- ner, en for antagelser og en for definisjoner. Da vi har tre varianter av forespørselsoperatoren, vil vi også ha tre varianter av svaroperatoren, en for hver forespørselsoperator. En forskningsagenda kan beskrives av en strategi som bestemmer hvilke forespørsler som skal utledes. En forsk- ningsagenda forstås som en samling ubesvarte forespørsler. Ved hjelp av disse operatorene skal jeg forklare hvordan vi kan forma- lisere noen aspekter ved spørsmål og svar i naturlig språk. Disse operato- rene tilsvarer spørsmål slik de er presentert av Olsson. Problemene som førte til introduksjonen av forskningsagendaer vil løses i det konstruktive typeteoretiske rammeverket ved hjelp av spørsmål og forespørsler.