zbMATH — the first resource for mathematics

Definitions: the primitive concept of logics, or the Leśniewski-Tarski legacy. (English) Zbl 1001.03009
In 1923, A. Tarski succeeded to show that conjunction can be defined in a second-order classical propositional calculus in terms of equivalence and universal quantification. This discovery allowed S. Leśniewski to achieve his goal – to construct a theory of propositional types based on equivalence as the single connective. The theory, called by him Protothetic, also demonstrated that definitions need not be treated as metalogical conventions staying outside the system; in fact, the position of Leśniewski was that definitions (formulated by means of the same connective) should be “first-class citizens” of a formal system along with its axioms and theorems, and should have the same status. This position, contradicting Russell’s one, never has been widely accepted by other logicians and have even been criticized; nevertheless, it has not been refuted.
Various attempts to investigate and even to reconstruct Leśniewski’s Protothetic have been made during the last four decades. The authors of the monograph under review have set an aim to develop a new, constructive system of protothetic: “not only the formalization should reflect constructive intuition, but the metatheory should also be constructively acceptable.” Actually their constructivism is intuitionism. Part One of the monograph contains, together with some historical notes, a more detailed account of the authors’ motivation.
The system itself, New Protothetic (or NP, for short), is set up in Part Two. Instead of the Leśniewskian inscriptional syntax, a more traditional approach is realized. Beside the primitive symbols \(\equiv\) and \(\bigwedge\), there are reserved symbols for propositional and functional parameters and (bound) variables, and also a special stock of identifiers to be used as the defined symbols in definitions. The underlying hierarchy of propositional types is essentially narrower than in Leśniewski’s system: only types \(S\) and \(S/S^n\) are allowed; in this respect NP is similar to Slupecki’s Elementary Protothetic. As to inferences, NP and its subsystem, Minimal Protothetic (MP, for short), are natural deduction systems. MP has only introduction and elimination rules for \(\equiv\) and propositional and functional universal quantifiers; so, this system corresponds to the protothetic in the sense of A. Church’s Introduction to mathematical logic. Vol. I [Princeton: Princeton Univ. Press (1944; Zbl 0060.02007)]. Given a sequence of Leśniewski style definitions, an unfolding of MP is obtained by adding a pair of introduction and elimination rules for every defined (propositional or functional) identifier. Now, New Protothetic is understood to be either any such an unfolding of MP or, sometimes, the collection of all of them. Furthermore, NP is provided with Beth semantics, and the weak completeness theorem (every formula forced in all Beth models is a theorem of NP) is obtained intuitionistically. By the way, formulas containing free parameters are allowed to appear in inferences; this is one more deviation from Leśniewski. Tarski’s proof that conjunction is definable in terms of equivalence and the universal quantifier can be carried out also in NP. NP is also shown to have the explicit disjunction property: if a disjunction is a theorem of NP, then so is at least one of its disjuncts.
In Part Three NP is used to give one more, and natural, answer to the old question raised by G. Kreisel: What is an intuitionistic propositional connective? The authors argue why they consider that intuitionistic protothetic is the place to look for such connectives. They even consider the providing of their answer as one of the purposes of introducing NP (probably, this also accounts for the restricted type hierarchy of NP: higher types were merely not needed). The offer is simple: the (pure logical) intuitionistic connectives are given by the truth-functional operators of NP. In turn, the latter have been characterized as those defined operators that are equivalence-invariant (or, in the old Leśniewskian terminology, obey the extensionality laws). A remarkable fact proven is that there is a monadic propositional connective not definable in the second-order intuitionistic propositional calculus (EIPC, for short), which is nevertheless definable in the intuitionistic protothetic. This means that NP is stronger than EIPC. It can be shown, in fact, that NP includes the full impredicative EIPC.
Part Four deals with two equivalence calculi contained in MP. To get a better understanding of equivalence in protothetic, the authors first study the Minimal Equivalence Calculus (MEC, for short) obtained from MP by eliminating everything but propositional parameters and \(\equiv\); the only rules are introduction and elimination rules for this connective. Completeness theorem for MEC is easily transferred from NP. It is shown that MEC has infinitely many inequivalent formulas in two parameters. A conservative extension of MEC is obtained by adding conjunction and the corresponding pair of rules.
In the most extensive Part Five the authors turn to algebraic logic. They construct the Lindenbaum algebras of the calculi of the preceding part and of MEC extended by an intuitionistic negation. Then they discuss the obtained algebraic structures, in particular, compare them with complete Heyting algebras, and prove algebraic completeness of the mentioned calculi.

03B15 Higher-order logic; type theory (MSC2010)
03B20 Subsystems of classical logic (including intuitionistic logic)
03G25 Other algebras related to logic
03F50 Metamathematics of constructive systems
03-03 History of mathematical logic and foundations
01A60 History of mathematics in the 20th century
06D20 Heyting algebras (lattice-theoretic aspects)
Full Text: DOI