From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.202.220.214 with SMTP id t205mr6951581oig.72.1506480563051; Tue, 26 Sep 2017 19:49:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.159.48.214 with SMTP id k22ls228783uab.10.gmail; Tue, 26 Sep 2017 19:49:22 -0700 (PDT) X-Received: by 10.31.135.71 with SMTP id j68mr7358500vkd.109.1506480562065; Tue, 26 Sep 2017 19:49:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1506480562; cv=none; d=google.com; s=arc-20160816; b=Yha+IF4xO0L1TqePUu5r2E4wUiu0Uzo/ZwnEknh3ylZqI7fF9CAl1isAyruoJ8hFib o8LEkxkauTZTlpIhQUSEfXI2AmZGEtH7fzpxX5h6n/RobqGQg8VwQExbPXsqfoBaGatG b+xGEsTLncbfOUJoOd79ShNkASpkRiCntsKlga4o0zMUpgrAq+wjAG4E6OXmcL8NbMfn WAHhQGGymTz9nRpWDyFfYO4uV9Mx9Eef8NyixUuYvC98KAn2wNEP1FgYPZgEYNBqNX7C 7jyTv3qX4c+3C/eGN5nk4voCnd0rTnd5gM7QVVuUpoH6Hm+c8YlGHLvColHXgaJ6aJus FDxg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:to:date:message-id:subject:from :arc-authentication-results; bh=5RhNcZdpw45n07jv1UmD7R+3csCaWpUsx8W0MWdi0fA=; b=KOp6WyazwExVbNla7+PUCP8rzmlDHbJTFIV6enZXS24IGACeKGjtPUW5ToSXAhIEAi EV8taAmiDCBK64wRY7Aront1n0vsK/yxIpM0myxpiDkxTxdB1RYNFX0k1p9xwUmDx4Zo 726K/12pg+tjc2d/BjLiU38CA+9sKMtAHwb8Qk613mmJf1Xb2fpSKWagb09k3zcYAGuq jz/O3I7xKqegl+f7R/z1VOkm0KRWaaIFJMlxFUwSKCX3N0Mp3hwwmUXBD5nYUkHNzkB2 bkwMWhG/L1enVJ8BpsCbmZ7InMrKANFbfpYWMxzvqYcBqlA1zdCbpGfcmp9vOgeRx9+6 qb8g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa02.Princeton.EDU. [128.112.128.216]) by gmr-mx.google.com with ESMTPS id p66si489923ywh.1.2017.09.26.19.49.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 26 Sep 2017 19:49:22 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) client-ip=128.112.128.216; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp203l.Princeton.EDU (csgsmtp203l.Princeton.EDU [140.180.223.156]) by ppa02.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v8R2nLZd028233 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Tue, 26 Sep 2017 22:49:21 -0400 Received: from [192.168.0.12] (cpe-66-108-10-124.nyc.res.rr.com [66.108.10.124]) (authenticated authid=dtsement bits=0) by csgsmtp203l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id v8R2nG1X024484 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Tue, 26 Sep 2017 22:49:19 -0400 From: Dimitris Tsementzis Content-Type: multipart/alternative; boundary="Apple-Mail=_55D41ED0-56F5-46EB-A4A1-4E47FDDE329A" Subject: First-Order Logic with Isomorphism Message-Id: Date: Tue, 26 Sep 2017 22:49:56 -0400 To: Univalent Mathematics , Homotopy Type Theory Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-09-26_10:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1709270040 --Apple-Mail=_55D41ED0-56F5-46EB-A4A1-4E47FDDE329A Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Hi all, I have just posted (https://arxiv.org/ab= s/1603.03092) a major update of a paper extending Makkai=E2=80=99s FOLDS to= a system which has natural semantics in the Univalent Foundations,=20 I now call the system in the paper =E2=80=9CFirst-Order Logic with Isomorph= ism=E2=80=9D (FOLiso). FOLiso takes the point of view that a signature for = a theory in UF should be a collection of dependently-typed data with specif= ied (possibly infinite) h-level and with some of the data (possibly) depend= ent on the identity types or transports of previously-defined data. To formalize this idea the signatures of FOLiso are defined as inverse cate= gories with extra structure in the form of a number for each object corresp= onding to its h-level and three specified types of objects: =E2=80=9Cisomor= phism sorts=E2=80=9D, =E2=80=9Creflexivity predicates=E2=80=9D and =E2=80= =9Ctransport structure=E2=80=9D. The signatures of FOLiso can then be used = to express theories that involve conditions on identity types (e.g. univale= nt categories) or even conditions on transported terms (e.g. split type cat= egories) etc. On top of this syntax I define a deductive system Diso that handles proposi= tions defined over FOLiso-singatures. Diso is basically a sequent calculus = for first-order logic together with (i) axioms expressing that there are al= ways trivial isomorphisms such that transporting along them is the identity= and (ii) a =E2=80=9Cfirst-order J-rule=E2=80=9D for isomorphism sorts.=20 The semantics of FOLiso are defined through a direct interpretation of the = syntax of FOLiso into the syntax of HoTT understood as MLTT+Pi,Sigma,Id,1,0= ,+,a univalent U and propositional truncation, with =E2=80=9Cisomorphism so= rts=E2=80=9D interpreted as identity types and =E2=80=9Ctransport structure= =E2=80=9D interpreted as (a relational version of) transport. Soundness of = Diso with respect to these semantics is then proven.=20 Although I give FOLiso a specific semantics in the paper, FOLiso is meant t= o be =E2=80=9Celementary=E2=80=9D in the sense that it can be defined indep= endently of any univalent type theory and so can be expected to have a sema= ntics in any formal system for the Univalent Foundations or in the categori= cal semantics of any such formal system. I believe it is important to have = such an =E2=80=9Celementary=E2=80=9D system independent of any specific for= mal system for UF as it allows one to state general facts and come up with = general constraints for UF-specific theories (e.g. univalent categories) th= at one can expect to be able to translate to any formal system for UF.=20 In other words, FOLiso is a proposed =E2=80=9Ccore logic=E2=80=9D for UF. O= ne can then use it to e.g. define a =E2=80=9Clogic enriched homotopy type t= heory=E2=80=9D or one can internalize it (e.g. in two-level type theory) et= c. Best, Dimitris --Apple-Mail=_55D41ED0-56F5-46EB-A4A1-4E47FDDE329A Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Hi all,

I have just posted (https://arxiv.org/abs/1603.03092= ) a major update of a paper extending Makkai=E2=80=99s FOLDS to a syst= em which has natural semantics in the Univalent Foundations, 

I now call the system in = the paper =E2=80=9CFirst-Order Logic with Isomorphism=E2=80=9D (FOLiso). FO= Liso takes the point of view that a signature for a theory in UF should be = a collection of dependently-typed data with specified (possibly infinite) h= -level and with some of the data (possibly) dependent on the identity types= or transports of previously-defined data.

To formalize this idea the signatures of FOLiso= are defined as inverse categories with extra structure in the form of a nu= mber for each object corresponding to its h-level and three specified types= of objects: =E2=80=9Cisomorphism sorts=E2=80=9D, =E2=80=9Creflexivity pred= icates=E2=80=9D and =E2=80=9Ctransport structure=E2=80=9D. The signatures o= f FOLiso can then be used to express theories that involve conditions on id= entity types (e.g. univalent categories) or even conditions on transported = terms (e.g. split type categories) etc.

On top of this syntax I define a deductive system Di= so that handles propositions defined over FOLiso-singatures. Diso is basica= lly a sequent calculus for first-order logic together with (i) axioms expre= ssing that there are always trivial isomorphisms such that transporting alo= ng them is the identity and (ii) a =E2=80=9Cfirst-order J-rule=E2=80=9D for= isomorphism sorts. 

The semantics of FOLiso are defined through a direct interpretatio= n of the syntax of FOLiso into the syntax of HoTT understood as MLTT+Pi,Sig= ma,Id,1,0,+,a univalent U and propositional truncation, with =E2=80=9Cisomo= rphism sorts=E2=80=9D interpreted as identity types and =E2=80=9Ctransport = structure=E2=80=9D interpreted as (a relational version of) transport. Soun= dness of Diso with respect to these semantics is then proven. 

Although I give FOLiso a= specific semantics in the paper, FOLiso is meant to be =E2=80=9Celementary= =E2=80=9D in the sense that it can be defined independently of any univalen= t type theory and so can be expected to have a semantics in any formal syst= em for the Univalent Foundations or in the categorical semantics of any suc= h formal system. I believe it is important to have such an =E2=80=9Celement= ary=E2=80=9D system independent of any specific formal system for UF as it = allows one to state general facts and come up with general constraints for = UF-specific theories (e.g. univalent categories) that one can expect to be = able to translate to any formal system for UF. 
<= br class=3D"">
In other words, FOLiso is a proposed = =E2=80=9Ccore logic=E2=80=9D for UF. One can then use it to e.g. define a = =E2=80=9Clogic enriched homotopy type theory=E2=80=9D or one can internaliz= e it (e.g. in two-level type theory) etc.

Best,

Dimitris --Apple-Mail=_55D41ED0-56F5-46EB-A4A1-4E47FDDE329A--