tff('s4_md_n.0017', logic, ($modal) == ([($modalities) == ($modal_system_S4)])).


tff(p1_decl, type, p1: $o).
tff(p2_decl, type, p2: $o).


tff(world_0_decl, type, world_0: $world).

tff(model_worlds, interpretation-worlds, 
((! [W: $world] : ( (W = world_0) ))
& ($local_world = world_0)
& (! [W: $world, V: $world]: $accessible_world(W, V))
)).

tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	(~p1
	& ~p2))
)).