Proposititional logic Proof Theory Transformational Proof Semantic Tableaux

• Valid arguments
• Invalid arguments: if and only if there is at least one BV in which the premises are T, but the conclusion is F.
  • Find a counterexample: a Boolean valuation where the premises are T and the conclusion is F. Cannot use a proof theory to show argument is invalid. Need to come up with a Boolean valuation in which the premises are T and the conclusion is F.
• Consistency of premises
• Inference Rules
• Subproofs
  • Conditional proof
  • Indirect proof
  • Case analysis

Natural Deduction

Definition: Natural deduction is a proof theory for showing the validity of an argument in propositional logic. A collection of rules, called inference rules, each of which allos us to infer new formulas from given formulas. A form of forward proof. Starting from the presmises, use inference rules to deduce new formulas that logically follow from the premises. Using the formulas we have proven and the premises, we use the rules to deduce more formulas, continue this process until we have deduced the conclusion. P1, P2, …, Pn $⊢$ Q

Inference Rules

Definition: An inference rule is a primitive valid argument form. Each inference rule enables the elimination or the introduction of a logical connective.

For each step, we list the inference rule and the line labels of the previously deduced formulas that are used to deduce the new formula.

Subproofs

In a subproof, we start by choosing a formula that we assume is true within the subproof. Then we see what we can prove based on that assumption and any previously deduced formulas.

3 proof rules use this approach:

• Conditional proof (imp_i)
• Indirect proof / proof by contradiction (raa)
• Case analysis (cases)

There can be nested subproofs.

Subproofs are enclosed within {…} and indented, with the opening line of the subproof stating the assumption made in that subproof. The first line after the indented part shows what we are able to conclude from subproof.

Conditional Proof

Within subproof, we assume R, and then prove Q. The subproof marks the scope of the temporary assumption. Any lines in the box depend on the assumption. Line within the subproof depend on the assumption. Ends with implication outside the subproof.

Indirect Proof

The not_e rule is often used to get false in the proof. Often only way is to make us of the formula is to prove something that contradicst with it and use raa.

Case Analysis