1. Введение

Лейбница по праву считают отцом-основателем современной символической логики и теории вычислений; его проект универсальной характеристики является прототипом современных символических исчислений. На синтаксическом уровне все такие исчисления вслед за Лейбницем используют атомистический принцип построения: задается алфавит атомарных символов, из которых затем строятся слова и более сложные символические выражения; допустимые символические выражения далее преобразуются по определенным фиксированным правилам. Как этот атомистический принцип построения синтаксиса проявляется в семантике? Прямолинейный ответ на этот вопрос был дан в 1918 г. Расселом в его метафизической доктрине логического атомизма [Russell 1918]; другой вариант той же доктрины представлен в «Трактате» Витгенштейна [Wittgenstein 1921]. Согласно этой доктрине, «мир состоит из фактов, а не из вещей» (Витгенштейн), причем среди этих фактов есть атомарные и сложные, которые составлены из атомарных. Факты являются онтологическими коррелятами высказываний (пропозиций), которые в символической логике выражаются символами или комбинациями символов. Применительно к системе символической логики (которая при таком подходе предполагается единственной) доктрина логического атомизма утверждает, что ее символический синтаксис точно отражает универсальные онтологически фундированные формы мышления. Таким образом, эта метафизическая доктрина позволяет смотреть на атомистический принцип построения символического синтаксиса в логических исчислениях как на прямое отражение атомарной структуры бытия.

Разумеется, логический атомизм Рассела и Витгенштейна – это далеко не единственный способ философского осмысления символической логики. Я специально останавливаюсь здесь на этой доктрине, поскольку она тематизирует атомистический принцип построения символического синтаксиса. Однако помимо атомистического принципа в этой доктрине присутствует второй основополагающий элемент: интерпретация символического исчисления, построенного в духе универсальной характеристики Лейбница, именно как логического. Как я постараюсь показать, этот момент на самом деле более проблематичен, чем это может показаться на первый взгляд. Дело в том, что Лейбниц и многие его последователи, включая Грассмана и Пеано, строили свои символические исчисления, имея в виду не только логику и философию, но и современную им математику. В этом кругу идей логика всякий раз рассматривалась в тесной связи с такими математическими дисциплинами, как комбинаторика, арифметика, алгебра и геометрия. Вопрос о том, как именно соотносятся друг с другом логика и математика (и в частности, логика и геометрия) и где точно проходит граница между этими дисциплинами (и есть ли она вообще), в разных случаях решался по-разному. Этот, на первый взгляд, частный вопрос в начале XX в. стал одной из линий водораздела между рождающейся аналитической традицией в философии (которая в современном мире стала доминирующей) и неокантианской традицией. Как я покажу на примере современных исследований по гомотопической теории типов и унивалентных оснований математики, диалектическое столкновение логических, алгебраических и геометрических подходов к конструированию символических исчислений и созданию на этой базе новых языков программирования остается продуктивным и сегодня. В этой связи я укажу на геометрический аспект идеи универсальной характеристики Лейбница и укажу на роль этого аспекта в последующем развитии названной идеи. Наконец, следуя примеру Рассела и Витгенштейна, я сформулирую доктрину логико-геометрического атомизма, которая, на мой взгляд, более адекватна современной математизированной науке, чем доктрина логического атомизма в ее обычной форме.

2. Лейбниц

Говоря об универсальной характеристике Лейбница, нужно иметь в виду, что это в первую очередь визионерский проект, идея, для реализации которой ее автор сделал только самые первые шаги. Более точно нужно говорить о целом семействе тесно друг с другом связанных, и тем не менее различных проектов, для которых Лейбниц использовал такие названия, как универсальная математика (mathesis universalis), универсальная наука (scientia universalis), универсальный язык (lingua universalis), рациональное исчисление (calculus ratiocinatur), комбинаторное искусство (ars combinatoria), геометрическая характеристика (characteristica geometrica) и другие. Большая часть этого материала разбросана по письмам, наброскам и неоконченным фрагментам Лейбница, которые долгое время оставались и частично до сих пор остаются неизданными. Основными опубликованными источниками для изучения этой части наследия Лейбница по сегодняшний день служат издания [Leibniz 1849–1863] (особенно том 7) и [Leibniz 1875–1890] (особенно том 5), ставшие доступными широкому научному сообществу во второй половине XIX в.; новый архивный материал регулярно появляется в печати в продолжающемся академическом издании [Leibniz 1923–].

