Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Deduction theorem
Résumé
In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i.e. to prove an implication A → B, it is sufficient to assume A as an hypothesis and then proceed to derive B. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction.
In more detail, the propositional logic deduction theorem states that if a formula is deducible from a set of assumptions then the implication is deducible from ; in symbols, implies . In the special case where is the empty set, the deduction theorem claim can be more compactly written as: implies . The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if is a closed formula). In general a deduction theorem needs to take into account all logical details of the theory under consideration, so each logical system technically needs its own deduction theorem, although the differences are usually minor.
The deduction theorem holds for all first-order theories with the usual deductive systems for first-order logic. However, there are first-order systems in which new inference rules are added for which the deduction theorem fails. Most notably, the deduction theorem fails to hold in Birkhoff–von Neumann quantum logic, because the linear subspaces of a Hilbert space form a non-distributive lattice.
"Prove" axiom 1: P→(Q→P) efn|See explanation of Notation § below.
P 1. hypothesis
Q 2. hypothesis
P 3. reiteration of 1
Q→P 4. deduction from 2 to 3
P→(Q→P) 5. deduction from 1 to 4 QED
"Prove" axiom 2:
P→(Q→R) 1. hypothesis
P→Q 2.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.