\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{Hegel's "Logic" as Modal Type Theory} \begin{quote}% under construction \end{quote} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{philosophy}{}\paragraph*{{Philosophy}}\label{philosophy} [[!include philosophy - contents]] \hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations} [[!include foundations - contents]] \hypertarget{physics}{}\paragraph*{{Physics}}\label{physics} [[!include physicscontents]] \textbf{Abstract} While [[analytic philosophy]] famously rejected the speculative [[metaphysics]] of [[Hegel]] in favor of the analysis of concepts by means of [[mathematical logic]], in particular [[predicate logic]], recent developments in the [[foundations of mathematics]] via [[homotopy type theory]] offer a way to re-read [[Hegel]] as having useful formal meaning not in [[predicate logic]], but in `[[modal type theory]]'. The essence of this suggestion has been made by [[Lawvere]] [[Some Thoughts on the Future of Category Theory|in 1991]], which however remains largely unnoticed. Here we aim to give a transparent account of this perspective both [[philosophy|philosophically]] as well as [[category theory|category-theoretically]]. We then further expand on Lawvere's formalization of Hegel's ``[[Science of Logic]]'' in terms of the [[categorical semantics]] given by [[cohesive (infinity,1)-topos|cohesive higher toposes]]. We discuss how there is a \emph{useful} formalization of a fair bit of modern fundamental [[physics]], in fact of [[local quantum field theory|local]] [[gauge field theory|gauge]] [[quantum field theory]], to be found here. \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{introduction}{Introduction}\dotfill \pageref*{introduction} \linebreak \noindent\hyperlink{modern_foundations__types_judgements_and_deduction}{Modern foundations -- Types, Judgements and Deduction}\dotfill \pageref*{modern_foundations__types_judgements_and_deduction} \linebreak \noindent\hyperlink{categorical_semantics_and_categorical_logic}{Categorical semantics and Categorical logic}\dotfill \pageref*{categorical_semantics_and_categorical_logic} \linebreak \noindent\hyperlink{modalities_moments_and_opposites}{Modalities, moments and opposites}\dotfill \pageref*{modalities_moments_and_opposites} \linebreak \noindent\hyperlink{formal_determinations_of_being}{Formal determinations of Being}\dotfill \pageref*{formal_determinations_of_being} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{introduction}{}\subsection*{{Introduction}}\label{introduction} With the rise of [[analytic philosophy]] in Britain, and its adoption and development of the new logic forged by [[Frege]] and [[Peano]], there came a radical rejection of the existing philosophical paradigm, the [[idealism]] of [[T. H. Green]] and [[F. H. Bradley]], and those considered to have provided its primary source, notably [[Hegel]]. [[Bertrand Russell]] was adamant that the new logic would thoroughly transform philosophy, as he made clear at the end of his chapter \emph{Logic As The Essence Of Philosophy}: \begin{quote}% The old logic put thought in fetters, while the new logic gives it wings. It has, in my opinion, introduced the same kind of advance into philosophy as Galileo introduced into physics, making it possible at last to see what kinds of problems may be capable of solution, and what kinds are beyond human powers. And where a solution appears possible, the new logic provides a method which enables us to obtain results that do not merely embody personal idiosyncrasies, but must command the assent of all who are competent to form an opinion. (Logic As The Essence Of Philosophy, 1914) \end{quote} In the same chapter, Hegel was taken to task for his attempt to widen logic to a form of [[metaphysics]]. Much of it appears to Russell to result from muddled thinking, for instance, a failure to distinguish the `is' of predication from the `is' of identity. This set the tone for analytic philosophy's opinion of Hegel for several decades. In 1951, the logical empiricist [[Hans Reichenbach]] wrote \begin{quote}% Hegel has been called the successor of Kant; that is a serious misunderstanding of Kant and an unjustified elevation of Hegel. Kant's system, though proved untenable by later developments, was the attempt of a great mind to establish rationalism on a scientific basis. Hegel's system is the poor construction of a fanatic who has seen one empirical truth and attempts to make it a logical law within the most unscientific of all logics. Whereas Kant's system marks the peak of the historical line of rationalism, Hegel's system belongs in the period of decay of speculative philosophy which characterizes the nineteenth century. (Reichenbach 1951, p. 72) \end{quote} However, despite the initial lengthy rejection of Hegelian ideas by analytic philosophy, there have recently been increasing signs of a willingness to re-engage with Hegel's writings, in particular on the part of [[John MacDowell]] and [[Robert Brandom]] (Redding, 2007). Interestingly, one feature of analytic philosophy which needs reconsidering according to Redding is the primacy of [[first-order logic|first-order]] predicate logic, not, however, that he is promoting an alternative formalization based on Hegel's ideas. It took a mathematician [[William Lawvere]] to find something formalizable of value in Hegel's \emph{Logic}, in particular the concept of a `[[unity of opposites|Unity of Opposites]]'. In this paper, taking our lead from Lawvere in seeing common elements between [[categorical logic]] and Hegel's logic, we will pursue this connection right up to [[modal type theory|modal]] forms of [[homotopy type theory]]. Now, Hegel's understanding of the term `Logik' was much broader than is normally the case. Indeed, the `Objective logic' of [[Science of Logic]] is more akin to a kind of [[metaphysics]]. While the [[Vienna Circle]], admirers of Russell, had adopted the [[positivism|positivist]] attitude towards [[metaphysics]], dismissing it as meaningless (\hyperlink{Carnap32}{Carnap 32}), later in the twentieth century there was a resurgence of analytic metaphysics. One important source of this resurgence was the rise of [[modal logic]] as a tool for philosophy, especially due to [[Saul Kripke]] in \emph{Naming and Necessity}. If the necessity of a proposition consists in its holding in all neighboring possible worlds, sense had to be made of these possible worlds. To what would have been Carnap's amazement, philosophers such as David Lewis proposed the reality of all possible worlds, the actual world being in no way special, except for its being our world. Today, standard topics for analytic metaphysics today include causality, necessity, space and time, identity, and mental states. Little attention is paid to the question of explaining the kind of physical principles which operate in our universe. It is noteworthy, however, that the need for some such questioning seems to be as strongly felt among modern physicists as it must have been to Hegel and his predecessors, as witnessed by \ldots{} debates such as critically reviewed in (\hyperlink{Albert12}{Albert 12}). (\ldots{}) Attempts to re-install this kind of metaphysics are these days undertaken by [[particle physics|particle physicists]] and [[cosmology|cosmologists]] themselves, whose success at formally describing remote aspects of the [[observable universe]] has emboldened many to feel as superior to modern philosophy as modern philosophy typically feels towards Hegel' idealism. (\ldots{}) \hypertarget{modern_foundations__types_judgements_and_deduction}{}\subsection*{{Modern foundations -- Types, Judgements and Deduction}}\label{modern_foundations__types_judgements_and_deduction} (\ldots{}) something like: analytic philosophy was certainly right to ask for a formal basis of philosophical reasoning, in order to make genuine intellectual progress possible. Back then [[predicate logic]] and [[set theory]] was the state of the art concerning the [[foundations of mathematics]] and so this is what analytic philosophy adopted and developed. But since then there has been much progress in the foundations of maths. \ldots{} [[intuitionistic type theory]] \ldots{} [[homotopy type theory]]\ldots{} Accordingly, the original starting point of analytic philosophy needs to be re-examined. While predicate logic has no way of making formal sense of Hegel's ``Logic'', for type theory the situation is rather different\ldots{} \hypertarget{categorical_semantics_and_categorical_logic}{}\subsection*{{Categorical semantics and Categorical logic}}\label{categorical_semantics_and_categorical_logic} \ldots{} type theory proper is a formal system for symbol manipulation \ldots{} useful for computer encoding, and much more readable than full formalization in, say, ZFC, but still not really what a discussion such as our here would directly work with\ldots{} \ldots{} instead, the [[syntax]] of type theory has [[semantics]] in [[categories]] -- [[categorical semantics]] \ldots{} [[relation between category theory and type theory]] -- and this semantic level is what we will be concerned with here \ldots{} originates with Lawvere's thesis, see also ``[[Adjointness in Foundations]]'' \hypertarget{modalities_moments_and_opposites}{}\subsection*{{Modalities, moments and opposites}}\label{modalities_moments_and_opposites} (\ldots{} basics of [[modalities]], [[modal operators]], [[monads]], leading up to [[adjoint modality]]/[[unity of opposites]]\ldots{}) \hypertarget{formal_determinations_of_being}{}\subsection*{{Formal determinations of Being}}\label{formal_determinations_of_being} \ldots{} using this and building on Lawvere's lead, we are led to objectively investigate the following: starting with bare homotopy type theory and adding [[adjoint modalities]] to it, what is the nature of the new propositions that can be proven with these modalities, hence what is the new ``quality'' of the types in the presence of these new axioms\ldots{} \ldots{} \begin{displaymath} \itexarray{ reines\;Sein && Dasein && Realitaet \\ being && existence && reality \\ pure being && determinate being \\ \\ && && \Re \\ && && \bot \\ && \int & \subset & \Im \\ && \bot && \bot \\ \emptyset &\subset& \flat & \subset & \& \\ \bot & & \bot && \\ \ast & \subset& \sharp } \end{displaymath} \begin{tabular}{l|l} symbol&$\;\;$ name\\ \hline $\int$&[[shape modality]]\\ $\flat$&[[flat modality]]\\ $\sharp$&[[sharp modality]]\\ $\Re$&[[reduction modality]]\\ $\Im$&[[infinitesimal shape modality]]\\ $\&$&[[infinitesimal flat modality]]\\ \end{tabular} (\ldots{}) \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[Rudolf Carnap]], \emph{\"U{}berwindung der Metaphysik durch logische Analyse der Sprache}, Erkenntnis Vol II (1932). Translated by A. Pap as \emph{The Elimination of Metaphysics Through Logical Analysis of Language} (\href{http://www.calstatela.edu/sites/default/files/dept/phil/pdf/res/Carnap-Elimination-of-Metaphysics.pdf}{pdf}) \item [[Georg Hegel]], \emph{[[Science of Logic]]} (1812) \item [[William Lawvere]], \emph{[[Some Thoughts on the Future of Category Theory]]} (1991) \item [[William Lawvere]] \emph{[[Cohesive Toposes and Cantor's ``lauter Einsen'']]} (1994) \item [[William Lawvere]] \emph{[[Unity and Identity of Opposites in Calculus and Physics]]} (1996) \item [[Higher toposes of laws of motion]] \item [[schreiber:Homotopy-type semantics for quantization]] \item Paul Redding, \emph{Analytic Philosophy and the Return of Hegelian Thought}, Cambridge University Press, 2007 (\href{http://ndpr.nd.edu/news/23465-analytic-philosophy-and-the-return-of-hegelian-thought/}{review} by Willem A. deVries) \item [[Bertrand Russell]], `Logic As The Essence Of Philosophy', chap. 2 of \emph{Our Knowledge of the External World}, (1914) \item [[Hans Reichenbach]], `The Rise of Scientific Philosophy', 1951. \item [[David Albert]], \emph{On the Origin of Everything}, book review of ``A Universe From Nothing'', by Lawrence M. Krauss, in the New York Times from March 25, 2012, on page BR20 of the \emph{Sunday Book Review} (\href{http://www.nytimes.com/2012/03/25/books/review/a-universe-from-nothing-by-lawrence-m-krauss.html?}{web}) \end{itemize} [[!redirects Lawverian formalization of Hegelian metaphysics]] \end{document}