В самом общем виде идея универсальной характеристики Лейбница состоит в том, чтобы каким-то образом совместить следующие три вещи: 1) искусственный символический язык с прозрачной грамматикой, который мог бы применяться для описания понятий и предметов самых разных типов; 2) систему формальной логики с четкими правилами вывода (по примеру традиционной силлогистики); 3) символическое исчисление по типу арифметического или алгебраического, которое позволило бы решать самые разнообразные проблемы, и в частности, делать логические выводы в режиме вычисления, то есть с помощью манипуляций с символами по определенным правилам. Оставляя сейчас в стороне 1) и 2), я скажу только несколько слов о 3). Современная Лейбницу алгебра – это символическое исчисление, впервые представленное Декартом в его «Геометрии» (см.: [Декарт 1938]) и затем незначительно модернизированное ближайшими последователями Декарта. Однако в области алгебры сам Лейбниц пошел гораздо дальше Декарта и его последователей, во-первых, создав свой алгебраический вариант дифференциального и интегрального исчисления и, во-вторых, предприняв попытку более глубокой «алгебраизации» геометрии, которая в дальнейшем привела, в частности, к возникновению новой математической дисциплины топологии. Сам Лейбниц использовал для этой новой теории название «анализ положения» (analysis situs), а соответствующее символическое исчисление называл «геометрической характеристикой». Критикуя алгебру (= аналитическую геометрию) Декарта, Лейбниц указывает на то, что это символическое исчисление отражает только метрические отношения между элементами геометрических построений, но не принимает в расчет взаимное расположение этих элементов, то есть те отношения, которые мы сегодня называем топологическими. Проект геометрической характеристики Лейбница направлен на то, чтобы исправить этот недостаток [Risi 2007].

Какое место занимают идеи универсальной и геометрической характеристики Лейбница в системе его философии вообще и метафизики в частности? Как мы сейчас увидим, ответ на этот вопрос не очевиден.

3. Борьба интерпретаций

В первые годы XX в. вопрос об интерпретации логических и математических текстов и фрагментов Лейбница стал предметом спора между Бертраном Расселом [Russell 1900] и Луи Кутюра [Couturat 1901] с одной стороны и Эрнстом Кассирером [Cassirer 1902] – с другой[1]. Этот спор не был чисто историческим: каждая из партий использовала наследие Лейбница для того, чтобы обосновать собственную философскую позицию. Рассел и Кутюра приписывают Лейбницу точку зрения логического атомизма (сформулированную Расселом в явном виде значительно позже [Russell 1918]), тогда как Кассирер (так же как немного позже Бронсвик [Brunschvicg 1912]) видит в Лейбнице прямого предшественника Канта и вслед за Германом Когеном [Cohen 1883] указывает на ключевую роль дифференциального и интегрального исчисления не только в математической, но и в философской мысли Лейбница. Если Рассел и Кутюра видят в логике Лейбница ключ к пониманию его метафизики, то Кассирер связывает метафизику Лейбница в первую очередь с его работами в области физической динамики. Основное возражение Кассирера Расселу (которое он делает и в других контекстах независимо от вопроса об интерпретации работ Лейбница [Cassirer 1907]) состоит в том, что формальная логика сама по себе не дает никакого ответа на вопрос о том, как и почему математические методы оказываются применимыми в физике. Вслед за Кантом Кассирер видит решение этой проблемы в указании на синтетический (в противоположность аналитическому) характер математических суждений и находит у Лейбница релевантное понятие синтетического отношения [Cassirer 1902, 534]. Рассел строит свою критику Кассирера на том тезисе, что развитие математики в XIX в., и в частности, открытие неевклидовых геометрий, убедительно показало ошибочность кантианской философии. Этот факт с точки зрения Рассела полностью дисквалифицирует интерпретацию Лейбница Кассирером. Свою рецензию Рассел завершает такими словами: «Почти все критические аргументы, представленные в этой рецензии, – это аргументы против самой кантианской философии. Сторонники этой философии найдут в книге доктора Кассирера именно то, что им нужно» [Russell 1903^b, 201]. Как мы видим, из своего ангажированного отношения к наследию Лейбница Рассел не делает секрета.

