0
$\begingroup$

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)
$\endgroup$
  • 1
    $\begingroup$ If thos are your axioms, what are your rules of inference? $\endgroup$ – Hagen von Eitzen Jun 17 '13 at 16:49
  • $\begingroup$ 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. $\endgroup$ – Lord_Farin Jun 17 '13 at 18:45
2
$\begingroup$

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).


Addendum in response to comment:

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$.

$\endgroup$
  • $\begingroup$ What does "⊩" mean? Also, does your proof give you a way to show some (multi-valued) structure for which CCpqCNqNp always equals the truth value used for truth, but CCNpNqCqp does not equal that truth value (while Frege and Simplification still hold)? If so, could you exhibit it? Thanks in advance, for your time. $\endgroup$ – Doug Spoonwood Jun 17 '13 at 23:39
  • $\begingroup$ @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. $\endgroup$ – Lord_Farin Jun 18 '13 at 6:44
  • $\begingroup$ I found a model using Mace4 cs.unm.edu/~mccune/mace4, which I've just learned about. Define C such that C00=C01=C11=1, C10=0, and N such that N0=N1=0. Then let q=1, p=0. CNpNq=C00=1, while Cqp=C10=0. So, CCNpNqCqp=0. But, since CNqNp=C00=1, CCpqCNqNp=1. Thus, we can't derive the first postulate set here given the second postulate set. $\endgroup$ – Doug Spoonwood Jul 1 '13 at 3:03
  • $\begingroup$ 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.) $\endgroup$ – Lord_Farin Jul 1 '13 at 7:30
  • $\begingroup$ For this model N(0)=0 and N(1)=0. So, for all x we can replace Nx with 0. Thus, CNpNq=C00=1. $\endgroup$ – Doug Spoonwood Jul 1 '13 at 11:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.