Diskussion:Gentzentypkalkül
Natürliches Schließen vs. Sequenzenkalkül[Quelltext bearbeiten]
Nicht jeder Kalkül, der mit Sequenzen arbeitet, ist ein Sequenzenkalkül. Ein wichtiger Teil (meiner Meinung nach eigentlich der wichtigste) von dem, was natürliches Schließen (das man auch mit expliziten Sequenzen formulieren kann) von einem richtigen Sequenzenkalkül unterscheidet, ist, dass einerseits Einführungs- und Eliminationsregeln für die einzelnen Konnektive formuliert werden, und andererseits Links- und Rechts- Regeln. Die Sakharov-Quelle stimmt bzgl. der Frage, was denn Sequenzenkalküle sind, damit m.M.n.m.o.w überein (der Teil "There are at least two logical rules for every propositional connective and every quantifier; one of them applies to the antecedent, whereas the other applies to the consequent." ist eigentlich Quatsch, aber naja...). NJ und NK (für die der Gentzensche Hauptsatz nicht recht passt) sollten daher hier nicht vorkommen, zumindest, wenn man bedeutungsschwer vom Gentzenschen Hauptsatz sprechen will. --Daniel5Ko (Diskussion) 22:32, 6. Nov. 2018 (CET)