|
|
alexandræ · formalisation des invariants logiques
formalisation des invariants logiques1er février 2024
les formules bien-formées (wff) sont des trucs définis via ç'qu'on appelle une grammaire formelle, qui les définit un peu récursivement commesuit :
- d'abord, t'as un tas de lettres \(p,q,r,s,t,u,v,\ldots\) qui constituent un alphabet. pour ce qui nous intéresse, on peut juste dire que ledit alphabet c'est n'importe quel ensemble. tous les éléments de l'alphabet constituent des wff, parfois dites wff atomiques.
- après tu peux définir encore plus de wff en rajoutant des symboles syntaxiques qui prennent d'autres formules comme arguments, genre "si \(\varphi,\psi\) sont des wff, alors \(\varphi*\psi\) aussi".
pour plus (+) d'info, y a un article sur proofwiki qui résume bien tout ç'qu'on utilise en général : [lien].
si on a deux grammaires formelles \(\mathcal G\) et \(\mathcal H,\) on peut définir leurs ensembles de wff respectifs comme \(\textbf{wff}_{\mathcal G}\) et \(\textbf{wff}_{\mathcal H}.\), et leurs ensembles de règles d'inférence respectifs \(R_{\mathcal G}\) et \(R_{\mathcal H}.\) on appelle \(\phi\) un invariant sous \(\rho_{\mathcal G}\subseteq R_{\mathcal G}\) si ça respecte les axiomes suivants :
- \(\varphi:\mathcal P(\textbf{wff}_{\mathcal G})\times\mathcal P(\textbf{wff}_{\mathcal G})\to\mathcal P(\textbf{wff}_{\mathcal H}).\)
- pour tout \(p,q\in\textbf{wff}_{\mathcal G}\) tel que \(p\vdash_{\rho_{\mathcal G}}q,\) (ce qui signifie qu'on peut déduire \(q\) de \(p\) juste en utilisant les règles d'inférence dans \(R\)), alors \(\vdash_{R_{\mathcal H}}\varphi(p,q).\)
notamment, si j'définis \(\mathcal H,\textbf{wff}_{\mathcal H},R_{\mathcal H}\) comme ceux associés à la théorie des ensembles usuelle, et définis \(\alpha:\mathcal P(\textbf{wff}_{\mathcal G})\to\mathcal P(\textbf{wff}_{\mathcal G})\) comme la fonction qui extrait toutes les wff atomiques dans \(\mathcal G\) qui soient présents dans au moins une des wff dans son entrée, je peux alors définir \(\varphi:(p,q)\mapsto\alpha(q)\subseteq\alpha(p),\) et dès qu'c'est un invariant \(\rho_{\mathcal G}\subset R_{\mathcal G},\) j'appelle \(\rho_{\mathcal G}\) un ensemble de règles d'inférences décroissantes. notamment, les règles d'introduction et d'élimination d'la conjonction sont décroissante, alors que la règle d'introduction de la disjonction et les tautologies ne le sont pas. ça peut s'avérer assez utile quand on cherche quelles règles choisir en logique paracohérente pour éviter l'principle d'explosion, même si utiliser uniquement des règles décroissantes c'est pas forcément top non plus. j'ai pas cherché une tonne d'invariants pour l'instant, mais clairement j'pense qu'y en a quand même une bonne poignée qui pourraient être assez utiles.
| ⟨ | cette fois où j'ai fait diviser pa... |
| | encore un "paradoxe" probabiliste, ... | ⟩ |
|
alexandræ
|
