Monday, October 13, 2025

Syllogistic after Ivo Thomas

This blog post presents Ivo Thomas’s 1949 system of formal syllogistic as documented by Arthur Prior here, but with new nicer notation, and with a bunch of extra proofs of meta results thrown in for good measure since it doesn’t cost any extra to add those. The main goals of doing this are, first, to give me a license to use traditional syllogistic forms whenever I want, because it’s all formalized here, and second, to spread this nice notation for the propositions which I thought was good, and which is based on the notation used by Wolfgang Lenzen to write about Leibniz’s “Theory of the Syllogism and Universal Calculus” in the book The Rise of Modern Logic by Gabbay and Woods, page 56. Really it is Lenzen’s notation but with the obvious modification to allow negative terms.

The system (i) admits negative terms and (ii) forbids empty terms. It is layered over classical propositional logic (with connectives ¬, ∧, →, ↔), and uses only modus ponens and uniform substitution for term variables at the propositional level. We give the syntax and intended semantics up front, state the axioms and rules precisely, and then derive the standard theorems. Given the possible choices of systems, I figured not allowing empty terms is best because it is closest to Aristotle and to natural language (which is, after all, where all syllogisms come from); if someone says “All As are Bs” and then it turns out there are no As, the main issue with their argument isn’t logical validity, it’s that by usual interpretation standards, they lied to me when stating that premise. Syllogisms are for the Agora, not for mathematicians. It happens that nowadays you have to have it all nice and formal somewhere or else someone gets suspicious, so this is what this post is. The parenthesized notation also adds brevity for when mentioning syllogisms on social media, etc.

Unicode is used for the things that did not involve any superscripts or subscripts, since that makes it easier to copy and paste the results, especially the syllogistic forms, which are the most useful results. \( \LaTeX \) is used for some results which were mostly meta results which only serve for bookkeeping anyway.

1. Language

1.1 Terms

  • Term variables: A, B, C, …
  • Term negation: if T is a term, so is ¬T (“non-T”).

We use term double-negation freely (see Rule R2): ¬¬T and T are interchangeable in term position.

1.2 Categorical forms

The primitive categorical form is A(B, C) read as “All B are C”.
We introduce the usual four schemata via definition by abbreviation (Defs D1–D3 below):

  • A(B, C) – universal affirmative
  • E(B, C) – universal negative
  • I(B, C) – particular affirmative
  • O(B, C) – particular negative

1.3 Propositional formation

If Φ and Ψ are formulas, so are ¬Φ, Φ ∧ Ψ, Φ → Ψ, Φ ↔ Ψ.
All tautologies of classical propositional logic are available, along with modus ponens and uniform substitution for term variables.

2. Definitions (usable both directions)

D1 (E as A with complement). E(B, C) ≝ A(B, ¬C).

D2 (I as not-E). I(B, C) ≝ ¬E(B, C) ≝ ¬A(B, ¬C).

D3 (O as not-A). O(B, C) ≝ ¬A(B, C).

Remark. With D1–D3 in hand, one may work in an A+¬ core (only A(–,–) plus propositional negation), treating E, I, O as shorthands.

3. Proof System

3.1 Propositional backbone

All classical tautologies over ¬, ∧, →, ↔; inference by Modus Ponens; uniform substitution for term variables inside categorical forms.

3.2 Special axioms (hold schematically for all terms A, B, C)

  • A1 (Reflexive A). A(B, B).
  • A2 (Reflexive I – existence). I(B, B).
  • A3 (Barbara). (A(B, C) ∧ A(A, B)) → A(A, C).
  • A4 (Ferio). (E(B, C) ∧ I(A, B)) → O(A, C).

3.3 Special rule about negative terms

  • R1 (Term Double-Negation, T-DN). Within any formula, you may replace any term ¬¬T by T (and conversely).

This rule is validated semantically by §4.3.

4. Intended Semantics