Таким образом, наследие Лейбница стало полем интеллектуального соперничества между двумя важнейшими направлениями европейской философии XX в.: неокантианской традицией, представленной Кассирером (и Бронсвиком, если считать его главу о философии Лейбница в [Brunschvicg 1912] продолжением той же дискуссии), и аналитической традицией, представленной молодым Расселом. В Европе первого десятилетия XX в. неокантианская традиция была уже прочно установленной, тогда как аналитическая философия еще не существовала в виде особой школы или традиции. Описанный выше эпизод принадлежит к самой ранней истории аналитической философии и является одним из моментов становления этой философской традиции. В наши дни ситуация перевернулась: аналитическая традиция оказалась доминирующей (по крайней мере, в философии математики и логике), тогда как неокантианская традиция стала в основном предметом исторических исследований и практически исчезла из поля зрения тех современных философов, которые, подобно Расселу и Кассиреру, продолжают сегодня работать в контексте новейших достижений науки, включая новую математику, математическую логику и математическую физику. Не ставя целью систематическую реабилитацию неокантианской философии науки, я постараюсь далее показать, что те аспекты философии и математики Лейбница, которые подчеркивал Кассирер и которыми, напротив, сознательно пренебрегал Рассел, действительно остаются релевантными новейшим исследованиям в области математической логики и вычислительной математики.

Что же касается отношения метафизики Лейбница к его логическим и математическим работам, то менее философски ангажированные и более исторически ориентированные исследования последних лет [Mercer 2001; Wilson 2008] показывают нам более сложную и запутанную картину, чем исследования Кутюра, Рассела и Кассирера. В частности, становится ясно, что сложные отношения Лейбница с философией атомизма, с которой Лейбниц был знаком по поэме Лукреция и работам Гассенди [Wilson 2007; Wilson 2008], не имеют никакой прямой связи с логическим атомизмом в смысле Рассела и Витгенштейна[2]. Помимо логических, математических и физических идей Лейбница, которые прочно вошли в анналы истории современной науки, его метафизика связана с рядом философских сюжетов, которые сейчас представляют только исторический интерес и адекватное понимание которых требует большой и скрупулезной исторической работы. Не ставя под вопрос ценность такого рода исторического знания, я далее в этой статье буду говорить только об «актуальной истории» идей Лейбница, то есть об истории только тех идей, адекватность которых современной науке я могу показать и обосновать. Более конкретно речь пойдет об идее геометрической характеристики, которой Рассел не придавал специального значения (хотя Кутюра описал ее достаточно подробно [Couturat 1901]), а Кассирер, напротив, считал ключевым элементом логико-математического инструментария Лейбница [Cassirer 1902, 142 ff].

4. Братья Грассманы и Пеано

В 1844 г. общество князя Яблоновского в Лейпциге объявило денежную премию, претенденты на которую должны были в современной форме изложить идею геометрической характеристики Лейбница или представить новый вариант подобного исчисления [Heath 1917, 37; Грассман, Грассман 2008, 466]. В 1846 г. эта премия была вручена Герману Грассману за эссе [Grassmann 1847], специально написанное для этого случая. Эта работа Грассмана, как и более систематические представления авторского учения о протяжении (Ausdehnungslehre), не получили признания при его жизни (за исключением упомянутой премии). Большинство историков объясняет это необычным для того времени способом изложения математических результатов, в котором важную роль играли философские аргументы, мотивирующие последующие математические выкладки [Lewis 1977]. Грассман показывает, что геометрическое исчисление, которое он развил независимым образом в рамках своего учения о протяжении, можно рассматривать как реализацию идеи геометрической характеристики Лейбница, которую сам Лейбниц смог технически реализовать только в очень незначительной степени. В 1872 г. брат Германа Грассмана Роберт опубликовал свое учение о форме, в работе над которым Герман также принимал активное участие [Грассман, Грассман 2008]. В этой работе братья Грассманы развивают общую систему формальных наук, в которой учение о протяжении соседствует с логикой (учением о понятиях). Более подробно эта система устроена так. Фундаментальной формальной дисциплиной, результатами которой пользуются все прочие формальные дисциплины, является учение о величинах представляющее собой вариант общей символической алгебры. Специальные варианты этой общей алгебры используются далее в логике, арифметике, комбинаторике, и наконец, в грассмановском учении о протяжении (которое можно назвать в широком смысле слова геометрическим). Такое соотношение между алгеброй, логикой, арифметикой и геометрией представляется очень необычным (чтобы не сказать некорректным или даже нелепым) с точки зрения основных программ философской логики и оснований математики XX в. Я думаю, что именно этим можно объяснить тот факт, на который указывает отечественный исследователь творчества братьев Грассманов Б.В. Бирюков [Грассман, Грассман 2008], что логическое наследие Грассманов до сих пор оставалось вне внимания историков и философов. Как я постараюсь показать ниже, новейшие результаты в математической логике и связанных с логикой областях математики дают повод для переоценки вклада братьев Грассманов в логику.

