Automath examples

ZFC.aut

#!/usr/local/bin/aut -Q

{
This is ZFC in AUT-QE, as opposed to AUT-68 which Wiedijk provides. The difference
is fewer primitive notions: we have 1+3+2+6+8+1=21 primitive notions, 
Wiedijk's AUT-68 version has 31 primitive notions.

To see Wiedijk's version, see https://www.cs.ru.nl/~freek/zfc-etc/
}


{ ----------------------------- the types --------------------------------1-- }

  * set : TYPE := PRIM

{ ----------------------------- first order logic ------------------------3-- }

  * false : PROP := PRIM
  * [a:PROP][b:PROP] imp:PROP := [x:a]b

  * [x:set][y:set] eq : PROP := PRIM
y * in : PROP := PRIM

  * [p:[z:set]PROP] for:=p:PROP

a * not : PROP := imp(false)
b * and : PROP := not(imp(a,not(b)))
b * or : PROP := imp(not(a),b)
b * iff : PROP := and(imp(a,b),imp(b,a))
p * ex : PROP := not(for([z,set]not(<z>p)))
p * unique : PROP :=
  for([z,set]imp(<z>p,for([z',set]imp(<z'>p,eq(z,z')))))
p * ex_unique : PROP := and(ex,unique)

{ ----------------------------- definition by cases ----------------------2-- }

y * [c:PROP] cases : set := PRIM
c * cases_axiom :
  and(imp(c,eq(cases(x,y,c),x)),imp(not(c),eq(cases(x,y,c),y))) := PRIM

{ ----------------------------- set theory -------------------------------6-- }

  * empty : set := PRIM
y * double : set := PRIM # {x,y}
x * unions : set := PRIM
x * powerset : set := PRIM
x * [f:[z,set]set] replace : set := PRIM
* omega : set := PRIM

x * single : set := double(x,x)
x * [q:[z,set]PROP] restrict : set :=
  unions(replace(x,[z,set]cases(single(z),empty,<z>q)))
y * inter : set := restrict(x,[z,set]in(z,y))
y * union : set := unions(double(x,y))
x * succ : set := union(x,single(x))
y * subset : PROP := for([z,set]imp(in(z,x),in(z,y)))
y * disjoint : PROP := eq(inter(x,y),empty)
x * omega_closed : PROP :=
  and(in(empty,x),for([n,set]imp(in(n,x),in(succ(n),x))))

{ ----------------------------- the axioms -------------------------------8-- }

y * extensionality :
  iff(eq(x,y),for([z,set]iff(in(z,x),in(z,y)))) := PRIM
x * foundation :
  imp(not(eq(x,empty)),ex([z,set]and(in(z,x),disjoint(z,x)))) := PRIM

  * empty_axiom : for([z,set]not(in(z,empty))) := PRIM
y * double_axiom :
  for([z,set]iff(in(z,double(x,y)),or(eq(z,x),eq(z,y)))) := PRIM
x * unions_axiom :
  for([z,set]iff(in(z,unions(x)),ex([y,set]and(in(z,y),in(y,x)))))
  := PRIM
x * powerset_axiom :
  for([z,set]iff(in(z,powerset(x)),subset(z,x))) := PRIM
f * replace_axiom :
  for([z,set]iff(in(z,replace(x,f)),ex([y,set]and(in(y,x),eq(z,<y>f)))))
  := PRIM
  * omega_axiom :
    and(omega_closed(omega),
      for([o,set]imp(omega_closed(o),subset(omega,o)))) := PRIM

{ ----------------------------- choice -----------------------------------1-- }

  * AC :
    for([x,set]imp(
     and(for([y,set]imp(in(y,x),not(eq(y,empty)))),
       for([y1,set]imp(in(y1,x),for([y2,set]imp(in(y2,x),
         or(eq(y1,y2),disjoint(y1,y2))))))),
     ex([x',set]for([y,set]imp(in(y,x),ex_unique([y',set]
       and(in(y',x'),in(y',y)))))))) := PRIM