К сожалению, предположение не подразумевает, что THE x. P x 'существует', по крайней мере, не в том смысле, в котором вы найдете удовлетворение.Поскольку HOL является полной логикой, в логике нет понятия «четкой определенности».
Если вы пишете THE x. P x, когда нет уникального x, удовлетворяющего P, тогда THE x. P x - это , все еще значение, которое «существует» в HOL, но такое, в котором вы не можете доказать ничего значимого (как, например, undefined константа) и, конечно, не то, для которого справедливо P.То же самое верно для SOME, что в основном совпадает с THE с той разницей, что для THE должен быть уникальный свидетель для свойства, а для SOME уникальность равнане требуется.
Типичный подход для показа чего-то о SOME x. P x заключается в том, что вы сначала показываете, что свидетель существует (т. е. ∃x. P x), а затем подключаете его к правилу, подобному someI_ex, которое затем сообщает вамчто P (SOME x. P x) действительно имеет место.
То же самое для THE, за исключением того, что там вы должны показать, что существует ровно один свидетель - что означает ∃! (см. теорему Ex1_def).Показать это уникальное существование можно, например, по правилам ex_ex1I или ex1I.Затем вы можете вставить этот факт в theI' и the1_equality, чтобы получить желаемые результаты.
Кстати, константа для SOME называется Eps (как в «операторе Гильберта ε») и остальные The и Ex1.Если вы наберете, например, term Eps, вы можете нажать Ctrl + 1044 *, и он перейдет к его определению (или, в случае Eps и The, скорее их аксиоматизации).
Естьтакже комбинатор LEAST для натуральных чисел, очень похожий на SOME и иногда весьма полезный (он называется «Наименее», а леммы LeastI_ex и Least_le).
Другая сторонапримечание: Идея, что просто потому, что вы можете записать термин, он не обязательно «четко определен» в интуитивном смысле, очень распространена в Изабель: вы можете делить на ноль, вы можете записать производную недифференцируемойфункция, мера неизмеримого множества, интеграл от неинтегрируемой функции и т. д. Затем вы получаете какое-то фиктивное значение (например, 0 для деления на ноль или что-то совершенно абсурдное, например THE x. False), но большинствотеоремы, которые говорят о реальных свойствах производных, интегралов и т. д., явно требуют, чтобы эта вещь была на самом деле хорошо определена.