Nuprl Definition : free-from-atom
The type ⌜a#x:T⌝ is inhabited (by ⌜Ax⌝)
iff there exists a token "a" and a term y such that a = "a" in Atom{$n} and x = y in T
such that token "a" does not occur in y.
Thus a#x:T is true iff a is an atom and there is some member of the equivalence class of x in T
that is free from a.
To see that this defines a type, we note that if a1 = a2 in Atom{n}, then there is a unique token "a" such that
"a" = a1 = a2 in Atom{n}, and if T1 = T2 in Universe{i} and x1 = x2 in T1,
then any y such that x1 = y in T1 and "a" does not occur in y also satisfies
x2 = y in T2 and "a" does not occur in y.
Thus we justify the rule for equality: freeFromAtomEquality .
One base case is ⌜a#a:Atom$n⌝ where a ∈ Atom$n. This is not inhabited because every term y = a in Atom$n
must mention the token "a" = a (otherwise we could permute ("a","b") and get y = "b" and hence "b"="a").
Since ⌜a#a:Atom$n⌝ is not a type unless ⌜a ∈ Atom$n⌝, if we have ⌜a#a:Atom$n⌝ as a hypothesis in a sequent
then a ∈ Atom$n, then since a#a:Atom$n is not inhabited, the sequent is trivially true.
We thus have the "absurdity rule"" freeFromAtomAbsurdity .
Another base case is that if ⌜atom-free{$n:n}(T; x)⌝ then ⌜Ax ∈ a#x:T⌝. This is because atom-free{$n:n}(T; x)
is, by definition,
∀a,b:Atom$n. (swap-atoms{$n:n}(a; b; x) = x)
, so we may choose b to be "fresh" w.r.t. x (i.e. an atom not occuring in x)
and take y = swap-atoms{$n:n}(a; b; x) = x, then whatever token "a" the atom a evaluates to, will not occur in
swap-atoms{$n:n}(a; b; x).
So, we have the first triviality rule: freeFromAtomTriviality .
The last base case is when x is an atom the is not equal to a. freeFromAtomBase .
Finally, if ⌜a#x:A⌝ and ⌜a#f:u:A ⟶ B[u]⌝ then
then for some token "a", "a" = a in Aton{n}, and there are x' = x in A and
f' = f in u:A ⟶ B[u] such that "a" does not occur in f' or x'.
Then (f' x') = (f x) in B[x], and "a" does not occur in f' x'. Therefore, ⌜a#f x:B[x]⌝.
So we have shown that the application rule freeFromAtomApplication is true.
Note that the contrapositive of the application rule in the form
⌜(¬a#f x:B[x]) ⇒ ((¬a#f:u:A ⟶ B[u]) ∨ (¬a#x:A))⌝ will not be constructively true.
We define ⌜inheres{n:n}(T; x; a)⌝ to be the negation, ⌜¬a#x:A⌝, and we read it as "a is inherent in x:T".
It says that it is not possible to find a representative of x in T which avoids "a", i.e. that
every member of the equivalence class of x in T must mention the atom a.
Now, if f x must mention a, there can't be representatives f' and x' of f and x which don't mention a,
so at least one of f or x has no such representative. But since the number of possible representatives is
infinite, we can't in general decide which of them has this property.
So we don't have ⌜inheres{n:n}(B[x]; f x; a) ⇒ (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝ in general.
We tried to define inherence as ⌜inheres{$n:n}(T; x; a) == ∃g:T ⟶ 𝔹. (↑matters{$n:n}(a; g; x))⌝ where
⌜matters{$n:n}(a; g; x)⌝ (read as "matters"(a,g,x))
was a boolean (provided ⌜atom-free{n:n}(Type; T)⌝) defined by (nu b. ⌜¬bg x =b g swap-atoms{n:n}(a; b; x)⌝).
Here, nu b. X[b] means choose a fresh atom b not occring in X and evaluate X[b] to normal form (a boolean in our case)
and evalute to that normal form if it does not mention the fresh b and diverge otherwise.
From this definition we could prove (for types that were atom-free) the strong application inherence property
⌜inheres{n:n}(B[x]; f x; a) ⇒ (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝
from a purported property of "matters" called
"conservation of matters". Unfortunately, the "conservation of matters" property is not true, as shown by the following
counter-example.
Let g <x,y> = ⌜¬b(x =a y ∧b (¬bx =a "a"))⌝,
let f = ⌜λx.<"a", x>⌝,
let x = "a".
Then g (f x) = g <"a","a"> = ⌜tt⌝.
Any tokens "b", "c" different from "a" do not occur in "a",g,f, or x, and
g (f swap-atoms{$n:n}(a; b; x)) = g <"a","b"> = ⌜tt⌝
g (swap-atoms{$n:n}(a; b; f) x) = g <"b","a"> = ⌜tt⌝
g (swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; c; x)) = g <"b","c"> = ⌜tt⌝, but
g (swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; b; x) ) = g <"b","b"> = ⌜ff⌝.
This example show that it is possible that
⌜(↑matters{$n:n}(a; g; f x))
∧ (¬↑matters{$n:n}(a; λX.(g (f X)); x))
∧ (¬↑matters{$n:n}(a; λF.(g (F x)); f))
∧ (¬↑matters{$n:n}(a; λF.matters{$n:n}(a; λX.(g (F X)); x); f))⌝
whereas "conservation of matters" purported to show that
⌜(↑matters{$n:n}(a; g; f x)) ⇒ (((↑matters{$n:n}(a; λX.(g (f X)); ...)) ∨ ...) ∨ ...)⌝...
a#x:T == PRIMITIVE
Rules referencing :
freeFromAtomEquality,
freeFromAtomAbsurdity,
freeFromAtomTriviality,
freeFromAtomBase,
freeFromAtom1Atom2,
freeFromAtomApplication,
freeFromAtomSet,
freeFromAtomAxiom
FDL editor aliases :
free-from-atom
Latex:
a\#x:T == PRIMITIVE
Date html generated:
2016_07_08-PM-04_46_51
Last ObjectModification:
2013_05_31-PM-02_44_21
Theory : atom_1
Home
Index