# Proof system for FOL
	Axiom Group1 : substitution in propositional tautologies
	Axiom Group2 : (\forall x \alpha -> \alpha[t,x]) for any term t substituting x in valid way (that is no free variable becomes bound). 
	Axiom Group3 : (\forall x (\alpha -> \beta) -> (\forall x \alpha -> \forall x \beta))
	Axiom Group4 : (\alpha -> (\forall x \alpha)), when x is not a free variable in \alpha

## Then Axioms=I({Axiom group1, Axiom group2, Axiom group3, Axiom group4}, {\forall x, \forall y,...})

## Any formula has a proof if it belongs to I(Axioms,{MP}). 

-- example of a proof.