重言式与公理模式探讨：一阶逻辑中为何选用重言式为公理模式？

Great question—this cuts to the heart of how formal proof systems are built, and it’s a common point of confusion when first diving into first-order logic! Let’s break this down clearly:

First, a quick recap: When we say a tautology is "universally true," we mean it holds no matter what interpretation we assign to non-logical symbols (like predicates, constants, or function symbols) in the formula. For example, P ∨ ¬P is true whether P stands for "the sky is blue" or "3 is even."

Now, even though tautologies don’t carry domain-specific "new knowledge," they’re absolutely critical to the design of a sound and usable proof system. Here’s why we include them as axiom schemas:

• They’re the foundational "truth anchors": Formal systems aim to be sound (only prove statements that are actually true) and complete (prove all true statements that can be expressed in the language). Tautologies are the most basic, self-evident truths of propositional logic, which is the foundation of first-order logic. By starting with these as axioms, we ensure every proof we build is rooted in a set of statements that can’t possibly be false.

• They simplify proof construction: Think of tautologies as the "logical building blocks" that let us manipulate formulas validly. Even if they don’t tell us anything new about math or computer science, they let us chain together reasoning steps. For example, if you’ve already proven A and A → B, the tautology (A ∧ (A → B)) → B (a form of modus ponens, though sometimes modus ponens is a separate inference rule) lets you formally derive B. Without these tautologies, you’d have no way to connect intermediate statements in a proof.

• They let us keep the inference rule set small: Many formal systems prioritize having a minimal number of inference rules (often just modus ponens) and use tautology axiom schemas to cover the rest. This makes the system easier to analyze mathematically—instead of juggling a dozen complex rules, you can focus on proving properties about the axiom schemas and how they interact with the few rules you have.

• They bridge propositional and first-order logic: First-order logic extends propositional logic, so we need a way to carry over all the valid propositional truths into the more expressive first-order system. Tautology axiom schemas do exactly this—any propositional tautology, when generalized to first-order formulas, is automatically accepted as a valid starting point.

It’s helpful to think of tautologies like the rules of grammar in a natural language: they don’t convey meaning on their own, but you can’t form coherent, meaningful sentences without them. They’re the structure that lets meaningful reasoning happen.

For a concrete example: The axiom schema φ → (ψ → φ) is a tautology. It might seem trivial at first glance, but it lets us take any formula we’ve already proven (φ) and derive that it follows from any other formula (ψ). This is a basic, essential step in building longer, more complex proofs.

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