Results 1 to 4 of 4

Math Help - Formal Verification Proof

  1. #1
    h2p
    h2p is offline
    Newbie
    Joined
    Oct 2005
    Posts
    5

    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)) <--

    I am probably going about this incorrectly... any help would be greatly appreciated.

    TIA!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Senior Member
    Joined
    Jun 2005
    Posts
    295
    Awards
    1
    You're jumping ahead. (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 (P\rightarrow Q) and (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 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.

    So your comment
    Follow Math Help Forum on Facebook and Google+

  3. #3
    h2p
    h2p is offline
    Newbie
    Joined
    Oct 2005
    Posts
    5
    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.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    h2p
    h2p is offline
    Newbie
    Joined
    Oct 2005
    Posts
    5
    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...
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Formal Proof
    Posted in the Geometry Forum
    Replies: 1
    Last Post: May 30th 2011, 01:12 PM
  2. Proof verification
    Posted in the Geometry Forum
    Replies: 1
    Last Post: March 7th 2011, 07:24 AM
  3. formal proof of set
    Posted in the Number Theory Forum
    Replies: 2
    Last Post: March 6th 2010, 10:36 PM
  4. Trig proof/verification help
    Posted in the Trigonometry Forum
    Replies: 1
    Last Post: January 28th 2010, 03:36 PM
  5. Formal Proof
    Posted in the Calculus Forum
    Replies: 0
    Last Post: November 12th 2008, 02:43 PM

Search Tags


/mathhelpforum @mathhelpforum