Ce projet est un développement Coq qui formalise la logique du premier ordre en utilisant la déduction naturelle. Il propose deux encodages des formules (par noms et localement sans noms) et démontre des propriétés métathéoriques comme le lemme de substitution et le théorème de complétude. Des exemples concrets (arithmétique de Peano, théorie des ensembles ZF) illustrent son utilisation.