Convincing yourself about choice of axioms for predicate calculus

Question

Consider some Hilbert-type formal system of predicate calculus. I will use the one from Kleene's "Introduction to Metamathematics" 1971. While developing predicate calculus in this style we list set of axioms (or axiom schemata depending on your choice) and set of inference rules. Then concepts of proof and theorem are defined.

But after thinking about it and being honest with myself, I have to admit that I have no idea for why specific axioms and inference rules are chosen (or any equivalent ones). I would like to hear your ideas about it and I will give you all my hypotheses for explanations and why I am unsatisfied with them.

For example, consider axiom schema where $A,B,C$ are metamathematical variables standing for formulas.

$$ 1. (A \Rightarrow B) \Rightarrow ((A \Rightarrow (B \Rightarrow C)) \Rightarrow (A \Rightarrow C)) $$

Also consider the following inference rules where $C$ denotes a formula not containing variable $x$ and $A$ denotes any formula:

$$2. \textrm{If } C \Rightarrow A(x) \textrm{ then } C \Rightarrow \forall x(A(x)) $$

$$3. \textrm{If } A(x) \Rightarrow C \textrm{ then } \exists xA(x) \Rightarrow C $$

Hypothesis 1: We take these and other axioms / axiom schemata / inference rules just because they work. For example, consistency can be shown. Also, because most of the "informal" theorems in mathematics can be reconstructed formally using this kind of predicate calculus. But then how one would come up with them? It seems pretty impossible to choose some of the equivalent sets of axioms/ inference rules just by wanting them to be consistent and for them to be able to formalize most of the "informal" mathematics. I think there should be some kind of intuition or interpretation behind this.

Hypothesis 2: Our choice is based also on the fact that under the interpretation it makes sense. But I have a hard time understanding that. For example, if one considers axiom schemata 1 then interpretation would be "If if $A$ then $B$ then if if $A$ then if $B$ then $C$ then if $A$ then $C$" which for me is extremely confusing and therefore not as readily accessible for intuition. For inference rules 2 and 3 I have no convincing interpretation and I would really appreciate if you could give your interpretation that convinces you for my given inference rules.

Hypothesis 3: Probably one could argue by model-theoretic arguments which formulas we should choose as axiom schemata but I am not that convinced here because for model theory of predicate calculus using finitary means we can only analyze cases when domain of variables of predicate calculus is finite, but usually, in practice, we use theories with an infinite domain. Maybe one can argue that if it holds for finite domain then it is reasonable to assume that it holds for infinite domain, but I am not sure. And then also one could ask why we choose truth tables in the way we do. Also, considering that some types of logic do not have truth tables, but still have axioms/ axiom schemata/ inference rules, I feel that this intuition might not be general enough.

Hypothesis 4: Probably one could also argue that we want certain deductive rules to hold like deduction theorem. But I always felt that philosophically they are not necessary and are just useful tools, but in principle, everything could be developed without these deductive rules. So one cannot argue using them because they are not fundamental to the theory in the first place.

Hypothesis 5: It might be that there is an equivalent predicate calculus with axioms and inference rules that are simpler and more intuitive. If that is the case, can someone give some references for what it is and why is it simpler and more intuitive?

I would appreciate your help and advice, and your own philosophical / intuitive thoughts about this. Especially for me it is interesting, how do you think about these things and how do you convince yourself that what you are doing is reasonable.

Answer 1

First of all, we have to consider that modern mathematical logic has many proof systems : Hilbert-style, Natural Deduction, Sequent calculus, Tableaux, Resolution, Equational.

Hilbert-style was the first one to be "codified" by G.Frege in 1879, and further developed by Russell and Whitehead's Principia (1910-13) and culminated into the first modern math log textbook : Hilbert and Ackermann's Grundzüge der Theoretischen Logik (1928).

In 1935 G.Gentzen developed Natural Deduction and Sequent calculus, that are rules-only proof systems.

Going back to Hilbert-style proof system, based on axioms and rules, we have to start from propositional calculus, where we have a big amount of different systems.

The tradition starting from Frege adopted few axioms and one only rule : Modus Ponens.

The first "variation" comes with the choice of the basic propositional connectives. Frege adopted $\to$ and $\lnot$ while Russell & Whitehead used $\lor$ and $\lnot$.

The approach to axiomatization of propositional calculus was reminescent of Euclid's Elements, trying to introduce "self evident" axioms.

You can read in this sense Russell & Whitehead's approach, avoiding the "tricky" $\to$ (material implication) and adopting the "more easy" $\lor$ (disjunction).

