Appendix B. Laws for conditional exhaustiveness
Atomic sentences
The first of the following laws is stated only for unanalyzed sentences because laws of the same form for equations and other predications are special cases of the second and third laws:
Γ, A ⊨ A, Σ
Γ ⊨ τ = υ, Σ (where τ and υ are co-aliases given the equations in Γ)
Γ, Pτ1…τn ⊨ Pυ1…υn, Σ (where τi and υi, for i from 1 to n, are co-aliases given the equations in Γ)
Non-atomic sentences
For each logical constant which forms non-atomic sentences, there are two laws, one for cases where it appears among the assumptions and one for cases where it appears among the alternatives.
| Constant | As an assumption | As an alternative |
| ⊤ |
Γ, ⊤ ⊨ Σ
if and only if Γ ⊨ Σ |
Γ ⊨ ⊤, Σ |
| ⊥ | Γ, ⊥ ⊨ Σ |
Γ ⊨ ⊥, Σ
if and only if Γ ⊨ Σ |
| ¬ |
Γ, ¬ φ ⊨ Σ
if and only if Γ ⊨ φ, Σ |
Γ ⊨ ¬ φ, Σ
if and only if Γ, φ ⊨ Σ |
| ∧ |
Γ, φ ∧ ψ ⊨ Σ
if and only if Γ, φ, ψ ⊨ Σ |
Γ ⊨ φ ∧ ψ, Σ
if and only if both Γ ⊨ φ, Σ and Γ ⊨ ψ, Σ |
| ∨ |
Γ, φ ∨ ψ ⊨ Σ
if and only if both Γ, φ ⊨ Σ and Γ, ψ ⊨ Σ |
Γ ⊨ φ ∨ ψ, Σ
if and only if Γ ⊨ φ, ψ, Σ |
| → |
Γ, φ → ψ ⊨ Σ
if and only if both Γ ⊨ φ, Σ and Γ, ψ ⊨ Σ |
Γ ⊨ φ → ψ, Σ
if and only if Γ, φ ⊨ ψ, Σ |
| ∀ |
Γ, ∀x θx ⊨ Σ
if and only if Γ, ∀x θx, θτ ⊨ Σ |
Γ ⊨ ∀x θx, Σ
if and only if Γ ⊨ θα, Σ |
| ∃ |
Γ, ∃x θx ⊨ Σ
if and only if Γ, θα ⊨ Σ |
Γ ⊨ ∃x θx, Σ
if and only if Γ ⊨ θτ, ∃x θx, Σ |
| where τ is any term and α is independent in the sense that it does not appear in θ, Γ, or Σ | ||