Natural constructive proofs of A via A -> B, proof paradoxes, and impredicativity

Mark van Atten (1)

1 PG,HCP - Pays germaniques , histoire - culture - philosophie (UMR8547)

Guided by a passage in Kreisel, this is a discussion of the relations between the phenomena in the title, with special attention to the method of analysis and synthesis in Greek geometry, fixed point theorems, and Kreisel's contact with Gödel.

Mots clés: analysis and synthesis; Brouwer; constructivity; informal proof; fixed points; formal proof; Gödel; Goodman; Greek geometry; Heyting; implication; impredicativity; intuitionistic logic; Kreisel; paradoxes; Troelstra

Domaines: Mathématiques [math]; Philosophie

Mark van Atten. Natural constructive proofs of A via A -> B, proof paradoxes, and impredicativity. 2021. ⟨hal-03296950v1⟩