Techniques pour montrer la non-dérivabilité dans les logiques et autres systèmes de preuve formels

Dans les systèmes de preuve pour la logique propositionnelle classique, si l'on veut montrer qu'une certaine formule n'est pas dérivable, on montre simplement que peut être dérivé (bien que d'autres techniques soient certainement possibles). La non-dérivabilité découle essentiellement de la solidité et de l'exhaustivité du système d'épreuve. $\psi$ $\neg\psi$

Malheureusement pour les logiques non classiques et les systèmes de preuve plus exotiques (comme les règles sous-jacentes à la sémantique opérationnelle), aucune technique directe de ce type n'existe. Cela pourrait être dû au fait que la non-dérivabilité de n'implique pas que soit dérivable, comme c'est le cas avec les logiques intuitionnistes, ou simplement qu'il n'existe aucune notion de négation. $\psi$ $\neg\psi$

Ma question est donnée un système de preuve , où , (et probablement sa sémantique), quelles techniques existent montrer la non-dérivabilité? $(\mathcal{L},\vdash)$ $\vdash\;\subseteq\mathcal{L}^*\times\mathcal{L}$

Les systèmes de preuve d'intérêt pourraient inclure la sémantique opérationnelle des langages de programmation, les logiques Hoare, les systèmes de types, une logique non classique ou des règles d'inférence pour ce que vous avez.

lo.logic Dave Clarke
la source

Dave, je pense qu'il y a une faute de frappe dans la question, pour montrer que n'est pas dérivable, nous ne montrons pas que est dérivable, nous montrons simplement qu'il est cohérent, et cela n'est basé que sur la cohérence du classique logique. Si la logique est une logique classique de premier ordre, alors il y a des phrases que nous ne pouvons ni prouver ni réfuter (sauf si nous parlons d'une théorie complète ). Ou suis-je mal interprété votre question?

φ

$\varphi$

\neg φ

$\lnot \varphi$

Kaveh

Je l'ai changé en logique propositionnelle classique. La question demande toute technique en dehors de la preuve de la négation, car de nombreux systèmes formels (collections d'axiomes et règles d'inférence) n'ont pas de négation, ou en fait peuvent même ne pas ressembler à de la "logique".

Dave Clarke

Merci pour la clarification, mon esprit va par défaut à la logique du premier ordre lorsque je lis la logique classique. :)

Kaveh

Réponses:

IME, la liste suivante est du plus facile au plus difficile (bien sûr, elle est aussi du moins au plus puissant):

Si votre système est sain, et vous pouvez prouver , alors vous avez un résultat nonderivability, bien sûr. $\lnot \phi$
Si vous avez une sémantique théorique du réseau pour votre logique, par rapport à laquelle toutes vos règles de preuve sont valides, alors si la signification d'une proposition n'est pas l'élément le plus haut du réseau, alors ce n'est pas une proposition dérivable.
Si vous savez que votre logique est complète par rapport à une classe de modèles, vérifiez s'il y a un modèle particulier dans cette classe qui invalide . $\phi$
Parfois, vous pouvez vous en sortir avec une traduction dans une autre logique et montrer que la dérivabilité ici implique un résultat connu de non-dérivabilité là-bas.
Si vous avez une déduction naturelle ou un calcul séquentiel, vérifiez s'il existe un résultat d'élimination des coupures connu, ou si vous pouvez en prouver un. Si tel est le cas, vous pouvez souvent exploiter la propriété subformula pour donner des arguments inductifs simples sur la non-dérivabilité. (Par exemple, la cohérence via l'élimination des coupures n'est que la déclaration qu'il n'y a pas de preuve de coupure sans coupure, et donc si toutes les coupures peuvent être éliminées, il n'y a pas d'incohérences.)
Si rien d'autre ne fonctionne, vous pouvez souvent afficher des résultats de cohérence / non-dérivabilité via un argument de relations logiques. C'est le gros canon, qui fonctionne quand rien d'autre ne le fait - en termes de théorie des ensembles, cela se résume à une utilisation de l'axiome de remplacement, qui vous permet de montrer que les énormes ensembles sont bien ordonnés. (C'est pourquoi vous pouvez l'utiliser pour prouver des choses comme la normalisation du système F.)

Neel Krishnaswami
la source

F

$F$

P A^{2}

$PA^2$

F^{2}

$F^2$

Merci, je vois maintenant ce que vous entendiez par "des choses comme la normalisation du système F". :)

Kaveh

@Kaveh, @Neel: Une forte normalisation du système F n'est pas un théorème de PA2, mais elle équivaut sur PA à la cohérence de PA2. Au contraire, une forte normalisation pour tous les termes de rang n (le rang étant la mesure de la profondeur maximale des quantificateurs de type nsted) peut être prouvée en utilisant ACA- n . J'aime parler de la construction de modèles de gerbes en secret ...

Charles Stewart

@Charles: J'ai appris cette idée grâce à certains articles de Jean Gallier, qui sont étonnamment sous-cités. Un peu pervers, cette vue fantaisiste m'a aidé à comprendre le récit plus simple de Mitchell & Scedrov.

Neel Krishnaswami