[FOM] First-Order Logic with Isomorphism

[Dimitris Tsementzis]

Dear FOM,

I have just posted a new version of my paper “First-Order Logic with Isomorphism” (FOLiso) which might be of interest to some readers of FOM interested in connections between set-theoretic foundations and univalent foundations. The paper is available here <https://arxiv.org/abs/1603.03092> (https://arxiv.org/abs/1603.03092).

FOLiso is meant as the minimal extension of (multi-sorted) FOL= that one would need to make in order to have a stand-alone core logic for the univalent foundations and the paper defines its syntax, deductive system and semantics. The main slogans of FOLiso, which reflect some of the key features of the univalent foundations, are as follows:

1) Everything is a structure. (“The world is the totality of things, not of facts.”)
2) Isomorphism of structures is itself a structure, not a proposition. (“One should not ask: is it true that structure X is isomorphic to structure Y? One should instead ask: what is the structure of the isomorphisms between X and Y?”)
3) Structures constructed on other structures can be transported along isomorphisms.  
4) Propositions are degenerate structures. (“A truth value is the simplest structure.”)
5) Structures are arranged in a hierarchy measuring how far isomorphisms between their components are from being propositions. (“h-levels”)

These slogans are captured by FOLiso as follows.

The syntax of FOLiso (Section 3) extends the syntax of FOL= to include a notion of dependent sorts of a certain h-level as well as three types of logical (i.e. specified) sorts: isomorphism sorts, reflexivity predicates and transport structure. Intuitively, dependent sorts capture constructions on structures and the specified logical sorts capture the idea that equality is a structure, not a proposition. Formally, this is done by defining the signatures of FOLiso to be so-called inverse categories with extra structure and properties.

The deductive system of FOLiso (Section 5) is a standard sequent calculus for FOL= supplemented by three additional rules: (i) there is always a trivial isomorphism (reflexivity), (ii) the trivial isomorphism is the identity (transport along reflexivity is the identity), (iii) any construction on a structure can be transferred along an isomorphism. 

The semantics for FOLiso in homotopy (type) theory (Section 4) interpret isomorphism sorts as path spaces, reflexivity predicates as trivial paths and transport structure as transport along a path. Intuitively, FOLiso can have semantics in any setting which does justice to slogans (1)-(5) above. Formally, FOLiso can have semantics in any version of homotopy type theory, or in any of the categorical semantics of homotopy type theory. 

Some things to note:

a) Even though the paper contains some quite technical arguments in the semantic sections, FOLiso stands apart from these sections in that it can be understood, and therefore also justified intuitively, without any knowledge of homotopy theory, as indeed is its purpose. 

b) Category theory is being used in order to give an elegant formulation of the syntax of FOLiso (following insights of Makkai in his work on FOLDS).

c) All of FOL= can be recovered as a special case of FOLiso. Formally, FOL= is identical to FOLiso over a restricted class of signatures, namely those of “height” at most 2. Intuitively, FOL= is identical to the fragment of FOLiso that deals only with set-level structures and propositional constructions on them.

Best,

Dimitris
 


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170926/711d5411/attachment.html>