Talk:Implicational propositional calculus

Relationship to Bernays–Tarski axiom system

See List of logic systems#Implicational propositional calculus. The Bernays–Tarski axiom system and a number of other systems of logic use the hypothetical syllogism

Axiom schema 2' $(A\to B)\to ((B\to C)\to (A\to C))\,$

instead of our

Axiom schema 2 $(A\to (B\to C))\to ((A\to B)\to (A\to C))\,.$

Axiom 2' is used as a lemma in our proof of completeness and is more convenient, in some cases, than axiom 2. But in other cases, it is insufficient for directly translating a deduction into an axiomatic proof.

I can see how to derive $(A\to A)\,$ and $(A\to (A\to B))\to (A\to B)\,$ in Bernays–Tarski. And if we can find a way to prove $(A\to (B\to C))\to (B\to (A\to C))\,,$ then I can go from there to prove axiom 2 and thus get completeness of Bernays–Tarski.

Do you-all feel that putting a section on this into the article would be worth while? JRSpriggs (talk) 05:20, 20 September 2010 (UTC)

Mentioning alternative axiom systems could be useful. But no more proofs, please. There should be less proofs in the article, not more. This is an encyclopedia, not a textbook.—Emil J. 09:56, 20 September 2010 (UTC)

Well yes, this is an encyclopedia, but this article is about logic. And what point is there to logic, if not to prove things? In particular, I would not feel comfortable just accepting a claim that, say, Bernays–Tarski is complete, unless I had personally verified the proof of that claim. Too many things (some false) are taken on faith. Logic was supposed to remove the need to take things on faith, at least in a tiny part of our lives.

What else is there to say about various axiom systems, but whether they can prove or not prove certain things? And if the purpose of proof is to convince people of a truth, then a proof which is not demonstrated (shown to the reader) is not doing its job. JRSpriggs (talk) 17:46, 20 September 2010 (UTC)

That this article happens to be about logic does not in any way make it exempt from core Wikipedia policies, such as WP:RS, WP:OR, WP:N. You are not supposed to take anything on faith, but to look it up in the given sources. We are not supposed to present explicit proofs, unless the proofs themselves, rather than the result, are intrinsically notable. That's certainly not the case here: the completeness proof in the article, as well as proofs of the equivalence of the two systems mentioned, are standard run-of-the-mill derivations that are a dime a dozen in propositional logic.

And no, the job of logic is not to produce unsightly derivations of such-and-such formula in such-and-such formal system. That's about as stupid an idea as that the job of mathematics is to compute what is 23789234 × 7816871 and similar stuff. The topic of logic is to prove something about (classes of) formal systems, not to prove anything in the formal systems (though the latter may be occasionally needed for the former).—Emil J. 18:55, 20 September 2010 (UTC)