В 1888 г. Джузеппе Пеано опубликовал свой модернизированный вариант грассмановского исчисления, дополнив его логическим исчислением высказываний [Peano 1888]. Роль исчисления высказываний в этой теоретической конструкции мне не кажется вполне ясной, однако в предисловии к этой работе Пеано замечает, что «операции дедуктивной логики совершенно аналогичны алгебраическим операциям и операциям геометрического исчисления» и что используемая в логической части нотация в дальнейшем используется в геометрической части. Чтобы лучше понять, каким образом Пеано представлял себе взаимосвязь между логикой, алгеброй, геометрией и символическими вычислениями, нужно также принять во внимание его проект математического Формуляра (Formulario), которым Пеано начал заниматься в том же 1888 г. и который в последующие годы стал главной целью всей его научной работы [Rroero 2011]. Формуляр Пеано представляет собой универсальную энциклопедию математических знаний, в которой все математические результаты представлены с помощью специального формального символического языка; как указывает сам Пеано, этот проект имеет много общего с лейбницевской идеей универсальной характеристики. В качестве языка Формуляра Пеано использует собственное символическое исчисление, ранний вариант которого мы находим в упомянутой выше работе 1888 г., посвященной Грассману. На издание Формуляра 1895 г. многократно ссылается Рассел в «Принципах математики» 1903 г., утверждая при этом, что он прямо следует «методу профессора Пеано» [Russell 1903^а, xvi]. Пеано, со своей стороны, видит между своим подходом и подходом Рассела существенные различия [Rroero 2011]. Ответ на вопрос о том, был ли у Пеано какой-то определенный альтернативный взгляд на отношения между логикой и математикой, который остался вне поля зрения Рассела, Гильберта, Геделя и других лидеров логики XX в., мне не представляется очевидным и требует дополнительного исторического исследования. Тем не менее ясно, что тот геометрический контекст, в котором логическое исчисление Пеано впервые появляется в работе 1888 г., в дальнейших дискуссиях о формализации и логических основаниях математики в XX в. не играет никакой специальной роли. Я подчеркиваю здесь это обстоятельство, поскольку, как мы сейчас увидим, аналогичный геометрический контекст, по всей видимости, играет ключевую роль в новом перспективном логическом исчислении, построенном уже в XXI в. Это позволяет предположить, что геометрия и логика на самом деле связаны друг с другом более тесным образом, чем об этом сегодня обычно принято думать.

5. Унивалентные основания

Унивалентные основания математики (УО) – это продолжающийся исследовательский проект, суть которого состоит в построении новых аксиоматических оснований математики с помощью гомотопической теории типов (ГТТ). Эти новые основания в отличие от оснований, построенных с помощью стандартных логических методов, допускают непосредственную реализацию в виде программного кода и таким образом ближе подходят к той цели, к которой стремился Лейбниц.

Впервые идея УО было сформулирована Владимиром Воеводским [Voevodsky 2006]; в 2012–2013 гг. Принстонский институт высших исследований финансировал специальную программу, направленную на развитие этой идеи, в которой, помимо Воеводского, участвовал большой международный коллектив математиков. Результаты этой работы представлены в коллективной монографии [Homotopy 2013], в которой основные идеи и математические принципы УО изложены систематически. Формальным скелетом УО является конструктивная теория типов, построенная Пером Мартином-Лёфом в последние десятилетия XX в. [Martin-Löf 1984]. ГТТ является интерпретацией теории типов Мартина-Лёфа (ТТМЛ) с помощью геометрической (в широком смысле слова «геометрический») теории гомотопии, которая является важной частью современной алгебраической топологии. Не имея сейчас возможности входить в математические детали, я только неформально опишу соотношение между логическим и геометрическим аспектами ГТТ, которое делает эту теорию непохожей на другие аксиоматические геометрические теории, построенные в XX в.

