applicazioni alla logica

Tesi.aux

@@ -1,25 +1,32 @@
 \relax 
 \abx@aux@refcontext{nty/global//global/global/global}
-\@writefile{toc}{\contentsline {section}{\numberline {0.1}Introduction}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {chapter}{\numberline {0}Introduction}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {0.2}Freyd cover of a category}{2}{}\protected@file@percent }
+\@writefile{lof}{\addvspace {10\p@ }}
-\newlabel{completenesscomma}{{0.2.3}{3}{}{definition.0.2.3}{}}
+\@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{push_1}{{1}{4}{}{equation.0.1}{}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {1}Freyd Cover}{5}{}\protected@file@percent }
-\newlabel{def-u}{{2}{5}{}{equation.0.2}{}}
+\@writefile{lof}{\addvspace {10\p@ }}
-\newlabel{x'y'}{{3}{6}{}{equation.0.3}{}}
+\@writefile{lot}{\addvspace {10\p@ }}
-\newlabel{x''y''}{{4}{6}{}{equation.0.4}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {1.1}Freyd cover of a category}{5}{}\protected@file@percent }
-\newlabel{pushoutarrinAB}{{5}{6}{}{equation.0.5}{}}
+\newlabel{completenesscomma}{{1.1.3}{6}{}{definition.1.1.3}{}}
-\newlabel{goalpush}{{6}{6}{}{equation.0.6}{}}
+\newlabel{push_1}{{1.1}{7}{}{equation.1.1}{}}
-\newlabel{uAuBarrow}{{7}{7}{}{equation.0.7}{}}
+\newlabel{def-u}{{1.2}{8}{}{equation.1.2}{}}
-\newlabel{pull}{{10}{10}{}{equation.0.10}{}}
+\newlabel{x'y'}{{1.3}{9}{}{equation.1.3}{}}
-\newlabel{pullstart}{{11}{10}{}{equation.0.11}{}}
+\newlabel{x''y''}{{1.4}{9}{}{equation.1.4}{}}
-\newlabel{cover of bicartesian}{{0.2.6}{11}{}{definition.0.2.6}{}}
+\newlabel{pushoutarrinAB}{{1.5}{9}{}{equation.1.5}{}}
-\newlabel{prodgoal}{{13}{12}{}{equation.0.13}{}}
+\newlabel{goalpush}{{1.6}{9}{}{equation.1.6}{}}
-\newlabel{coverheyting}{{0.2}{14}{}{definition.0.2.8}{}}
+\newlabel{uAuBarrow}{{1.7}{10}{}{equation.1.7}{}}
+\newlabel{pull}{{1.10}{13}{}{equation.1.10}{}}
+\newlabel{pullstart}{{1.11}{13}{}{equation.1.11}{}}
+\newlabel{cover of bicartesian}{{1.1.6}{14}{}{definition.1.1.6}{}}
+\newlabel{prodgoal}{{1.13}{15}{}{equation.1.13}{}}
+\newlabel{coverheyting}{{1.1}{17}{}{definition.1.1.8}{}}
+\newlabel{exp goal}{{1.14}{18}{}{equation.1.14}{}}
+\newlabel{global section in cover rmk}{{1.1.9}{18}{}{definition.1.1.9}{}}
 \abx@aux@cite{0}{angiuli2022canonicity}
 \abx@aux@segm{0}{0}{angiuli2022canonicity}
