Tableaux (First-Order Logic)

first-order-logic

Definition

Tableaux (First-Order Logic)

The first-order tableaux is a proof system for first-order logic. It works by systematically decomposing signed formulas of the form $t:\phi$ (true) and $f:\phi$ (false) using inference rules for the logical connectives and quantifiers.

Completion

Complete

Definition

Complete Tableaux (First-Order Logic)

A tableau is complete when all of its branches are complete.

Link to original

Open

Definition

Open Tableaux (First-Order Logic)

A tableau is open when at least one of its branches is open.

Link to original

Closed

Definition

Closed Tableaux (First-Order Logic)

A tableau is closed when all of its branches are closed.

Link to original

Branches

Complete Branch

Definition

Complete Branch (First-Order Tableaux)

A branch in a first-order tableau is complete when no further tableau rules can be applied to any signed formula on the branch.

Link to original

Open Branch

Definition

Open Branch (First-Order Tableaux)

A branch in a first-order tableau is open when it is complete (no further rules can be applied) and contains no pair $t:\phi$ and $f:\phi$ for the same formula $\phi$.

An open branch certifies that the initial formula is satisfiable.

Link to original

Closed Branch

Definition

Closed Branch (First-Order Tableaux)

A branch in a first-order tableau is closed when it contains both $t:\phi$ and $f:\phi$ for some formula $\phi$.

A tableau is closed when all of its branches are closed. A closed tableau certifies that the initial formula is unsatisfiable.

Link to original

Axioms

Conjunction

Definition

Definition

Conjunction (Propositional Tableaux)

$$\frac{t:(A\wedge B)}{t:At:B}\frac{f:(A\wedge B)}{f:A\mid f:B}$$

The $t$-rule for $\wedge$ creates a single branch (both conjuncts must hold). The $f$-rule creates two branches (at least one conjunct must fail).

Link to original

Link to original

Disjunction

Definition

Definition

Disjunction (Propositional Tableaux)

$$\frac{t:(A\vee B)}{t:A\mid t:B}\frac{f:(A\vee B)}{f:Af:B}$$

Link to original

Link to original

Negation

Definition

Definition

Negation (Propositional Tableaux)

$$\frac{t:(\neg A)}{f:A}\frac{f:(\neg A)}{t:A}$$

Link to original

Link to original

Implication

Definition

Definition

Implication (Propositional Tableaux)

$$\frac{t:(A\to B)}{f:A\mid t:B}\frac{f:(A\to B)}{t:Af:B}$$

Link to original

Link to original

Equivalence

Definition

Definition

Equivalence (Propositional Tableaux)

$$\frac{t:(A\leftrightarrow B)}{\begin{array}{c}t:At:B\\ \mid \\ f:Af:B\end{array}}\frac{f:(A\leftrightarrow B)}{\begin{array}{c}t:Af:B\\ \mid \\ f:At:B\end{array}}$$

Link to original

Link to original

Universal Quantifier

Definition

Universal Quantifier (First-Order Tableaux)

$$\frac{t:\forall xF}{t:F[t/x]}\frac{f:\forall xF}{f:F[c/x]}$$

• $t$: instantiate with any ground term $t$ (may be applied repeatedly).
• $f$: instantiate with a fresh parameter $c$ that does not yet appear on the branch.

Link to original

Existential Quantifier

Definition

Existential Quantifier (First-Order Tableaux)

$$\frac{t:\exists xF}{t:F[c/x]}\frac{f:\exists xF}{f:F[t/x]}$$

• $t$: instantiate with a fresh parameter $c$ that does not yet appear on the branch.
• $f$: instantiate with any ground term $t$ (may be applied repeatedly).

Link to original