2
$\begingroup$

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.

2 Answers 2

3

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$.

  • 0
    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.2011-01-26
3

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$.