This approach has been further streamlined by Peter Andrews, with MP rule and the following axioms schema:

$(A \lor A) \to A$

$A \to (B \lor A)$

$A \to (B \to ((C \lor A) \to (B \lor C))).$

Quite similar is Joseph Shoenfield's system, with ony one axiom (schema): $\lnot A \lor A$, and rule-versions of the above axioms, plus Cut Rule in place of MP.

But also Frege's original approach was further refined; see e.g. A.Church's system.

The said evolution was driven by different goals :

• evidence of the axioms chosen;

• reduce the number of axioms (and connectives);

• "pragmatic" needs: adopt the axioms necessary to prove as soon as possible the Deduction Theorem and the Soundness and Completeness one.

The second driver produced the single axiom-single connective versions, at the expenses of evidence (and sometimes intelligibility).

But the reductionist approach is useful for proving meta-theorems: usually they require proofs by induction and a reduced number of connectives and axioms means less cases to be surveyed.

The third driver is essential: we want proof systems that are sound and complete, i.e. able to derive all valid formulas (according to the suitable semantics).

From this point of view, the most successfull propositional axiom systems: Church's, Mendelson's, usually made of three axioms and one rule (with axioms: $A \to (B \to A)$ and $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$ that are sufficient for the proof of the DT)) are very practical, compared also to Natural Deduction with many rules.

The Natural Deduction approach was transferred to Hilbert-style systems by Bernays and Kleene, trying to merge the benefits of the two: metalogical "practicality" with the more intuitive approach to the connectives, with pair of introduction-elimination rules (and the corresponding axioms).

In addition, this approach is suitable for Intuitionsitic Logic, where the connectives are not inter-definable.

Conclusion (up to now): there is a trade-off (and a tension) between prgamatic reasons (your Hypos.1 and 4) and "evidence".

Very useful : John Corcoran, Three Logical Theories (1969).

---

The issue about predicate calculus is similar.

First of all, the choice of axioms is based on the previous choice about the propositional part.

Some proof systems choose to stay with only one rule of inference: Modus Ponens (see: Enderton) and thus they have to add suitable axioms for the quantifier; and again, we have in classical logic the choice about introducing both quantifiers as basic insread of defining one in terms of the other.

A different choice is to introduce also inference rules for quantifiers, following Frege's and R&W's systems, that used Generalization rule.

Again, we have different solutions to the goals discussed above: Kleene's system is again an "Hilbert-version" of Natural Deduction approach.

Again, the "minimalist" approach has many possibilities. Shoenfield uses the quantifier axiom: $A[x/a] \to \exists x A$ and the $\exists$-Introduction Rule : "If $x$ is not free in $B$, infer $\exists x A \to B$ from $A \to B$ (see also Tourlakis).

Here, IMO, we have a new "tension" in place. The axiom is quite natural (as well as Universal Instantiation axiom and rule are), but the introduction rule is not.

Generalization rule is more intutitive, but it is tricky, and we have problems in the interaction withthe Deduction Th.

Conclusion (provisional): also for quantifiers, Natural Deduction approach, with the pair introduction-elimination for each of them, is quite ... "natural".

If we adopt an Hilbert-style approach, the basic trade-off is between "naturality" (translating ND into axioms+rules) and paucity.

Obviously, ensuring that the system has the fundamental properties of Soundness and Completeness.

Answer 2

I am only responding because I work on various axiomatizations. My work will never be published.

My principal motivation came from my experience as a student. My professors generally used definite descriptions and epistemic reasoning which actually involved explanations for existence and uniqueness claims. The history of formal systems is such that these practices are not supported in any meaningful sense.

There are excellent source books with English translations (I only speak one language.) available, and, you should consult them to answer some of your questions. There are always motivations. Bolzano did not trust "geometry". Berkeley did not trust "fluxions". Although irrelevant to most of modern mathematics, Hilbert rid geometry of its "temporal" qualities (so, space and time do not measure each other reciprocally as defenders of Newton had proclaimed).

There are always motivations.

I do not work with sequent calculi very much. However, as I understand matters, Gentzen had been very satisfied with himself for the symmetry behind the sequents for negations. There are always motivations. If one does not feel one's own motivations, then one can only learn other people's stuff. And, as Carnap observed, once something is formalized, what has been learned by the effort seems lost. It is personal.

You should not let yourself believe that semantics is a good motivation. In 1999, Pavicic and Megill demonstrated that the "faithful" model of the axioms for the classical propositional calculus is not the Boolean model,

https://arxiv.org/pdf/quant-ph/9906101.pdf

