Debates and Proofs: Course Goals

We claim that winning debates is easier than providing formal proofs. One form of doing a debate for a claim c would be: The verifier and the falsifier provide a proof in a formal system, and a proof checker decides who has won the debate.

Only a few people can do formal proofs and most proofs are informal and beyond the limits of a proof checker.

That is why we use debates based on semantic games. They are much more light-weight than proofs and their constructive nature has several benefits.

Structural Argument

We build our argument that debates are simpler than proofs on the rules for semantic games. In the following table, v stands for verifier and f for falsifier. A is a structure defined by sets, functions and relations.

ForAll

The verifier must have a reason (but not necessarily a proof) why no refutation is possible by falsifier. If the verifier wins, the debate does not give a reason why.

Example: ForAll n in Nat: B(n)=C(n). The verifier of this claim must have strong arguments why the equality holds. Ideally, the verifier should be able to derive C(n) from B(n).

This example illustrates Karl Popper's views on Conjectures and Refutations: http://plato.stanford.edu/entries/popper/.

Exists

The verifier needs an algorithm to defend the claim but does not necessarily need a proof why the algorithm is correct. If the falsifier wins, the debate does not give a reason why.

And

The verifier must have a reason (but not necessarily a proof) why both subexpressions are true, i.e., why no refutation is possible by falsifier.

Or

The verifier needs an algorithm to decide which subexpression can be defended but not necessarily a proof why the algorithm is correct.

Special Case: Debate Results in Proof

If the claim only involves the universal quantifier ForAll and the Boolean connective "and", and the falsifier wins, the debate results in a proof that the claim is false.

If the claim only involves the existential quantifier Exists and the Boolean connective "or", and the verifier wins, the debate results in a proof that the claim is true.

In the above two cases one side takes all actions during the debate.

What We Want to Achieve

Course Goal 1: Given a claim related to algorithms, you correctly choose the right side (verifier or falsifier) and you successfully defend the chosen side against another participant. In other words, you don't let yourself be pushed into a contradiction.

Course Goal 2: For simple claims related to algorithms you can give an informal proof why they are true or false.

Opportunity to Improve

The debater taking the correct decision (verifier or falsifier) will always have a chance of improving its strategy when it loses, while the debater taking the incorrect decision will not always have that chance. Therefore, assuming that the two parties are keen on winning, then, eventually, after playing several SGs and improving their strategies between SGs, the debater taking the correct decision will discover the winning strategy and will always win.

Formal Debates | Study Groups | Domain Discourse Predicates