Кіріспе

Логикалық операция

Логикада, теріске шығару, сондай-ақ логикалық емес немесе логикалық толықтыру деп аталады, бұл бір ұйғарымды екінші ұйғарымға, яғни "емес" ұйғарымына айналдыратын операция, "ақиқат емес" дегенді білдіреді, және жазылады немесе . Бұл интуитивті түрде, егер жалған болса, шындыққа, ал егер ақиқат болса, жалғанға тең болады деп түсіндіріледі. Осылайша, теріске шығару – біржақты логикалық байланыс. Оны түсініктерге, ұйғарымдарға, шындық мәндеріне немесе жалпы семантикалық мәндерге операция ретінде қолдануға болады. Классикалық логикада теріске шығару әдетте ақиқатты жалғанға (және керісінше) айналдыратын шындық функциясымен теңестіріледі. Интуиционистік логикада, Браувер–Хейтинг–Колмогоровтың интерпретациясына сәйкес, ұйғарымның терістелуі – бұл ұйғарымның жорамалды дәлелдемелерінің терістеуі болып табылады. Теріске шығарудың операторы – неганд немесе негатум деп аталады. Жинақтар теориясында, "жинаққа жатпайды" дегенді білдіреді: – U жинағының A жинағына жатпайтын барлық элементтерінің жиынтығы. Оны қалай белгілесе немесе символмен көрсетсе де, терістеуді "P емес", "P емес деп айтуға болады" немесе көбінесе жай ғана "емес P" деп оқылуы мүмкін.

Екі есе терістеу

Классикалық логика жүйесінде қос теріскеулік, яғни бір сөйлемнің теріскеуінің теріскеуі, логикалық тұрғыдан сол сөйлеммен тең болады. Символдармен көрсеткенде, интуиционисттік логикада бір сөйлем өзінің қос теріскеуінен туындайды, бірақ керісінше емес. Бұл классикалық және интуиционисттік теріскеу арасындағы маңызды айырмашылықты көрсетеді. Алгебралық тұрғыдан, классикалық теріскеу екінші дәрежелі инволюция деп аталады. Дегенмен, интуиционисттік логикада әлсіз теңдестік орын алады. Өйткені интуиционисттік логикада тек құрамының қысқартылған түрі ғана, және бізде сондай-ақ бар. Соңғы импликацияны үштік теріскеумен біріктіргенде, туындайды. Осының нәтижесінде, сөйлемдік жағдайда, егер оның қос теріскеуі интуиционисттік тұрғыдан дәлелденсе, онда сол сөйлем классикалық тұрғыдан да дәлелденеді. Бұл нәтиже Гливенко теоремасы деп белгілі.

Сандық көрсеткіштердің терістелуі

Бірінші реттік логикада екі квантор бар, біреуі – әмбебап квантор («барлығы үшін» дегенді білдіреді), ал екіншісі – экзистенциалдық квантор («бар» дегенді білдіреді). Бір квантордың жоқтығы екінші квантормен өрнектеледі (және). Мысалы, егер P предикаты «x – өлшеді» болса және x домені барлық адамдар жиынтығы болса, онда «барлық адамдардың арасында x өлшеді» немесе «барлық адамдар өлшеді» дегенді білдіреді. Оның жоқтығы – , яғни «барлық адамдардың арасында өлмейтін x адам бар» немесе «мәңгі өмір сүретін біреу бар».

Қорытындылау ережесі

Теріс ережелерді қалыптастырудың бірнеше эквивалентті жолдары бар. Классикалық терістілікті табиғи дедукция аясында тұжырымдаудың бір әдеттегі жолы – терістілік енгізуді ( берілгеннен және , infer; бұл ереже reductio ad absurdum деп те аталады), терістілік жоюды ( және -ден infer; бұл ереже де ex falso quodlibet деп аталады) және қос терістілік жоюды ( -ден infer) бастапқы тұжырымдама ережелері ретінде қабылдау болып табылады. Интуиционистік терістіліктің ережелері де осылай алынады, бірақ қос терістілік жою ережесі алынып тасталады. Терістілік енгізу ережесі былай тұжырымдайды: егер берілгеннен абсурдты қорытынды ретінде алуға болады, онда ол жарамсыз болады (яғни, классикалық тұрғыдан жалған, интуиционистік тұрғыдан жоққа шығарылуға болады, т.б.). Терістілік жою ережесі кез келген нәрсенің абсурдтан туындайтынын білдіреді. Кейде терістілік жою ережесі бастапқы абсурд белгісін пайдалана отырып тұжырымдалады. Бұл жағдайда ережеде айтылғандай, және -ден абсурд туындайды. Қос терістілік жою ережесімен бірге біз бастапқыда тұжырымдаған ережені, атап айтқанда, кез келген нәрсенің абсурдтан туындайтынын тұжырымдауға болады. Әдетте интуиционистік терістілік ретінде анықталады. Осы жағдайда терістілік енгізу және жою ережелері – импликация енгізудің (шартты дәлелдеу) және жоюдың (modus ponens) ерекше жағдайлары болып табылады. Бұл жағдайда бастапқы ереже ретінде ex falso quodlibet ережесін де қосу қажет.

Крипке семантикасы

Крипке семантикасында формулалардың семантикалық мәндері мүмкін әлемдер жиыны болған жағдайда, жоққа шығару жиындық теориялық толықтыру ретінде қарастырылуы мүмкін (толығырақ ақпарат үшін мүмкін әлемдер семантикасын қараңыз).