We fix the “intended” class of models in which the calculus is evaluated.

4.1 Structures and term denotations

A structure is a pair \( \mathcal M=\langle U, v\rangle \) where:

  1. \(U\) is a nonempty universe.
  2. Each term (built from variables by prefix ¬) is assigned a subset of \(U\) by an interpretation function \(v\), subject to:
  • Properness / non-emptiness: for every term (T),
    \( \varnothing \neq v(T) \subsetneq U\).
  • Complement clause for term negation:
    \( v(\neg T) ;=; U \setminus v(T)\).

Note. The properness clause for every term \(T\) and its complement \( \neg T\) immediately implies \(|U|\ge 2\).

4.2 Truth for categorical formulas

Truth of categoricals is defined from subsethood; propositional connectives use classical truth tables.

  • \( \mathcal M \models A(B,C) \) iff \( v(B) \subseteq v(C)\).

  • The remaining forms are abbreviations (Defs D1–D3):

  • \(E(B,C) := A(B,\neg C)\),

  • \(I(B,C) := \neg E(B,C) \equiv \neg A(B,\neg C)\),

  • \(O(B,C) := \neg A(B,C)\).

Thus, for example, \( \mathcal M \models I(B,C)\) iff \(v(B)\cap v(C)\neq\varnothing\), and \( \mathcal M \models O(B,C)\) iff \(v(B)\nsubseteq v(C)\).

4.3 Consequences used later

From 4.1–4.2 we record basic facts used in proofs:

  • (S1) \(X \subseteq X\).
  • (S2) If \(X \subseteq Y\) and \(Y \subseteq Z\), then \(X \subseteq Z\).
  • (S3) \(X \subseteq U\setminus Y\) iff \(X\cap Y=\varnothing\).
  • (S4) If \(X\cap Y\neq\varnothing\) and \(Y\subseteq U\setminus Z\), then \(X\nsubseteq Z\).
  • (S5) For every term \(T\), both \(v(T)\) and \(v(\neg T)=U\setminus v(T)\) are nonempty (by properness).

Two immediate semantic validations we will appeal to:

  • Term double-negation (R1): \(v(\neg\neg T)=U\setminus(U\setminus v(T))=v(T)\).
  • Existence axiom (A2): \(I(T,T)\) is true because \(I(T,T)\equiv \neg A(T,\neg T)\), and \(A(T,\neg T)\) would force \(v(T)\subseteq U\setminus v(T)\), impossible by (S5).

Why substitution is sound. Because \(v(\neg T)\) is fixed as set-complement and all categorical truth conditions are expressed purely in terms of the sets \(v(\cdot)\), uniformly replacing term variables by (possibly negated) terms preserves truth in every structure.

5. Elementary Equivalences (Obversion)

We record the standard obversions as theorems provable by definitional replacement (D1–D3) and T-DN.

T1 (Obversion A/E with complement). A(B, C) ↔ E(B, ¬C).
Proof. E(B, ¬C) ≝ A(B, ¬¬C) (D1), T-DN on C.

T2 (Obversion E/A with complement). E(B, C) ↔ A(B, ¬C). (This is D1.)

T3 (Obversion I/O with complement). I(B, C) ↔ O(B, ¬C).
Proof. I(B, C) ≝ ¬A(B, ¬C) (D2+/-D1) and O(B, ¬C) ≝ ¬A(B, ¬C) (D3).

T4 (Obversion O/I with complement). O(B, C) ↔ I(B, ¬C).
Proof. O(B, C) ≝ ¬A(B, C) (D3); I(B, ¬C) ≝ ¬A(B, ¬¬C) (D2+/-D1), T-DN on C.

6. Conversion and Symmetry

