Mate’s formalism introduced sentential calculus first following Łukasiewicz’s ‘Polish’ notation — “C” for prefix implication and “N” for not. Lower case letters denoted unspecified sentences. Truth tables are defined and shown to provide a decision method for sentential calculus. Three axioms plus modus ponens were informally proven to provide the same theorems as the truth tables. Truth tables and axioms both produced theorems such as “a ∨ ¬a”.
Next came the predicate calculus with quantification and identifiers for predicates and individuals. The new sentences filled the role of previously unspecified sentences of the sentential calculus and we had first order predicate calculus. It was first order because only individual variables but not predicates could be quantified.
Of course a few axiom schemas were necessary; we used three. A schema is a well formed formula with a few Greek letters each appearing a few times. To get an axiom each Greek letter is replaced by some well formed formula, after which the whole formula is closed by prefixing it with a universal quantifier for each free variable within. For specific axioms there are conditions on the free variables appearing in the expressions denoted by the Greek letters. Thus was an axiom derived from an axiom schema. There were three axiom schemas but an infinite number of axioms. Modus ponens was brought forth from sentential calculus and the result was declared to be the predicate calculus.
All of this work was informal—informal logic about formal logic. The separation was rigorous and while the meanings of the symbols were never hidden it was absolutely forbidden to use those meanings in any way.
A few weeks were devoted to proving famous theorems of predicate calculus.
Then we adopted a simple model theory good enough to define validity for a sentence meaning that for every possible interpretation of the predicates and individual constants, that the sentence was true. (Tarski’s Wahrheitsbegriff) This could be said to give a highly technical meaning to those symbols and these meanings entered into the completeness proof. With this definition in hand we proceeded to Henkin’s proof that for every valid sentence of the predicate calculus, there was a proof of that sentence. I had never been so impressed with so inobvious a theorem. I still marvel at it. The proof is informal and slightly long and I spent more time combing that proof than I have ever spent on any proof. It was the first non-constructive proof I had paid any close attention to. Here is a synopsis of the proof. Some Meta Math.