-\newlabel{exp goal}{{14}{15}{}{equation.0.14}{}}
+\newlabel{cover of cc is cc}{{1.1.13}{19}{}{definition.1.1.13}{}}
-\newlabel{cover of cc is cc}{{0.2.12}{15}{}{definition.0.2.12}{}}
+\newlabel{pullback condition}{{1.16}{20}{}{equation.1.16}{}}
-\newlabel{pullback condition}{{16}{17}{}{equation.0.16}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {1.2}Application to Logic}{24}{}\protected@file@percent }
 \abx@aux@read@bbl@mdfivesum{A692FE2EF8541C6E6F38713971A59175}
 \abx@aux@defaultrefcontext{0}{angiuli2022canonicity}{nty/global//global/global/global}
-\gdef \@abspage@last{21}
+\gdef \@abspage@last{27}

Tesi.blg

@@ -1,15 +1,15 @@
 [0] Config.pm:328> INFO - This is Biber 2.21
 [0] Config.pm:331> INFO - Logfile is 'Tesi.blg'
-[31] biber:342> INFO - === Thu May 14, 2026, 14:51:25
+[33] biber:342> INFO - === Sun May 17, 2026, 17:50:23
-[42] Biber.pm:421> INFO - Reading 'Tesi.bcf'
+[138] Biber.pm:421> INFO - Reading 'Tesi.bcf'
-[72] Biber.pm:1002> INFO - Found 1 citekeys in bib section 0
+[167] Biber.pm:1002> INFO - Found 1 citekeys in bib section 0
-[80] Biber.pm:4487> INFO - Processing section 0
+[174] Biber.pm:4487> INFO - Processing section 0
-[84] Biber.pm:4678> INFO - Looking for bibtex file 'Bibliografia.bib' for section 0
+[180] Biber.pm:4678> INFO - Looking for bibtex file 'Bibliografia.bib' for section 0
-[84] bibtex.pm:1713> INFO - LaTeX decoding ...
+[181] bibtex.pm:1713> INFO - LaTeX decoding ...
-[85] bibtex.pm:1519> INFO - Found BibTeX data source 'Bibliografia.bib'
+[182] bibtex.pm:1519> INFO - Found BibTeX data source 'Bibliografia.bib'
-[102] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'normalization = NFD' with 'normalization = prenormalized'
+[201] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'normalization = NFD' with 'normalization = prenormalized'
-[102] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'variable = shifted' with 'variable = non-ignorable'
+[201] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'variable = shifted' with 'variable = non-ignorable'
-[103] Biber.pm:4307> INFO - Sorting list 'nty/global//global/global/global' of type 'entry' with template 'nty' and locale 'en-US'
+[201] Biber.pm:4307> INFO - Sorting list 'nty/global//global/global/global' of type 'entry' with template 'nty' and locale 'en-US'
-[103] Biber.pm:4313> INFO - No sort tailoring available for locale 'en-US'
+[201] Biber.pm:4313> INFO - No sort tailoring available for locale 'en-US'
-[103] bbl.pm:676> INFO - Writing 'Tesi.bbl' with encoding 'UTF-8'
+[202] bbl.pm:676> INFO - Writing 'Tesi.bbl' with encoding 'UTF-8'
-[104] bbl.pm:779> INFO - Output to Tesi.bbl
+[202] bbl.pm:779> INFO - Output to Tesi.bbl

Tesi.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.29 (TeX Live 2026/Arch Linux) (preloaded format=pdflatex 2026.4.6)  15 MAY 2026 20:28
+This is pdfTeX, Version 3.141592653-2.6-1.40.29 (TeX Live 2026/Arch Linux) (preloaded format=pdflatex 2026.4.6)  17 MAY 2026 18:04
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -813,33 +813,43 @@ File: umsb.fd 2013/01/14 v3.01 AMS symbols B
 ) [1
 
 
-{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2{/usr/share/texmf-dist/f
+{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2
-onts/enc/dvips/cm-super/cm-super-ts1.enc}] [3]
-Underfull \vbox (badness 1365) has occurred while \output is active []
 
- [4]
+]
-[5] [6] [7] [8]
+Chapter 0.
+[3] [4
+
+]
+Chapter 1.
+[5{/usr/share/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}] [6]
+[7] [8] [9] [10] [11]
 Underfull \vbox (badness 10000) has occurred while \output is active []
 
- [9]
+ [12]
-Overfull \hbox (1.52892pt too wide) in paragraph at lines 396--400
+Overfull \hbox (10.66771pt too wide) in paragraph at lines 396--400
 \OT1/cmr/m/n/12 Now, con-sider the cou-ple $(\OML/cmm/m/it/12 u[]; u[]\OT1/cmr/
-m/n/12 )$; by com-mu-ta-tiv-ity of (11[]) if $(\OML/cmm/m/it/12 u[]; u[]\OT1/cm
+m/n/12 )$; by com-mu-ta-tiv-ity of (1.11[]) if $(\OML/cmm/m/it/12 u[]; u[]\OT1/
-r/m/n/12 ) :
+cmr/m/n/12 ) :
  []
 
-[10] [11]
+[13] [14]
 Overfull \hbox (25.67044pt too wide) detected at line 469
 []
  []
 
