The Royal Swedish Academy of Sciences(4)

Thereportisorganizedasfollows.InSection2weintroducethebrackettypes.InSection3wegivethesemanticsofbrackettypesinregularcat-egories,andproveitssoundnessandcompleteness.InSection4westudysomepropertiesofbrackettypes.InSection5weshowhowbrackettypesareusedinconjunctionwithotherdependenttypestode nethelogicalconnectivesandquanti erswithintypetheory.InSection6weusebrackettypestocomparetwointerpretationsoflogic:thestandard“propositionsastypes”interpretation,andtheusual rst-orderone.

2BracketTypes

WeconsideraMartin-L¨ofstyledependenttypetheory[ML84,ML98].Fortheformulationofbrackettypeswedonotneeddependentsumsorproducts,butwesometimesassumethattheyarepresentinthetypetheory.Weworkinatypetheorywithstrongandextensionalequalityandstrongdependentsums,cf.[Jac99].Forreference,welisttherulesinAppendixA.

Amongthetypes,therearesomethatsatisfythefollowingconditionof“proofirrelevance”:

Γ PtypeΓ q:P

Γ p=q:PΓ p:P(1)

Inwords,thismeansthatanytwotermspandqofsuchatypePare(extensionally)equal.Wecallthetypessatisfyingproofirrelevanceproposi-tions.TheywerecalledmonotypesbyMaietti[Mai98],andthereareotherequivalentformulations.

3

搜索“diyifanwen.net”或“第一范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，第一范文网，提供最新人文社科The Royal Swedish Academy of Sciences(4)全文阅读和word下载服务。