Replacing set of tautologies with a single formula

370 Views Asked by At

Here is a question I have about first order logic using the conventions in Enderton:

First-order deductions in our proof system are obtained via 1) being a member of a set of formulas $\Gamma$, 2) being an instance of six axioms, the set of which we call $\Lambda$, enter image description here or 3) obtained via modus ponens from formulas obtained in the previous two ways. Now, consider that the first axiom is that we have an infinite set of first-order tautologies.

(1) Could we have replaced this infinite set of tautologies by a single formula? (2) Could we have replaced this infinite set of tautologies set by a single formula schema? (where we define a schema as being obtained by quantifying over all possible subformulas) i.e., some formula containing generic subformulas.

Here are my thoughts: For question (1), I believe that it is not the case that we can replace all tautologies with a single formula. The obvious candidate is the formula consisting of the conjunction of all tautologies, let's call this formula $\psi$. This formula would be of countable length, but determining whether we are able to write a given formula $\varphi$ in any deduction would no longer involve simply checking whether $\varphi \in \Lambda$. We would now need to check whether $\vdash \{\psi, \varphi\}$ or equivalently $\{\psi, \varphi\}$ is consistent, which presents an equally complicated problem and requires the use of the infinite set of tautologies to determine.

For question (2), the obvious candidate is the schema $\alpha \leftrightarrow (\beta \rightarrow \beta)$ for an atomic formula $\beta$, (which we can easily convert to the limited language provided be Enderton). We are simply providing a formula which checks whether some formula $\alpha$ is tautologically implied by a known tautology. Now, I am not certain whether verification of whether this holds requires the infinite set of tautologies.

I'd greatly appreciate any tips as to whether I'm on the right track.

1

There are 1 best solutions below

11
On BEST ANSWER

(1) Could we have replaced this infinite set of tautologies by a single formula? (2) Could we have replaced this infinite set of tautologies set by a single formula schema?

Yes; there are many equivalent axiomatization of propositional calculus that needs only modus ponens as rule of inference.

A very "classic" one is the three-axioms set used by Mendelson (see e.g. this post).

You can see List of Hilbert systems for many other axiom systems, including the single-axiom systems proposed by Łukasiewicz-Tarski and Meredith (for systems with $\to$ and $\lnot$ as primitive).


Comments: the conjunction of all tautologies is not a well-formed formula of "standard" propositional and first-order logics, where a formula must have finite lenght.

The schema $α ↔ (β → β)$ is not a tautology, and thus it is not allowed as axiom, because it implies the inconsistency of the system.