-[12] [13] [14] [15]
+[15] [16] [17] [18] [19] [20] [21] [22] [23] [24]
-Underfull \vbox (badness 10000) has occurred while \output is active []
+Overfull \hbox (7.45313pt too wide) in paragraph at lines 799--802
+\OT1/cmr/m/n/12 Now, since $\OML/cmm/m/it/12 ^^W\OT1/cmr/m/n/12 (\OML/cmm/m/it/
+12 ^^^ \OMS/cmsy/m/n/12 _ \OML/cmm/m/it/12  \OT1/cmr/m/n/12 ) = \OML/cmm/m/it/1
+2 ^^W\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 ^^^\OT1/cmr/m/n/12 ) \OMS/cmsy/m/n/12 ^^
+H \OML/cmm/m/it/12 ^^W\OT1/cmr/m/n/12 (\OML/cmm/m/it/12  \OT1/cmr/m/n/12 )$ the
+re ex-ists a global sec-tion $\OML/cmm/m/it/12 g \OT1/cmr/m/n/12 : 1[] \OMS/cms
+y/m/n/12 !
+ []
 
- [16]
+[25] [26
-[17] [18] [19] [20] [21
 
-] (./Tesi.aux)
+] [27] (./Tesi.aux)
  ***********
 LaTeX2e <2025-11-01>
 L3 programming layer <2026-01-19>
@@ -849,10 +859,10 @@ Package logreq Info: Writing requests to 'Tesi.run.xml'.
 
  ) 
 Here is how much of TeX's memory you used:
- 26644 strings out of 469515
+ 26647 strings out of 469515
- 568736 string characters out of 5470808
+ 568827 string characters out of 5470808
- 1334979 words of memory out of 5000000
+ 1335039 words of memory out of 5000000
- 54938 multiletter control sequences out of 15000+600000
+ 54941 multiletter control sequences out of 15000+600000
  640012 words of font info for 86 fonts, out of 8000000 for 9000
  14 hyphenation exceptions out of 8191
  84i,21n,104p,966b,1242s stack positions out of 10000i,1000n,20000p,200000b,200000s
@@ -875,10 +885,10 @@ exmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texmf-dist/fonts
 msfonts/cm/cmti12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/symbol
 s/msam10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.
 pfb></usr/share/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb>
-Output written on Tesi.pdf (21 pages, 323585 bytes).
+Output written on Tesi.pdf (27 pages, 334393 bytes).
 PDF statistics:
- 192 PDF objects out of 1000 (max. 8388607)
+ 211 PDF objects out of 1000 (max. 8388607)
- 121 compressed objects within 2 object streams
+ 134 compressed objects within 2 object streams
  0 named destinations out of 1000 (max. 500000)
  13 words of extra memory for PDF output out of 10000 (max. 10000000)
 

Tesi.tex

@@ -35,9 +35,9 @@
 	
 	\maketitle
 	
-	
+	\setcounter{chapter}{-1}
-	\section{Introduction}
+	\chapter{Introduction}
-	
+	\chapter{Freyd Cover}
 	\section{Freyd cover of a category}  
 	\begin{definition}[Comma Category]
 		Let $\mathcal{A,B,C}$ locally small categories and let $F: \mathcal{A} \to \mathcal{C}, G: \mathcal{B} \to \mathcal{C}$ two functors 
@@ -571,9 +571,14 @@
 			Now, commutativity at the level of $Set$ is ensured by universal property of $Y^X$ in $Set$ plus the coerence condition of $(Y^X)_{a \leq b}$ with respect to $a \to b$. Now, in $\mathcal{H}$ we have that $c \land a \leq b$ we have that $c\land a \leq b \iff c \leq a \to b$ so we have commutativity at the level of $\mathcal{H}$. It remains to check the well definition of the abstraction: let $Z \neq \emptyset$, then $h(m) \in \mathcal{H}(1_\mathcal{H}, c)$ for $m \in Z$, hence $1_\mathcal{H} \leq c$ and so, since $c \land a \leq b$, then $a \leq b$ and so $\hat{u} (m) \in (Y^X)_{a \leq b}$ wihch ensure well definition of abstraction arrows. Notice that uniqueness of abstraction follows directly form uniqueness of abstractions in $Set$ and $\mathcal{H}$. Thus $Cov(\mathcal{H})$ is a bicartesian cloed category.\\
 			Concerning $\Pi_2$, the proof is identical to \ref{completenesscomma} since the $\mathcal{H}$ level of the exponential object is the exponential object in $\mathcal{H}$ and so $\Pi_2$ is a bicartesian closed functor and we are done.
 			\end{proof}