Классический пример современной аксиоматической теории был дан Гильбертом [Hilbert 1899]; по той же схеме, но более формальным образом (с использованием средств символической логики) построена аксиоматическая теория множеств Цермело – Френкеля [Fraenkel, Bar-Hillel 1958], которая до сих пор играет роль «официального» основания математики. Идея такого рода аксиоматизации состоит в следующем. Используется некоторое логическое исчисление (обычно классическое исчисление предикатов первого порядка), затем вводятся некоторые нелогические константы (в теории Цермело – Френкеля эту роль играет символ 2 обозначающий отношение принадлежности), с помощью которых записываются аксиомы, то есть синтаксически корректные комбинации символов, которые при стандартной семантической интерпретации символов интерпретируются как содержательные истинные высказывания. Список аксиом теории порождает новые высказывания (теоремы) в соответствии с правилами вывода, которые являются частью спецификации данного логического исчисления.

Я хочу обратить здесь внимание на следующий момент. Различение логических и нелогических констант, как правило, делается непосредственно при описании синтаксиса теории – несмотря на то, что по своему смыслу это различение имеет семантический характер. После введения системы формальных аксиом рассматриваются различные интерпретации только нелогического словаря. Именно такие интерпретации порождают различные модели данной теории. Например, в Гильбертовых аксиомах для евклидовой геометрии формальный термин «точка» можно интерпретировать либо как обычную геометрическую точку Евклидова пространства, либо как пару чисел; в последнем случае мы получаем (если также подходящим образом интерпретируем все необходимые геометрические отношения) арифметическую модель евклидовой геометрии. Семантика логического словаря при таком подходе обычно предполагается фиксированной заранее. Вопрос об альтернативных семантиках (моделях) одного и того же логического исчисления, хотя и ставился в различных разделах логики по крайней мере с 1930-х гг. [Tarski 1956], но до самых недавних пор, насколько мне известно, никогда не рассматривался в контексте формализации и аксиоматизации конкретных содержательных теорий.

Итак, стратегия формализации, которую использовал Гильберт и которая в XX в. стала общепринятой [Tarski 1941], состоит в том, чтобы сначала определиться с логикой (задав ее синтаксис и семантику), а уже затем использовать эту формальную логическую систему для формализации и аксиоматизации различных содержательных теорий и дальнейшего изучения различных моделей этих теорий. Эта стратегия отражает фундаментальную эпистемологическую предпосылку, согласно которой логика эпистемологически первична по отношению к любым теориям, поскольку все формализованные теории «используют» логику, то есть содержат какое-то логическое исчисление. Хотя этот взгляд на логику в XX в. иногда ставился под вопрос (например, Патнэмом в его дискуссии с Даммитом о природе квантовой логики [Putnam 1968; Dummett 1976]), альтернативные эпистемологические подходы до последнего времени не имели в своем распоряжении никаких специальных формальных средств, которые могли бы составить конкуренцию стандартному подходу. Я считаю, что ГТТ представляет собой средство как раз такого рода. Дело в том, что содержательная теория гомотопий нетривиальным образом интерпретирует ТТМЛ даже без добавления к этой последней теории новых аксиом (таких как аксиома унивалентности, которую ввел Воеводский). Таким образом, ГТТ представляет собой особого рода логико-геометрическую теорию, где одни и те же символы, символические выражения и синтаксические операции с этими выражениями имеют как геометрическую, так и логическую интерпретацию. Аксиома унивалентности была первоначально мотивирована геометрически, но она также имеет и прозрачный логический смысл (обобщение принципа пропозициональной экстенсиональности Черча). Получается, что в ГТТ стандартное различение между логической формой и геометрическим содержанием не срабатывает, поскольку сама логическая форма этой теории имеет геометрическую природу. Такое положение вещей вряд ли можно назвать совсем уж неожиданным, если учесть, что понятие формы играет в традиционной геометрии по крайней мере такую же важную роль, как и в традиционной логике. Эффект неожиданности связан скорее с тем, что стандартный логический анализ геометрии, начало которому в XX в. положили указанные выше классические труды Гильберта и Тарского, сделал понятие геометрической формы (отличной от логической формы, с одной стороны, и геометрического содержания, с другой стороны) по видимости излишним. ГТТ/УО позволяет нам утверждать, что этот стандартный анализ является слишком грубым и в этом смысле неадекватным.

