Шығарылған орта заңы

Кіріспе

Логикалық теорема

Логикада ортаны жоққа шығару заңы немесе ортаны жоққа шығару принципі кез келген ұсыныс үшін, бұл ұсыныс немесе оның жоқтығы рас екенін айтады. Бұл үш ойлау заңының бірі, қайшылыққа қарсы заңмен және сәйкестік заңымен бірге; алайда, ешбір логикалық жүйе тек осы заңдарға негізделмеген, және бұл заңдардың ешқайсысы modus ponens немесе Де Морган заңдары сияқты логикалық қорытынды шығару ережелерін ұсынбайды. Бұл заң латын тілінде principium tertii exclusi деп белгілі. Бұл заңның тағы бір латынша атауы – tertium non datur, яғни «үшінші [мүмкіндік] жоқ». Классикалық логикада бұл заң таутология болып табылады. Бұл принципті әрбір ұсыныс дұрыс немесе жалған екенін білдіретін семантикалық екімәнділік принципімен шатастыруға болмайды. Екімәнділік принципі әрдайым ортаны жоққа шығару заңын білдіреді, ал керісінше әрдайым дұрыс емес. Көбінесе келтірілетін қарсы мысал, қазір дәлелденбеген, бірақ болашақта дәлелденетін мәлімдемелерді пайдалана отырып, екімәнділік принципі орындалмаған кезде ортаны жоққа шығару заңы қолданылуы мүмкін екенін көрсетеді.

Principia Mathematica-дағы ортаның алынып тасталуының заңының салдары

Principia Mathematica-дағы ✸2.1 формуласы, алынып тасталған ортаның заңынан Уайтхед пен Расселл логик аргументтеу құралдарының ең қуатты құралдарын тудырады. (Principia Mathematica-да формулалар мен ұйғарымдар жетекші жұлдызшамен және екі санмен, мысалы "✸2.1" арқылы анықталады.) ✸2.1 ~p ∨ p "Бұл – алынып тасталған ортаның заңы" (PM, 101-бет). ✸2.1-дің дәлелі шамамен былай: "алғашқы идея" 1.08 p → q = ~p ∨ q деп анықтайды. Бұл ережеде q орнына p қойсақ, p → p = ~p ∨ p теңдігі шығады. p → p дұрыс болғандықтан (бұл 2.08 теоремасы, ол жеке дәлелденген), онда ~p ∨ p да дұрыс болуы керек. ✸2.11 p ∨ ~p (Аксиома 1.4 бойынша ұйғарымдардың орналасуына рұқсат етіледі)
✸2.12 p → ~(~p) (Қос терістеу принципінің 1-бөлімі: егер "Бұл раушан қызыл болса" дұрыс болса, онда "Бұл раушан қызыл емес" дұрыс емес.) ✸2.13 p ∨ ~{~(~p)} (2.12-мен бірге қолданылатын лемма, 2.14-ті тудыру үшін)
✸2.14 ~(~p) → p (Қос терістеу принципінің 2-бөлімі)
✸2.15 (~p → q) → (~q → p) (Төрт "Транспозиция принципінің" бірі. 1.03, 1.16 және 1.17-ге ұқсас. Бұл жерде өте ұзақ дәлелдеу қажет болды.) ✸2.16 (p → q) → (~q → ~p) (Егер "Егер бұл раушан қызыл болса, онда бұл шошқа ұшады" дұрыс болса, онда "Егер бұл шошқа ұшпаса, онда бұл раушан қызыл емес" дұрыс.) ✸2.17 (~p → ~q) → (q → p) ("Транспозиция принципінің" тағы бірі.) ✸2.18 (~p → p) → p ("Reductio ad absurdum-ның толықтыруы. Ол өз жалғандығының гипотезасынан туындайтын ұйғарымның шын екенін көрсетеді" (PM, 103–104-беттер).) Бұл теоремалардың көпшілігі – әсіресе ✸2.1, ✸2.11 және ✸2.14 – интуиционизммен қабылданады. Бұл құралдар Колмогоровтың "Хилберттің төрт аксиомасы" және "Хилберттің екі аксиомасы" деп атаған басқа бір формаға қайта құрылады (Колмогоров, ван Хейеноорт, 335-бет). ✸2.12 және ✸2.14, "қос терістеу":
Л. Е. Ж. Браувердің интуиционисттік жазбалары ол "көптеген түрлердің өзара байланысы принципі, яғни әрбір жүйе үшін қасиеттің дұрыстығы осы қасиеттің мүмкін еместігінен туындайтын принцип" деп атаған нәрсеге сілтеме жасайды (Браувер, сол жерде, 335-бет). Бұл принципті әдетте "қос терістеу принципі" деп атайды (PM, 101–102-беттер). Алынып тасталған ортаның заңынан (✸2.1 және ✸2.11) PM ✸2.12 принципін тікелей тудырады. 2.11-де p-ні ~p-мен алмастырсақ, ~p ∨ ~(~p) теңдігі шығады, ал импликацияның анықтамасы бойынша (яғни 1.01 p → q = ~p ∨ q) ~p ∨ ~(~p) = p → ~(~p). QED (2.14-тің тудырылуы сәл күрделірек.)

