# Are These Postulate Sets Interderivable?

One common axiom set for propositional calculus with rule of inference modus ponendo ponens: "From C$\alpha$$\beta$, $\alpha$, we may infer $\beta$", and uniform substitution is:

1) CqCpq (simplification)
2) CCpCqrCCpqCpr (Frege or self-distribution)
3) CCNpNqCqp


Can we change only 3) and work with this one instead?:

1) Simplification
2) Frege
3) CCpqCNqNp (deduction metatheorm on modus tollens)

• If thos are your axioms, what are your rules of inference? – Hagen von Eitzen Jun 17 '13 at 16:49
• I suspect not. From a meta point of view, the second axiom set is only ever going to increase the number of Ns after starting from a set of premises. Therefore I don't think that it will be able to prove CNNpp. – Lord_Farin Jun 17 '13 at 18:45

I have come up with a proof to back my intuition as it was expressed in a comment:

I suspect not. From a meta point of view, the second axiom set is only ever going to increase the number of Ns after starting from a set of premises. Therefore I don't think that it will be able to prove CNNpp.

It is well known that Simplification and Frege are theorems of intuitionistic propositional calculus. They will hence be satisfied by any Kripke structure. We write $(P,\le)$ in place of Wikipedia's $(W,\le)$ and $v(x)$ in place of $M_x$.

We exhibit a Kripke structure that satisfies CCpqCNqNp while it violates CCNpNqCqp. This proves the inequivalence of the two systems.

The underlying poset will be $\{0,1\}$, with $0 \le 1$. We define $v(0) = \{q\}, v(1) = \{p,q\}$.

First, we will prove that $0 \Vdash \mathsf{CC}pq\mathsf{CN}q\mathsf Np$:

By definition of $\Vdash$, this means showing that for each $x \ge 0$, if $x \Vdash\mathsf Cpq$ then also $x \Vdash\mathsf{CN}q\mathsf Np$.

We check that $0 \Vdash \mathsf Cpq$ and $0\Vdash \mathsf{CN}q\mathsf Np$; by the nature of $\Vdash$ on implication, this implies they hold for $1$, too:

$0 \Vdash \mathsf Cpq$: Whenever $x \Vdash p$ for $x \ge 0$, also $x \Vdash q$ (by $0 \Vdash q$ and the persistency condition, or by explicit checking);
$0 \Vdash \mathsf{CN}q\mathsf Np$: For each $x \ge 0$, $x \not\Vdash \mathsf Nq$, making the implication vacuously true.

Now, we verify that $0 \not\Vdash \mathsf{CCN}p\mathsf Nq\mathsf Cqp$:

$0 \not\Vdash \mathsf Np$ and $1 \not\Vdash \mathsf Np$, since $1 \Vdash p$; hence $0 \Vdash \mathsf{CN}p\mathsf Nq$; but clearly $0 \not\Vdash \mathsf Cqp$, since $0\Vdash q$ but $0 \not\Vdash p$.

Hence $0 \not\Vdash\mathsf{CCN}p\mathsf Nq\mathsf Cqp$.

NB. This Kripke structure with two points is the "smallest" instance of the failing of Double Negation Elimination: $0 \Vdash \mathsf{NNp}$ but $0 \not\Vdash p$ (of course, we don't need that $q$ in this case and we may leave it out).

We can define the $(P,\le,v)$-truth value of a proposition $\phi$ by $[\phi]_{P,v} = \{x \in P: x \Vdash \phi\}$ (Caution: I just invented the notation so it is likely not canonical). By persistence, this set is upper closed in $P$; conversely, any upper closed set can arise as $[\phi]_{P,v}$ for suitable $\phi$ and $v$.
We define the overall truth value $\top$ as the whole set $P$. With this definition of truth, Frege and Simplification hold (as they must). We have essentially proved that $\mathsf{CCN}p\mathsf Nq\mathsf Cqp$ is not a tautology in $P$.
• @DougSpoonwood $\Vdash$ is the customary way of denoting $\models$ in Kripke structures; sometimes, one pronounces it "forces". See also the Wikipedia link for a full definition. I'll edit to answer your second question. – Lord_Farin Jun 18 '13 at 6:44
• Huh? Your first line seems wrong. $\mathsf{CN}p\mathsf{N}q = \mathsf{C}10 = 0$. I chose to use intuitionistic logic because the two rules are equivalent in classical logic. (I'm very busy right now so I can't expand my answer to include the analogue of a truth table.) – Lord_Farin Jul 1 '13 at 7:30