L5 (Simple Conversion of E). E(B, C) → E(C, B).
Proof.
(1) From A4 with A := C: (E(B, C) ∧ I(C, B)) → O(C, C).
(2) By D3, O(C, C) ≝ ¬A(C, C).
(3) So E(B, C) → (I(C, B) → ¬A(C, C)).
(4) Instantiation of the tautology ((P → ¬R) → (R → ¬P)) with P := I(C, B), R := A(C, C) yields (I(C, B) → ¬A(C, C)) → (A(C, C) → ¬I(C, B)).
(5) From (3) and (4): E(B, C) → (A(C, C) → ¬I(C, B)).
(6) By A1, A(C, C).
(7) Hence E(B, C) → ¬I(C, B).
(8) By D2, ¬I(C, B) ↔ E(C, B). QED.

Corollary 6.1 (E is symmetric). E(B, C) ↔ E(C, B) (by repeating the same derivation with B, C swapped).

Corollary 6.2 (Symmetry of I). I(B, C) ↔ I(C, B) (by D2 from Cor. 6.1).

7. Contraposition and Subalternation

T7 (Contraposition for A). A(B, C) → A(¬C, ¬B).
Proof.
(1) By T1, A(B, C) ↔ E(B, ¬C).
(2) By L5, E(B, ¬C) → E(¬C, B).
(3) By D1, E(¬C, B) ≝ A(¬C, ¬B).
Chain (1)–(3). QED.

T8 (Subalternation with non-empty subjects).
(i) A(B, C) → I(B, C).
(ii) E(B, C) → O(B, C).

Proof.
(i) Darii (see T10 below) says (A(B, C) ∧ I(A, B)) → I(A, C).
Instantiate A := B, then use A2 (I(B, B)): A(B, C) → I(B, C).
(ii) From A4 (Ferio) with A := B and A2: E(B, C) → O(B, C). QED.

8. Standard Syllogisms

I thought to include all 24 forms for easy reference. They’re all valid here because there are no empty terms.

Figure 1

A3 (Barbara – axiom – AAA-1). (A(B, C) ∧ A(A, B)) → A(A, C).

T9 (Celarent – EAE-1). (A(A, B) ∧ E(B, C)) → E(A, C).
Proof. E(B, C) ≝ A(B, ¬C) (D1). By A3 with C := ¬C, obtain A(A, ¬C). Obvert via D1 to E(A, C).

T10 (Darii – AII-1). (A(B, C) ∧ I(A, B)) → I(A, C).
Proof. From A(B, C) obvert (T1) to E(B, ¬C). Apply A4 (Ferio) with C := ¬C to get (E(B, ¬C) ∧ I(A, B)) → O(A, ¬C). Obvert (T4) O(A, ¬C) ↔ I(A, C).

A4 (Ferio – axiom – EIO-1). (E(B, C) ∧ I(A, B)) → O(A, C).

From here we begin using S for the subject (major term), M for the middle term, P for the predicate (minor term).

T11 (Barbari – AAI-1). (A(M, P) ∧ A(S, M)) → I(S, P).
Proof. A3 yields A(S, P); then Subalternation T8(i) gives I(S, P).

T12 (Celaront – EAO-1). (E(M, P) ∧ A(S, M)) → O(S, P).
Proof. T9 gives E(S, P); then Subalternation T8(ii) yields O(S, P).

Figure 2

T13 (Cesare – EAE-2). (E(P, M) ∧ A(S, M)) → E(S, P).
Proof. Convert E(P, M) to E(M, P) (E-symmetry, §6); apply T9.

T14 (Camestres – AEE-2). (A(P, M) ∧ E(S, M)) → E(S, P).
Proof. Convert E(S, M) to E(M, S); apply T9 with A := P, B := M, C := S to get E(P, S); convert back by E-symmetry to E(S, P).

T15 (Festino – EIO-2). (E(P, M) ∧ I(S, M)) → O(S, P).
Proof. Convert E(P, M) to E(M, P); apply A4 with B := M, C := P, A := S.

