Axiomes des théories des ensembles/Négation dans les prédicats finitaires
Pour élargir l’ontologie de Enum, on introduit la négation dans les prédicats.
Non est un opérateur unaire fondamental.
PredNon Si p est un prédicat alors (Non p) est un prédicat
La définition de la vérité et de la fausseté des formules
modifier« est faux » est un prédicat unaire fondamental.
Les règles Vrai1 et Vrai2 de Enum sont complétées par les deux suivantes.
Faux1 Si x n’est pas dans y alors (x Dans y) est faux
Faux2 Si non(x = y) alors (x Égale y) est faux
Faux1 et Faux2 ne sont pas des règles de production des ensembles énumérables parce que leurs prémisses contiennent une négation et ne sont donc pas atomiques.
Faux-non Si p est vrai alors (Non p) est faux
Vrai-non Si p est faux alors (Non p) est vrai
FauxOu Si p et q sont faux alors (p Ou q) est faux
Asser4 Si p est une assertion alors (Non p) est une assertion
FauxEt Si p est faux et q est une assertion alors (p Et q) et (q Et p) sont faux
FauxExist Si z est une Z-variable et p est un prédicat et (pour tout c) (si c est une constante et c est simple et subst qczp alors q est faux) alors (Il existe un z tel que p) est faux
FauxExist n’est pas une règle de production des ensembles énumérables, à cause du quantificateur (pour tout c).
Frege3 Si p est un prédicat finitaire et q est obtenu par une suite correcte de substitutions de la liste c dans p et q est faux alors c n’est pas dans Extension de p
Les prédicats finitaires avec négation
modifier« est un prédicat sans variables liées » est un prédicat unaire fondamental.
PredFinNon Si p est un prédicat finitaire et q est un prédicat sans variables liées et q a toutes ses variables dans p alors ((Non q) Et p) et (p Et Non q) sont des prédicats finitaires
PredDansNvl Si x est un Z-terme et (y est un ensemble ou y est une Z-variable) alors (x Dans y) est un prédicat sans variables liées
PredEgaleNvl Si x et y sont des Z-termes alors (x Égale y) est un prédicat sans variables liées
PredEtNvl Si p et q sont des prédicats sans variables liées alors (p Et q) est un prédicat sans variables liées
PredOuNvl Si p et q sont des prédicats sans variables liées alors (p Ou q) est un prédicat sans variables liées
PredNonNvl Si x est un prédicat sans variables liées alors (Non x) est un prédicat sans variables liées
Règles auxiliaires pour les variables
modifierSubNon Si Subst vwxu et u est un prédicat alors Subst(Non v)wx(Non u)
OrVarNon Si x est une Z-variable et p est un prédicat et x est premier dans p alors x est premier dans (Non p)
OcZvar6 Si x a au moins une occurrence dans p et p est un prédicat alors x a au moins une occurrence dans Non p
IncVarPred5 Si p et q sont des prédicats et p a toutes ses variables dans q alors p a toutes ses variables dans (Non q)
IncVarPred6 Si p et q sont des prédicats et p a toutes ses variables dans q alors (Non p) a toutes ses variables dans q
Le complémentaire d’un ensemble dans un autre
modifierL’opérateur binaire de différence entre deux ensembles peut être défini par un prédicat finitaire qui contient une négation.
x Moins y =def Extension de Z Dans x Et Non(Z Dans y)
x Moins y est aussi appelé le complémentaire de y dans x.
On peut alors dériver les deux règles suivantes.
M1 Si x et y sont des ensembles alors x Moins y est un ensemble
M2 Si z est dans x et z n’est pas dans y alors z est dans x Moins y
x n’est pas dans y est la façon courante de dire non( x est dans y) .
Comme Faux1 et Faux2 et pour la même raison, M2 n’est pas une règle de production des ensembles énumérables.
Quand on enrichit l’ontologie de Enum en introduisant la négation dans les prédicats finitaires, avec l’opérateur Non, on obtient une ontologie finitaire élémentaire mais suffisamment riche pour formuler la plupart des questions des mathématiques finitaires.
La production des non-équations entre expressions formelles
modifierToutes les non-équations entre expressions formelles sont produites par les quatre règles suivantes.
x ≠ y est une abréviation pour non(x = y)
NeqEform1 Si x est une expression formelle alors sx ≠ o
NeqEform2 Si x et y sont des expressions formelles alors axy ≠ o et bxy ≠ o
NeqEform3 Si x et y sont des expressions formelles et x ≠ y alors sx ≠ sy
NeqEform4 Si w, x, y et z sont des expressions formelles et w ≠ x alors awy ≠ axz et ayw ≠ azx et bwy≠ bxz et byw ≠ bzx
Les non-équations entre listes d’expressions formelles sont obtenues avec les règles suivantes.
NeqSimp Si x est simple et y et z sont des constantes alors x ≠ Cyz
NeqListe Si x ≠ y et w et z sont des constantes alors Cxw ≠ Cyz et Cwx ≠ Czy
