La déduction naturelle propose une liste de règles de production basés sur l'introduction et l'élimination de chaque connecteur du langage :
N1 : `(a|--b) |-- a"→"b`
N2 : `a, a"→"b |-- b`
N3 : `(a"→⊥")"→⊥"|-- a`
# Introduction de l'implication.
# Élimination de l'implication.
# Élimination de l'antilogie
L'introduction de l'implication `(a|--b) |-- a"→"b` a comme prémisse, une sous-preuve `a|--b` qui commence par une supposition `a`. À tout endroit d'une preuve ou d'une sous preuve il est possible de commencer une sous sous preuve commençant par une supposition, et ainsi de suite.
On démontre d'abord la règle `"L1"` :
L1 : `"⊥"|--a`
Démonstration :
Supposons `"⊥"`
Supposons `a`
N1: `(a|--"⊥") |-- a"→⊥"`
-----------
Supposons `a"→⊥"`
N1: `(a"→⊥"|--"⊥") |-- (a"→⊥")"→⊥"`
-----------
N3 : `(a"→⊥")"→⊥" |-- a`
N1 : `("⊥"|--a) |-- "⊥→"a)`
Pour démontrer qu'un tel système produit bien toutes les propositions vrai et uniquement celles-ci, on utilise le même procédé que pour le système de Hilbert. On recourt à la récurrence. Etant donnée deux propositions `p, q` tel que le système démontre soit `p` ou bien soit `p"→⊥"`, et aussi `q` ou bien `p"→⊥"`, alors nous démontrerons que pour la proposition `p"→"q`, le système démontre `p"→"q` ou bien il démontre sa négation `(p"→"q)"→⊥"` selon le cas logique définit par l'hypothèse. Le langage propositionnelle `sfP` étant définit par cette unique procédé de construction comme l'indique sa grammaire, `sfP = {sfV,(sfP"→"sfP)}` et `sfV = {"⊥", x_1,x_2,x_3,...}`, nous aurons démontré ainsi que toutes propositions ou sa négation est produite par le système de déduction naturel. Cela consiste concrètement à montrer que le système engendre les `4` règles de déductions suivantes :
`p,q"→⊥" |-- (p"→"q)"→⊥"`
`p"→⊥",q |--p"→"q`
`p"→⊥","¬"q |-- p"→"q`
Puis, pour prouver que le système ne produit seulement que les propositions tautologiques, il suffit de vérifier en utilisant la table de vérité de l'implication que chaque règle `"N1"`, `"N2"` appliquée à des prémisses de valeur booléenne `1`, produisent des propositions de valeur booléenne `1`.
---- 19 avril 2026 ----
La démonstration est triviale :
`"N1"` : `(p |-- q) |-- p"→"q`
Supposons `p`
`"N2"` : `p, p"→⊥" |-- "⊥"`
`"N4"` : `"⊥" |-- q`
`N1" : `(p|--q ) |-- p"→"q`
La démonstration est la même :
Supposons `p`
`"N2"` : `p, p"→⊥" |-- "⊥"`
`"N4"` : `"⊥" |-- q`
`N1" : `(p|--q ) |-- p"→"q`