Download Th`ese

2.2 Calcul propositionnel du second ordre faiblement pédagogique
n = n0 + 1 : soient W l’ensemble à n0 éléments et α la variable tels que Vl(σ ·
F ) = W ∪ {α} ; par hypothèse le jugement `2f σ · F est dérivable, et nous
dérivons le jugement `2f ∀α.σ·F par la règle (∀i ) ; par hypothèse de récurrence
le jugement `2f µ|W ·(∀α.σ ·F ) est dérivable, et nous avons µ|W ·(∀α.σ ·F ) =
∀α.µ|W σ·F car α 6∈ W par définition ; finalement nous dérivons le jugement
`2f µ σ·F par la règle (∀e ).
2.2.2
Non-nullité syntaxique des jugements
Dans [31], Nelson introduit le concept d’implication nulle : une implication
A → B est nulle quand la formule A est fausse quel que soit l’instanciation de ses
variables libres. Dans le cas contraire, l’implication est dite non-nulle. La nullité
est principalement un concept sémantique car il fait intervenir la notion de vérité.
Comme nous travaillons dans un contexte purement syntaxique, nous introduisons
le concept d’implication syntaxiquement nulle : une implication A → B est syntaxiquement nulle quand la formule A n’est pas motivable ; dans le cas contraire,
l’implication est syntaxiquement non-nulle. La non-nullité est une propriété très
forte qui n’est évidemment pas toujours vérifiée ; en particulier, le calcul F-CP2
admet des occurrences d’implications nulles dans certaines dérivations :
Exemple. dérivation du jugement `2f (∀α.α) → (∀α.α) :
1) `2f > par (P-Ax) ;
2) β `2f β par (P-Hyp) et 1 ;
3) `2f β → β par (→i ) et 2 ;
4) `2f ∀β.β → β par (∀i ) et 3 ;
5) `2f (∀α.α) → (∀α.α) par (∀e ) et 4.
La formule ∀α.α, définissant l’absurde dans CP2 , n’est évidemment pas motivable
car CP2 est un calcul cohérent ; l’implication (∀α.α) → (∀α.α) est donc nulle dans
F-CP2 ; elle l’est également dans CP2 . Comme ∀α.α est une formule close, elle
n’est pas motivable ; donc l’implication (∀α.α) → (∀α.α) est aussi syntaxiquement
nulle.
La propriété de nullité des jugements est définissable de la même manière que
la nullité des implications : un jugement Γ ` F est nul quand la conjonction des
formules de Γ est fausse quel que soit l’instanciation de ses variables libres. De
même, le jugement Γ ` F est syntaxiquement nul quand le contexte Γ n’est pas
motivable. Nous allons démontrer que dans F-CP2 , tous les jugements apparaissant
dans les dérivations sont non-nuls. Définissons d’abord formellement la non-nullité
des jugements :
Définition 2.2.3. Soit C un calcul dont la morphologie est constitué par l’ensemble
23