Return to Article Details Basic first-order model theory in Mizar Download Download PDF