-			
+			\begin{remark}[Structure of $Cov(\mathcal{C})(1, A \oplus B)$] \label{global section in cover rmk}
+				Let $(u,v): 1 \to (X \oplus Y, a \lor b, f \oplus g)$ and consider $u: 1_{Set} \to X \oplus Y$. Since the coproudct in $Set$ is precisely the disjoint union, then $u(\star)$ is either in $X$ or in $Y$. Assume $u(\star) = x_0 = \iota_X(x_0) \in X$ for some $x_0 \in X$, then $(f \oplus g) \circ u = \Gamma v \circ  un $ implies $v(\star)= (\iota_1)_\mathcal{C} \circ f (x_0)$. Since this argument is simmetrical if $u(\star) \in Y$ we have the following decomposition:
+				\[
+				Cov(\mathcal{C})(1, A \oplus B) \cong Cov(\mathcal{C})(1, A ) \sqcup Cov(\mathcal{C})(1, B)
+				\]
+			\end{remark}
 			\begin{definition}
-				Let $\mathcal{H}$ be an Heyting Algebra, then we call its Feryd cover the Frey-Heyting cover of $\mathcal{H}$
+				Let $\mathcal{H}$ be an Heyting Algebra, then we call its Freyd cover the Freyd-Heyting cover of $\mathcal{H}$
 			\end{definition}
 			\begin{definition}
 				We say that $\textbf{biCC}$ is the category with objects bicartesian closed categories and morphisms functors preserving the bicartesian structure up to isomorphism 
@@ -746,15 +751,54 @@
 					\arrow[between={0.2}{0.8}, maps to, from=0, to=1]
 				\end{tikzcd}\]
 				where $F\cdot f: X \to \Gamma (FA)$  is the set function defined sending $x \in X$ into the global setion of $FA$ given by $F( f(x)) : 1_\mathcal{B} \to FA$   
+			\end{proposition} 
 			\begin{proof}
 				By lemma \ref{cover of cc is cc} $Cov(-)$ exentend to a class function from \textbf{biCC} to itself. Then notice that the action of $Cov(-)$ over arrows of \textbf{biCC} is well defined since the commutativity condition of the arrow is preserved under the action of $F$. Indeed by definition of $F \cdot f$ and $F \cdot g$ we have:
 				\[
 				(F \cdot g) \circ h = F(\Gamma k) \circ (F \cdot f)
 				\]
+				Ando so for $F: A \to B$ we proved $Cov(F): Cov(\mathcal{A}) \to Cov(\mathcal{B})$ is a well defined functor. Moreover, clearly $Cov(Id_\mathcal{A})= Id_{Cov(\mathcal{A})}$ and by definition of $F \cdot f$ thaking $F: \mathcal{A} \to \mathcal{B}$ and $G: \mathcal{B} \to \mathcal{C}$ we have that $Cov(G \cdot F) = Cov(G) \cdot Cov(F)$. Thus $Cov(-): \textbf{biCC} \to \textbf{biCC}$ is a well defined endofunctor
 			\end{proof}
-			\end{proposition}
-			
 			
+			\begin{corollary}
+				Taking posettal reflection of a lattice - i.e. an ordered bicartesian closed category - gives rise to an endofunctor: 
+				\[
+				Pcov(-): \textbf{bLat} \to \textbf{bLat}
+				\]
+				where $Pcov(-) := Pos \circ Cov (-) : \textbf{bLat} \to\textbf{bLat}$ and \textbf{bLat} is the category of bounded lattices - i.e. lattice with top and bottom objects - with lattice homomorpishms as arrows.
+			\end{corollary}
+			\begin{proof}
+				By lemma \ref{cover of bicartesian} the cover of a lattice has a bicartesian structure and by lemma \ref{cover of cc is cc} the cover of a lattice is also a cartesian closed category. Therefore we are done, since the posettal reflection of a bicartesian closed category is a bounded lattice (the posettal reflection preserves bicartesian closed struture of the category) 
+			\end{proof}
 			
