China
Africa
Explore chapters and articles related to this topic
Logics and Proofs
Published in B. V. Senthil Kumar, Hemen Dutta, Discrete Mathematical Structures, 2019
B. V. Senthil Kumar, Hemen Dutta
Note: Rule CP means rule of Conditional Proof.Rule CP is also called the deduction theorem.In general, whenever conclusion is of the form R → S (in terms of conditional), we should apply Rule CP. In such case, R is taken as an additional premise, and S can be derived from the given premises and R.
Propositional logic
Published in Richard E. Neapolitan, Xia Jiang, Artificial Intelligence, 2018
Richard E. Neapolitan, Xia Jiang
Notice that to use the Deduction theorem, we first temporarily assume a proposition to be true (e.g., step 1), then we conclude that a second proposition is true (e.g., step 2), and finally we conclude that the assumed proposition implies the second proposition (e.g., step 3). At this point we discharge the assumed proposition because we do not really know it to be true. We just temporarily assumed this so as to derive an implication. ■
Axiomatic and dual systems for constructive necessity, a formally verified equivalence
Published in Journal of Applied Non-Classical Logics, 2019
Lourdes del Carmen González-Huesca, Favio E. Miranda-Perea, P. Selene Linares-Arévalo
The above statement is a generalisation of the Deduction Theorem formulated as a rule (GDT), and allows us to discharge any assumption from the context. At this point we could think that the process of deriving new theorems, like that of Example 3.2, can be simplified by means of the rules provided by 3.3, 3.5 and 3.7. However, while this is clearly true to prove pure propositional formulae, for the case of boxed formulae we are faced with trouble. For the deduction, theorem is incompatible with the necessitation rule in that the former introduces hypotheses to the context, which later forbids the application of necessitation. For instance, to prove the sequent of example 3.2, it suffices to show that but now we cannot prove the conclusion by necessitation for the context is not empty. This poses a big challenge for proof construction. We will solve this problem below by defining a rule of generalised necessitation, but before let us discuss some relevant structural rules.
Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss
Published in Journal of Applied Non-Classical Logics, 2018
The proofs provided by Bonet and Buss have three characteristic features. First, they deal with classical logic only (although their results also hold for some non-classical logics as shown in Bolotov, Kozhemiachenko, and Shangin (2018)). Second, they rely heavily on the deduction theorem. Third, they extensively use the fact that there is a formula containing only A and B such that the formula is valid iff A classically entails B. This third feature is what allows Bonet and Buss to simulate various calculi with Frege systems.