T16 (Baroco – AOO-2). (A(P, M) ∧ O(S, M)) → O(S, P).
Proof. From A3, (A(S, P) ∧ A(P, M)) → A(S, M). With O(S, M) ≝ ¬A(S, M), propositional reasoning yields ¬A(S, P), i.e., O(S, P).

T17 (Cesaro – EAO-2). (E(P, M) ∧ A(S, M)) → O(S, P).
Proof. By T13 obtain E(S, P); Subalternation T8(ii) yields O(S, P).

T18 (Camestros – AEO-2). (A(P, M) ∧ E(S, M)) → O(S, P).
Proof. By T14 obtain E(S, P); Subalternation T8(ii) yields O(S, P).

Figure 3

T19 (Datisi – AII-3). (A(M, P) ∧ I(M, S)) → I(S, P).
Proof. Convert I(M, S) to I(S, M) (I-symmetry, §6); apply T10 with B := M, C := P, A := S.

T20 (Disamis – IAI-3). (I(M, P) ∧ A(M, S)) → I(S, P).
Proof. Convert I(M, P) to I(P, M); apply T10 with A := P, B := M, C := S to get I(P, S); convert back via I-symmetry.

T21 (Ferison – EIO-3). (E(M, P) ∧ I(M, S)) → O(S, P).
Proof. Convert I(M, S) to I(S, M); apply A4 with B := M, C := P, A := S.

T22 (Bocardo – OAO-3). (O(M, P) ∧ A(M, S)) → O(S, P).
Proof. From A3, (A(S, P) ∧ A(M, S)) → A(M, P). With O(M, P) ≝ ¬A(M, P), propositional reasoning yields ¬A(S, P), i.e., O(S, P).

T23 (Felapton – EAO-3). (E(M, P) ∧ A(M, S)) → O(S, P).
Proof. From A2 (I(M, M)) and A(M, S), T10 gives I(M, S); I-symmetry gives I(S, M). Combine with E(M, P) and apply A4 with B := M, C := P, A := S.

T24 (Darapti – AAI-3). (A(M, P) ∧ A(M, S)) → I(S, P).
Proof. From A2 and A(M, S), T10 yields I(M, S); I-symmetry gives I(S, M). With A(M, P) and I(S, M), T10 yields I(S, P).

Figure 4

T25 (Calemes – EAE-4). (E(P, M) ∧ A(S, M)) → E(S, P).
Proof. Convert E(P, M) to E(M, P) (E-symmetry) and apply T9. (Same reduction pattern as T13/Cesare, in 4th-figure form.)

T26 (Dimatis – IAI-4). (I(P, M) ∧ A(M, S)) → I(S, P).
Proof. Convert I(P, M) to I(M, P); apply T10 with A := P, B := M, C := S to obtain I(P, S); I-symmetry gives I(S, P).

T27 (Fresison – EIO-4). (E(P, M) ∧ I(M, S)) → O(S, P).
Proof. Convert E(P, M) to E(M, P) and I(M, S) to I(S, M); apply A4.

T28 (Calemos – EAO-4). (E(P, M) ∧ A(M, S)) → O(S, P).
Proof. From A2 and A(M, S), T10 gives I(M, S); I-symmetry gives I(S, M). Convert E(P, M) to E(M, P); apply A4.

T29 (Fesapo – EAO-4). (E(P, M) ∧ A(S, M)) → O(S, P).
Proof. Subalternation T8(i) gives I(S, M) from A(S, M); convert E(P, M) to E(M, P); apply A4.

T30 (Bamalip – AAI-4). (A(P, M) ∧ A(M, S)) → I(S, P).
Proof. From A2 and A(M, S), T10 gives I(M, S); I-symmetry yields I(S, M). With A(P, M) and I(S, M), T10 concludes I(S, P).

9. Soundness proof