+			\section{Application to Logic}
+			After defining the construction of Freyd Cover and proving some baisc property of this constuction we are ready to use the categorical property of $Cov(-)$ to show some logical poperty of intuitionistic logic. In this section we will prove categorically that the propositional logic satisfy the disjunction property using the Freyd Cover construction. 
+			\begin{theorem}
+				Let the following disjunction $\phi \lor \psi$ be derivable in the intuitionistic propositional logic. Then either $\phi$ or $\psi$ is derivable.
+			\end{theorem}
+			\begin{proof} \, \\
+				\textbf{Idea}: We will apply our construction to the Lindembaum-Tarski algebra of the initial intuitionistic propositional logic $\mathcal{T}_0$. Notice that the projection $\Pi_2: Cov(\mathcal{A}_i(\mathcal{T}_0)) \to \mathcal{A}_i(\mathcal{T}_0)$ "preserves" the Lindembaum component of element of $Cov(\mathcal{A}_i(\mathcal{T}_0))$,therefore a clever model build upon $Cov(\mathcal{A}_i(\mathcal{T}_0))$ respects the categorical semantics of $\mathcal{T}_0$. We will use this property to construct, from the fact that $\phi \lor \psi$ holds, a global section of $\phi$ or $\psi$, proving the disjunction property. \\
+				\textbf{Proof}: Let $\mathcal{T}_0$ be the initial intuitionistic propositional theory and consider the Lindembaum-Tarki algebra $\mathcal{A}_i(\mathcal{T}_0)$. Notice that $Pcov(\mathcal{A}_i(\mathcal{T}_0))$is an heyting algebra, so we can define a model 
+				\[
+				\nu : Frm(\mathcal{T}_0) \to Pcov(\mathcal{A}_i(\mathcal{T}_0))
+				\]
+				in the following way: let $A$ be a propositional variable, then
+				\[
+				A \to \nu(A)= [(X_A, [A], e_A)]
+				\]
+				where $X_A$ is the terminal object in $Set$ if $1 \leq_{\mathcal{A}_i(\mathcal{T}_0)} [A]$ and initial otherwise:
+				\[
+				X_A := \{ x = 0 | 1 \leq_{\mathcal{A}_i(\mathcal{T}_0)} [A]  \}
+				\]
+				notice that $[(X_A,[A],e_A)]$ is a well defined element of $Pcov(\mathcal{A}_i(\mathcal{T}_0))$. In fact if $A$ is the top in $\mathcal{A}_i(\mathcal{T}_0)$ then the set global section of the class $[A]$ is terminal and so $e_A$ is uniquely defined. Otherwise $X_A$ is inital in $Set$ and thus again $e_A$ is uniquely defined. Now, this definition can be extended inductively by lifting the Lindembaum-Tarski evalutation to the Freyd Cover, namely by setting $\nu(\psi \land psi) = \nu (\psi) \times \nu (\psi)$, $\nu (\psi \lor \psi) = \nu(\phi) \oplus \nu(\psi)$ and $\nu(\phi \to \psi)= \nu(\psi)^{\nu(\phi)}$. Therefore for an arbitrary formula $\phi$ we have:
+				\[
+				\nu(\phi) = [(X_\phi, [\phi], e_\phi)]
+				\]
+				for some $X_\phi$ in $Set$ and $e_\phi : X_\phi \to \Gamma [\phi]$. Notice that in this model the evaluation of a propositional variable $A$ and $\neg A$ is neither the top or the bottom (this follows immediatly by construction). \\
+				Let $\phi \lor \psi$ be a tautology in $\mathcal{T}_0$, therefore \[\nu(\phi \lor \psi) = 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} = [(1_{Set}, 1_{\mathcal{A}_i(\mathcal{T}_0)},un)]
+				\]
+				Now, since $\nu (\phi \lor \psi)= \nu(\phi) \oplus \nu(\psi)$ there exists a global section $g: 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} \to [(X_\phi , [\phi] , e_\phi)] \oplus [(X_\psi , [\psi], e_\psi)]$.
+				By remark \ref{global section in cover rmk} $g = (g_1,g_2): 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} \to \nu(\phi)$ or $g = (g_1,g_2): 1_{Pcov(\mathcal{A}_i(\mathcal{T}_0))} \to \nu(\psi)$. Now, in the first case $e_\phi (g_1(\star)) \in \Gamma [\phi]$ hence $\phi$ is provable in the logic. In the second case $e_\psi (g_1(\star)) \in \Gamma [\psi]$ and so $\psi$ is provable in the logic. Thus the disjunctin property is proved and so we are done.
+			\end{proof}
 			\printbibliography
 \end{document}