Между подходом Воеводского и геометрической линией развития идеи характеристики Лейбница у Грассмана и Пеано, о которой мы говорили выше, существует очевидная понятийная связь: во всех этих случаях речь идет о формальном символическом исчислении, семантика которого включает в себя как логический, так и геометрический аспект. Более подробное изучение этого вопроса, конечно, требует дальнейшего исследования. Интерпретация Расселом идей Лейбница в терминах логического атомизма, о которой мы говорили выше, может оказаться для этого полезной. Используя такую интерпретацию, необходимо также учесть аргументы Кассирера [Cassirer 1902] и принять также во внимание геометрический аспект проблемы. «Атомы» ГТТ – это гомотопические типы[3], которые с геометрической точки зрения можно описать как топологические пространства, определенные с точностью до гомотопической эквивалентности. Гомотопические типы имеют также более конкретные геометрические реализации. Рабочая модель гомотопического типа, которую Воеводский использовал на начальном этапе своих исследований, это симплициальное множество. Симплициальное множество – это обобщенный симплициальный комплекс, который уже нетрудно себе представить, пользуясь понятиями элементарной геометрии. Это геометрическая конструкция, построенная (в соответствии с простыми и интуитивно прозрачными правилами, на которых я не буду останавливаться) из симплексов, элементарными примерами которых служат точка, отрезок, треугольник и тетраэдр.

Тот факт, что ГТТ также является не только геометрическим, но логическим исчислением (постольку, поскольку так можно охарактеризовать ТТМЛ, понимая термин «логический» достаточно широко), позволяет рассматривать атомы (то есть примитивные термины) этой теории в качестве исходного материала для построения самых различных математических (и, говоря более обще, математизированных) теорий. Принимая во внимание то, каким образом математические методы используются сегодня в физике и других естественных науках, можно ожидать, что геометрическая форма ГТТ позволит более успешно применять это исчисление в математизированных естественных науках, чем стандартные формально-логические методы. Важно также отметить, что, в отличие от большинства логических методов, ГТТ допускает непосредственную компьютерную реализацию (в частности, в виде программных продуктов COQ и AGDA), что позволяет думать о применении этой теории в современных информационных технологиях представления знаний. Насколько таким надеждам суждено оправдаться, покажет дальнейшая работа в этих направлениях. Но уже сегодня можно с уверенностью утверждать, что старая идея Лейбница за три с лишним века еще далеко не исчерпала своего потенциала.

Источники – Primary Sources in Russian

Грассман, Грассман 2008 – Грассман Г., Грассман Р. Логика и философия математики. Избранное. Перевод и комментарии Б.В. Бирюкова. М.: Наука, 2008 (Grassmann H., Grassmann R. Selected Works. Translation and Commentary by B. Biryukov. 2008).

Декарт 1938 – Декарт Р. Геометрия. М.: Гостехиздат, 1938 (Descartes. La Géométrie. Russian Translation 1938).

Primary Sources

Leibniz 1849–1863 – Leibnizes mathematische Schriften. C.I. Gerhardt (ed.). Berlin; Halle: A. Asher & Co, 1849–1863.

Leibniz 1875–1890 – Die Philosophischen Schriften von G.W. Leibniz. C.I. Gerhardt (ed.). 7 Bd. Berlin: Weidmannsche Buchhandlung, 1875–1890.

Leibniz 1923– – Leibniz G.W. Sämtliche Schriften und Briefe. Berlin: Akademie-Verlag, 1923–.

References

Brunschvicg 1912 – Brunschvicg L. Les étapes de la philosophie mathématique. Paris: Félix Alcan, 1912.

Cassirer 1902 – Cassirer Е. Leibniz’ System in seinen wissenschaftlichen Grundlagen. Marburg: Elwert, 1902.

Cassirer 1907 – Cassirer Е. Kant und die moderne Mathematik // Kant-Studien. 1907. H. 12. Р. 1–40.

Cohen 1883 – Cohen H. Das Prinzip der Infinitesimalmethode und seine Geschichte: ein Kapitel zur Grundlegung der Erkenntniskritik. Berlin: Dümmler, 1883.

Couturat 1901 – Couturat L. La Logique de Leibniz. D’après des documents inédits. Paris: Félix Alcan, 1901.

Couturat 1903 – Couturat L. Opuscules et fragments inédits de Leibniz. Paris: Félix Alcan, 1903.

Dummett 1976 – Dummett M. Is logic empirical? / H.D. Lewis (ed.). Contemporary British Philosophy. 4th series. London: Allen and Unwin, 1976. Р. 45–68.

Fraenkel, Bar-Hillel 1958 – Fraenkel A., Bar-Hillel I. Foundations of Set Theory. Amsterdam: North-Holland, 1958.

