%------------------------------------------------------------------------------ % File : PUZ087^1 : TPTP v7.1.0. Released v4.0.0. % Domain : Logic Calculi (Espistemic logic) % Problem : Wise men puzzle % Version : [Ben09] axioms. % English : Once upon a time, a king wanted to find the wisest out of his % three wisest men. He arranged them in a circle and told them that % he would put a white or a black spot on their foreheads and that % one of the three spots would certainly be white. The three wise % men could see and hear each other but, of course, they could not % see their faces reflected anywhere. The king, then, asked to each % of them to find out the colour of his own spot. After a while, the % wisest correctly answered that his spot was white. % Refs : [Gol92] Goldblatt (1992), Logics of Time and Computation % : [Bal98] Baldoni (1998), Normal Multimodal Logics: Automatic De % : [Ben09] Benzmueller (2009), Email to Geoff Sutcliffe % Source : [Ben09] % Names : mmex4.p [Ben09] % Status : Theorem % Rating : 0.62 v7.0.0, 0.71 v6.4.0, 0.67 v6.3.0, 0.60 v6.2.0, 0.71 v6.1.0, 0.86 v5.5.0, 0.83 v5.4.0, 0.80 v5.1.0, 1.00 v5.0.0, 0.80 v4.1.0, 0.67 v4.0.0 % Syntax : Number of formulae : 101 ( 0 unit; 37 type; 31 defn) % Number of atoms : 571 ( 36 equality; 164 variable) % Maximal formula depth : 11 ( 6 average) % Number of connectives : 439 ( 4 ~; 4 |; 8 &; 415 @) % ( 0 <=>; 8 =>; 0 <=; 0 <~>) % ( 0 ~|; 0 ~&) % Number of type conns : 197 ( 197 >; 0 *; 0 +; 0 <<) % Number of symbols : 41 ( 37 :; 0 =) % Number of variables : 101 ( 3 sgn; 29 !; 6 ?; 66 ^) % ( 101 :; 0 !>; 0 ?*) % ( 0 @-; 0 @+) % SPC : TH0_THM_EQU_NAR % Comments : %------------------------------------------------------------------------------ %----Include embedding of quantified multimodal logic in simple type theory include('Axioms/LCL013^0.ax'). %------------------------------------------------------------------------------ thf(a,type,( a: $i > $i > $o )). thf(b,type,( b: $i > $i > $o )). thf(c,type,( c: $i > $i > $o )). thf(fool,type,( fool: $i > $i > $o )). thf(ws,type,( ws: ( $i > $i > $o ) > $i > $o )). thf(axiom_1,axiom, ( mvalid @ ( mbox @ fool @ ( mor @ ( ws @ a ) @ ( mor @ ( ws @ b ) @ ( ws @ c ) ) ) ) )). thf(axiom_2_a_b,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( ws @ a ) @ ( mbox @ b @ ( ws @ a ) ) ) ) )). thf(axiom_2_a_c,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( ws @ a ) @ ( mbox @ c @ ( ws @ a ) ) ) ) )). thf(axiom_2_b_a,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( ws @ b ) @ ( mbox @ a @ ( ws @ b ) ) ) ) )). thf(axiom_2_b_c,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( ws @ b ) @ ( mbox @ c @ ( ws @ b ) ) ) ) )). thf(axiom_2_c_a,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( ws @ c ) @ ( mbox @ a @ ( ws @ c ) ) ) ) )). thf(axiom_2_c_b,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( ws @ c ) @ ( mbox @ b @ ( ws @ c ) ) ) ) )). thf(axiom_3_a_b,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( mnot @ ( ws @ a ) ) @ ( mbox @ b @ ( mnot @ ( ws @ a ) ) ) ) ) )). thf(axiom_3_a_c,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( mnot @ ( ws @ a ) ) @ ( mbox @ c @ ( mnot @ ( ws @ a ) ) ) ) ) )). thf(axiom_3_b_a,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( mnot @ ( ws @ b ) ) @ ( mbox @ a @ ( mnot @ ( ws @ b ) ) ) ) ) )). thf(axiom_3_b_c,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( mnot @ ( ws @ b ) ) @ ( mbox @ c @ ( mnot @ ( ws @ b ) ) ) ) ) )). thf(axiom_3_c_a,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( mnot @ ( ws @ c ) ) @ ( mbox @ a @ ( mnot @ ( ws @ c ) ) ) ) ) )). thf(axiom_3_c_b,axiom, ( mvalid @ ( mbox @ fool @ ( mimplies @ ( mnot @ ( ws @ c ) ) @ ( mbox @ b @ ( mnot @ ( ws @ c ) ) ) ) ) )). thf(t_axiom_for_fool,axiom, ( mvalid @ ( mforall_prop @ ^ [A: $i > $o] : ( mimplies @ ( mbox @ fool @ A ) @ A ) ) )). thf(k_axiom_for_fool,axiom, ( mvalid @ ( mforall_prop @ ^ [A: $i > $o] : ( mimplies @ ( mbox @ fool @ A ) @ ( mbox @ fool @ ( mbox @ fool @ A ) ) ) ) )). thf(i_axiom_for_fool_a,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ fool @ Phi ) @ ( mbox @ a @ Phi ) ) ) )). thf(i_axiom_for_fool_b,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ fool @ Phi ) @ ( mbox @ b @ Phi ) ) ) )). thf(i_axiom_for_fool_c,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ fool @ Phi ) @ ( mbox @ c @ Phi ) ) ) )). thf(a7_axiom_for_fool_a_b,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ a @ Phi ) @ ( mbox @ b @ ( mbox @ a @ Phi ) ) ) ) )). thf(a7_axiom_for_fool_a_c,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ a @ Phi ) @ ( mbox @ c @ ( mbox @ a @ Phi ) ) ) ) )). thf(a7_axiom_for_fool_b_a,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ b @ Phi ) @ ( mbox @ a @ ( mbox @ b @ Phi ) ) ) ) )). thf(a7_axiom_for_fool_b_c,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ b @ Phi ) @ ( mbox @ c @ ( mbox @ b @ Phi ) ) ) ) )). thf(a7_axiom_for_fool_c_a,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ c @ Phi ) @ ( mbox @ a @ ( mbox @ c @ Phi ) ) ) ) )). thf(a7_axiom_for_fool_c_b,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mbox @ c @ Phi ) @ ( mbox @ b @ ( mbox @ c @ Phi ) ) ) ) )). thf(a6_axiom_for_fool_a_b,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mnot @ ( mbox @ a @ Phi ) ) @ ( mbox @ b @ ( mnot @ ( mbox @ a @ Phi ) ) ) ) ) )). thf(a6_axiom_for_fool_a_c,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mnot @ ( mbox @ a @ Phi ) ) @ ( mbox @ c @ ( mnot @ ( mbox @ a @ Phi ) ) ) ) ) )). thf(a6_axiom_for_fool_b_a,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mnot @ ( mbox @ b @ Phi ) ) @ ( mbox @ a @ ( mnot @ ( mbox @ b @ Phi ) ) ) ) ) )). thf(a6_axiom_for_fool_b_c,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mnot @ ( mbox @ b @ Phi ) ) @ ( mbox @ c @ ( mnot @ ( mbox @ b @ Phi ) ) ) ) ) )). thf(a6_axiom_for_fool_c_a,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mnot @ ( mbox @ c @ Phi ) ) @ ( mbox @ a @ ( mnot @ ( mbox @ c @ Phi ) ) ) ) ) )). thf(a6_axiom_for_fool_c_b,axiom, ( mvalid @ ( mforall_prop @ ^ [Phi: $i > $o] : ( mimplies @ ( mnot @ ( mbox @ c @ Phi ) ) @ ( mbox @ b @ ( mnot @ ( mbox @ c @ Phi ) ) ) ) ) )). thf(axiom_4,axiom, ( mvalid @ ( mnot @ ( mbox @ a @ ( ws @ a ) ) ) )). thf(axiom_5,axiom, ( mvalid @ ( mnot @ ( mbox @ b @ ( ws @ b ) ) ) )). thf(conj,conjecture, ( mvalid @ ( mbox @ c @ ( ws @ c ) ) )). %------------------------------------------------------------------------------