First-order logic is kind of neat in that there are several ways to think about it that all turn out to give identical results.
When Γ is a set of formulas and P is a formula, the notation
Γ ⊢ P
called syntactic entailment, is the assertion that there is a deductive proof of P using the formulas in Γ as hypotheses. e.g. conjunction introduction is the axiom
P, Q ⊢ P ∧ Q
One formulation of proof by contradiction is
Γ, P ⊢ Q
Γ, P ⊢ ¬Q
therefore
Γ ⊢ ¬P
Some versions of logic have a symbol ⊥ that means "contradiction", in which case we would likely instead formulate this as
Γ, P ⊢ ⊥
therefore
Γ ⊢ ¬P
such proof forms may often use of
P, ¬P ⊢ ⊥
The conditional can be thought of as a means of converting the notion of entailment into propositional form; specifically
Γ, P ⊢ Q if and only if Γ ⊢ P → Q
Then, rather than working with the notion of entailment, one instead manipulates propositions. e.g. modus ponens
P, P → Q ⊢ Q
but we might instead see it given as the tautology
⊢ (P ∧ (P → Q)) → Q
Similarly, we can rephrase proof by contradiction as
(P → Q), (P → ¬Q) ⊢ ¬P
or as the tautology
⊢ ((P → Q) ∧ (P → ¬Q)) → ¬P
Using the contradiction symbol, we could also put this as
⊢ (P → ⊥) → ¬P
There's another notation
Γ ⊨ P
called semantic entailment. Since we're talking propositional logic, one ways to define this is that it is the assertion that every truth valuation that makes every statement in Γ true also makes P true.
(a truth valuation is simply a choice of truth value for each atomic proposition and computing the truth of more complex propositions by using the corresponding boolean operators on truth values)
For example, we can prove
P ⊨ P ∨ Q
by truth tables -- that is, by checking that each row of the truth table where P = true
also has P ∨ Q = true
.
We want implication to behave the same way: for example,
Γ, P ⊨ Q if and only if Γ ⊨ P → Q
Observe that the assertion P⊨Q is identical to
it's impossible to assign truth values in a way that makes P true and Q false
Consequently, the rows in the truth table that are false for P→Q
must be exactly the rows where P
is true and Q
is false — no more, no less.
Then, the magical thing about propositional logic (and of first-order logic) are the completeness theorem and the soundness theorem, which together say
Γ ⊢ P if and only if Γ ⊨ P
So that's what we're doing when we look at truth values — we are doing calculations and tabulations of truth values to work out semantic entailment, and using this theorem to determine syntactic entailment.
x=1 -> x*x=1
is true? You would surely also agree that it is possible forx=2
to be true?