Below we verify that every axiom schema and the term double-negation rule are valid in the intended semantics given earlier (universe nonempty; every term—positive or negative—denotes a proper nonempty subset of the universe; ¬ on terms is set-complement; A(B,C) means ⟦B⟧ ⊆ ⟦C⟧; the other forms are by D1–D3).

We also note why the propositional backbone (tautologies + modus ponens + uniform substitution of terms) is sound.

9.1. Preliminaries

We work throughout in the intended semantics fixed in §4:

  • Structures \( \langle U,v\rangle \) have \(U\neq\varnothing\); every term denotes a proper, nonempty subset; and \(v(\neg T)=U\setminus v(T)\).
  • Categorical truth is defined by \(A(B,C)\) as subsethood; \(E,I,O\) are abbreviations (D1–D3).
  • We freely use the set-theoretic facts (S1)–(S5) from §4.3.

With these conventions:

  • Definitions D1–D3 are satisfied by construction (they are abbreviations for the given truth conditions).
  • Rule R1 (term double-negation) is valid by \(v(\neg\neg T)=v(T)\).
  • The propositional backbone (tautologies + modus ponens + uniform substitution on term variables) is sound because the semantics is compositional and treats term negation as Boolean complement (see the note at the end of §4.3).

(The subsequent soundness checks in §9.2–§9.4 now proceed by citing §4 rather than re-introducing the semantics.)

9.2. Soundness of Definitions

By inspection of the clauses above, D1–D3 are satisfied in every structure (they are not extra assumptions but the truth-conditions for E, I, O). Thus replacing an occurrence of E, I, O by its definiens (or conversely) preserves truth in all structures.

9.3. Soundness of the Special Rule R1 (by §4.3)

R1 (Term double-negation). For every term T, v(¬¬T) = U∖(U∖v(T)) = v(T), so intersubstituting T and ¬¬T in any term position preserves the denotation and hence the truth-value of any formula. Therefore R1 is valid.

9.4. Soundness of the Special Axioms

All are schemas in the term variables; we prove each is true in every structure under every assignment.

A1 (Reflexive A). A(B,B).
True because v(B) ⊆ v(B) by (F1).

A2 (Reflexive I). I(B,B).
By D2, this is ¬A(B,¬B). But A(B,¬B) would mean v(B) ⊆ U∖v(B), which is impossible unless v(B)=∅; since v(B)≠∅ by (F5), A(B,¬B) is false, hence I(B,B) is true.

A3 (Barbara). (A(B,C) ∧ A(A,B)) → A(A,C).
Assume the antecedent is true: v(B)⊆v(C) and v(A)⊆v(B). Then by (F2), v(A)⊆v(C), so the consequent A(A,C) is true.

A4 (Ferio). (E(B,C) ∧ I(A,B)) → O(A,C).
By D1, E(B,C) is A(B,¬C), i.e. v(B)⊆U∖v(C).
By D2, I(A,B) is ¬A(A,¬B), i.e. not v(A)⊆U∖v(B), equivalently v(A)∩v(B)≠∅.
Pick x ∈ v(A)∩v(B). Since x ∈ v(B)⊆U∖v(C), we have x ∉ v(C); yet x ∈ v(A). Hence v(A)⊄v(C), i.e. ¬A(A,C). By D3, that is O(A,C). Therefore the implication holds.

Thus A1–A4 are valid.

9.5. Soundness of the Propositional Backbone and Substitution

  • Classical propositional tautologies are valid by definition of the connectives.
  • Modus Ponens preserves validity: if Φ and Φ→Ψ are true in every structure, then so is Ψ.
  • Uniform substitution for term variables (e.g., replacing A,B,C by arbitrary terms built using ¬) preserves validity because our semantics is compositional in term denotations and v(¬T) is fixed as complement; thus if a schema is true for all denotations of its term variables, it remains true after any uniform replacement of those variables by possibly negated terms.

9.6. Conclusion