Grassmann 1847 – Grassmann H. Geometrische Analyse, geknüpft an die von Leibniz erfundene geometrische Charakteristik. Leipzig: Weidmann, 1847.

Heath 1917 – Heath A.E. The geometrical analysis of Grassmann and its connection with Leibniz’s Characteristic // Monist. 27–1 (1917). P. 36–56.

Hilbert 1899 – Hilbert D. Grundlagen der Geometrie. Leipzig: Teubner, 1899.

Homotopy 2013 – Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (Princeton). http://homotopytypetheory.org/book/, 2013.

Ishiguro 1990 – Ishiguro H. Leibniz’s Philosophy of Logic and Language. Cambridge: Cambridge University Press, 1990.

Lewis 1977 – Lewis A.С. H. Grassmann’s 1844 Ausdehnungslehre and Schleiermacher’s Dialektik // Annals of Science. 34(2) (1977). Р. 103–162.

Marquis 2009 – Marquis J.-P. From a Geometrical Point of View: A Study of the History and Philosophy of Category Theory. Berlin et al.: Springer, 2009.

Marquis 2010 – Marquis J.-P. Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics // Synthese 190(12) (2010). Р. 2141–2164.

Martin-Löf 1984 – Martin-Löf P. Intuitionistic Type Theory (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli: BIBLIOPOLIS, 1984.

Mercer 2001 – Mercer C. Leibniz’s Metaphysics: Its Origins and Development. Cambridge: Cambridge University Press, 2001.

Peano 1888 – Peano G. Calcolo Geometrico secondo l’Ausdehnungslehre di H. Grassmann, preceduto dale operazioni della logica deduttiva. Torino: Fratelli Bocca Editori, 1888.

Putnam 1968 – Putnam H. Is logic empirical? / R. Cohen, M. Wartofsky (eds.) Logical and Epistemological Studies in Contemporary Physics (Boston Studies in the Philosophy of Science XII). Boston; Dordrecht: D. Reidel, 1968. Р. 216–241.

Rabouin 2012 – Rabouin D. Interpretations of Leibniz’s Mathesis Universalis at the beginning of the XX-th century / R. Krömer and Y. Chin-Drian (eds.), New Essays on Leibniz Reception in Science and Philosophy of Science in 1800–2000. Berlin et al.: Springer, 2012. Р. 187–202.

Risi 2007 – Risi V. de. Geometry and Monadology: Leibniz’s Analysis Situs and Philosophy of Space. Basel; Boston; Berlin: Birkhäuser, 2007.

Rroero 2011 – Rroero C.S. The formulario between mathematics and history / F. Skof (ed.) Giuseppe Peano between Mathematics and Logic, Proceeding of the International Conference in honour of Giuseppe Peano on the 150^th anniversary of his birth and the centennial of the Formulario Mathematico, Turin (Italy), 2008. Berlin et al.: Springer, 2011. Р. 83–134.

Russell 1900 – Russell B. A Critical Exposition of the Philosophy of Leibniz. London: Allen and Unwin, 1900.

Russell 1903^b – Russell B. Recent work on the philosophy of Leibniz // Mind (New Series).12(46) (1903). Р. 177–201.

Russell 1903^а – Russell B. Principles of Mathematics. London: Allen and Unwin, 1903.

Russell 1918 – Russell B. The philosophy of logical atomism // The Monist 28 (1918) Р. 495–527.

Tarski 1941 – Tarski A. Introduction to Logic and to the Methodology of Deductive Sciences. Oxford: Oxford University Press, 1941.

Tarski 1956 – Tarski A. Sentential calculus and topology. Logic, Semantics, Metamathematics: Papers from 1923 to 1938 translated by J.H. Woodger. Oxford: Clarendon Press, 1956. Р. 421–454.

Voevodsky 2006 – Voevodsky V. A very short note on the homotopy lambda-calculus [2006]. Unpublished.

Wilson 2007 – Wilson C. Two opponents of material atomism: Cavendish and Leibniz / P. Phemister and S. Brown (eds.). Leibniz and the English-Speaking World. Berlin et al.: Springer, 2007. P. 35–50.

Wilson 2008 – Wilson C. Epicureanism at the Origins of Modernity. Oxford: Oxford University Press, 2008.

Wittgenstein 1921 – Wittgenstein L. Logisch-Philosophische Abhandlung. Leipzig: Unesma, 1921.