Кіріспе
Гипотезалардан қорытынды шығаруға қабілетті жүйелі логикалық процесс. Логика және логика философиясында, тұжырымдау ережесі, шешім шығару ережесі немесе түрлендіру ережесі – бұл үй-жайларды қабылдайтын, олардың синтаксисін талдайтын және қорытындыны (немесе қорытындыларды) қайтаратын логикалық форма. Мысалы, modus ponens деп аталатын тұжырымдау ережесі екі үй-жайды қабылдайды: біреуі "Егер p болса, онда q" және екіншісі "p" түрінде, ал нәтижесінде "q" қорытындысын береді. Бұл ереже классикалық логиканың семантикасына (сондай-ақ көптеген басқа классикалық емес логикалардың семантикасына) қатысты жарамды, яғни егер үй-жайлар дұрыс болса (біріншілік түсіндіру бойынша), онда қорытынды да дұрыс болады. Әдетте, тұжырымдау ережесі шындықты, семантикалық қасиетті сақтайды. Көпмәнді логикада ол жалпы белгіленуді сақтайды. Бірақ тұжырымдау ережесінің әрекеті таза синтаксистік болып табылады және ешқандай семантикалық қасиетті сақтаудың қажеті жоқ: формулалар жиынтығынан формулаға дейінгі кез келген функция тұжырымдау ережесі ретінде қарастырылады. Көбінесе тек рекурсивті ережелер маңызды; яғни, ережеге сәйкес формулалардың берілген жиынтығынан кез келген формуланың қорытынды екенін анықтау үшін тиімді процедура бар. Бұл мағынада тиімді емес ережеге мысал ретінде шексіз ω ережесін келтіруге болады. Пропозициялық логикадағы танымал тұжырымдау ережелеріне modus ponens, modus tollens және контрапозиция жатады. Бірінші реттік предикаттық логика логикалық кванторлармен жұмыс істеу үшін тұжырымдау ережелерін пайдаланады.
In philosophy of logic and logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of inference called modus ponens takes two premises, one in the form "If p then q" and another in the form "p", and returns the conclusion "q". The rule is valid with respect to the semantics of classical logic (as well as the semantics of many other non classical logics), in the sense that if the premises are true (under an interpretation), then so is the conclusion. Typically, a rule of inference preserves truth, a semantic property. In many valued logic, it preserves a general designation. But a rule of inference's action is purely syntactic, and does not need to preserve any semantic property: any function from sets of formulae to formulae counts as a rule of inference. Usually only rules that are recursive are important; i. e. rules such that there is an effective procedure for determining whether any given formula is the conclusion of a given set of formulae according to the rule. An example of a rule that is not effective in this sense is the infinitary ω rule. Popular rules of inference in propositional logic include modus ponens, modus tollens, and contraposition. First order predicate logic uses rules of inference to deal with logical quantifiers.
Қабылдауға және шығаруға қабілеттілік
Ережелер жиынтығында, тұжырымдама ережесі артық болуы мүмкін, яғни рұқсат етілетін немесе шығарылатын болып табылады. Шығарылатын ереже – оның қорытындысы басқа ережелерді қолдану арқылы оның алғышарттарынан шығарылатын ереже. Барлық шығарылатын ережелер рұқсат етіледі. Олардың айырмасын түсіну үшін, табиғи сандарды анықтауға арналған келесі ережелерді қарастырайық (мүмкіндік - табиғи сан екенін көрсетеді): Бірінші ереже 0 – табиғи сан дейді, ал екінші ереже n болса, s(n) – табиғи сан дейді. Бұл дәлелдеу жүйесінде, табиғи санның екінші ізбасары да табиғи сан екенін көрсететін келесі ереже шығарылады: Оның шығарылуы – жоғарыдағы ізбасар ережесінің екі рет қолданылуының нәтижесі. Кез келген нөлдік емес санның алдағысы бар екенін көрсететін келесі ереже тек қана рұқсат етіледі: Бұл индукция арқылы дәлелденетін табиғи сандардың рас фактісі. (Бұл ереженің рұқсат етілетіндігін дәлелдеу үшін, алғышарттың туындысын қабылдап, оған қатысты туындысын алу үшін индукция қолданыңыз.) Дегенмен, ол шығарылмайды, өйткені ол алғышарттың туындысының құрылысына байланысты. Осы себепті, туындылық дәлелдеу жүйесіне қосылғанда тұрақты болады, ал рұқсат етілу тұрақты болмайды. Айырмасын көру үшін, дәлелдеу жүйесіне келесі мағынасыз ереже қосылған деп есептейік: Бұл жаңа жүйеде екі рет ізбасар ережесі әлі де туынды. Алайда, алдағысын табу ережесі енді рұқсат етілмейді, өйткені туындысының алуға жол жоқ. Рұқсат етілудің осалдығы оның дәлелдену тәсілінен туындайды: дәлелдеме алғышарттардың туындысының құрылымына тәуелді болғандықтан, жүйеге кеңейтулер осы дәлелдемеге жаңа жағдайларды қосады, олар енді дұрыс болмауы мүмкін. Рұқсат етілетін ережелерді дәлелдеу жүйесінің теоремалары деп қарастыруға болады. Мысалы, кесуді жою орындалатын тізбекті есептеуде кесу ережесі рұқсат етіледі.
The first rule states that 0 is a natural number, and the second states that s(n) is a natural number if n is. In this proof system, the following rule, demonstrating that the second successor of a natural number is also a natural number, is derivable:
Its derivation is the composition of two uses of the successor rule above. The following rule for asserting the existence of a predecessor for any nonzero number is merely admissible:
This is a true fact of natural numbers, as can be proven by induction. (To prove that this rule is admissible, assume a derivation of the premise and induct on it to produce a derivation of .) However, it is not derivable, because it depends on the structure of the derivation of the premise. Because of this, derivability is stable under additions to the proof system, whereas admissibility is not. To see the difference, suppose the following nonsense rule were added to the proof system:
In this new system, the double successor rule is still derivable. However, the rule for finding the predecessor is no longer admissible, because there is no way to derive The brittleness of admissibility comes from the way it is proved: since the proof can induct on the structure of the derivations of the premises, extensions to the system add new cases to this proof, which may no longer hold. Admissible rules can be thought of as theorems of a proof system. For instance, in a sequent calculus where cut elimination holds, the cut rule is admissible.