diff --git a/Tesi.aux b/Tesi.aux index e7e7cd0..c4fbd2e 100644 --- a/Tesi.aux +++ b/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 {section}{\numberline {0.2}Freyd cover of a category}{2}{}\protected@file@percent } -\newlabel{completenesscomma}{{0.2.3}{3}{}{definition.0.2.3}{}} -\newlabel{push_1}{{1}{4}{}{equation.0.1}{}} -\newlabel{def-u}{{2}{5}{}{equation.0.2}{}} -\newlabel{x'y'}{{3}{6}{}{equation.0.3}{}} -\newlabel{x''y''}{{4}{6}{}{equation.0.4}{}} -\newlabel{pushoutarrinAB}{{5}{6}{}{equation.0.5}{}} -\newlabel{goalpush}{{6}{6}{}{equation.0.6}{}} -\newlabel{uAuBarrow}{{7}{7}{}{equation.0.7}{}} -\newlabel{pull}{{10}{10}{}{equation.0.10}{}} -\newlabel{pullstart}{{11}{10}{}{equation.0.11}{}} -\newlabel{cover of bicartesian}{{0.2.6}{11}{}{definition.0.2.6}{}} -\newlabel{prodgoal}{{13}{12}{}{equation.0.13}{}} -\newlabel{coverheyting}{{0.2}{14}{}{definition.0.2.8}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {0}Introduction}{3}{}\protected@file@percent } +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {chapter}{\numberline {1}Freyd Cover}{5}{}\protected@file@percent } +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {section}{\numberline {1.1}Freyd cover of a category}{5}{}\protected@file@percent } +\newlabel{completenesscomma}{{1.1.3}{6}{}{definition.1.1.3}{}} +\newlabel{push_1}{{1.1}{7}{}{equation.1.1}{}} +\newlabel{def-u}{{1.2}{8}{}{equation.1.2}{}} +\newlabel{x'y'}{{1.3}{9}{}{equation.1.3}{}} +\newlabel{x''y''}{{1.4}{9}{}{equation.1.4}{}} +\newlabel{pushoutarrinAB}{{1.5}{9}{}{equation.1.5}{}} +\newlabel{goalpush}{{1.6}{9}{}{equation.1.6}{}} +\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}{{0.2.12}{15}{}{definition.0.2.12}{}} -\newlabel{pullback condition}{{16}{17}{}{equation.0.16}{}} +\newlabel{cover of cc is cc}{{1.1.13}{19}{}{definition.1.1.13}{}} +\newlabel{pullback condition}{{1.16}{20}{}{equation.1.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} diff --git a/Tesi.blg b/Tesi.blg index b236029..2c2a09a 100644 --- a/Tesi.blg +++ b/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 -[42] Biber.pm:421> INFO - Reading 'Tesi.bcf' -[72] Biber.pm:1002> INFO - Found 1 citekeys in bib section 0 -[80] Biber.pm:4487> INFO - Processing section 0 -[84] Biber.pm:4678> INFO - Looking for bibtex file 'Bibliografia.bib' for section 0 -[84] bibtex.pm:1713> INFO - LaTeX decoding ... -[85] 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' -[102] 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' -[103] Biber.pm:4313> INFO - No sort tailoring available for locale 'en-US' -[103] bbl.pm:676> INFO - Writing 'Tesi.bbl' with encoding 'UTF-8' -[104] bbl.pm:779> INFO - Output to Tesi.bbl +[33] biber:342> INFO - === Sun May 17, 2026, 17:50:23 +[138] Biber.pm:421> INFO - Reading 'Tesi.bcf' +[167] Biber.pm:1002> INFO - Found 1 citekeys in bib section 0 +[174] Biber.pm:4487> INFO - Processing section 0 +[180] Biber.pm:4678> INFO - Looking for bibtex file 'Bibliografia.bib' for section 0 +[181] bibtex.pm:1713> INFO - LaTeX decoding ... +[182] bibtex.pm:1519> INFO - Found BibTeX data source 'Bibliografia.bib' +[201] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'normalization = NFD' with 'normalization = prenormalized' +[201] UCollate.pm:68> INFO - Overriding locale 'en-US' defaults 'variable = shifted' with 'variable = non-ignorable' +[201] Biber.pm:4307> INFO - Sorting list 'nty/global//global/global/global' of type 'entry' with template 'nty' and locale 'en-US' +[201] Biber.pm:4313> INFO - No sort tailoring available for locale 'en-US' +[202] bbl.pm:676> INFO - Writing 'Tesi.bbl' with encoding 'UTF-8' +[202] bbl.pm:779> INFO - Output to Tesi.bbl diff --git a/Tesi.log b/Tesi.log index fb8dc03..c9bfe22 100644 --- a/Tesi.log +++ b/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 -onts/enc/dvips/cm-super/cm-super-ts1.enc}] [3] -Underfull \vbox (badness 1365) has occurred while \output is active [] +{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2 - [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] -Overfull \hbox (1.52892pt too wide) in paragraph at lines 396--400 + [12] +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 -r/m/n/12 ) : +m/n/12 )$; by com-mu-ta-tiv-ity of (1.11[]) if $(\OML/cmm/m/it/12 u[]; u[]\OT1/ +cmr/m/n/12 ) : [] -[10] [11] +[13] [14] Overfull \hbox (25.67044pt too wide) detected at line 469 [] [] -[12] [13] [14] [15] -Underfull \vbox (badness 10000) has occurred while \output is active [] +[15] [16] [17] [18] [19] [20] [21] [22] [23] [24] +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] -[17] [18] [19] [20] [21 +[25] [26 -] (./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 - 568736 string characters out of 5470808 - 1334979 words of memory out of 5000000 - 54938 multiletter control sequences out of 15000+600000 + 26647 strings out of 469515 + 568827 string characters out of 5470808 + 1335039 words of memory out of 5000000 + 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> -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) - 121 compressed objects within 2 object streams + 211 PDF objects out of 1000 (max. 8388607) + 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) diff --git a/Tesi.pdf b/Tesi.pdf index 62d365a..164a4f9 100644 Binary files a/Tesi.pdf and b/Tesi.pdf differ diff --git a/Tesi.synctex.gz b/Tesi.synctex.gz index 9b5770b..13d8cc5 100644 Binary files a/Tesi.synctex.gz and b/Tesi.synctex.gz differ diff --git a/Tesi.tex b/Tesi.tex index 222cd1b..db6f9ee 100644 --- a/Tesi.tex +++ b/Tesi.tex @@ -35,10 +35,10 @@ \maketitle - - \section{Introduction} - - \section{Freyd cover of a category} + \setcounter{chapter}{-1} + \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 % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXG1hdGhjYWx7QX0iXSxbMiwwLCJcXG1hdGhjYWx7Q30iXSxbNCwwLCJcXG1hdGhjYWx7Qn0iXSxbMCwxXSxbMiwxXV0= @@ -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 @@ -745,16 +750,55 @@ \arrow[""{name=1, anchor=center, inner sep=0}, "{(h,Fk)}", from=2-3, to=3-3] \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$ + 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} \ No newline at end of file