\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{SCT072-1.p} Arrow Order 255\_4

Formalization of two proofs of Arrow's impossibility theorem. One
 formalization is based on utility functions, the other one on 
 strict partial orders.




$\mbox{v\_thesis\_\_\_\_}\mbox{ or }\mbox{v\_a} = \mbox{v\_b}\qquad\mbox{cnf}(\mbox{cls\_that}_0,\mbox{axiom})$

$\mbox{c\_List\_Odistinct}(\mbox{c\_List\_Olist\_OCons}(\mbox{v\_sko\_\_CHAINED\_}_1,\mbox{c\_List\_Olist\_OCons}(\mbox{v\_sko\_\_CHAINED\_}_2,\mbox{c\_List\_Olist\_OCons}(\mbox{v\_sko\_\_CHAINED\_}_3,\mbox{c\_List\_Olist\_ONil}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt})\qquad\mbox{cnf}(\mbox{cls\_CHAINED}_0,\mbox{axiom})$

$\neg\,\mbox{v\_thesis\_\_\_\_}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{v\_thesis\_\_\_\_}\mbox{ or }\mbox{v\_x} = \mbox{v\_xa}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

\medskip\textbf{SCT101-1.p} Arrow Order 34\_12

Formalization of two proofs of Arrow's impossibility theorem. One
 formalization is based on utility functions, the other one on 
 strict partial orders.




$\mbox{c\_List\_Odistinct}(\mbox{c\_List\_Olist\_OCons}(\mbox{v\_sko\_\_CHAINED\_}_1,\mbox{c\_List\_Olist\_OCons}(\mbox{v\_sko\_\_CHAINED\_}_2,\mbox{c\_List\_Olist\_OCons}(\mbox{v\_sko\_\_CHAINED\_}_3,\mbox{c\_List\_Olist\_ONil}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt})\qquad\mbox{cnf}(\mbox{cls\_CHAINED}_0,\mbox{axiom})$

$\mbox{v\_x} = \mbox{v\_a}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

\medskip\textbf{SCT029-1.p} Arrow Order 156\_1

Formalization of two proofs of Arrow's impossibility theorem. One
 formalization is based on utility functions, the other one on 
 strict partial orders.




$\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OIIA}(\mbox{v\_F})\mbox{ or }\mbox{c\_in}(\mbox{v\_sko\_\_Arrow\_\_Order\_\_Mirabelle\_\_XIIA\_\_def\_}_2(\mbox{v\_F}),\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OProf},\mbox{tc\_fun}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oindi},\mbox{tc\_fun}(\mbox{tc\_prod}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt},\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_bool})))\qquad\mbox{cnf}(\mbox{cls\_IIA\_\_def}_4,\mbox{axiom})$

$\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_Ounanimity}(\mbox{v\_F})\mbox{ or }\mbox{c\_in}(\mbox{v\_sko\_\_Arrow\_\_Order\_\_Mirabelle\_\_Xunanimity\_\_def\_}_2(\mbox{v\_F}),\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OProf},\mbox{tc\_fun}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oindi},\mbox{tc\_fun}(\mbox{tc\_prod}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt},\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_bool})))\qquad\mbox{cnf}(\mbox{cls\_unanimity\_\_def}_1,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_x},\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OProf},\mbox{tc\_fun}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oindi},\mbox{tc\_fun}(\mbox{tc\_prod}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt},\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_bool})))\mbox{ and }\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_Odictator}(\mbox{v\_F},\mbox{v\_i}) ) \ \Rightarrow \ \mbox{hAPP}(\mbox{v\_F},\mbox{v\_x}) = \mbox{hAPP}(\mbox{v\_x},\mbox{v\_i})\qquad\mbox{cnf}(\mbox{cls\_dictator\_\_def}_0,\mbox{axiom})$

$\mbox{hBOOL}(\mbox{hAPP}(\mbox{v\_S},\mbox{v\_x})) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_x},\mbox{v\_S},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_mem\_\_def}_1,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_x},\mbox{v\_S},\mbox{t\_a}) \ \Rightarrow \ \mbox{hBOOL}(\mbox{hAPP}(\mbox{v\_S},\mbox{v\_x}))\qquad\mbox{cnf}(\mbox{cls\_mem\_\_def}_0,\mbox{axiom})$

$\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OIIA}(\mbox{v\_F})\mbox{ or }\mbox{c\_in}(\mbox{v\_sko\_\_Arrow\_\_Order\_\_Mirabelle\_\_XIIA\_\_def\_}_3(\mbox{v\_F}),\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OProf},\mbox{tc\_fun}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oindi},\mbox{tc\_fun}(\mbox{tc\_prod}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt},\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_bool})))\qquad\mbox{cnf}(\mbox{cls\_IIA\_\_def}_5,\mbox{axiom})$

$\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_Odictator}(\mbox{v\_F},\mbox{v\_i})\mbox{ or }\mbox{c\_in}(\mbox{v\_sko\_\_Arrow\_\_Order\_\_Mirabelle\_\_Xdictator\_\_def\_}_1(\mbox{v\_F},\mbox{v\_i}),\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OProf},\mbox{tc\_fun}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oindi},\mbox{tc\_fun}(\mbox{tc\_prod}(\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt},\mbox{tc\_Arrow\_\_Order\_\_Mirabelle\_Oalt}),\mbox{tc\_bool})))\qquad\mbox{cnf}(\mbox{cls\_dictator\_\_def}_1,\mbox{axiom})$

$\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_OIIA}(\mbox{v\_F})\qquad\mbox{cnf}(\mbox{cls\_assms\_I3\_J}_0,\mbox{axiom})$

$\mbox{hAPP}(\mbox{v\_F},\mbox{v\_sko\_\_Arrow\_\_Order\_\_Mirabelle\_\_Xdictator\_\_def\_}_1(\mbox{v\_F},\mbox{v\_i})) = \mbox{hAPP}(\mbox{v\_sko\_\_Arrow\_\_Order\_\_Mirabelle\_\_Xdictator\_\_def\_}_1(\mbox{v\_F},\mbox{v\_i}),\mbox{v\_i}) \ \Rightarrow \ \mbox{c\_Arrow\_\_Order\_\_Mirabelle\_Odictator}(\mbox{v\_F},\mbox{v\_i})\qquad\mbox{cnf}(\mbox{cls\_dictator\_\_def}_2,\mbox{axiom})$

$\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_Ounanimity}(\mbox{v\_F})\qquad\mbox{cnf}(\mbox{cls\_u}_0,\mbox{axiom})$

$\neg\,\mbox{c\_Arrow\_\_Order\_\_Mirabelle\_Odictator}(\mbox{v\_F},\mbox{v\_x})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_fequal}(\mbox{v\_x},\mbox{v\_x},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_ATP\_\_Linkup\_Oequal\_\_imp\_\_fequal}_0,\mbox{axiom})$

$\mbox{c\_fequal}(\mbox{v\_X},\mbox{v\_Y},\mbox{t\_a}) \ \Rightarrow \ \mbox{v\_X} = \mbox{v\_Y}\qquad\mbox{cnf}(\mbox{cls\_ATP\_\_Linkup\_Ofequal\_\_imp\_\_equal}_0,\mbox{axiom})$

\medskip
\end{document}