Holes

Up: Corpus of Examples
Previous: Fitting
Next: Kinematics

Definition HOLES.D1

Let region RH be a subset of region R. Surface S is an outlet of RH from R if S is a surface thickly connected component of boundary(RH) intersect boundary(R).

Declaration:
outlet(S: surface; RH,R : region) -- Predicate.

Formalism:
outlet(S,RH,R) < = > surf_tcc(S,boundary(RH) intersect boundary(R))

Definition HOLES.D2

Let region RH be a subset of region R. RH extends through R if RH has at least two outlets from R.

Declaration:
extends_through(RH, R : region)

Formalism: extends_through(RH,R) < = >
exists(SU1,SU2 : surface) outlet(SU1,RH,R) ^ outlet(SU2,RH,R) ^ SU1 != SU2.

Definition HOLES.D3

Let R and RF be regions, and let RHS be a set of regions. RHS is the set of holes through R relative to filling-in RF if:

RF = the union of R with the union of the elements of RHS.
R is externally connected to each of the elements of RHS.
Each element of RHS extends through RF
The union of any two elements of RHS is not thickly connected.

Note that the set of holes depends on both R and RF, not just on R.

Declaration: holes(RHS : set[region]; R, RF : region)

Formalism:
holes(RHS,R,RF) < = >
rcc_TPP(R,RF) ^ RF = R union set-union(RHS) ^ [forall(RH in RHS) rcc_EC(RH,R)] ^
[forall(RH in RHS) extends_though(RH,RF)] ^
[forall(RH1, RH2 in RHS) RH1 !=RH2 => ~thickly_connected(RH1 union RH2)].

Citation: See Varzi and Cassati, Holes for a fascinating discussion of holes, particularly individuation criteria.

Fact HOLES.F1

Let R be a region. Let SS be a set of surface patches in the boundary of R such that no two elements of SS have a surface thickly connected union. Then there exists a region RH whose outlets from R are equal to SS.

Characteristics: Topology.

Formalism:
forall(R : region; SS: set[surface])
[[forall(S in SS) PP(S,boundary(R))] ^
[forall(S1,S2 in SS) S1 != S2 => ~surf_tcc(S1 union S2)]] =>
exists(RH) extends_through(RH,R) ^ SS = \{ S | outlet(S,RH,R) \}

Definition HOLES.D4

Surface S slices through region RR splitting it into pieces R1 and R2 if R=R1 union R2 and S is the unique surface thickly connected component of boundary(R1) intersect boundary(R2).

Declaration
slices(S : surface; RR, R1, R2 : region) -- Predicate.

Formalism
slices(S,RR,R1,R2) < = >
RR = R1 union R2 ^
[forall(S1 : surface) surf_tcc(S1,boundary(R1) intersect boundary(R2)) < = > S1=S]

Definition HOLES.D5

Let O be a generalized object and let POH, POSU1, POSU2 be pseudo-objects with the same source, where POSU1 and POSU2 are outlets of POH. The event of O going through hole POH of POR, entering through surface POSU1 and exiting at surface POSU2, occurs in history H if the following conditions hold:

At start(H), O meets POSU1, but O does not intersect with interior(POH).
At end(H), O meets POSU2, but O does not intersect with interior(POH).
At all intermediate times, O intersects interior(POH).

Declaration:
goes_through(O ; g_object; POH : pseudo-object[region], POSU1, POSU2 : pseudo-object[surface]) : event -- Function.

Formalism:
occurs(H,goes_through(O,POH,POSU1,POSU2)) < = >
source(POSU1) = source(POSU2) = source(POH) != source(O) ^
[exists(POX) outlet(POSU1,POH,POX) ^ outlet(POSU2,POH,POX)] ^
holds(start(H),C^*(O,POSU1)) ^ holds(end(H),C^*(O,POSU2)) ^ forall(S in H) start(H) < S < end(H) => holds(S,C^*(O,interior⁺(POH))

Fact HOLES.F2

(Monotonicity of goes_through under inclusion.) If OG goes through POH in H and OX remains in OG throughout H, then OX goes through POH in some subhistory of H.

Characteristics: Topology -- time.

Formalism:
forall [occurs(H,goes_through(O,POH,POS1,POS2)) ^ forall(S in H) holds(S,P^*(OX :g_object,O))] =>
exists(H1) subhistory(H1,H) ^ occurs(H1,goes_through(OX,POH,POS1,POS2)).

Fact HOLES.F3

If O goes through POH from POS1 to POS2 in H, then O goes through POH from POS2 to POS1 in the reversal of H.

Characteristics: Topology -- time.

Formalism:
occurs(H,goes_through(O,POH,POS1,POS2)) => occurs(reverse(H),goes_through(O,POH,POS2,POS1)).

Fact HOLES.F4

Suppose that in history H, object O goes through POH entering at POS1 and exiting at POS2. Suppose that surface POSM slices POH into two parts: POR1 which contains POS1 and POR2 which contains POS2. Then, there is a subhistory of H in which O goes through POR1 entering POS1 and exiting POSM and a subhistory of H in which O goes through POR2 entering POSM and exiting POS2.

Characteristics: Topology -- time.

Formalism:
[occurs(H,goes_through(O,POH,POS1,POS2)) ^ slices(POSM, POH, POR1, POR2 : g_object) ^ P(POS1,boundary(POR1)) ^ P(POS2,boundary(POR2))] =>
exists(H1,H2) subhistory(H1,H) ^ subhistory(H2,H) ^ occurs(H1,goes_through(O,POR1,POS1,POSM)) ^ occurs(H2,goes_through(O,POR2,POSM,POS2))

Definition HOLES.D6

Object O fits through POH entering at POS1 and exiting at POS2.

Declaration: fits_through(O ; g_object; POH : pseudo-object[region], POSU1, POSU2 : pseudo-object[surface]) -- Predicate.

Formalism: fits_through(O,POH,POS1,POS2) < = >
exists(H) occurs(H,goes_through(O,POH,POS1,POS2)).

Fact HOLES.F5:

(Sufficient condition for "fits_through".) If the hole POH is a right prism, and POS1 and POS2 are the top and bottom, and some projection of O fits inside POS1 then O fits through POH from POS1 to POS2.

Characteristics: Geometry -- time.

Formalism:
[right_prism(POH,POSU1,POSU2) ^ fits1(projection(O,PS1),POSU1) =>
fits_through(O,POH,POSU1,POSU2).

Fact

(Necessary condition for "fits_through"). If O fits through POH from POS1 to POS2 and O contains a sphere of radius D, then some projection of POS1 must contain a circle of radius D.

Characteristics: Geometry.

Formalism:

fits_through(O,POH,POS1,POS2) ^ fits1(sphere(D),O) => exists(L) fits1(circle(D),projection(OS1,L))

Comment: I haven't been able to prove this, and so am not sure it's true. It seems plausible.