First-order logic and quantifiers

Question

In "G"odel's Incompleteness Theorems" (p. 29), R. Smullyan gives the axioms of a version of first-order logic with identity (Kalish & Montague) as:

L1: $(F \supset (G\supset F))$

L2: $(F\supset (G\supset H))\supset ((F\supset G) \supset (F\supset H))$

L3: $((\sim F\supset \sim G)\supset (G\supset F))$

L4: $(\forall v(F\supset G)\supset (\forall v F\supset \forall v G))$

L5: $(F\supset \forall v F)$ ($v$ does not occur in $F$).

L6: $\exists v(v=t)$ ($v$ does not occur in $t$).

L7: $(v=t \supset (XvY \supset XtY))$ (Where $XvY$ is an atomic formula).

Here $F, G, H $ are formulas, $t$ is a term (the notion depends on the language, but let's say we're talking first-order arithmetic, in which case a 'term', roughly consists of variables, numerals, + and .) and $v$ is a variable. Further, the rules of inference are 1) Modus ponens and 2) from $F$ infer $\forall v F$.

So here's my question: How do you prove any formula of the type $\exists v F$? Doesn't look like you can get much from L6. The reason for my question is that after this (p. 61), when discussing $\omega$-consistency, he argues that from $F(\bar n)$ provable for some $n$ follows $\exists v F(v)$ provable.

Answer 1

For that matter, how do you use a formula of the type $\exists vF$?

The most likely assumption is that $\exists vF$ is considered to be an abbreviation for ${\sim}\forall v\,{\sim}F$ -- and you can then prove it using propositional reasoning together with the rules for $\forall$.

Answer 2

Not sure if this is the shortest possible way to do it, but here is how to prove $\exists x (Fx \supset Fx)$. For brevity's sake, I will not show the proofs of propositional validities (anything provable from L1$-$L3 alone).

1. $Fx \supset Fx$: Any formula of the form $\alpha \rightarrow \alpha$ is provable from L1$-$L3.

2. $x = y \supset (Fx \supset Fx)$: Weaking of 1., immediate with L1 and MP.

3. $\neg (Fx \supset Fx) \supset \neg (x = y)$: Contraposition of 2., provable from L1$-$L3.

4. $\forall x (\neg (Fx \supset Fx) \supset \neg (x = y))$: From 3. by inference (2).

5. $\forall x[\neg (Fx \supset Fx)] \supset \forall x[\neg (x=y)]$: From 4. by using L4 and MP.

6. $\forall x[\neg (Fx \supset Fx)] \supset \neg\neg\forall x[\neg (x=y)]$: Inserting double negation (derivable because $\alpha \supset \neg\neg\alpha$ and transitivity are derivable from L1$-$L3).

7. $\forall x[\neg (Fx \supset Fx)] \supset \neg \exists x(x=y)$: Putting $\exists x$ for $\neg\forall x\neg$ (by definition)

8. $\exists x (x = y) \supset \neg\forall x[\neg(Fx \supset Fx)]$: Contraposition of 6.

9. $\neg\forall x[\neg(Fx \supset Fx)]$: From 8. by using L6 and MP.

10. $\exists x (Fx \supset Fx)$: Again putting $\exists x$ for $\neg\forall x\neg$.

Edit: I've fiddled around with the calculus a bit more, and and as a simple example of universal instantiation, here is a how to derive $\forall x(Fx)\supset Ft$ (this will also work if we put a function expression or so for $t$, as long as $x$ doesn't occur in $t$, because of step 4)

1. $x=t \supset (Fx \supset Ft)$: Instance of L7

2. $\neg Ft \supset (Fx \supset \neg(x=t))$: Derivable from 1., because $(\alpha \supset (\beta \supset \gamma)) \supset (\neg\gamma \supset (\beta \supset \neg\alpha))$ is propositionally valid and provable from L1$-$L3.

3. $\forall x(\neg Ft) \supset \forall x[Fx \supset \neg(x=t)]$: From 2. by applying inference (2) and L4.

4. $\neg Ft \supset \forall x (\neg Ft)$: Instance of L5

5. $\forall x [Fx \supset \neg(x=t)] \supset (\forall x(Fx) \supset \forall x (\neg x=t))$: Instance of L4

6. $\neg Ft \supset (\forall x(Fx) \supset \forall x (\neg x=t))$: From 4., 3., 5. by transitivity.

7. $\neg \forall x (\neg x=t)$: Instance of L6

8. $\neg Ft \supset \neg \forall x (Fx)$: From 6. and 7. by propositional logic

9. $\forall x (Fx) \supset Ft$: Contraposition of 8.

Note that this does not automatically transfer if we put more complex formulae for $Fx$, since we would first have to extend L7. For instance, if we want to use this scheme to derive $Ft \supset \exists x (Fx)$, we need to prove $x=t \supset (\neg Fx \supset \neg Ft)$ as a starting point.