Wikipedia:Reference desk/Archives/Mathematics/2022 December 8

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

December 8

BHK, don't get it

I've a question regarding BHK. Why they do not just make a generalization of the negation of first order predicat logic? 2A02:908:424:9D60:1728:3390:1D6B:BA69 (talk) 07:46, 8 December 2022 (UTC)

You have, apparently, a simple way in mind of dealing with negation, but it is not clear from what you write what it is, which makes it hard to discuss why it is not followed. First-order logic is not one specific logic but a term that applies to many logics; do you mean first-order intuitionistic logic? First-order logics are formal systems, consisting of a syntax for forming propositional formulas and a system of deduction rules for deriving theorems. As such, they have no semantics; the formulas are just sequences of symbols without inherent meaning. BHK is about assigning an interpretation to these symbols that gives a compositional semantics for these formulas, one under which the deduction rules are obviously sound. If quantification over propositions is allowed, one can define absurdity as $\forall p.p,$ or any provably equivalent formula. However, this is beyond first order, and BHK also assigns an interpretation to pure propositional logic, without quantification. One can, however, avoid the introduction of the concept of absurdity as follows:

A proof of $\neg P$ is a function that converts a formula $Q$ into a proof of $P\to Q.$

It is then easy to see that a proof of, e.g., $P\land \neg P$ implies that a proof can be produced for any formula.  --Lambiam 09:27, 8 December 2022 (UTC)