Every instance of the special axioms A1–A4 and the rule R1 is true in every structure under the intended semantics. Together with the propositional backbone, this yields the soundness of the proof system: any theorem derivable from these axioms and rules is valid in all intended models.

10. Completeness proof

Below is a standard canonical-model (Lindenbaum) completeness proof tailored to this system.
We write ⊢ for derivability in the calculus from §3 of the write-up and ⊨ for truth in the intended class of models from §4 (nonempty universe; every term denotes a proper, nonempty set; term negation is set complement; A(B,C) means inclusion).

Theorem (Completeness): For every formula \( \varphi \) in the language, if \( \models \varphi \) (true in all intended structures), then \( \vdash \varphi \).

We prove the contrapositive: if \( \nvdash \varphi \), there is an intended structure \( \mathcal M \) with \( \mathcal M \nvDash \varphi \).

10.1. Maximal (propositionally) consistent theory

Assume \( \nvdash \varphi \). By classical propositional completeness/compactness (our backbone) there exists a maximal consistent set \( \Sigma \) of formulas such that:

  • \( \Sigma \) contains all theorems of the system (axioms and their consequences),
  • \( \neg \varphi \in \Sigma \),
  • for every formula \( \psi \), exactly one of \( \psi,\neg\psi \) is in \( \Sigma \).

We will build a model of \( \Sigma \) (hence a countermodel to \( \varphi \)).

10.2. Propositional skeleton over term-membership

Introduce propositional variables \( p_T \) for every term \(T\) (including negated terms).

Let \(H_\Sigma\) be the following propositional theory:

  • (H1) Implications from all (A)-theorems.
    For every \(A(X,Y) \in \Sigma\) put the clause \((p_X \rightarrow p_Y)\) into \(H_\Sigma\).

  • (H2) Complement coherence.
    For every term \(T\), include
    \[
    (p_T \leftrightarrow \neg p_{\neg T}) \quad\text{and}\quad (p_T \leftrightarrow p_{\neg\neg T}).
    \]
    (This enforces that ( \neg ) on terms acts as Boolean complement and validates term double-negation.)

Call a Boolean valuation (v) admissible iff (v \models H_\Sigma).

Two immediate facts (using only propositional logic and the theorems A1, A2):

  • F1 (Existence of admissible valuations with prescribed polarity).
    For any term \(T\), both \(H_\Sigma \cup{p_T}\) and \(H_\Sigma \cup{\neg p_T}\) are satisfiable.
    Reason. If \(H_\Sigma \cup{p_T}\) were inconsistent, then \(H_\Sigma \models \neg p_T\), which (unwinding H2) would amount to deriving \(A(T,\neg T)\); but \(\neg A(T,\neg T)\) is the theorem \(I(T,T)\) (A2). Similarly for \(\neg p_T\) using \(I(\neg T,\neg T)\).

  • F2 (Separation for non-derivable inclusions).
    If \(A(B,C)\notin \Sigma\), then there is an admissible \(v\) with \(v(p_B)=1\) and \(v(p_C)=0\).
    Reason. Otherwise \(H_\Sigma\models(p_B\rightarrow p_C)\), hence by (H1) \(A(B,C)\in\Sigma\), contradiction.

10.3. Canonical model \( \mathcal M_\Sigma \)

  • Universe. \(U := {, v \mid v \text{ is an admissible valuation for } H_\Sigma ,}\) (nonempty by F1).

  • Interpretation of terms.
    \(⟦ T⟧ := {, v\in U \mid v(p_T)=1 ,}\).

