Implicative algebras and their relationship with triposes

The paper aims to analyze the concept of "implicative algebras" -introduced by Alexandre Miquel in "Implicative algebras: a new foundation for realizability and forcing"- focusing primarily on their relationship with the notion of tripos. In the first part, we introduce the structure of "implicative algebra", defining the concepts of "implicative structure" and "separator" and analyzing how the implicative algebras can interpret first-order logic. Later, we recall the notion of tripos and some of its properties and prove how every IA induces a particular type of tripos, called "implicative tripos". Then, fixed a tripos from Set to HA, we show how we can define a particular IA such that the implicative tripos induced by it is isomorphic to the initial tripos. Furthermore, we recall the notion of "geometric morphism between triposes"; then we study which type of function between the corresponding IA is induced by a geometric morphism between implicative triposes. Finally, we define a new type of morphism between triposes, called "first-order logic morphism" and, as before, we analyze which function is induced by this type of morphism.

L'elaborato intende affrontare un'analisi delle "implicative algebras" (IA) -introdotte da Alexandre Miquel in "Implicative algebras: a new foundation for realizability and forcing"- con particolare riferimento alle loro relazioni con il concetto di tripos. Lo studio si avvia analizzando la struttura di implicative algebra, introducendo quindi i concetti di "implicative structure" e di "separator" e ponendo particolare attenzione su come ogni IA possa essere utilizzata per interpretare la logica del primo ordine. Richiamate la nozione di tripos e alcune sue proprietà, viene dimostrato come ogni implicative algebra ne induca un particolare tipo, detto "implicative tripos". Quindi è dimostrato come -fissato un tripos da Set in HA- sia possibile definire una particolare implicative algebra tale che l'implicative tripos, indotto da quest'ultima, sia isomorfo al tripos iniziale. Successivamente viene ripreso il concetto di "geometric morphism between triposes"; fissatone uno tra implicative triposes, si individua quale tipo di funzione esso induca tra le IA corrispondenti. Viene poi definita la nozione di "first order logic morphism": un particolare tipo di morfismo tra triposes. Analogamente a quanto sopra, viene analizzato quale tipo di funzione venga indotto da quest'ultimo tipo di morfismo.