2

I have seen some systems where propositional logic can be written by a single axiom plus an inference rule such as Nicod's axiom.

This to me seems like two rewrite rules. If Nicod's axiom is $N(a,b,c,d)$ then any statements $a\land b\land c\land d \land e$ can be replaced by $N(a,b,c,d) \land e$ which could be written in terms of NANDs. And modus ponens which says $(a ⊼ (b ⊼ c))\land a$ can be replaced by $b$. Actually there are probably a few hidden implied rewrite rules here too for example $a \land a $ replacing $a$ and $a \land (b \land c)$ replacing $(a \land b) \land c$.

Can propositional calculus be defined using a single rewrite rule?

Further if we have a single binary operator $(|)$ and an atomic unit could we encode propositional calculus in terms of propositions encoded like:

$$( ( (|)| (|))|(|))$$

And then use a single rewrite rule which encode both the single axiom the inference rule in one? i.e. essentially it would be to encode every propositional statement in terms of binary trees and the axiom/inference rule as a rewrite/substitution rule on the trees.

Is this possible?

Edit: Thinking about it. I think this would be impossible seeing as one rewrite rule needs to increase the length of the string while the second needs to decrease it. Hence to get anything interesting we would need at least two rewrite rules. Is this argument correct? So are two rewrite rules possible?

Edit2: Actually this argument is false as a single rule could both increase and decrease the length (see comments)

zooby
  • 4,343
  • $PQP \mapsto QPQ$ is capable of both increasing and decreasing the length of a string, depending on what $P$ and $Q$ are. Or do you count that as infinitely many rules rather than just one? –  Apr 27 '18 at 20:17
  • @Hurkyl You're right! Well you proved me wrong about my assumption. So maybe it could be possible with a single rule. – zooby Apr 27 '18 at 22:29
  • "And modus ponens which says (a⊼(b⊼c))∧a can be replaced by b." There's a rather common error here. You've written modus ponens as if it involved a single premise. But, modus ponens is an inference rule which involves two assumptions, and a conclusion. You might see something like {(p$\rightarrow$q), p} $\vdash$ q. But, in that the ',' is a separator, not a symbol for a conjunction. – Doug Spoonwood Apr 29 '18 at 00:42
  • "This to me seems like two rewrite rules." A rewrite rule involves rewriting subterms of a formula with other terms. https://en.wikipedia.org/wiki/Rewriting A well-formed formula in propositional calculus doesn't involve any sort of rewriting of terms. Nicod's modus ponens also detaches a subformula from a formula in contrast to rewriting the entire formula. So, I wouldn't call an axiom, nor a rule of inference like Nicod's modus ponens, or regular modus ponens, a rewrite rule. – Doug Spoonwood Apr 29 '18 at 00:47
  • My guess is 'no'. At least for any conditional-negation propositional calculus. I'm not all too familiar with rewriting systems, but if we have a single rewrite formula, then we'll eventually end up with (p$\rightarrow$p) or equivalently in a NAND system (p⊼(p⊼p)). – Doug Spoonwood Apr 29 '18 at 00:57
  • @Doug I can't see the difference between stating two true propositions as ${p,q}$ and combining them as one as $p \land q$. Except you would use modus ponens slightly differently. – zooby Apr 29 '18 at 17:16
  • {p, q} is one set of two propositions. (p$\land$q) is one proposition. No proposition is a set. And one proposition does not equal two propositions, since one does not equal two. – Doug Spoonwood Apr 29 '18 at 19:54
  • Also, you do NOT have any sort of conjunction in a system like Nicod's. You only have NANDs. So, Nicod's modus ponens is not some sort of conjunction. – Doug Spoonwood Apr 29 '18 at 19:56
  • OK if you say so. – zooby Apr 29 '18 at 22:27

0 Answers0