Demonstrações informais e formais com quantificadores. Exemplo. As regras da intanciação universal (AElim), generalização existencial (EIntro). Constantes novas para nomear objetos que advêm de asserções de existência: a regra da instanciação existencial (EElim). Exemplo.