一阶逻辑有限域与有效性半可判定性：为何仍需无限解释？

Great question—this gets to a key distinction between local validity (on a specific domain) and global validity (on all domains) in first-order logic (FOL). Let’s unpack this with clear examples to make it concrete.

First, Let’s Clarify Definitions #

• A FOL formula is valid if it is true in every possible interpretation, including interpretations with infinite domains.
• Semi-decidability means we have an algorithm that can prove all valid formulas (by enumerating proofs in a complete system like natural deduction), but we have no algorithm that can definitively say "this formula is invalid"—because invalidity might only show up in an infinite domain we can’t check exhaustively.

Why Finite Domains Aren’t Enough #

The core issue is that finite and infinite domains have fundamentally different structural properties. There exist formulas that:

1. Are true in all finite domains but false in some infinite domain.
2. Are true in all infinite domains but false in all finite domains.

In both cases, checking only finite domains can lead us to the wrong conclusion about global validity. Let’s look at examples of each.

Example 1: True in All Finite Domains, False in Infinite Domains #

Consider this formula, which asserts "there is no injective (one-to-one) function from the domain to itself that isn’t surjective (onto)":

¬∃f (∀x∀y (f(x) = f(y) → x = y) ∧ ∃z ∀x (f(x) ≠ z))

• In any finite domain: A one-to-one function on a finite set must map every element to a unique target, so it has to cover every element (it’s onto). So no such function exists, making the formula true.
• In an infinite domain (e.g., the natural numbers ℕ): Define f(x) = x + 1. This is one-to-one (if x+1 = y+1, then x=y) but not onto (there’s no x where f(x)=0). So the formula is false here.

If we only checked finite domains, we’d incorrectly think this formula is valid—but it’s not, because it fails in infinite domains.

Example 2: True in All Infinite Domains, False in All Finite Domains #

Now consider a formula that asserts "the domain is a totally ordered set with no maximum element":

∀x ∃y (y > x) 
∧ ∀x∀y∀z ((x > y ∧ y > z) → x > z) 
∧ ∀x∀y (x > y ∨ y > x ∨ x = y)

• In any finite domain: A finite totally ordered set always has a maximum element (e.g., the largest number in a finite set of integers). So the first conjunct (∀x ∃y (y > x)) is false, making the whole formula false.
• In an infinite domain (e.g., ℕ with the standard < relation): Every number has a larger number after it, the order is transitive, and every pair is comparable. So the formula is true here.

This formula isn’t globally valid (since it fails in finite domains), but if we only checked infinite domains, we’d get the wrong idea.

Why This Leads to Semi-Decidability #

Global validity requires checking every possible domain—finite and infinite. But infinite domains are infinite in number and size, so we can’t exhaustively check them all.

We can, however, use a complete proof system for FOL to enumerate all valid formulas: every valid formula has a finite proof, so we can generate proofs one by one and verify them. But for invalid formulas, there’s no way to guarantee we’ll ever find a counterexample (it might be in some infinite domain we haven’t checked), so we can’t definitively say "this formula is invalid." Hence, validity is semi-decidable.

内容的提问来源于stack exchange，提问作者Tantaros