Bourbaki and foundations

[Lawrence Paulson]

Dear Neil,

Perhaps more accurate word would be "admissible”. I wonder why beginners find it difficult. “Proof by contradiction” is simply double negation, so not relevant. The question is what happens if 1=0, and in any specific context (Peano arithmetic, ZF, lambda-calculus) deriving x=y is a trivial calculation, so the principle is a codification of that. Computationally it corresponds to type systems in which non-terminating computations can be assigned any type.

I guess it’s not a situation that mathematicians bump into every day, thank goodness!

Larry

> On 15 May 2022, at 22:57, Tennant, Neil <tennant.9 at osu.edu> wrote:
> 
> Since EFQ (from absurdity infer any proposition you please) is typically taken to be a rule of inference, I take you to be claiming that EFQ is valid, rather than true. But EFQ is certainly not obviously valid. Beginners in formal find it highly counterintuitive. It’s also the main source of irrelevance. IMHO it’s a rule that students are just brainwashed into accepting.  
> Moreover, mathematical and scientific deductive reasoning has no need for it at all.