|
|
alexandræ · formalising logical invariants
formalising logical invariantsfebruary 1st, 2024
wff (well-formed formulas) are things defined via what we call a formal grammar, which defines wff kinda recursively as such :
- first off, you have a bunch of letters like \(p,q,r,s,t,u,v,\ldots\) which constitute an alphabet. for all intents and purposes, the alphabet is basically just any set. all elements of the alphabet constitute wff, sometimes called atomic wff.
- then you can define more wff by adding syntactical symbols that take other wff as arguments, like "if \(\varphi,\psi\) are wff, then so is \(\varphi*\psi\)".
for more info, there's a cool article on proofwiki that summarises the usual stuff we use : [link].
if we have two formal grammars \(\mathcal G\) and \(\mathcal H,\) we can define their respective sets of wff as \(\textbf{wff}_{\mathcal G}\) and \(\textbf{wff}_{\mathcal H}.\), and respective sets of rules of inference as \(R_{\mathcal G}\) and \(R_{\mathcal H}.\) we call \(\phi\) an invariant under \(\rho_{\mathcal G}\subseteq R_{\mathcal G}\) if it follows these axioms :
- it is a function \(\varphi:\mathcal P(\textbf{wff}_{\mathcal G})\times\mathcal P(\textbf{wff}_{\mathcal G})\to\mathcal P(\textbf{wff}_{\mathcal H}).\)
- for all \(p,q\in\textbf{wff}_{\mathcal G}\) such that \(p\vdash_{\rho_{\mathcal G}}q,\) (which means that can derive \(q\) from \(p\) only using \(R\text{'s}\) rules of inference), then \(\vdash_{R_{\mathcal H}}\varphi(p,q).\)
notably, if i define \(\mathcal H,\textbf{wff}_{\mathcal H},R_{\mathcal H}\) as the ones associated to usual set theory, and define \(\alpha:\mathcal P(\textbf{wff}_{\mathcal G})\to\mathcal P(\textbf{wff}_{\mathcal G})\) as the function that extracts the set of atomic wff of \(\mathcal G\) that are present in at least one of the wff in its input, i can define \(\varphi:(p,q)\mapsto\alpha(q)\subseteq\alpha(p),\) and whenever it is an invariant to \(\rho_{\mathcal G}\subset R_{\mathcal G},\) i say \(\rho_{\mathcal G}\) is a set of decreasing rules of inference. notably, introduction and elimination rules of conjunction are decreasing rules of inference, whilst the introduction rules of disjunction and tautologies aren't. this makes it quite useful to pick and choose what rules to choose in paraconsistent logics when you try to avoid the principle of explosion, although only using decreasing rules may not be the best option either. i didn't search too many invariants so far, but obviously i think there are quite a few that could be quite useful.
| ⟨ | that time i got chatgpt to divide b... |
|
alexandræ
|
