Talk:Implicational propositional calculus

	This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects:
Mathematics Low‑priority Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks. Low This article has been rated as Low-priority on the project's priority scale.

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' ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))\,}$

instead of our

Axiom schema 2 ${\displaystyle (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 ${\displaystyle (A\to A)\,}$ and ${\displaystyle (A\to (A\to B))\to (A\to B)\,}$ in Bernays–Tarski. And if we can find a way to prove ${\displaystyle (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)[reply]

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)[reply]

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)[reply]

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)[reply]

Substantial improvements needed

Please consider joining the feedback request service. An editor has requested comments from other editors for this discussion. This page has been added to the following list: Maths, science, and technology When discussion has ended, remove this tag and it will be removed from the list. If this page is on additional lists, they will be noted below.

On 22 April 2025 (02:19) I updated the article Implicational propositional calculus. A few hours later the update was reverted with the argument that "I am missing the whole point which is to avoid using falsum in the formulas". Could a third party please verify that claim.

Aside from that, in my opinion the article needs substantial improvements:

• The article should place implicational calculus in its historical context by tracing its development from ‘’Begriffsschrift’’, through ‘’Principia Mathematica’’, and on to later contributions by the Lwów–Warsaw school, Gentzen, and others. This would reveal the evolution from the axiomatic Hilbert-style proof systems to the more intuitive methods of analytic tableaux, natural deduction or sequent calculus.
• The article should highlight that implicational calculus — with ${\displaystyle \bot }$— adequately covers classical logic, but does not suffice for full intuitionistic logic, where conjunction (${\displaystyle \land }$) and disjunction (${\displaystyle \lor }$) are essential, rather than merely syntactic sugar. This important distinction should not be overlooked.

As to the sections,

• The section Completeness is either undocumented or based on (forbidden) original research. The reader loses track in the midst of formal derivations.
• The section The Bernays–Tarski axiom system should either be relocated to the article List of axiomatic systems in logic or better justified in context. Highlighting one alternative among a plethora of axiom systems appears arbitrary and lacks relevance to the broader purpose of the article.
• The section Satisfiability and validity discusses the NP-complexity of the propositional satisfiability problem. Either the computational complexity angle should be considered as beyond the scope of the article and removed, or should be addressed with appropriate context. Note that the examples provided implicitly use the method of analytic tableaux, while the article only deploys Hilbert-style deduction systems.
• The section Adding an axiom schema illustrates that adding non-tautologies —think of a bare propositional variable ${\displaystyle P}$— as axioms makes the system inconsistent. This is a trivial point and comes across as unprofessional. The section should be removed.
• The section An alternative axiomatization is undocumented and lacks references. Without a proper citation, it appears to be original research and should either be sourced or omitted.

––– Marc Schroeder (talk) 12:52, 22 April 2025 (UTC)[reply]

As the article says "... , Łukasiewicz's paper derives the Bernays–Tarski axioms from Łukasiewicz's sole axiom as a means of showing its completeness.". This is why I put in a section showing that Bernays–Tarski axioms are sufficient to get the deduction metatheorem. I am completing the proof given in the referenced paper that his axiom schema is complete (in the sense of classical (not intuitionist) logic) for propositions containing only implication as a connective. JRSpriggs (talk) 15:09, 22 April 2025 (UTC)[reply]

Close RFC: RFCs are used to ask the community to ask for input on one particular notable change. This discussion appears to be asking for several different suggestions. ―Howard • 🌽³³ 14:35, 2 May 2025 (UTC)[reply]