diff --git a/Tesi.log b/Tesi.log index b38c1fa..47fcda8 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) 19 MAY 2026 15:31 +This is pdfTeX, Version 3.141592653-2.6-1.40.29 (TeX Live 2026/Arch Linux) (preloaded format=pdflatex 2026.4.6) 19 MAY 2026 15:33 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -885,7 +885,7 @@ exmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb> -Output written on Tesi.pdf (27 pages, 334360 bytes). +Output written on Tesi.pdf (27 pages, 334331 bytes). PDF statistics: 211 PDF objects out of 1000 (max. 8388607) 134 compressed objects within 2 object streams diff --git a/Tesi.pdf b/Tesi.pdf index edf9353..b5c262d 100644 Binary files a/Tesi.pdf and b/Tesi.pdf differ diff --git a/Tesi.synctex.gz b/Tesi.synctex.gz index c9ef6f3..f4fc295 100644 Binary files a/Tesi.synctex.gz and b/Tesi.synctex.gz differ diff --git a/Tesi.tex b/Tesi.tex index 7b028cb..3517070 100644 --- a/Tesi.tex +++ b/Tesi.tex @@ -798,7 +798,7 @@ 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 disjunction property is proved and so we are done.$e_\phi (g_1(\star)) \in \Gamma [\phi]$ + 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 disjunction property is proved and so we are done. \end{proof} \printbibliography \end{document} \ No newline at end of file