Relative to an assignment function, the two-dimensional models of Section 4 evaluate formulas as true or false at pairs of elements of a set W, and so formulas can be understood as interpreted using sets of pairs of elements of W. Several specific ways of interpreting 
based on a binary relation R on W are explored and rejected. The aim of this appendix is to provide the formal basis for generalizations of these arguments. To make these generalizations as strong as possible, 
will be allowed to be interpreted in the most general way which respects the following compositionality constraint: under an assignment function, the interpretation of a formula of the form 
is determined by the interpretation of 
. Thus, each pair 
will be associated with a set of sets of pairs – the set of interpretations of formulas to which 
is to be applied in 
. Such functions are commonly studied under the labels of neighborhood and Scott–Montague semantics. So, define a generalized 2D model to be a structure 
such that W and 
are as in standard 2D models, and 
.
It will be useful to be able to refer easily to the set of pairs at which a given formula is true under a given assignment, so let 
. With this, extend the interpretation of formulas described in Section 4 by the following clause for 
:
iff 
The first result to be established concerns formulas of the language 
including propositional variables and quantifiers. For a class 
of generalized 2D models, let the logic of 
be the set of 
-formulas true at each proper point under each variable assignment in each model in 
. In the following, p will be used to indicate a propositional variable; note that assignment functions map such variables to ‘barcodes’, whereas atomic sentences which are not variables may be interpreted as arbitrary sets of pairs.
Proposition 1: If 
is a class of generalized 2D models whose logic includes all instances of the schemas
(1)
and(2)
,
and
,and is closed under the schematic rule
(3)
/ ,
/ 
, then the logic of 
includes all instances of the schema
(4)
.
.Proof: Consider any formula 
, model 
in 
, 
and assignment function g such that 
; we show that 
. For any formula 
, we write 
for 
being in the logic of 
.
That 
will be shown as follows: We produce an assignment function f which agrees with g on the free variables in 
and a formula 
such that 
and 
. It follows by (1) that 
, and so with the fact that f agrees with g on the free variables in 
that 
. The idea behind the construction of 
and f is to let 
be a conjunction 
, where p is a propositional variable not free in 
which f maps to the barcode true at 
and no other proper point, and 
is a formula interpreted as the set of proper points. We show that 
applies to p and 
at 
, and conclude that it also applies to their conjunction 
, which is true only at 
. Since 
is true there, 
is interpreted as the set of all points, to which 
applies, which completes the the proof.
In more detail, let p be a propositional variable not free in 
, 
, and f the assignment function which differs from g only in that 
. Since 
, it follows with (2) that 
.
To construct 
, let 
, and 
. By the semantics of A, 
, and so by (3), 
; in particular 
. Furthermore, letting 
, 
, and so also 
.
Since the logic of any class of generalized 2D models includes all substitution instances of tautologies and is closed under modus ponens, it is routine to derive the schema 
using (1) and (3). Letting 
, it follows that 
.
. By assumption 
, which is identical to 
since f and g agree on the free variables in 
. So 
. By (3), 
, so 
. Hence 
, and so with (1), 
. Since f and g agree on the free variables in 
, 
. 
Although propositional quantifiers are not explicitly mentioned in the statement of Proposition 1, the proof relies on an application of rule (3) to the quantified formula 
. However, a variant of the result can be established which does not rely on the presence of quantifiers, by considering classes of frames rather than classes of models. Let a generalized 2D frame be a structure 
, with W and D as above; let the quantifier-free logic of a class 
of generalized 2D frames be the set of formulas in the language 
(which omits propositional variables and quantifiers) which are in the logic of the class of generalized 2D models whose underlying frames are in 
.
Proposition 2: For every class 
of generalized 2D frames 
which satisfy
(2*)
only if , for all barcodes b and ,
only if 
, for all barcodes b and 
, if the quantifier-free logic of 
includes all instances of schema (1) and is closed under schematic rule (3), then it includes all instances of schema (4).
Proof: Like the proof of Proposition 1, but using atomic formulas 
and 
not occurring in 
instead of p and 
, respectively, considering a variant interpretation function mapping 
to b and 
to d instead of f, and appealing to (2*) instead of (2). 
Further variants of these two results can immediately be obtained by replacing the requirement of the relevant logic being closed under rule (3) with the requirement of containing all instances of the schemas
(3a)
,(3b)
, and(3c)
.
,
, and
.
