2

It is common sense that to derive a formula with existential quantifier is only necessary to prove that a formula is valid for any term , ie:

$\Gamma$ , $\phi$ [t/x] $\vdash$ $\exists$x$\phi$.

By definition t could be any term since it is free for x in $\phi$. So my question is, If I want to prove $\exists$x$\phi$ then I can prove that $\phi$ is true for a constant or weird function in a particular universe ?

For example:

Let $\phi$ = Even(x). I wish to prove that 2 is even, denoted by Even(2), in a Universe = $\mathbb{Z}.$ 2 = 2 * 1. Then by definition $\exists$x(2 = 2x). Even(2). Therefore $\exists$x($\phi$[2/x]).

Is this correct, can i prove any existential quantifier for any function that involves x, variable or constant?

Peter
  • 51

2 Answers2

2

In Natural Deduction, we have the $\exists$-introduction rule [following Trismegistos correction]:

if a derivation $D$ of $\phi(t/x)$ exists, then we can infer $\exists x \phi(x)$, and its undischarched assumptions are those of $D$ (provided that $t$ is free for $x$ in $\phi$).

So, if $\Gamma$ is the set of closure of FO Peano Axioms, and you will provide a proof of "$2$ is even" (i.e. $\phi(2)$) from them (i.e. a derivation $D$ of $\phi(2)$ from $\Gamma$) youn can "add" to $D$ a new step using $\exists$-intro and obtain a proof of "there are even numbers" (i.e. $\exists x\phi(x)$).

The First-Order logical calculus is sound : if $\Gamma \vdash \phi$ then $\Gamma ⊨ \phi$. This means that, if $\Gamma$ is as above, all theorems you can prove from FO Peano Axioms are logical consequences of them, i.e. are true in all models of the Axioms.

Mauro ALLEGRANZA
  • 94,169
  • Actually this rule says that if derivation $D$ of $\phi[t/x]$ exists and $t$ is some term substitutable for $x$ in $\phi$ than we can infer $\exists x\phi(x)$ and its undischarched assumptions are those of $D$ – Trismegistos Dec 11 '13 at 08:45
  • Thanks. So how $\exists$-intro is related to the usual informal way we prove things in math ? – Peter Dec 12 '13 at 03:56
  • Assume that we are working with first-ordr arithmetic (i.e.with FO Peano Axioms) and assume that we have introduced the numerals (terms "naming" the numbers). If we are able to prove the formula expressing the porperty "x is even" whith the numeral "2" in place of the variable "x", then ∃-introduction allows us to conclude that "there exist even numbers". – Mauro ALLEGRANZA Dec 12 '13 at 07:20
  • @MauroALLEGRANZA that's exactly it, thank you – Peter Dec 12 '13 at 22:14
1

As far as I understood, $\Gamma$ was a set of sentences. In that case, proving $\Gamma \vdash \exists x\phi$ is the same as proving that sentence in every model of $\Gamma$. That is, if $\mathcal M \models \Gamma$, then $\mathcal M \models \exists x\phi$. In your example, you checked for only one model.

Because you don't know for which model you should get the realization of the formula, you cannot specify a constant, if the constant is not included in your language. You should really find a term realizing the formula. And in the case, when there are constants in your language realizing the formula, those constants are particular cases of terms too.

Tigran Hakobyan
  • 815
  • Oh sorry, I should have set a model, but taking into account that I want to prove phi for a particular theory, as set theory or graph theory. – Peter Dec 11 '13 at 07:27