By (H2): \(⟦ \neg T⟧ = U\setminus ⟦ T⟧\) and \(⟦ \neg\neg T⟧=⟦ T⟧\).
By F1: for every \(T\), both \(⟦ T⟧\) and \(U\setminus⟦ T⟧=⟦\neg T⟧\) are nonempty, so every term denotes a proper, nonempty subset. Thus \( \mathcal M_\Sigma \) is an intended structure.

  • Truth condition for (A).
    For any terms \(X,Y\),
    \[
    \mathcal M_\Sigma \models A(X,Y) \quad\Longleftrightarrow\quad
    \forall v\in U,(v(p_X)=1 \Rightarrow v(p_Y)=1).
    \]
    But by (H1) every \(v\in U\) satisfies \((p_X\rightarrow p_Y)\) iff \(A(X,Y)\in\Sigma\). Hence

Truth Lemma for (A). \( \mathcal M_\Sigma \models A(X,Y) \) iff \( A(X,Y) \in \Sigma \).

  • Other categorical forms.
    (E, I, O) are definitions (D1–D3), and term \( \neg \) coincides with set complement in \( \mathcal M_\Sigma \); hence the Truth Lemma extends immediately:
    \[
    \mathcal M_\Sigma \models \Psi \quad\Longleftrightarrow\quad \Psi\in\Sigma
    \]
    for every atomic categorical \( \Psi\in{A(E!/!I!/!O)(-, -)} \).

  • Propositional connectives.
    The semantics is classical and \( \Sigma \) is maximal consistent; thus the usual induction on formula complexity gives the full Truth Lemma:

Truth Lemma (full). For every formula \( \Phi\), \( \mathcal M_\Sigma \models \Phi \) iff \( \Phi\in\Sigma\).

(Inductive steps: for \( \neg\Phi\), use maximality of \( \Sigma\); for \( \Phi\land\Psi, \Phi\to\Psi\) use classical truth tables; for atomics, use the (A)-case plus D1–D3.)

10.4. Countermodel to \( \varphi \)

Since \( \neg\varphi\in\Sigma\), the Truth Lemma yields \( \mathcal M_\Sigma \models \neg\varphi\); hence \( \mathcal M_\Sigma \nvDash \varphi\). As \( \mathcal M_\Sigma \) is an intended structure, \( \varphi \) is not valid.

Taking the contrapositive completes the proof. \(\square\)

10.5. Remarks

  1. The only “set-theoretic” ingredient is ordinary propositional completeness/compactness used in Step 1 and in F1–F2. No quantifier Henkinization is needed.
  2. The model explicitly enforces the term negation as set-complement (H2) and validates term double-negation automatically.
  3. Axiom A2 (the “no empty terms” principle) is exactly what guarantees properness (both ( ⟦ T⟧ ) and ( ⟦\neg T⟧ ) are nonempty) in the canonical model.

11. Extra results

This is more stuff someone could want.

11.1 Compactness

The logic is compact for satisfiability and entailment.
Reason: the completeness proof (Section 10) already builds a canonical model from a maximal propositional theory and uses only classical propositional compactness. Thus, if every finite Γ₀ ⊆ Γ is satisfiable (in the intended semantics), then Γ is satisfiable.

11.2 Finite / small model property

Let Γ be any finite set of formulas mentioning the distinct term letters (T_1,\dots,T_n).

  • Finite model property. If Γ is satisfiable, it has an intended model with finite universe.
  • Explicit small bound. There is a model of size ≤ (2^n) satisfying Γ (and, because every term and its complement must be nonempty, the size is also ≥ 2 whenever Γ is consistent with A2).

Sketch. Expand Γ using D1–D3 so that only literals of the shape \(A(X,Y)\) and ¬\(A(X,Y)\) remain. Form the finite Horn theory \(H_\Gamma\) consisting of \(p_X \to p_Y\) for every positive \(A(X,Y)\) in Γ together with the complement clauses \(p_T \leftrightarrow \neg p_{\neg T}\) and \(p_T \leftrightarrow p_{\neg\neg T}\) for each \(T\) occurring. Let U be the set of all Boolean valuations of the finitely many \(p_{T_i}\) that satisfy \(H_\Gamma\).

  • Then the universe is \(U\) (finite, (|U|\le 2^n)\).
  • Interpret each term by \(⟦ T⟧={,v\in U: v(p_T)=1,}\).
  • Positive \(A(X,Y)\) hold because every \(v\in U\) satisfies \(p_X\to p_Y\).
  • For each negative ¬\(A(B,C)\) in Γ, consistency guarantees at least one \(v\in U\) with \(v(p_B)=1, v(p_C)=0\), which witnesses \(⟦ B⟧\nsubseteq⟦ C⟧\).
  • A2 ensures we can realize both polarities \(p_T\) and \(\neg p_T\) among valuations, so every \(⟦ T⟧\) and its complement are nonempty.

