1. Formal Verification Proof

Hello, I am confused on much of the following...

Determine if the following formulas are satisfiable. P' is the negation of P.

(P→Q)→(Q'→P') <-- I read this as being P=true then Q=true, Q'=false then P'=false, so Q=true implies Q'=false???

(Q→R)→((P→Q)→(P→R)) <-- I read this as (Q→R)→(Q→R) because (P→Q)→(P→R) = (Q→R) right???

(P∧Q)→ (P∨Q) <-- AND versus OR ???

(Q→R)→((P∨Q)→(P∨R)) <--

TIA!

2. You're jumping ahead. $\displaystyle (P\rightarrow Q) \rightarrow (Q' \rightarrow P')$ is a single formula and so has a truth table which you can check by trying all four possible values for P and Q (it comes out true every time, that is, it is a tautology). In your example, P=true and Q=true we have $\displaystyle (P\rightarrow Q)$ and $\displaystyle (Q' \rightarrow P')$ both true, and so the overall formula is true.

A reason why propositional calculus is interesting is that, for an appropriate set of axioms, one can show that a propositional formula is deducible if and and only if it is a tautology.

Another reason is that the implication operator "captures" the notion of deducibility in the formal system: that is, Q can be deduced from P together with the axioms, if $\displaystyle P\rightarrow Q$ can be deduced from the axioms alone. This is a theorem, not part of the definition -- but of course the axioms are set up so that the theorem can be proved.

3. I understand the concepts of the truth tables and have gone ahead and generated those tables, however I am confused on the overall concept of "satisfiable". What exactly does this term mean?

Also, thanks for pointing out the "type" of calculus... now I can research it a bit more on the web.

4. Here is one such example...

p∨q = (p→q) → q

p q p→q P∨ q q
0 0 1 0 0
0 1 0 1 1
1 0 0 1 0
1 1 1 1 1

Hopefully the table is correct...