1
$\begingroup$

Can someone provide me with hints for, or a rough sketch of, a proof of ~~P from P in the Hilbert system? I had very little trouble proving the reverse, that P is provable from ~~P, but seem to be totally stuck on this guy. My axioms are the following:

φ->(ψ->φ) (1)

[φ->(ψ->χ)]->[(φ->ψ)->(φ->χ)] (2)

(~ψ->~φ)->[(~ψ->φ)->ψ] (3)

and my one rule of inference is modus ponens.

I am also allowed to work with tools like ex falso quodlibet, transitivity, weakening the consequent, etc.

Any help would be greatly appreciated; thank you!

$\endgroup$
1
  • $\begingroup$ This short proof uses contraposition as an axiom. You might find it easier to prove $(\neg a \implies \neg b)\implies (b \implies a)$ instead of $\neg \neg a \implies a$. $\endgroup$ – Przemek Oct 1 '17 at 14:43
1
$\begingroup$

You say you can derive $P$ from $\neg \neg P$. Using the Deduction theorem, you can therefore prove $\neg \neg P \rightarrow P$. And that means that we can use $\neg \neg \varphi \rightarrow \varphi$ as a Lemma.

Now, let's show that $\neg \psi \rightarrow \neg \varphi, \varphi \vdash \psi$:

  1. $\neg \psi \rightarrow \neg \varphi$ Premise
  2. $\varphi$ Premise
  3. $\varphi \rightarrow (\neg \psi \rightarrow \varphi)$ Axiom 1
  4. $\neg \psi \rightarrow \varphi$ MP 2,3
  5. $(\neg \psi \rightarrow \neg \varphi) \rightarrow ((\neg \psi \rightarrow \varphi) \rightarrow \psi$ Axiom 3
  6. $(\neg \psi \rightarrow \varphi) \rightarrow \psi$ MP 1,5
  7. $\psi$ MP 4,6

Using the Deduction Theorem, that means we can also prove $(\neg \psi \rightarrow \neg \phi) \rightarrow (\varphi \rightarrow \psi)$ (this statement is usually used as the third axiom in the Hilbert System ... so let's call it Axiom 3')

OK, so then:

  1. $P$ Premise
  2. $\neg \neg \neg P \rightarrow \neg P$ Lemma
  3. $(\neg \neg \neg P \rightarrow \neg P) \rightarrow (P \rightarrow \neg \neg P)$ Axiom 3'
  4. $P \rightarrow \neg \neg P$ MP 2,3
  5. $\neg \neg P$ MP 1,4
$\endgroup$
4
  • $\begingroup$ Thank you Bram28, this makes sense. My only question is in regard to step 3: how are you getting this, using the third axiom? $\endgroup$ – Juliam Oct 1 '17 at 15:20
  • $\begingroup$ I think he switched the third lemma from $(A \to (B \to C)) \to \dots$ to $(B \to (A \to C)) \to \dots$ which is correct but requires generous application of the deduction theorem (using the fact that $A,B \vdash C$ is the same as $B,A \vdash C$) $\endgroup$ – DanielV Oct 1 '17 at 15:58
  • $\begingroup$ @Juliam Oh! My bad ... The Hilbert system is usually presented with $(\neg \psi \rightarrow \neg \varphi) \rightarrow (\varphi \rightarrow \psi)$ as the third axiom, so that's what I used .. OK, let me edit my post! $\endgroup$ – Bram28 Oct 2 '17 at 0:03
  • $\begingroup$ Sorry I meant second axiom not third axiom. $\endgroup$ – DanielV Oct 2 '17 at 0:38
0
$\begingroup$

Here's a computer generated rough sketch of a detachment based proof. I used the theorem prover, Prover9, which is freely available online courtesy of Argonne National Laboratory near Chicago. You'll need to find the substitution instances of axioms and theorems in order to fill in the details. I used '~' instead of $\lnot$ as a symbol. I didn't use any strategy whatsoever. I merely embedded the axioms into the first-order context appropriate for the theorem-prover and used "-P(x-> y) | -P(x) | P(y)." since under hyperressolution (the hyper referenced in the proof) it behaves like condensed detachment does in propositional calculus:

% -------- Comments from original proof -------- 
% Proof 1 at 0.03 (+0.00) seconds. 
% Length of proof is 17. 
% Level of proof is 7. 
% Maximum clause weight is 20. 
% Given clauses 48.

1 P(~(~(x)) -> x) # label(non_clause) # label(goal).  [goal]. 
2 -P(x-> y) | -P(x) | P(y).  [assumption]. 
3 P(x -> (y -> x)).  [assumption]. 
4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))). [assumption]. 
5 P((~(x) -> ~(y)) -> ((~(x) -> y) -> x)). [assumption]. 
6 -P(~(~(c1)) -> c1).  [deny(1)]. 
7 P(x -> (y -> (z ->> y))).  [hyper(2,a,3,a,b,3,a)]. 
8 P(((x -> (y -> z)) -> (x -> y)) ->((x -> (y -> z)) -> (x -> z))).  [hyper(2,a,4,a,b,4,a)]. 
10 P((x -> y)-> (x -> x)).  [hyper(2,a,4,a,b,3,a)]. 
11 P(((~(x) -> ~(y)) -> (~(x) -> y)) -> ((~(x) -> ~(y)) -> x)).  [hyper(2,a,4,a,b,5,a)]. 
17 P(x -> x).  [hyper(2,a,10,a,b,7,a)]. 
20 P(x -> (y -> y)). [hyper(2,a,3,a,b,17,a)]. 
27 P((x -> ((y -> x) -> z)) -> (x -> z)). [hyper(2,a,8,a,b,7,a)]. 
71 P((~(x) -> ~(~(x))) -> x). [hyper(2,a,11,a,b,20,a)]. 
77 P(x -> ((~(y) -> ~(~(y))) -> y)). [hyper(2,a,3,a,b,71,a)]. 
255 P(~(~(x)) -> x). [hyper(2,a,27,a,b,77,a)]. 
256 $F.  [resolve(255,a,6,a)].

============================== end of proof ==========================
$\endgroup$

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.