Nuprl Definition : free-from-atom

The type ⌜a#x:T⌝ is inhabited (by ⌜Ax⌝
iff there exists token "a" and term such that "a" in Atom{$n} and in 
such that token "a" does not occur in y.

Thus a#x:T is true iff is an atom and there is some member of the equivalence class of in T
that is free from a.

To see that this defines type, we note that if a1 a2 in Atom{n}, then there is 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 such that x1 in T1 and "a" does not occur in also satisfies
x2 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 in Atom$n 
must mention the token "a" a  (otherwise we could permute ("a","b") and get "b" and hence "b"="a").
Since ⌜a#a:Atom$n⌝ is not type unless ⌜a ∈ Atom$n⌝if we have ⌜a#a:Atom$n⌝ as hypothesis in 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 to be "fresh" w.r.t. (i.e. an atom not occuring in x)
and take swap-atoms{$n:n}(a; b; x) x, then whatever token "a" the atom 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 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" in Aton{n}, and there are x' in and
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 representative of in which avoids "a", i.e. that
every member of the equivalence class of in must mention the atom a.
Now, if must mention a, there can't be representatives f' and x' of and which don't mention a,
so at least one of or 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]; 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 boolean (provided ⌜atom-free{n:n}(Type; T)⌝defined by (nu b. ⌜¬b=b swap-atoms{n:n}(a; b; x)⌝).
Here, nu b. X[b] means choose fresh atom not occring in 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 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]; x; a)  (inheres{n:n}(u:A ⟶ B[u]; f; a) ∨ inheres{n:n}(A; x; a))⌝
 from purported property of "matters" called
"conservation of matters". Unfortunately, the "conservation of matters" property is not true, as shown by the following
Let g <x,y> = ⌜¬b(x =a y ∧b b=a "a"))⌝,
let = ⌜λx.<"a", x>⌝,
let "a".
Then (f x) g <"a","a"> = ⌜tt⌝.
Any tokens "b", "c" different from "a" do not occur in "a",g,f, or x, and
(f swap-atoms{$n:n}(a; b; x)) g <"a","b"> = ⌜tt⌝
(swap-atoms{$n:n}(a; b; f) x) g <"b","a"> = ⌜tt⌝
(swap-atoms{$n:n}(a; b; f) swap-atoms{$n:n}(a; c; x)) g <"b","c"> = ⌜tt⌝but
(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; 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; x))  (((↑matters{$n:n}(a; λX.(g (f X)); ...)) ∨ ...) ∨ ...)⌝...


Rules referencing :  freeFromAtomEquality freeFromAtomAbsurdity freeFromAtomTriviality freeFromAtomBase freeFromAtom1Atom2 freeFromAtomApplication freeFromAtomSet freeFromAtomAxiom
FDL editor aliases :  free-from-atom

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