Hi Bruno, > > Can you give a particular example of a sentence p such that > > B(Bp->p) is true? > Take any proposition you can prove, for example the tautology > (p -> p), or t. (...) > So once you have prove t, all the proposition of the shape > > <anyproposition> -> t > > is easily deducible, by applying modus ponens and the a fortiori axiom. > > In particular Bt -> t is justified. > > And thus B(Bt -> t) is true. (or, by necessitation B(Bt -> t) > follows). > > So an example of such a p making B(Bp -> p) true, is p = t.
But then any proposition of the form B(q->p)->Bp would be true as well. Why is that not an axiom? Further, by your explanation above it seems that the axiom should be more like Bp->B(q->p). Since as I understood it, if you can justify p, then you can justify any sentence of the form q->p. On the other direction, suppose it is justifiable that ~p. That is, B(~p) and I suppose ~Bp with the excluded middle. So it is true that Bp->q for any q, and in particular for q=p. So B(Bp->p). But Bp is false by assumption so B(Bp->p)->Bp is false. What's wrong? Eric.