From the law of excluded middle, formula ✸2.1 in Principia Mathematica, Whitehead and Russell derive some of the most powerful tools in the logician's argumentation toolkit. (In Principia Mathematica, formulas and propositions are identified by a leading asterisk and two numbers, such as "✸2.1".) ✸2.1 ~p ∨ p "This is the Law of excluded middle" (PM, p. 101). The proof of ✸2.1 is roughly as follows: "primitive idea" 1.08 defines p → q = ~p ∨ q. Substituting p for q in this rule yields p → p = ~p ∨ p. Since p → p is true (this is Theorem 2.08, which is proved separately), then ~p ∨ p must be true. ✸2.11 p ∨ ~p (Permutation of the assertions is allowed by axiom 1.4)
✸2.12 p → ~(~p) (Principle of double negation, part 1: if "this rose is red" is true then it's not true that this rose is not red' is true".) ✸2.13 p ∨ ~{~(~p)} (Lemma together with 2.12 used to derive 2.14)
✸2.14 ~(~p) → p (Principle of double negation, part 2)
✸2.15 (~p → q) → (~q → p) (One of the four "Principles of transposition". Similar to 1.03, 1.16 and 1.17. A very long demonstration was required here.) ✸2.16 (p → q) → (~q → ~p) (If it's true that "If this rose is red then this pig flies" then it's true that "If this pig doesn't fly then this rose isn't red.") ✸2.17 ( ~p → ~q ) → (q → p) (Another of the "Principles of transposition".) ✸2.18 (~p → p) → p (Called "The complement of reductio ad absurdum. It states that a proposition which follows from the hypothesis of its own falsehood is true" (PM, pp. 103–104).) Most of these theorems—in particular ✸2.1, ✸2.11, and ✸2.14—are rejected by intuitionism. These tools are recast into another form that Kolmogorov cites as "Hilbert's four axioms of implication" and "Hilbert's two axioms of negation" (Kolmogorov in van Heijenoort, p. 335). Propositions ✸2.12 and ✸2.14, "double negation":
The intuitionist writings of L. E. J. Brouwer refer to what he calls "the principle of the reciprocity of the multiple species, that is, the principle that for every system the correctness of a property follows from the impossibility of the impossibility of this property" (Brouwer, ibid, p. 335). This principle is commonly called "the principle of double negation" (PM, pp. 101–102). From the law of excluded middle (✸2.1 and ✸2.11), PM derives principle ✸2.12 immediately. We substitute ~p for p in 2.11 to yield ~p ∨ ~(~p), and by the definition of implication (i. e. 1.01 p → q = ~p ∨ q) then ~p ∨ ~(~p)= p → ~(~p). QED (The derivation of 2.14 is a bit more involved.)