| разы systeme sequentiel couleurs a memoire, что означает: последовательная система цветного телевидения с запоминанием. Предложена франц. инж. А. де Франсом в 1958. Принята во Франции, СССР и др. странах.
СЕКАНС [лат. secans, здесь - секущая (прямая); от seco - режу, рассекаю], одна из тригонометрических функций; обозначение sec. В прямоугольном треугольнике С. острого угла называют отношение гипотенузы к катету, прилежащему к этому углу.
СЕКАТОР (франц. secateur, от лат. seco - секу, режу), садовые ножницы. С. обрезают побеги и нетолстые ветви при формировании и прореживании кроны деревьев, кустарник, а также нарезают черенки винограда.
СЕКАЧ, взрослый самец котика и кабана.
СЕКВАНЫ (лат. Sequani), кельтское племя (расселение С. см. на карте при ст. Кельты).
СЕКВЕНС (Sequens) Йиржи (р. 23.4. 1922, Брно), чехословацкий кинорежиссёр. В 1946 окончил драматич. отделение консерватории в Брно, в 1946-47 учился во ВГИКе (Москва), затем в Ин-те высшего кинообразования (Париж). Работал режиссёром в театре. В 1949 дебютировал в кино как сценарист, в 1951 осуществил первую режиссёрскую работу. Поставил один из лучших чехосл. приключенч. фильмов "Загадка старой штольни" (1955), а также кинокартины: "Непобеждённые" (1956), "Бегство из тени" (1958; Золотая медаль на 1-м Междунар. кинофестивале в Москве, 1959), "Покушение" (1964; Золотая медаль на 4-м Междунар. кинофестивале в Москве, 1965), "Хроника знойного лета" (1973) и др.
СЕКВЕНЦИЙ ИСЧИСЛЕНИЕ (позднелат. sequentia - последовательность, следствие), секвенциальные исчисления, исчисления способов заключений, модификации понятия логич. исчисления, в к-рых основными объектами преобразования являются не формулы, а т. н. секвенции, т. е. выражения вида A1, ..., Al-> B1, ..., Вт, где -> аналогична знаку выводимости, А1, ..., Al и В1, ..., Вт - произвольные формулы; первыеобразующие антецедент секвенции, вторые - её сукцедент. При l, т >= 1 секвенция А1, ..., Al-> B1, ..., Вт интерпретируется как формула
[2312-5.jpg]
операции), секвенция с пустым антецедентом интерпретируется как истина, а секвенция с пустым сукцедентом -как ложь (и, следовательно, секвенция ->, состоящая из одной стрелки,- как противоречие). Аксиомами (исходными секвенциями) в С. и. являются все секвенции вида С -> С (и только они). Правила вывода делятся на т. н. структурные и логические. Первые кодифицируют допустимые изменения "формульного состава" антецедента и сукцедента, вторые-введение в секвенции различных логич. символов. Структурные правила - это "уточнение" (добавление произвольной формулы к антецеденту или сук-цеденту), "сокращение" (вычёркивание повторяющихся формул), перестановка произвольных формул в антецеденте или сукцеденте, а такж" "сечение"
[2312-6.jpg]
(латинскими буквами обозначаются произвольные формулы, греческими -строчки формул, разделённых запятыми, над чертой пишется посылка правила, под чертой - заключение). Логич. правила вывода имеют для секвенциального классич. исчисления высказываний следующий вид:
[2312-7.jpg]
Если и структурные, и логич. правила вывода ограничить условием, согласно к-рому в сукцеденте каждой секвенции должно быть не более одной формулы, то получим секвенциальное интуиционистское исчисление высказываний: это условие оказывается достаточным для невыводимости в С. и. исключённого третьего принципа (а также закона снятия двойного отрицания). Секвенциальное исчисление предикатов получается присоединением к предыдущим правилам ещё двух пар правил введения кванторов общности и существования. Основной результат нем. математика Г. Генцена состоит в установлении возможности приведения каждого вывода в С. и. к "нормальной форме", не содержащей применений правила сечения и тем самым представляющей в нек-ром смысле "прямой" вывод. Из многочисленных приложений этого результата особенно важны доказательства непротиворечивости арифметич. формальных систем, использующие математич. технику, выходящую за рамки гильбертовского финитизма (см. Аксиоматический метод, Метаматематика), и тем самым обходящие в известном смысле трудности, обусловленные теоремой К. Гёделя о неполноте формальной арифметики. Эта же основная теорема Генцена лежит в основе большинства алгоритмов выводимости для логич. и логико-математич. исчислений (см. Разрешения проблема), чем и обусловлена исключит. важность С. и. для интенсивно развивающихся исследований в области машинного поиска логич. вывода, являющихся важным примером моделирования интеллектуальной деятельности человека.
Лит.: Г е н ц е н Г., Исследования логических выводов, пер. с нем., в кн.: Математическая теория логического вывода, М., 1967, с. 9 - 74; его же, Непротиворечивость чистой теории чисел, там же, с. 77 -153; его же, Новое изложение доказательства непротиворечивости для чистой теории чисел, там же, с. 154-90; Карри X. Б., Основания математической логики, -пер. с англ., М., 1969, гл. 5С, 6В, 7В и 8В; Алгорифм машинного поиска естественного логического вывода в исчислении высказываний, М.- Л., 1965.
2315. |
