Description: Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in Megill p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of Tarski p. 77 and Axiom C5-1 of Monk2 p. 113.
(This theorem simply repeats ax-5 so that we can include the following note, which applies only to the obsolete axiomatization.)
This axiom islogically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen , ax-c4 , ax-c5 , ax-11 , ax-c7 , ax-7 , ax-c9 , ax-c10 , ax-c11 , ax-8 , ax-9 , ax-c14 , ax-c15 , and ax-c16 : in that system, we can derive any instance of ax-5 not containing wff variables by induction on formula length, using ax5eq and ax5el for the basis together with hbn , hbal , and hbim . However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax5ALT |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 |