What is a proof?

You've worked with proofs before. What is a proof?

Propositional Logic

Logic & Proofs

An unambiguous formal language, akin to a programming language.

• Syntax - vocabulary for expressing concepts without ambiguity
• Semantics - connection to what we're reasoning about
  • Interpretation — what the syntax means
  • Domain knowledge
• Reasoning - how to prove things
  • What steps are allowed

Domain knowledge

Previously, you've mostly seen proofs that heavily rely on domain knowledge, e.g., geometry, algebra, calculus. After all, the point was to learn about those domains. Here, the point is to learn about logic and proofs, so we will typically deemphasize domain knowledge.

Propositional Logic

One of many logics. One of the simplest and most common. The core of (almost) all other logics.

Soon, the course will also cover a more powerful logic.

Introduce syntax & semantics simultaneously.

Boolean constants

True, False

Propositions and Truth assignments

• E.g., circuits — "wire f is on"
• E.g., programs — "(at this program point) variable x has value 3"
• E.g., modeling life — "Dr. Greiner teaches Shakespeare on Film"
• However, propositions can't be parameterized
  • E.g., teaches(Greiner,comp280), teaches(Subramanian,comp140) not allowed
  • Severely limits flexibility — We'll allow this sort of thing later.

So, how can we model WaterWorld? What kinds of knowledge do we need to model?

Formulas

• Connectives — e.g., ∧, ∨, ¬, →
• Truth tables — a way to define the semantics of connectives
  • What a truth table is.
  • Examples for connectives.
  • English usage can be confusing — "or", "if"
• Parentheses & operations' associativity
• Defining other connectives
  • How many different truth tables for 2 inputs?
  • Define each function in terms of ∧, ∨, ¬, →
  • xor: ⊕
  • How many different truth tables for n inputs?

Axioms

A.k.a. assumptions — i.e., formulas we assume are true.

Two forms:

• Domain knowledge. E.g., in WaterWorld — game rules — suggestions?
• What is true in the given problem. E.g., in WaterWorld, what we currently know about the board

Domain knowledge example — WaterWorld

• Simple domain to use as a running example
• /home/comp280/bin/waterworld
• Quick demo
• Suggest propositions.
• Suggest axioms.