Секатор
Сека'тор (франц. sécateur, от лат. seco — секу, режу), садовые ножницы. С. обрезают побеги и нетолстые ветви при формировании и прореживании кроны деревьев, кустарник, а также нарезают черенки винограда.
Секач
Сека'ч, взрослый самец котика и кабана.
Секваны
Секва'ны (лат. Sequani), кельтское племя (расселение С. см. на карте при ст. Кельты).
Секвенс Йиржи
Се'квенс (Sequens) Йиржи (р. 23.4. 1922, Брно), чехословацкий кинорежиссёр. В 1946 окончил драматическое отделение консерватории в Брно, в 1946—47 учился во ВГИКе (Москва), затем в институте высшего кинообразования (Париж). Работал режиссёром в театре. В 1949 дебютировал в кино как сценарист, в 1951 осуществил первую режиссёрскую работу. Поставил один из лучших чехословацких приключенческих фильмов «Загадка старой штольни» (1955), а также кинокартины: «Непобежденные» (1956), «Бегство из тени» (1958; Золотая медаль на 1-м Международном кинофестивале в Москве, 1959), «Покушение» (1964: Золотая медаль на 4-м Международном кинофестивале в Москве, 1965), «Хроника знойного лета» (1973) и др.
Секвенций исчисление
Секве'нций исчисле'ние (позднелатинское sequentia — последовательность, следствие), секвенциальные исчисления, исчисления способов заключений, модификации понятия логического исчисления, в которых основными объектами преобразования являются не формулы, а т. н. секвенции, т. е. выражения вида A1,..., Al ® B1,..., Bm, где ® аналогична знаку выводимости, A1,..., Al и B1,..., Bm — произвольные формулы; первые — образующие антецедент секвенции, вторые — её сукцедент. При l, m ³ 1 секвенция A1,..., Al ® B1,... Bm интерпретируется как формула
A1&... &A1 ÉB1 Ú...Ú Bm.
(& — знак конъюнкции, É — импликации, Ú — дизъюнкции, см. Логические операции), секвенция с пустым антецедентом интерпретируется как истина, а секвенция с пустым сукцедентом — как ложь (и, следовательно, секвенция ®, состоящая из одной стрелки, — как противоречие). Аксиомами (исходными секвенциями) в С. и. являются все секвенции вида С ® С (и только они). Правила вывода делятся на т. н. структурные и логические. Первые кодифицируют допустимые изменения «формульного состава» антецедента и сукцедента, вторые — введение в секвенции различных логических символов. Структурные правила — это «уточнение» (добавление произвольной формулы к антецеденту или сукцеденту), «сокращение» (вычёркивание повторяющихся формул), перестановка произвольных формул в антецеденте или сукцеденте, а также «сечение»
(латинскими буквами обозначаются произвольные формулы, греческими — строчки формул, разделённых запятыми, над чертой пишется посылка правила, под чертой — заключение). Логические правила вывода имеют для секвенциального классического исчисления высказываний следующий вид:
Если и структурные, и логические правила вывода ограничить условием, согласно которому в сукцеденте каждой секвенции должно быть не более одной формулы, то получим секвенциальное интуиционистское исчисление высказываний: это условие оказывается достаточным для невыводимости в С. и. исключенного третьего принципа (а также закона снятия двойного отрицания). Секвенциальное исчисление предикатов получается присоединением к предыдущим правилам ещё двух пар правил введения кванторов общности и существования.
Основной результат немецкого математика Г. Генцена состоит в установлении возможности приведения каждого вывода в С. и. к «нормальной форме», не содержащей применений правила сечения и тем самым представляющей в некотором смысле «прямой» вывод. Из многочисленных приложений этого результата особенно важны доказательства непротиворечивости арифметических формальных систем, использующие математическую технику, выходящую за рамки гильбертовского финитизма (см. Аксиоматический метод, Метаматематика), и тем самым обходящие в известном смысле трудности, обусловленные теоремой К. Гёделя о неполноте формальной арифметики. Эта же основная теорема Генцена лежит в основе большинства алгоритмов выводимости для логических и логико-математических исчислений (см. Разрешения проблема), чем и обусловлена исключительная важность С. и. для интенсивно развивающихся исследований в области машинного поиска логического вывода, являющихся важным примером моделирования интеллектуальной деятельности человека.
Лит.: Генцен Г., Исследования логических выводов, пер. с нем., в кн.: Математическая теория логического вывода, М, 1967, с. 9—74; его же. Непротиворечивость чистой теории чисел, там же, с. 77—153; его же, Новое изложение доказательства непротиворечивости для чистой теории чисел, там же, с. 154—90; Карри Х. Б Основания математической логики. пер. с англ., М., 1969, гл. 5С, 6B, 7B и 8B; Алгорифм машинного поиска естественного логического вывода в исчислении высказываний, М. — Л., 1965.
Секвестр (в гражд. праве)
Секве'стр (от лат. sequestro — ставлю вне, отделяю), в буржуазном гражданском праве запрещение или ограничение, налагаемое государственной властью в интересах государства на пользование каким-либо имуществом (взрывчатыми веществами, наркотиками, ядами и др.).