Prova

term: Prova etymology: 'Do latim proba — "teste", "demonstração".' summary: 'Sequência finita de proposições onde cada uma é axioma, hipótese ou consequência das anteriores, terminando na proposição a demonstrar.' relatedModules: [proof-methods] seeAlso: [teorema, axioma, fim-de-prova]

Definição

Sequência finita de proposições onde cada uma é um axioma, uma hipótese, ou consequência das anteriores por regras de inferência, terminando na proposição a demonstrar.

Intuição

O caminho da derivação. Não é "convencer alguém" — é exibir a rota formal do ponto A (axiomas) ao ponto B (teorema).

Registro computacional

Pelo isomorfismo de Curry-Howard, uma prova é um programa. Prova e programa são literalmente a mesma coisa em sintaxes diferentes.