Barbara Term Logic example proved using Resolution

Problem

Case: “All A are B; All B are C; therefore All A are C.”

Premise 1. ∀x (A(x) → B(x))
Premise 2. ∀x (B(x) → C(x))
Conclusion. ∀x (A(x) → C(x))

Syllogistic mood: Barbara. In sets: A ⊆ B and B ⊆ C ⟹ A ⊆ C.

Answer

Valid. Using the Resolution method, the premises together with the negation of the conclusion yield a contradiction (empty clause).

Reason Why

Resolution-style justification (mathematical English)

  1. Encode “All A are B” and “All B are C” as clausal forms:
    ∀x(A→B) ≡ ∀x(¬A(x) ∨ B(x)) and ∀x(B→C) ≡ ∀x(¬B(x) ∨ C(x)).
  2. Negate the conclusion and clausify: ¬∀x(A→C) ≡ ∃x(A(x) ∧ ¬C(x)).
    Skolemize the witness to a new constant k, yielding unit clauses A(k) and ¬C(k).
  3. Apply Resolution (unification is trivial, x:=k):
    From (¬B(x) ∨ C(x)) and ¬C(k), resolve to ¬B(k).
    From (¬A(x) ∨ B(x)) and ¬B(k), resolve to ¬A(k).
    From A(k) and ¬A(k), resolve the empty clause ⟂.
  4. Unsatisfiability of the premises plus negated conclusion shows the original argument is valid; hence ∀x(A→C) follows from the premises.

This uses the Resolution Principle for Relational Logic (Stanford Ch.14) and the usual reading of Term Logic “All S are P” as ∀x(S(x)→P(x)).

Check (harness) #1

Direct set-inclusion check on a concrete model

Construct A ⊆ B ⊆ C explicitly and verify A ⊆ C.

Check (harness) #2

Randomized finite models (200 trials)

Sample random universes; enforce A ⊆ B ⊆ C; assert A ⊆ C always.

Check (harness) #3

Exhaustive search for counterexamples (|U| ≤ 3)

Enumerate all A ⊆ B ⊆ C configurations; report how many violate A ⊆ C (should be 0).

Check (harness) #4

Predicate implication on ℕ<50

Let M(x): “x is even”, W(x): “x divisible by 4”, A(x): “x is even or multiple of 3”. Verify ∀x(W→M) ∧ ∀x(M→A) ⟹ ∀x(W→A).

Check (harness) #5

Edge case: A = ∅

With A empty and B ⊆ C, premises hold and A ⊆ C holds vacuously.

Check (harness) #6

Your data: paste CSV sets for A, B, C

Format: lines “A: …”, “B: …”, “C: …” with comma-separated elements. The page validates premises and conclusion.

Check (harness) #7

Automated Resolution trace for Barbara

Runs the clausal proof of validity: premises + ¬conclusion ⟶ ⟂.