Hence Γ has a finite intended model; the bound follows from \(|U|\le 2^n\).

11.3 Decidability (two easy procedures)

(A) Conjunctions of categoricals (the “pure syllogistic” fragment)

When premises are a conjunction of A/E/I/O and the goal is a single categorical (or satisfiability of the premises), the problem reduces to graph reachability:

  1. Expand E/I/O using D1–D3 to obtain a set S of positive inclusions \(A(X,Y)\) and a set N of negative inclusions ¬\(A(B,C)\).
  2. Close S under reflexivity, transitivity, and contraposition (T7): from \(A(X,Y)\) add \(A(\neg Y,\neg X)\).
  3. Consistency check: reject if S forces \(A(T,\neg T)\) for some T (violates A2).
  4. Witness check for each ¬(A(B,C)) ∈ N: reject iff \(B\) reaches \(C\) in the closure (i.e., \(A(B,C)\) is already entailed).

All steps are polynomial-time on the number of distinct terms (essentially reachability on a directed graph over the 2n nodes \(T_1,\neg T_1,\dots,T_n,\neg T_n)\).

(B) Full language (arbitrary propositional combos)

For an arbitrary formula Φ:

  • Normalize with D1–D3 so only atoms \(A(X,Y)\) appear under propositional connectives.
  • Decide satisfiability by a standard SAT-style search over truth assignments to the finitely many \(A(X,Y)\)-atoms, using the polynomial-time oracle from \(A\) to accept/reject each candidate conjunction.
    By compactness and the small model property, this terminates, giving a decision procedure for satisfiability (and hence validity/entailment).

(We did not optimize complexity here; the point is: the logic is decidable by an elementary, effective procedure.)

11.4 Independence: the “no empty terms” axiom A2

A2 (I(B,B)) is independent of the remaining principles (propositional backbone, substitution, R1, A1, A3, A4).

Reason. Consider the same semantics as in §4 but drop the properness requirement (allow some term denotations to be empty).

  • Then A1 (reflexivity), A3 (Barbara), and A4 (Ferio) all remain valid (their semantic justifications use only subset facts and, for A4, the nonemptiness premise is inside \(I(A,B)\) itself).
  • However A2 fails in any such model taking \(v(B)=\varnothing\): then \(A(B,\neg B)\) is true and so \(I(B,B)\equiv \neg A(B,\neg B)\) is false.
    Thus A2 cannot be derived from the others.

11.5 Model-size spectrum

Independent of any particular theory Γ, the class of intended models contains structures of every finite size ≥ 2 (and infinite ones).
Construction: fix \(|U|=m\ge2\); assign to each term \(T\) any proper nonempty subset of \(U\) (e.g., singletons), with \(v(\neg T)=U\setminus v(T)\). This shows there are arbitrarily large finite intended structures.

11.6 Normal forms and conservativity

  • The system is a definitional extension of its A+¬ core: every formula is propositionally equivalent to a Boolean combination of atoms \(A(X,Y)\) only (E/I/O are eliminable using D1–D3, R1 removes ¬¬ in term position).
  • Consequently, metatheory (soundness/completeness/compactness/decidability) can be proved working only with A+¬, and then transferred to the full language by definitional equivalence.
at

No comments:

Post a Comment