Indeed, they point out that the "faithful" model cannot be represented numerically.

In my own work, I have developed 4096 axioms that place 16 constants into relation with one another so that the truth table relations are recovered. Since axioms for NAND are recovered, I have classical propositional logic through Nicod's work. My motivation had come from recognizing that the system of truth tables satisfied the axioms of a finite affine geometry. The question I answered had asked how to reconstruct compositionality relations from named geometric points. If you wish to get a sense of the complexity involved, take a look at "trilattice logics". And keep in mind that the authors of that logic had not been faced with labeling 16 points with 16 symbols. I actually think their work was more difficult.

It took a great deal of effort to "unlearn" Euler diagrams and to really grasp that representing logic in set theory (Kunen, for example) is simply not "faithful". But, since Boolean models are actually models of the calculus, I have no way to demonstrate to an adherent that there is a problem.

With regard to your questions about the logical axioms, examples are key. I learned from a book entitled "Symbolic Logic" by James A. Thomas. It uses "stroked" proofs that track subsidiary deductions and offers numerous examples. The reason your quantificational axioms have the structure that they do is because quantifiers are often manipulated in subsidiary deductions. Although somewhat outdated, Russell's "Principles of Mathematics" has a good discussion of what is involved in taking the propositional axioms that he takes.

Today, one is expected to go from one logic to another without explanation. But, explanations are dangerous. It is at the border with philosophy.

Undoubtedly, there are those who pursue specific objectives. But, that is more recent simply because our experience with many logics is greater. The one issue that must be addressed in any logic is the preservation of truth across syntactic transformations. That is why "first-order" is so important. Russell gives good arguments for what ought to be called "substantiation" in his paper, "On denoting". Relations and functions cannot provide a basis for extensional truth, and, it is the notion of extension upon which Frege-Russell logicism became a part of mathematics.

But, does mathematics need to be extensional? Technically, "formal axiomatics" is nothing more than nominalism. I once confused "formalism" with this notion. Reams of extramathematical metamathematics in which everything is "encoded" has convinced me otherwise. I now think about foundations from a "nominalism first" point of view.

I have no opinion of mathematics outside of axioms except as application of what occurs within axioms.

For my part, I did have to pursue specific goals when approaching logical axioms (kicking and screaming!!!). The expression "the set universe" in the context of Zermelo-Fraenkel set theory is a definite description outside of the theory. Because of this, I had slowly realized that the logic which I needed to understand had been negative free logic. Free logics and descriptions are intertwined. My logical axioms support the idea of the indiscernibility of non-existents without ever requiring a non-existent to be substantiated. So, with axioms admitting self-membership, I can introduce a set universe as the unique self-membered individual using a description.

The reason my logic can do this is that I recognized how one of Tarski's axioms from his work on cylindric algebra (transitivity) could introduce identity statements with "existential import". So, I could accommodate the negative free logic principle if I could also have a relation without existential import that only conveyed discernibility. So, the logic I wrote distinguishes between "instantiability" (existential import), "discernibility" (formal distinctness), and "substitutivity" (within the calculus).

With regard to the treatment of definite descriptions, many things have changed since Russell's account. Strawson introduced the possibility that definite descriptions ought to be understood referentially. Reimer has argued for descriptively-defined names on the basis of examples like the introduction of the name "Neptune" before the discovery of an actually observed planet. This has convinced Neale to change his mind. He has proposed a syntax by which one might implement this kind of account. And, Abraham Robinson discussed the structure of a formal language built in such a manner in his "On constrained denotation". I feel no obligation to be bound by Padoa's method and the Beth definability theorem.

After writing my logic, I discovered a very similar set of axioms in Russell's "Principles of Mathematics" where he discusses "quantity" and "magnitude". Like my axioms, existential import is not automatically granted. What Russell is talking about is essentially geometric. It may be compared with the point at which one forms Euclidean point spaces or affine spaces in typical treatments of how to get to metric spaces after building algebraic systems. But, if one holds that numerical identity is primarily a geometric phenomenon, then this is where one would expect to draw insights.

I do not know if someone could write a logic without some purposeful objectives. Gentzen had had his. I cannot deny mine.

With regard to intuitiveness, I doubt there is anything simpler than the standard account of first-order quantification. Had I not had the example of professors doing things differently from what had been presented to me as "mathematical", I might never have had contrary intuitions. Now, I have a classical propositional logic whose quantificational logic is comparable with "apartness" and "identity" from constructive mathematics motivated by a principle of negative free logic.

That is what is "intuitive" to me.

Good luck with your studies.