Can we see natural deduction rules as functions or even as formal grammars?

Question

Is there a way of seeing natural deduction rules as functions or even as formal grammars, maybe context-free grammars or Lambek grammars? It seems quite "easy" to see the rules as functions which take arguments and inputs and transform them to conclusions which will be the outputs. I want this in order to represent proofs as certain configurations of this functions, compositions etc. However I'm not sure if they will behave exactly as functions, or if weird things can happen.

Answer 1

If we take a look at say the Schaum's Outline of Logic, it states one rule of conjunction elimination as "From a conjunction, we may infer either of its conjuncts." Thus, given two wffs the output of conjunction elimination is not unique and thus not a function. Also, if we were to reason from

Cpq, Crq, Apr to q

we would call that a use of disjunction elimination and also if we reasoned from

Apr, Cpq, Crq to q

we would also a use of disjunction elimination also.

But, from a functional perspective, we would have to use distinct functions, since the parameters of the first case above interpreted as above would consist of first a conditional, second another conditional, and third a disjunction (and here Polish notation can help, since finding the type of function can get done easily by just taking the letter of the wff), while the second case's function parameters would consist of first a disjunction, second a conditional, and third a conditional.

Now, that isn't to say that you couldn't fairly easily transform natural deduction rules into a bunch of functions which suffice. As usual, take care with conditional introduction and scope. For example, we could transform Jaskowski's system of rules into a bunch of functions basically as follows (I'm working from memory here) using more modern terminology:

Conditional Elimination: (Cpq, p) $\rightarrow$ q.

Negation Elimination: (CNpNq, CNpq) $\rightarrow$ p.

Conditional Introduction: (p, q) $\rightarrow$ Cpq, provided that 'p' and 'q' have the same scope level and have the same scope class (each time you introduce a hypothesis the scope level increases by one, and a new scope class is created. Scope class and scope level are independent... e. g. if we introduce a hypothesis at the start it has scope level 1 and scope class A. Then if we discharge it, and then introduce another hypothesis that second hypothesis has scope level 1 also, but has scope class B... compare how Fitch style proofs work or Jaskowski's proof boxes). Also, define the scope of all (formal) theorems or axioms as having scope level 0. If x and y have scope level 0, then Cxy has scope level 0. Note here that above p and q were constants, but x and y are different and not constants. Otherwise, where "number" indicates the scope level of p and q, Cpq has scope level (number - 1).

How scope works for the other functions should also get specified, but in all cases scope works the same. Suppose the greatest scope class happens at the level of axioms or theorems. Then, all arguments in any use of the function have to come as orderable in terms of their scope class, and an output of any of the functions has to occur at the least scope class (scope class is not a linear order). In other words, if we apply the conditional elimination function say in a proof like the following:

 hypothesis  1 | Cpq
 hypothesis  2 || r
 2-2 C-in    3 | Crr
 hypothesis  4 || s
 hypothesis  5 ||| p

And we want to infer q via conditional elimination, we have the scope class of Cpq and p ordered such that scope_class(Cpq) > scope_class(p), and thus the output of the function has to happen in the same scope class as that of p. I've included 'r' here to indicate that though 'r' and 's' have the same scope level, they have different scope classes.

But also note that the above three functions qualify as distinct from the natural deduction rules of inference. The above three weaker rules of inference, along with hypothesis introduction and assumption introduction, suffice to produce the same results as a natural deduction system. However, in the corresponding natural deduction system the rules are more like:

Conditional Elimination: {Cpq, p} $\rightarrow$ q.

Negation Elimination: {CNpNq, CNpq} $\rightarrow$ p.

Conditional Introduction: {p, q} $\rightarrow$ Cpq

where {p, q} indicates a set and (p, q) indicates the specific type of set known as a sequence (or a tuple if you prefer). Except, though {Cpq, p} = {p, Cpq}, the order matters for a function, and thus you can't use sets as input of functions. Thus, from a functional perspective, Jaskowski's natural deduction system is more like the following five functions:

Conditional Elimination_1: (Cpq, p) $\rightarrow$ q.

Negation Elimination_1: (CNpNq, CNpq) $\rightarrow$ p.

Conditional Introduction: (p, q) $\rightarrow$ Cpq

Conditional Elimination_2: (p, Cpq) $\rightarrow$ q.

Negation Elimination_2: (CNpq, CNpNq) $\rightarrow$ p.

But, since CpCCppq and CCNpqCCNpNqp (p and q still constants) can get shown from the first three functions, it ends up that the last two functions are not necessary if we have the first three functions (other possibilities are available here).

So, the answer to your question goes something like: "No, we can't see natural deduction rules as functions. Natural deduction rules of inference correspond to classes (or sets) of functions. But, if we use functional rules instead of natural deduction rules which get suggested by natural deduction rules, we can use weaker rules of inference that produce the same results."