Section 2 introduces the turnstile which turns an idea which may be true into an assertion that it does hold true . Section 5 introduces implication, . Section 6 introduces the single rule of interference relied upon, modus ponens ax-mp. Section 7 introduces negation and with in synonyms for or , and , and two for exclusive-or corresponding to df-or, df-an, dfxor4, dfxor5.
Section 8 introduces the problematic notation for identity of conceptual content which must be separated into cases for biimplication or class equality in this adaptation. Section 10 introduces "truth functions" for one or two variables in equally troubling notation, as the arguments may be understood to be logical predicates or collections. Here f() is interpreted to mean where the content of the "function" is specified by the latter two argments or logical equivalent, while g() is read as and h() as . This necessarily introduces a need for set theory as both and cannot hold unless is a set. (Also .)
Section 11 introduces notation for generality, but there is no standard notation for generality when the variable is a proposition because it was realized after Frege that the universe of all possible propositions includes paradoxical constructions leading to the failure of naive set theory. So adopting f() as would result in the translation of f () as . For collections, we must generalize over set variables or run into the same problems; this leads to g() being translated as and so forth.
Under this interpreation the text of section 11 gives us sp (or simpl and simpr and anifp in the propositional case) and statements similar to cbvalivw, ax-gen, alrimiv, and alrimdv. These last four introduce a generality and have no useful definition in terms of propositional variables.
Section 12 introduces some combinations of primitive symbols and their human language counterparts. Using class notation, these can also be expressed without dummy variables. All are A, , alex, eqv; Some are not B, , exnal, pssv, nev; There are no C, , alnex, eq0; There exist D, , df-ex, 0pss, n0.
Notation for relations between expressions also can be written in various ways. All E are P, , dfss6, df-ss, dfss2; No F are P, , alinexa, disj1; Some G are not P, , exanali, nssinpss, nss; Some H are P, , exnalimn, 0pssin, ndisj.