Necessary in order to define a provabilty predicate, Godel defined the relation, $Fl(x,y,z)$ ("$x$ is an immediate consquence of $y$ and $z$"). But the definition leaves me flat. I understand what it says, but I don't get how it is any proper or substantive characterization of "immediate consequence." This definition can be found on page 55 of the original paper, or on page 61 of this pdf of Meltzer's translation. It seems that $Fl(x,y,z)$ is satisfied whenever $y$ and $z$ code a conditional and it's antecedent, and $x$ codes the consequent, or else $x$ codes the universal generalization of another variable, $v$, within the formula coded by $y$. That is, informally, according to Godel, $x$ codes an immediate consequence of the formulas coded by $y$ and $z$ iff either:
(Where "$@k$" expresses the formula coded by $k$.)
- $@y$ = $@a \to @b$, for some $a$ and $b$, and $@z$ = $@a$, and $@x$ = $@b$, or else,
- $@x$ = $\forall @v @y$,where $@v$ may or may not appear in $@y$ at all, let alone free.
According to your own lights, does this definition do the job? Can you explain how it works? I think this is a pretty important hinge in Godel's proof, and I can't believe he would have 'phoned it in,' so to speak. But I can't see what he was up to with this, $Fl(x,y,z)$. Maybe every other mode of logical consequence is in some sense equivalent to modus ponens? I just don't know.
Best Answer
Welcome to Math.SE!
Yes, modus ponens is the only propositional inference rule defined in Principia Mathematica (there are also six axioms governing the connectives $\neg$ and $\vee$). Any other inferences are derived, their validity shown by reducing them to multiple invocations of the axioms and the modus ponens rule. One can derive all other usual forms of inference (modus tollens, constructive dilemma, etc.) in the system of Principia Mathematica this way.
Similarly, the only inference rule governing the quantifiers in Principia Mathematica is the rule of universal generalization.
Accordingly, the immediate consequences of two premises are the ones that follow by a single application of one of these two rules. Other consequences are not immediate, since they require multiple uses of the inference rules. This would have been a long-standing, well-understood notion to the target audience of Gödel's On Formally Undecidable Propositions of Principia Mathematica and Related Systems, so he probably didn't feel the need to comment on it further.
Note also that which inference rules you consider basic is not a "load-bearing" part of Gödel's argument: if you formulate your logic with different sets of basic inference rules that nonetheless suffice to prove everything that Principia Mathematica proves, the resulting system will still be incomplete or inconsistent.