First-Order Logic with Isomorphism

[Dimitris Tsementzis]

Hi all,

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

I now call the system in the paper “First-Order Logic with Isomorphism” (FOLiso). FOLiso 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 number for each object corresponding to its h-level and three specified types of objects: “isomorphism sorts”, “reflexivity predicates” and “transport structure”. The signatures of FOLiso can then be used to express theories that involve conditions on identity 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 Diso that handles propositions defined over FOLiso-singatures. Diso is basically a sequent calculus for first-order logic together with (i) axioms expressing that there are always trivial isomorphisms such that transporting along them is the identity and (ii) a “first-order J-rule” for isomorphism sorts. 

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 “isomorphism sorts” interpreted as identity types and “transport structure” interpreted as (a relational version of) transport. Soundness 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 “elementary” in the sense that it can be defined independently of any univalent type theory and so can be expected to have a semantics in any formal system for the Univalent Foundations or in the categorical semantics of any such formal system. I believe it is important to have such an “elementary” 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. 

In other words, FOLiso is a proposed “core logic” for UF. One can then use it to e.g. define a “logic enriched homotopy type theory” or one can internalize it (e.g. in two-level type theory) etc.

Best,

Dimitris