INFIX	150T	in
OUTFIX		{ }
OUTFIX		{  :  }

BIND    x SCOPE P IN	{ x : P }

CONJECTUREPANEL "Teoria degli insiemi"
THEOREM (OBJECT x,OBJECT y,OBJECT z) IS
 tt l= !x.!y.(((!z.((z in x) <=> (z in y))) & P(x)) => P(y))
THEOREMS Abstraction(P,OBJECT x,OBJECT y) ARE
 tt l= !x.	(x in { z : P(z) } => P(x)) AND
 tt l= !x.	(P(x) => x in { z : P(z) })
END
BUTTON "Apply" IS Apply ApplicaC COMMAND
BUTTON "Property" IS Apply applyAsAProperty COMMAND 
BUTTON "Instance" IS Apply applyAsAnExample COMMAND 
BUTTON "Apply as Rule" IS Apply applyInLineInference COMMAND
END

CONJECTUREPANEL "Teoria degli insiemi -- problemi"
THEOREMS Sets(OBJECT x,OBJECT z) ARE
 tt l= !x.(!z.	(z in x <=> z in {w : w in x}))
END
THEOREMS Easy ARE
 tt l= !x.(~(x in { x : ff })) AND
 tt l= !x.	(x in { z : P(z) } <=> P(x)) AND
 z in {w:w in x & w in y} l= z in {w:w in x} & z in {w:w in y} AND
 z in {w:w in x} & z in {w:w in y} l= z in {w:w in x & w in y} AND
 tt l= !x.!y.
    (!z.((z in {w:w in x & w in y}) <=> (z in {w:w in x} & z in {w:w in y})))
END
THEOREMS RussellParadox(OBJECT x,OBJECT y) ARE
 {x : ~(x in x)} in {x : ~(x in x)} l=| 
	~({x : ~(x in x)} in {x : ~(x in x)}) AND
 {x : ~(x in x)} in {y : ~(y in y)} l=| 
	~({x : ~(x in x)} in {y : ~(y in y)}) AND
 tt l= ff
END
BUTTON "Apply" IS Apply ApplicaC COMMAND
BUTTON "Property" IS Apply applyAsAProperty COMMAND 
BUTTON "Instance" IS Apply applyAsAnExample COMMAND 
BUTTON "Apply as Rule" IS Apply applyInLineInference COMMAND
END

/*------------Assiomatizzazione della Teoria di Frege----------------*/
CONJECTUREPANEL "Teoria degli insiemi"
PROOF "tt l =!x.(x in{z:P(z)}=>P(x))"
(P, OBJECT x)
INFER tt l =!x.(x in{z:P(z)}=>P(x))
FORMULAE
0 tt,
1 !x.(x in{z:P(z)}=>P(x))
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Teoria degli insiemi"
PROOF "tt l =!x.(P(x)=>x in{z:P(z)})"
(P, OBJECT x)
INFER tt l =!x.(P(x)=>x in{z:P(z)})
FORMULAE
0 tt,
1 !x.(P(x)=>x in{z:P(z)})
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Teoria degli insiemi"
PROOF "tt l =!x.!y.((!z.((z in x)<=>(z in y))&P(x))=>P(y))"
(OBJECT x, OBJECT y, OBJECT z)
INFER tt l =!x.!y.((!z.((z in x)<=>(z in y))&P(x))=>P(y))
FORMULAE
0 tt,
1 !x.!y.((!z.((z in x)<=>(z in y))&P(x))=>P(y))
IS
Axiom[0,1\P,Q]
END