tff(semantics, logic, ($alethic_modal) == ([($domains) == ($constant),($designation) == ($rigid),($terms) == ($local),($modalities) == ($modal_system_M)])).

tff(person_decl, type, person: $tType).
tff(product_decl, type, product: $tType).

tff(alex_decl, type, alex: person).
tff(chris_decl, type, chris: person).
tff(leo_decl, type, leo: product).
tff(work_hard_decl, type, work_hard: ((person * product) > $o)).
tff(gets_rich_decl, type, gets_rich: ((person) > $o)).

tff(d_person_decl, type, d_person: $tType).
tff(d2person_decl, type, d2person: d_person > person).
tff(d_person_0_decl, type, d_person_0: d_person).
tff(d_person_1_decl, type, d_person_1: d_person).
tff(d_product_decl, type, d_product: $tType).
tff(d2product_decl, type, d2product: d_product > product).
tff(d_product_0_decl, type, d_product_0: d_product).

tff(world_0_decl, type, world_0: $world).
tff(world_1_decl, type, world_1: $world).
tff(world_2_decl, type, world_2: $world).
tff(world_3_decl, type, world_3: $world).
tff(world_4_decl, type, world_4: $world).

tff(model_worlds, interpretation-worlds, 
((! [W: $world] : ( (W = world_0) | (W = world_1) | (W = world_2) | (W = world_3) | (W = world_4) ))
& $distinct(world_0, world_1, world_2, world_3, world_4)
& ($local_world = world_0)
& (! [W: $world, V: $world]: $accessible_world(W, V))
)).

tff(model_domains, interpretation-domains,
($distinct(d_person_0, d_person_1)
& (! [W: $world]: ($in_world(W,
	((! [O: person]: (? [DO: d_person]: O = d2person(DO)))
	& (! [DO1: d_person, DO2: d_person]: ( (d2person(DO1) = d2person(DO2)) => (DO1 = DO2) ))
	& (! [DO: d_person]: ( (DO = d_person_0) | (DO = d_person_1) ))
	& (? [DO: d_person]: (DO = d_person_0))
	& (? [DO: d_person]: (DO = d_person_1))))))

& (! [W: $world]: ($in_world(W,
	((! [O: product]: (? [DO: d_product]: O = d2product(DO)))
	& (! [DO1: d_product, DO2: d_product]: ( (d2product(DO1) = d2product(DO2)) => (DO1 = DO2) ))
	& (! [DO: d_product]: ( (DO = d_product_0) ))
	& (? [DO: d_product]: (DO = d_product_0))))))
)).


tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	((alex = d2person(d_person_0))
	& (chris = d2person(d_person_1))
	& (leo = d2product(d_product_0))
	& (! [V1: person, V2: product]: work_hard(V1, V2))
	& (! [V1: person]: ~(gets_rich(V1)))))
& $in_world(world_1,
	((alex = d2person(d_person_0))
	& (chris = d2person(d_person_1))
	& (leo = d2product(d_product_0))
	& (! [V1: person, V2: product]: work_hard(V1, V2))
	& (! [V1: person]: ~(gets_rich(V1)))))
& $in_world(world_2,
	((alex = d2person(d_person_0))
	& (chris = d2person(d_person_1))
	& (leo = d2product(d_product_0))
	& (! [V1: person, V2: product]: work_hard(V1, V2))
	& (! [V1: person]: ~(gets_rich(V1)))))
& $in_world(world_3,
	((alex = d2person(d_person_0))
	& (chris = d2person(d_person_1))
	& (leo = d2product(d_product_0))
	& (! [V1: person, V2: product]: work_hard(V1, V2))
	& (! [V1: person]: ~(gets_rich(V1)))))
& $in_world(world_4,
	((alex = d2person(d_person_0))
	& (chris = d2person(d_person_1))
	& (leo = d2product(d_product_0))
	& (! [V1: person, V2: product]: work_hard(V1, V2))
	& gets_rich(d2person(d_person_1))
	& gets_rich(d2person(d_person_0))))
)).