4
$\begingroup$

I have a homework assignment that I am a little stumped on, the questions is:

Describe a sound and complete proof system (axioms and proof rules) for proposition logic. Explain in detail why you believe your proof system is sound and complete. Is your proof system terminating? If yes, explain why. If no, explain why not?

I am stumped for two reasons:

1) I can't seem to find an example of a "sound and complete proof system" my thinking here is that for a proof system to be useful it needs to be both sound and complete, so proof systems dont seem to bother to "state" that they are such.

2) When I asked the lecturer about the assignment, he said that we had discussed two proof systems in class that could be used. The only topics discussed seem to be proof by contradiction and proof by induction, however - I can't seem to find any reference as to what the axioms of these two are. For example, is the only axiom of proof by contradiction that: if $\bot \lnot A$ then $\top A$?

I'd appreciate any help/direction in this.

$\endgroup$
3
  • 1
    $\begingroup$ Have you seen the Wikipedia page of proposition calculus? There are some examples which might be worth looking at. Also, you may hack the question by implementing the brute-force algorithm, i.e. truth-table checking, but it seems like more work than doing what your professor intended you to do. $\endgroup$
    – dtldarek
    Oct 1, 2013 at 21:41
  • $\begingroup$ I havent looked at that page yet, I'm looking at axioms and modus ponens at the moment, trying to wrap my head around the idea of proofs a bit better - but I will look at that page shortly, presumably prop logic and prop calculus are closely related? $\endgroup$
    – Zack Newsham
    Oct 1, 2013 at 21:52
  • $\begingroup$ A proof system doesn't need to come as complete in order to qualify as useful. Some subsystems of classical logic aren't complete for two-valued logic, but DO come as useful for studying classical logic with respect to the independence of axioms, as well as finding other axiom sets for classical logic, and other metatheoretical topics. $\endgroup$
    – Doug Spoonwood
    Oct 2, 2013 at 4:48

1 Answer 1

Reset to default
4
$\begingroup$

I can't seem to find an example of a "sound and complete proof system".

It sounds as if your attention flickered at some point in class -- if your lecturer said that at some point he had discussed two proof systems, he probably did -- e.g. an axiomatic system, and/or a natural deduction alternative, or a proof system which goes via converting to disjunctive or conjunctive normal forms, or ....

Proof by contradiction would be a rule (one among a number of rules) in an ND system. (Induction though wouldn't be a rule in proof system for propositional logic; you may have encountered it being used in metatheorical proofs about propositional logic, but not in proofs in propositional logic.)

OK: have you been to the library? Chased up the lecturer's references/suggested course reading? Looked at some other elementary logic texts? Every single one will give you a sound and complete proof system for propositional logic, in one style of another. Look at a few such books, then.

Elementary areas of mathematics in general, and logic in particular, are wonderfully supplied with excellent textbooks. Consult them! That is what they are there for ...

$\endgroup$
3
  • $\begingroup$ thanks for the answer, I will try to get to a library and find some books on logic, but really - I don't think I "flickered" in the lecture, I have re-read the slides (ece.uwaterloo.ca/~vganesh/TEACHING/F2013/SATSMT/index.html) several times, and have found no reference to sound or complete proof systems, we have discussed induction and contradiction as my question said, and rules of how to convert to CNF, DNF, NNF as well as Demorgans laws, but none of those seem particularly relevant to this question (if your saying that proof by contradiction and induction are rules, not proofs) $\endgroup$
    – Zack Newsham
    Oct 1, 2013 at 22:44
  • $\begingroup$ From the slides: "To determine satisfiability, convert formula to DNF and just do a syntactic check." Is that a sound method? is it complete? $\endgroup$
    – Peter Smith
    Oct 1, 2013 at 23:16
  • $\begingroup$ It would depend on the check performed - but I do understand that by proving any one of the clauses true, you prove the entire expression, however - it doesn't discuss any proof rules used to determine the truth of any one clause, unless the previous statement can be considered rules, i.e. 1) does not contain false; 2) does not contain a negation of a literal and the same literal? $\endgroup$
    – Zack Newsham
    Oct 1, 2013 at 23:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .