What is $r^{-1}(B)$ if $r$ is a rule and $B$ is an expression in a proof system?

37 Views Asked by At

enter image description here

In the first paragraph, what does $r^{-1}(B)$ mean? Does it have something to do with relations? e.g if $A$ is a relation then $A^{-1}$ is the inverse of that relation.

Its from a paper about the hilbert system: https://www3.cs.stonybrook.edu/~cse541/chapter8.pdf

1

There are 1 best solutions below

0
On

It is stated that "$MP^{-1}(B)$ is countably infinite", so I suppose $r^{-1}(B)$ is the set of all sequences of well-formed formulas (wffs) that result in wff $B$ when rule $r$ is applied on such a sequence.

For example, modus ponens (⊢ψ,⊢ψ→φ ⇒ ⊢φ) takes two arguments, therefore all elements of $MP^{-1}(B)$ are pairs of formulas, specifically $MP^{-1}(B) = \{(A, A\rightarrow B)\,|\,A\text{ is wff}\}$.

On another example, necessitation (⊢ψ ⇒ ⊢□ψ) takes one argument, therefore all elements of $NE^{-1}(B)$ are just formulas, specifically $NE^{-1}(B) = \{A\,|\,B=□A\}$. Note that $NE^{-1}(B)$ is empty whenever $B$ does not start with $□$, and otherwise it has precisely one element.