# Direct and indirect proof, syntactical and semantical

A first-order sentence is (logically) valid iff it's true in every interpretation. And it's valid iff it can be deduced from the FO axioms alone.

One normal case of showing that a FO sentence is true is deducing it (syntactically).

I guess that indirect proofs have to be interpreted more "semantically":

"Assume that ~F is true in an interpretation. [Deduction of a contradiction] Thus ~F couldn't have been true. Thus F must be true in every interpretation." (But we are left without a deduction of F from the axioms.)

Is this reading of indirect proofs correct?

Are there also direct proofs that work "semantically", i.e. that show directly that a sentence is true in every interpretation?

Like truth tables do.

-

We can easily turn an indirect proof of a theorem (or proof of a theorem by contradiction) into an ordinary direct syntactic proof. This is a special case of the Deduction Theorem which tells us that if $\Sigma \cup \{A\} \vdash B$ for some collection of statements $\Sigma$ and specific statements $A$ and $B$, then $\Sigma \vdash A \rightarrow B$. Specifically, if we let $A$ be $\lnot F$ and $B$ be some contradiction $C \land \lnot C$ derived from $\Sigma \cup \{\lnot F\}$, then the deduction theorem tells us that we have a proof of $\lnot F \rightarrow (C \land \lnot C)$ from $\Sigma$. But since $F$ is a tautological consequence of this last statement, we can extend such a proof of this $\Sigma$-theorem to a proof of $F$. This direct syntactic proof of $F$ then gives us a direct semantic proof by Gödel's completeness theorem for first-order logic.

Note that the Deduction Theorem itself is a metatheorem that can be proven by induction on the length of the proof of $B$ from $\Sigma \cup \{A\}$, and its proof provides us with a constructive way of getting the actual proof of $A \rightarrow B$ from $\Sigma$.

-
I am right, that we have a proof of of ¬F→(C∧¬C) from Σ, but we don't know it? Or is the Deduction Theorem constructive? –  Hans Stricker Jan 25 '11 at 12:34
The proof of the Deduction Theorem is constructive: We will know exactly what a specific proof of $\lnot F \rightarrow (C \land \lnot C)$ from $\Sigma$ looks like given a proof of $C \land \lnot C$ from $\Sigma \cup \{\lnot F\}$. –  Jason Jan 25 '11 at 14:40
Why then proofs by contradiction are not accepted by intuitionstic logic? –  Hans Stricker Jan 26 '11 at 8:19
That's because the last part about going from $\lnot F \rightarrow (C \land \lnot C)$ to $F$ is not valid in intuitionistic logic. You may find a related MO question interesting: mathoverflow.net/questions/12342/… –  Jason Jan 26 '11 at 9:23
I just realized your concern. In intuitionistic logic, proving that $\lnot F$ leads to a contradiction only allows you to conclude $\lnot\lnot F$ both syntactically and semantically; it does not allow you to conclude $F$ in general as in classical logic. –  Jason Jan 26 '11 at 11:45

I hope I won't mess this up; been some time since I played around with logics.

A key feature of every sound, consistent logic is that you can not prove $false$. If you add $\neg F$ to the assumptions (what is exactly what you do) and can now prove $false$ (by deriving a contradiction) -- syntactically, i.e. for all interpretations! -- the only reason for that can be that $\neg F$ is not true for any interpretation. This implies that $F$ holds for any interpretation.

Note that if you want to enter this in an interactive theorem prover, you might have to take care that all variables in $F$ are free or bound only in $F$.

-