https://dl.dropbox.com/u/34693999/nonobv.pdf
Rob, I like your 2nd proof (although I think your 4 cases are about P and not
P, instead of P and Q), and it got me thinking, and I now have some
understanding of Los's Logic problem. The problem with Los's result is it
makes no sense: P is symmetric and transitive, Q is transitive, P or Q is true,
show either all P or all Q. Our reaction is What is going on??? That's why
it's so impressive you solved it. But I made some progress understanding it:
The result is almost about entirely about P, with Q almost being ~P. So let's
prove the case special case Q = ~P first. That turns out to have a
comprehensible proof! Then we just have to fiddle with the proof a bit to
handle the general case. Below is my miz3 proof of Los's Logic result, to a
large extent a modification of your 2nd proof.
--
Best,
Bill
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let SymTransImpliesSkewTrans_THM = thm `;
let P be A->A->bool;
assume ∀ x y z. P x y ∧ P y z ⇒ P x z [Ptrans];
assume ∀x y. P x y ⇒ P y x [Psym];
thus ∀ x y z. P x y ∧ ¬P y z ⇒ ¬P x z
proof
∀ x y z. P y x ∧ ¬P y z ⇒ ¬P x z by Ptrans;
qed by -, Psym`;;
(* That was an comprehensible result I detected in your proof. The next result
solves Los's problem in case Q = ~P. *)
let RobLosPnotP_THM = thm `;
let P be A->A->bool;
assume ∀ x y z. P x y ∧ P y z ⇒ P x z [Ptrans];
assume ∀ x y z. ¬P x y ∧ ¬P y z ⇒ ¬P x z [notPtrans];
assume ∀x y. P x y ⇒ P y x [Psym];
thus (∀x y. P x y) ∨ (∀x y. ¬P x y)
proof
∀ x y z. P x y ∧ ¬P y z ⇒ ¬P x z by Ptrans, Psym,
SymTransImpliesSkewTrans_THM;
∀ x y z. ¬P y z ⇒ ¬P x z [almost_done] by -, notPtrans;
assume ¬(∀x y. P x y);
consider a b such that
¬P a b [notPab] by -;
¬P b a [notPba] by -, Psym;
∀x y. ¬P x y
proof
let x y be A;
¬P x a ∧ ¬P y b by notPba, notPab, almost_done;
qed by -, Psym, notPab, notPtrans;
qed by -`;;
(* My proof below of Los's result is more complicated than I'd like, but it's a
straightforward modification of the above comprehensible proof. The MESON
solved at number 108 is a bit lower than the the above proof, and I get a
strange error miz3 message for I believe some step of the proof:
Warning: No useful-looking instantiations of lemma
*)
let LosLogic_THM = thm `;
let P Q be A->A->bool;
assume ∀ x y z. P x y ∧ P y z ⇒ P x z [Ptrans];
assume ∀ x y z. Q x y ∧ Q y z ⇒ Q x z [Qtrans];
assume ∀x y. P x y ⇒ P y x [Psym];
assume ∀x y. P x y ∨ Q x y [PunionQ];
thus (∀x y. P x y) ∨ (∀x y. Q x y)
proof
∀ x y z. ¬P x y ∧ ¬P y z ⇒ Q x z ∧ Q z x [nearnotPtrans] by PunionQ,
Qtrans, Psym;
∀ x y z. P x y ∧ ¬P y z ⇒ ¬P x z ∧ ¬P z x by Ptrans, Psym,
SymTransImpliesSkewTrans_THM, Psym;
∀ x y z. P x y ∧ ¬P y z ⇒ Q x z ∧ Q z x by -, PunionQ;
∀ x y z. ¬P y z ⇒ Q x z ∧ Q z x [good_enough] by nearnotPtrans, -;
assume ¬(∀x y. P x y);
consider a b such that
¬P a b ∧ ¬P b a [notPab] by -, Psym;
Q a b ∧ Q b a [Qab] by -, Psym, PunionQ;
∀x y. Q x y
proof
let x y be A;
Q x a ∧ Q b y by notPab, good_enough;
qed by -, Qab, Qtrans;
qed by -`;;
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
