Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
add comment

2 Answers

up vote 3 down vote accepted

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

share|improve this answer
    
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
add comment

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

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.