🚀 go-pugleaf

In article <1993Jan10.151351.19163@husc3.harvard.edu> zeleny@husc10.harvard.edu (Mikhail Zeleny) writes:
>
>To recapitulate the substance of past battles, Alfred Tarski, in his
>article "On Extensions of Incomplete Systems of Sentential Calculus",
>appeals to what has come to be known as Lindenbaum's Lemma, proving that
>there exists but one (absolutely) complete and consistent extension of
>incomplete sentential calculi, which contain as theorems certain
>formulae (namely, CpCqp, CpCCpqq, and CCqrCCpqCpr), expressing naturally
>evident properties of material implication.

It is worth mentioning that CpCCpqq (i.e. p->((p->q)->q)) is derivable
from the other two (that is, from p->(q->p) (= K) and
(q->r) -> ((p->q)->(p->r))) (= S) by modus ponens, mainly via the same
derivation by which the lambda calculus combinator C (converse, Cfxy
reduces to fyx) is derived from the combinators K and S by
application.  This yields (p->(q->r)) -> (q->(p->r)), now substitute
q->r for p and the rest is clear.  K and S as propositions constitute a
complete axiomatization of the implicational fragment of intuitionistic
logic.  Peirce's axiom ((p->q)->p)->p supplies an example of an
implicational proposition that is in the classical theory but not the
intuitionistic.
-- 
Vaughan Pratt			There's safety in large condition numbers.