A set of propositions $S$ is independent if $\forall t \in S$ we have $S-\{t\}\nvdash t$.

The syntactic axioms defined in our logic course are:

1) $\forall p,q \in L : p\Rightarrow (q \Rightarrow p)$

2) $\forall p,q,r \in L : (p\Rightarrow (q \Rightarrow r))\Rightarrow ( (p\Rightarrow q) \Rightarrow (p \Rightarrow r) )$

3) $ \forall p \in L : \neg \neg p \Rightarrow p$

The task is to prove their independence.

If it is too long to prove all three you can give me some hints on how to prove that $ \{1,2\} \nvdash {3}$.

I am new to the concept 'It can't be proved from p and q'; most of the standard results we deduced (completeness, compactness, decidability theorem) use the fact that all three axioms hold.

Edit: I just realised that the use of $\vdash$ is quite controversial in this case. $S \vdash t$ if you can prove t from S and modus ponens.

  • 1
    $\begingroup$ $\vdash$ is not controversial; it clearly means "derive". You should be able to use whatever rules of inference (and metatheorems) are available in your proof system, and using them with two axioms as premises not be able to derive the third. $\endgroup$ – Graham Kemp Jun 19 '18 at 3:02
  • $\begingroup$ Completeness theorem is written as $ \vdash t \Leftrightarrow \vDash t $. $\endgroup$ – George Aliatimis Jun 19 '18 at 3:08
  • $\begingroup$ I don't think that $\vdash$ is the same as the one I am using here. $\endgroup$ – George Aliatimis Jun 19 '18 at 3:09
  • $\begingroup$ What textbook are you using, what type of proof system are you using, etc.? $\endgroup$ – Not_Here Jun 19 '18 at 3:12
  • $\begingroup$ for the easiest semantic approach, these are all tautologies in classical logic, but one can find a multivalued logic respected by the deductive system such that 1 and 2 are 'true' in all models but not the third $\endgroup$ – spaceisdarkgreen Jun 19 '18 at 3:14

First an aside, which does have some importance. $\lnot$p in your system abbreviates (p⇒$\bot$). So, ($\lnot$$\lnot$p⇒p) abbreviates 3)' (((p⇒$\bot$)⇒$\bot$)⇒p). This matters, because although, even if all strings get fully parenthesized, {1), 2), 3)'} allows us to deduce all tautologies having ⇒ and $\bot$, but

{1), 2), 3)} does not allow us to deduce all tautologies having ⇒ and $\lnot$.

For example, without the abbreviation, (p⇒($\lnot$p⇒q)) is independent of {1), 2), 3)} (once each one gets parenthesized).

It sometimes works out to set up a model, such as an algebra, for the set of axioms {S$_1$, ..., S$_n$} such that the model satisfies every member of {S$_2$, ..., S$_n$}, but does not satisfy S$_1$.

For your example, let's consider an algebra where ⇒ computes as follows:

($\bot$⇒$\bot$) = $\bot$

($\bot$⇒$\top$) = $\top$

($\top$⇒$\bot$) = $\bot$

($\top$⇒$\top$) = $\bot$

You can check to see that 1) and 2) will always compute to $\bot$. But, suppose that p has truth value of $\top$. Then, (((p⇒$\bot$)⇒$\bot$)⇒p) equals (($\bot$⇒$\bot$)⇒$\top$) which equals ($\bot$⇒$\top$) which equals $\top$. Thus, in such an algebra 1) and 2) will always have truth value of $\bot$, but 3)' will not. So, if the axioms were dependent, a deduction wouldn't necessarily preserve the truth value of the axioms even when only substitution and detachment got used as rules of inference. Since the rules of inference still preserve truth values, there is no way to start with {1), 2)} and deduce 3)'.

I didn't come up with this model myself. I basically converted the axioms to a format for a freely available program called Mace4 and it produced the model.

Edit: A different approach:

For the system {1), 2)} the set of most general tautologies derivable are all conditionals without any instance of $\bot$ in them. We can insist that variables always appear in a certain order, since substitution allows us to derive any other tautologies when we do that. Thus, if we suppose that (((p⇒⊥)⇒⊥)⇒p) is derivable from some tautology Q it will have to come as derivable by substitution of variable(s) in Q only where Q has only "p", parentheses, and ⇒ in it. That leaves us with a number of possible candidates for Q:

  1. Q is (((p⇒q)⇒r)⇒s). But, this is not a tautology.
  2. Q is (((p⇒q)⇒r)⇒r). But, if r is false, and p is false, this is false also.
  3. Q is (((p⇒q)⇒r)⇒q). But, if r is false, q is false, and p is false, this is false also.
  4. Q is (((p⇒q)⇒r)⇒p). Again, if p, q, and r are false, this is false.
  5. Q is (((p⇒q)⇒q)⇒r). This is not a tautology since no tautologies have a variable which appears in the consequent which does not appear in the antecedent.
  6. Q is (((p⇒q)⇒q)⇒q). But, if p is true, and q false, this is false.
  7. Q is (((p⇒q)⇒q)⇒p). If q is false, and p is false, this is false.
  8. Q is (((p⇒q)⇒p)⇒r). This is not a tautology due to reason used in 5.
  9. Q is (((p⇒q)⇒q)⇒q). If p is true, and q is false, this is false.
  10. Q is (((p⇒q)⇒q)⇒p). If both p and q are false, then this is false.
  11. Q is (((p⇒q)⇒p)⇒r). See 5.
  12. Q is (((p⇒q)⇒p)⇒q). If p is true, and q is false, this is false.
  13. Q is (((p⇒q)⇒p)⇒p). This is a tautology, but (((p⇒$\bot$)⇒$\bot$)⇒p) is not obtainable by substitution from this.
  14. Q is (((p⇒p)⇒q)⇒r). But, we can't obtain (((p⇒$\bot$)⇒$\bot$)⇒p) from this by substitution, since any substitution for p has to apply to both instances of p. The rest of the cases are similar to this one.

So, 3)' is not derivable from {1), 2)}.

  • $\begingroup$ @George Aliatimis I updated my answer to include a different approach. $\endgroup$ – Doug Spoonwood Jun 19 '18 at 16:08
  • 1
    $\begingroup$ The first method is not right. "Since the rules of inference used will always preserve truth values no matter what sort of model, or algebra, you pick to interpret them..." No. When you change the interpretation of logical symbols you change what is and what isn't a truth-preserving inference rule based on manipulation of those symbols. Here you have changed the meaning of $\Rightarrow$ and so (may) have changed whether MP preserves truth. The second works, though it has a few errors and doesn't need to be that complicated. (Also I don't think the method generalizes to the other independences) $\endgroup$ – spaceisdarkgreen Jul 1 '18 at 0:26
  • $\begingroup$ @spaceisdarkgreen Thanks, I've updated it. Specifically, modus ponens and substitution still preserve truth values. If (p$\rightarrow$q) has truth value of $\bot$ and p has truth value of $\bot$, q will have truth value of $\bot$. $\endgroup$ – Doug Spoonwood Jul 1 '18 at 15:58
  • $\begingroup$ Okay, I thought your example didn't work as well, but I guess I got mixed up. $\endgroup$ – spaceisdarkgreen Jul 2 '18 at 1:38

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.