Foundations table

This is based on the ending of Foundations without Foundationalism by Steward Shapiro.

Make a table comparing these foundations (including full SOL)

Here’s a quick side-by-side of the contenders (plus plain FOL and full SOL for context):

System / foundation	What it adds beyond FOL	Compact?	Up-LS?	Down-LS?	Effective completeness?	Can define finitude?	ℕ categorical?	ℝ categorical?	One-line vibe
First-order logic (FOL)	—	✓	✓	✓	✓	✗	✗	✗	Tame meta-theory, limited expressiveness.
Full second-order logic (SOL)	Quantify over all relations/functions	✗	✗	✗	✗	✓	✓	✓	Max expressiveness; “unmanageable” meta-theory.
Monadic SOL (MSO)	Quantify only over unary sets	✗	✗	✗	✗	✓	✓¹	✓¹	Often as strong as SOL (with pairing); some decidable fragments.
Weak SOL	SO vars range over finite relations	✗	✗	✓	✗	✓	✓	✗	Builds finitude in; stronger than FOL but < SOL.
(L(Q_0))	Quantifier (Qx,\Phi) = “infinitely many (x)”	✗	✗	✓	✗	✓	✓	✗	Talks infinity natively; still weaker than SOL.
(\omega)-logic	Validity only in (\omega)-models	✗	✗	✓	✗	✓	✓	✗	Bakes in natural-number shape of (<).
Ancestral logic	Operator for ancestral/closure (R^*)	✗	✗	✓	✗	✓	✓	✗	Great for “least closure”/reachability facts.
Quasi-weak SOL (L2q)	Quantify over countable relations	✗	✗	(to ≤ c)²	✗	✓	✓	✓	Adds countability power; can pin down analysis.
Infinitary (L_{\omega_1\omega})	Countable ∧/∨ (finitary quantifiers)	✗	✗	✓ (ℵ₀)	partial³	✓	✓	✗⁴	“Brute-force” expressiveness; still below SOL.
Substitutional semantics (FOL)	Truth via terms (all denoting)	✗	✗	✗	✗	◐⁵	✓⁶	✗⁷	Language-dependent strength; every element named.
Free-variable SOL ( (L2K^{-}) )	Only free SO vars; instantiate sets	—⁸	—	—	weak only	◐⁹	✓	✓	Avoids existential commitment to relations; not closed under complements.
First-order ZFC (as meta-foundation)	Uniform set-theoretic semantics	✓	✓	✓	✓	✓*	✗	✗	Powerful common metalanguage; nonstandard-model issues if taken model-theoretically.

Legend. ✓ = yes; ✗ = no; ◐ = limited/with caveats; — = not a standard/meaningful entry.

Notes

1. With a definable pairing (e.g., arithmetic has (f(x,y)=2^x3^y)), monadic SOL matches full SOL for arithmetic/analysis, so it categorically pins down (\mathbb N) and (\mathbb R). Without pairing, strength drops and some fragments are even decidable.
2. For (L2q), there’s a Skolem-type downward result to a structure of size ≤ continuum while preserving (L2q)-truths.
3. (L_{\omega_1\omega}) has completeness for countable sets of premises (not full strong completeness).
4. (\mathbb R) becomes categorical at (L_{\omega_1\omega_1}), not already at (L_{\omega_1\omega}).
5. No general finitude characterization: depends heavily on how many constants/terms are in the language (you can force small finite models, but not “finiteness” in general).
6. You can make arithmetic categorical by naming all numerals (or with a small finite signature under a tweak), but this hinges on the signature; uncountable structures aren’t reachable unless you have uncountably many terms.
7. In practice you can’t categorically fix (\mathbb R) unless you add uncountably many non-logical terms.
8. Compactness/LS aren’t the right yardsticks here: (L2K^{-}) drops bound SO quantifiers; consequence behaves more like first-order with predicate parameters.
9. You can express FIN(A) for a given predicate (A) and get well-foundedness for given relations, but you can’t state arbitrary SO-existence claims (no bound SO ∃/∀), nor complements of all SO-definable properties.

If you want, I can pare this down to just the few you’re weighing—or expand any row with sample axioms that achieve the “ℕ categorical”/“ℝ categorical” claims.