{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T05:34:18Z","timestamp":1663824858006},"reference-count":26,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2021,7,6]],"date-time":"2021-07-06T00:00:00Z","timestamp":1625529600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,9,15]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>A version of intuitionistic type theory is extended with opposite types, allowing a different formalization of negation and obtaining a paraconsistent type theory ($\\textsf{PTT} $). The rules for opposite types in $\\textsf{PTT} $ are based on the rules of the so-called constructible falsity. A propositions-as-types correspondence between the many-sorted paraconsistent logic $\\textsf{PL}_\\textsf{S} $ (a many-sorted extension of L\u00f3pez-Escobar\u2019s refutability calculus presented in natural deduction format) and $\\textsf{PTT} $ is proven. Moreover, a translation of $\\textsf{PTT} $ into intuitionistic type theory is presented and some properties of $\\textsf{PTT} $ are discussed.<\/jats:p>","DOI":"10.1093\/jigpal\/jzab022","type":"journal-article","created":{"date-parts":[[2021,5,20]],"date-time":"2021-05-20T03:15:47Z","timestamp":1621480547000},"page":"777-806","source":"Crossref","is-referenced-by-count":1,"title":["Type Theory with Opposite Types: A Paraconsistent Type Theory"],"prefix":"10.1093","volume":"30","author":[{"given":"Juan C","family":"Agudelo-Agudelo","sequence":"first","affiliation":[{"name":"Instituto de Matem\u00e1ticas , Universidad de Antioquia, Medell\u00edn, Colombia"}]},{"given":"Andr\u00e9s","family":"Sicard-Ram\u00edrez","sequence":"additional","affiliation":[{"name":"Departamento de Ciencias Matem\u00e1ticas , Universidad EAFIT, Medell\u00edn, Colombia"}]}],"member":"286","published-online":{"date-parts":[[2021,7,6]]},"reference":[{"key":"2022092120485072100_ref1","doi-asserted-by":"crossref","first-page":"231","DOI":"10.2307\/2274105","article-title":"Constructible falsity and inexact predicates","volume":"49","author":"Almukdad","year":"1984","journal-title":"The Journal of Symbolic Logic"},{"key":"2022092120485072100_ref2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","article-title":"Introduction to generalized type systems","volume":"1","author":"Barendregt","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"2022092120485072100_ref3","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-1-4020-6324-4_1","article-title":"Logics of formal inconsistency","volume-title":"Handbook of Philosophical Logic","author":"Carnielli","year":"2007"},{"key":"2022092120485072100_ref4","first-page":"227","article-title":"An analysis of Girard\u2019s paradox","volume-title":"Symposium on Logic in Computer Science","author":"Coquand","year":"1986"},{"key":"2022092120485072100_ref5","volume-title":"A Mathematical Introduction to Logic","author":"Enderton","year":"2001"},{"key":"2022092120485072100_ref6","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1017\/S0960129599002856","article-title":"Some logical and syntactical observations concerning the first-order dependent type system $\\lambda \\mathrm{p}$","volume":"9","author":"Geuvers","year":"1999","journal-title":"Mathematical Structures in Computer Science"},{"key":"2022092120485072100_ref7","first-page":"1127","article-title":"Negationless intuitionistic mathematics","volume":"49","author":"Griss","year":"1946","journal-title":"Koninklijke Nederlandsche Akademie van Wetenschappen"},{"key":"2022092120485072100_ref8","volume-title":"Intuitionism: An Introduction","author":"Heyting","year":"1971"},{"key":"2022092120485072100_ref9","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/BFb0014058","article-title":"A simplification of Girard\u2019s paradox","volume-title":"Typed Lambda Calculi and Applications (TLCA 1995)","author":"Hurkens","year":"1995"},{"key":"2022092120485072100_ref10","doi-asserted-by":"crossref","first-page":"405","DOI":"10.3166\/jancl.15.405-435","article-title":"Natural deduction systems for Nelson\u2019s paraconsistent logic and its neighbors","volume":"15","author":"Kamide","year":"2005","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2022092120485072100_ref11","first-page":"3","article-title":"Automating and computing paraconsistent reasoning: Contraction-free, resolution and type systems","volume":"45","author":"Kamide","year":"2010","journal-title":"Reports on Mathematical Logic"},{"key":"2022092120485072100_ref12","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1016\/1385-7258(72)90053-4","article-title":"Refutability and elementary number theory","volume":"75","author":"L\u00f3pez-Escobar","year":"1972","journal-title":"Indagationes Mathematicae (Proceedings)"},{"key":"2022092120485072100_ref13","volume-title":"Extensions of First Order Logic","author":"Manzano","year":"1996"},{"key":"2022092120485072100_ref14","first-page":"73","article-title":"An intuitionistic theory of types: Predicative part","volume-title":"Logic Colloquium \u201873 (Bristol, 1973)","author":"Martin-L\u00f6f","year":"1975"},{"key":"2022092120485072100_ref15","first-page":"153","article-title":"Constructive mathematics and computer programming","volume-title":"Logic, Methodology and Philosophy of Science VI (Hannover 1979)","author":"Martin-L\u00f6f","year":"1982"},{"key":"2022092120485072100_ref16","volume-title":"Intuitionistic Type Theory (Notes by Giovanni Sambin of a Series of Lectures Given in Padua 1980)","author":"Martin-L\u00f6f","year":"1984"},{"key":"2022092120485072100_ref17","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f","year":"1996","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"2022092120485072100_ref18","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1093\/oso\/9780198501275.003.0010","article-title":"An intuitionistic theory of types","volume-title":"Twenty-Five Years of Constructive Type Theory","author":"Martin-L\u00f6f","year":"1998"},{"key":"2022092120485072100_ref19","doi-asserted-by":"crossref","first-page":"16","DOI":"10.2307\/2268973","article-title":"Constructible falsity","volume":"14","author":"Nelson","year":"1949","journal-title":"The Journal of Symbolic Logic"},{"key":"2022092120485072100_ref20","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"Prawitz","year":"1965"},{"key":"2022092120485072100_ref21","doi-asserted-by":"crossref","first-page":"467","DOI":"10.2307\/2274694","article-title":"The logic of first order intuitionistic type theory with weak sigma-elimination","volume":"56","author":"Swaen","year":"1991","journal-title":"The Journal of Symbolic Logic"},{"key":"2022092120485072100_ref22","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","article-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"2022092120485072100_ref23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-94-017-0458-8_1","article-title":"Intuitionistic Logic","volume-title":"Handbook of Philosophical Logic","author":"van Dalen","year":"2002"},{"key":"2022092120485072100_ref24","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56734-8","article-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Logic of Information Structures","author":"Wansing","year":"1993"},{"key":"2022092120485072100_ref25","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1093\/logcom\/ext035","article-title":"Falsification, natural deduction and bi-intuitionistic logic","volume":"26","author":"Wansing","year":"2016","journal-title":"Journal of Logic and Computation"},{"key":"2022092120485072100_ref26","first-page":"413","article-title":"Natural deduction for bi-connexive logic and a two-sorted typed $\\lambda $-calculus","volume":"3","author":"Wansing","year":"2016","journal-title":"Journal of Applied Logics"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/5\/777\/45878699\/jzab022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/5\/777\/45878699\/jzab022.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T21:07:11Z","timestamp":1663794431000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/30\/5\/777\/6311410"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,6]]},"references-count":26,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2021,7,6]]},"published-print":{"date-parts":[[2022,9,15]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzab022","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,10]]},"published":{"date-parts":[[2021,7,6]]}}}