First order logic derivations

312 Views Asked by At

I need to prove a variety of derivations of the first order formula $F$ using axioms and inferences rules of the proof system for first order logic. These are:

\begin{gather} \vdash F \vee (F \rightarrow G) \\ \vdash F \rightarrow G \mbox{ implies } \vdash F \rightarrow G \vee H \\ \vdash \exists x \exists x \leftrightarrow \exists x H \end{gather}

I need to prove these without using soundness or completeness.

1

There are 1 best solutions below

0
On

Everything will depend on the proof system you are using. Proof strategies are system-dependent.

But here are some hints for the first two (the third makes no sense and must be a typo).

For (1) Can you prove $F \lor \neg F$? Can you show that from $\neg F$ you can derive $F \to G$? If so, can you see how to put those two proofs together to get what you want?

(2) Should be easy: How do you prove a conditional? Suppose the antecedent $A$ and derive the consequent $C$ and then use conditional proof to infer $A \to C$. Use that rule, then. So suppose $F$. From your assumption you can derive $G$, and can you see how to proceed from there?