3. Всякий фермер, имеющий осла, счастлив,
4. ∀x (Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Happy(x)),
но по сути ближе всего следующая формализация:
5. ∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, y)),
содержащая свободное вхождение y. Эванс предлагает, что, поскольку местоимения отсылают нас к объекту, они должны интерпретироваться как определенные описания; а если местоимение встречается во второй части условного предложения, дескриптивные условия определяются антецедентом. Такие рассуждения приводят нас к следующей интерпретации фразы (1), в духе Е-анализа:
∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, ιy ( Donkey(y) ∧ Owns(x, y)))
(ιx – это оператор определенного описания). Проблема здесь состоит в том, что в стандартном анализе оператор определенного описания подразумевает единственность объекта, то есть предложение (5) будет ложным в том случае, если у фермера больше одного осла. Один из возможных выходов – это ввести новый оператор, whe (whoever, whatever), работающий как обобщающий квантор [Neale, 1991]:
∀x ((Farmer(x) ∧ ∃y (Donkey(y) ∧ Owns(x, y)) → Beats(x, whe y (Donkey(y) ∧ Owns(x, y)))
Как было отмечено фон Хойсингером [1994], при подходе Нила местоимениям могут соответствовать как определенные описания (ι-выражения), так и whe-выражения, причем это соответствие в высшей степени неоднозначно. Хойсингер предлагает вместо этого использовать ε-операторы, помеченные функциями выбора (зависящими от контекста). Согласно его идее, анализ фразы (1) имеет вид
Для любой функции выбора i:
∀x (Farmer(x) ∧ Owns(x, εiy Donkey (y)) → Beats (x, εa*y Donkey (y))
a* – это функция выбора, зависящая от i и первой части условного предложения: если i – это функция, выбирающая εiy Donkey (y) из множества всех ослов, то εa*y Donkey (y) выбирает из множества ослов, принадлежащих x.
Такой подход к пониманию местоимений, привлекающий ε-операторы, индексированные функциями выбора, позволил фон Хойсингеру разобраться со многими различными ситуациями (см. [Egli and von Heusinger, 1995]; [von Heusinger, 2000]).
Приложения ε-исчисления к формальным семантикам и функциям выбора вообще вызывают в последнее время значительный интерес. Фон Хойсингер и Эгли [2000a] среди прочих упоминают следующие тематики: представления вопросительных предложений [Reinhart, 1992], специальные неопределенности [Reinhart 1992; 1997; Winter 1997], местоимения E-типа [Hintikka and Kulas 1985; Slater 1986; Chierchia 1992, Egli and von Heusinger 1995] и определенные именные группы [von Heusinger, 1997, 2004].
Приложения ε-исчисления к лингвистике и философии языка также обсуждаются в статье Б. Слейтера «epsilon calculi» (точная ссылка приведена ниже в разделе «Другие Интернет-ресурсы»), а также в сборниках (доступных онлайн) под редакцией фон Хойсингера и других (см. список литературы).
Эпсилон-исчисление также оказывается полезно в качестве логического подхода в рассуждениях об абстрактных объектах. В [Meyer Viol, 1995] проводится сравнение ε-исчисления с теорией абстрактных объектов Файна [1995]. В самом деле, несложно увидеть эту связь: для данной эквивалентности ∀x A(x) ≡ A(εx (¬A)) терм εx (¬A) является абстрактным объектом в том смысле, что это такой объект, A от которого истинно тогда и только тогда, когда A тождественно истинно.
Работы [Meyer Viol, 1995, 1995a] содержат дальнейшие исследования ε-исчисления как инструмента в теории доказательств и теории моделей; при этом особенное внимание уделяется интуиционистскому подходу в ε-исчислении. В рамках последнего ε-теоремы более не имеют места, то есть введение ε-термов дает неконсервативное расширение интуиционистской логики. На самом деле, как было показано Беллом [1993a, 1993b; Meyer Viol, 1995], добавление ε-оператора к интуиционистской предикативной логике позволяет нам доказать отвергаемые в интуиционизме принципы ¬A ∨ ¬¬A и (A → B) ∨ (A → B). Что же касается принципа исключенного третьего, то во всей полноте он может быть доказан только если мы добавим также следующую аксиому ε-экзистенциональности:
∀x (A(x) ↔ B(x)) → εx A = εx B
Этот результат доставляет нам строгое обоснование изначальной гипотезы Гильберта о том, что принцип исключенного третьего является в некотором смысле частным случаем аксиомы выбора, и только при наличии ε-экзистенциональности мы можем получить принцип выбора во всей его полноте.
Другие теоретико-модельные исследования ε-операторов в интуиционистской логике представлены у Де Види [1995]. Об использовании ε-операторов в многозначной логике см. Работу Мостовски [1963], о модальном ε-исчислении см. работу Фиттинга [1975].
Приведенный здесь список литературы содержит работы, полезные для первоначального ознакомления с теорией, но не в коей мере не претендует на полноту.
В этом списке перечислены некоторые оригинальные работы:
· Bennacerraf, P., Putnam, H. (eds.), 1983, Philosophy of Mathematics , 2nd ed., Cambridge: Cambridge University Press
· Ewald, W. B. (ed.), 1996, From Kant to Hilbert. A Source Book in the Foundations of Mathematics, Vol. 2, Oxford: Oxford University Press
· Mancosu, P. (ed.), 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press
· van Heijenoort, J. (ed.), 1967, From Frege to Gödel. A Source Book in Mathematical Logic. Cambridge, Mass.: Harvard University Press
Исторические обзоры, касающееся развития логики и теории доказательств в рамках школы Гильберта:
· Avigad J. and Reck, E., 2001, ‘Clarifying the nature of the infinite": the development of metamathematics and proof theory’, Carnegie Mellon University Technical Report CMU-PHIL-120 [Available online in PDF]
· Hallett, M., 1995, ‘Hilbert and logic’, M. Marion and R. S. Cohen, Quebec Studies in the Philosophy of Science, Vol. 1, Dordrecht: Kluwer, 135-187
· Mancosu, P., 1998a, ‘Hilbert and Bernays on metamathematics’, in Mancosu, 1998, 149-188
· Moore, G. H., 1997, ‘Hilbert and the emergence of modern mathematical logic’, Theoria (Segunda Epoca), 12:65-90
· Peckhaus, V., 1990, Hilbertprogramm und Kritische Philosophie, Göttingen: Vandenhoek & Ruprecht
· Sieg, W., 1988, ‘Hilbert's program sixty years later’, Journal of Symbolic Logic, 53: 338-348
· Sieg, W., 1990, ‘Reflections on Hilbert's program’, W. Sieg (ed.), Acting and Reflecting, Dordrecht: Kluwer
· Sieg, W., 1999, ‘Hilbert's Programs: 1917-1922’, Bulletin of Symbolic Logic, 5: 1-44 [Available online in Postscript]
· Zach, R., 1999, ‘Completeness before Post: Bernays, Hilbert, and the development of propositional logic’, Bulletin of Symbolic Logic, 5: 331--366 [Available online in Postscript]
· Zach, R., 2003, ‘The practice of finitism. Epsilon calculus and consistency proofs in Hilbert's Program’, Synthese 137:211-259. [Preprint available online]
Оригинальные работы:
· Ackermann, W., 1924, ‘Begründung des ’’tertium non datur’’ mittels der Hilbertschen Theorie der Widerspruchsfreiheit’, Mathematische Annalen, 93:1-36
· Ackermann, W., 1937-38, ‘Mengentheoretische Begründung der Logik’, Mathematische Annalen, 115:1-22
· Ackermann, W., 1940, ‘Zur Widerspruchsfreiheit der Zahlentheorie’, Mathematische Annalen, 117:162-194
· Hilbert, D., 1922, ‘Neubegründung der Mathematik: Erste Mitteilung’, Abhandlungen aus dem Seminar der Hamburgischen Universität , 1:157-177, English translation in Mancosu, 1998, 198-214 and Ewald, 1996, 1115-1134
· Hilbert, D., ‘Die logischen Grundlagen der Mathematik’, Mathematische Annalen, 88:151-165, English translation in Ewald, 1996, 1134--1148
· Hilbert, D., Bernays, P., 1934, Grundlagen der Mathematik , Vol. 1, Berlin: Springer
· Hilbert, D., Bernays, P., 1939, Grundlagen der Mathematik , Vol. 2, Berlin: Springer
· von Neumann, J., 1927, ‘Zur Hilbertschen Beweistheorie’, Mathematische Zeitschrift, 26:1-46
Доказательство Аккермана 1940 года обсуждается в
· Hilbert, D., Bernays, P., 1970, ‘Grundlagen der Mathematik’, Vol. 2, 2nd, edition, Berlin: Springer, Supplement V
· Wang, H., 1963, A Survey of Mathematical Logic, Peking: Science Press
В следующих работах Мэхара показал, как можно доказать вторую ε-теорему при помощи устранения сечений, и впоследствии усилил ее так, чтобы она включала схему экзистенциональности.
· Maehara, S., 1955, ‘The predicate calculus with ε-symbol’, Journal of the Mathematical Society of Japan, 7:323-344
· Maehara, S., 1957, ‘Equality axiom on Hilbert's ε-symbol’, Journal of the Faculty of Science, University of Tokyo, Section 1, 7:419-435
Одним из ранних приложений метода устранения ε-символов была неконтрпримерная интерпретация Джорджа Крейселя.
· Kreisel, G, 1951, ‘On the interpretation of non-finitist proofs - part I’, Journal of Symbolic Logic, 16:241-267
В следующих работах представлен современный взгляд на эпсилон-исчисление Гильберта; впрочем, мы бы не рекомендовали их для начинающих.
· Leisenring, A. C., 1969, Mathematical Logic and Hilbert's Epsilon-Symbol, London: Macdonald
· Mints, G., 1996, ‘Thoralf Skolem and the epsilon substitution method for predicate logic’, Nordic Journal of Philosophical Logic, 1:133-146 [Available online]
· Moser, G., 2000, The Epsilon Substitution Method, Master's Thesis, University of Leeds
· Moser, G., Zach, R., 2006, ‘The epsilon calculus and Herbrand complexity’, Studia Logica, 82(1):133-155. [Preprint available online in PDF]
Corrections to errors in the literature (including Leisenring's book) can be found in
· Flannagan, T. B., 1975, ‘On an extension of Hilbert's second ε-theorem’, Journal of Symbolic Logic, 40:393-397
· Ferrari, P. L., 1987, ‘A note on a proof of Hilbert's second ε-theorem’, Journal of Symbolic Logic, 52:214-215
· Yashahura, M., 1982, ‘Cut elimination in ε-calculi’, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28:311-316
Разновидность эпсилон-исчисления, основанная на функциях Сколема и, таким образом, совместимая с логикой первого порядка, обсуждается в работе
· Davis, M., and R. Fechter, 1991, ‘A free variable version of the first-order predicate calculus’, Journal of Logic and Computation, 1:431-451
· Buss, S. (ed.), 1998. The Handbook of Proof Theory, Amsterdam: North-Holland
· Takeuti, G., 1987, Proof Theory, second edition. Amsterdam: North-Holland, Amsterdam
· Troelstra, A. S., Schwichtenberg, H., 2000, Basic Proof Theory, second edition. Cambridge: Cambridge University Press
В следующих работах можно найти несколько результатов из теории доказательств, которые доказываются с применением методов наподобие тех, что исполь-зовались Гильбертом, Бернайсом и Аккерманом, хотя и в терминах функций Сколема, а не эпсилон-термов.
· Shoenfield, J., 1967, Mathematical Logic, Reading, Mass.:Addison-Wesley, republished by the Association for Symbolic Logic, 2001
For more on ordinal analysis, see, for example:
· Takeuti, G., Proof Theory (see above)
· Pohlers, Wolfram, 1998, ‘Subsystems of set theory and second-order number theory’, in S. Buss (ed.), The Handbook of Proof Theory (see above), 209-335
Теорема Эрбрана впервые была сформулирована в
· Herbrand, J., 1930, Recherches sur la thèorie de la dèmonstration, Dissertation, University of Paris
Английский перевод можно найти в работе Хейеноорта (см. выше) и в
· Herbrand, J., 1971, Collected Works. W. Goldfarb (ed.), Cambridge, Mass.: Harvard University Press
Дополнительную информацию об истории этой теоремы можно найти в
· Dreben, B., Andrews, P., Aanderaa, S., 1963, ‘False lemmas in Herbrand’, Bulletin of the American Mathematical Society, 69:699-706
Имеется множество литературы, касающейся теоремы Эрбрана. В добавление к приведенным выше работам, в которых она возникает в связи с теорией доказательств, перечислим также ряд общих обзоров:
· Buss, S., 1995, ‘On Herbrand's theorem’, Logic and Computational Complexity (Indianapolis, IN, 1994), Lecture Notes in Computer Science 960, Berlin: Springer, 195-209 [Available online in PDF]