next up previous
Next: Deriving Facts from Counterfactuals Up: Useful Counterfactuals Previous: Axiomatization

Deriving Counterfactuals

Proof: We use the first property of our assignment functions to derive that, in our new world, tex2html_wrap_inline1698 .

tex2html_wrap_inline1698 is a shorthand for the result of equating a term in the frame, tex2html_wrap_inline1702 , to the term tex2html_wrap_inline1704 .

We use the second property of our assignment function a to derive that tex2html_wrap_inline1708 . This follows as tex2html_wrap_inline1689 is in the frame, and tex2html_wrap_inline1708 is true in our current world, so we have that its value persists. We also show that tex2html_wrap_inline1714 in the same way.

We now use the effect axiom to derive that

Finally the definition of tex2html_wrap_inline1458 , which is in the core theory gives us

tex2html_wrap_inline1718

theorem369

Proof: We use the first property of our assignment functions to derive that in our new world, tex2html_wrap_inline1722 as above.

We use the second property of our assignment functions to derive that tex2html_wrap_inline1708 and tex2html_wrap_inline1714 as we did previously.

We now use the frame axiom 18 to derive that

using the given fact that tex2html_wrap_inline1708 and tex2html_wrap_inline1714 . Finally the definition of tex2html_wrap_inline1458 gives us

tex2html_wrap_inline1718


John McCarthy
Wed Jul 12 14:10:43 PDT 2000