I've been wondering, whether or not first order logic can be reduced to the propositional calculus.

Rosser's system RS_1, described by Irving M. Copi in 'Symbolic Logic', has 5 axioms or postulates:

Let P, Q, R be any well formed formulas, or wffs

P 1. P → (P ∧ P)

P 2. (P ∧ Q) → P

P 3. (P → Q) → [¬(Q ∧ R) → ¬ (R ∧ P)]

P 4. ∀ x[P → Φ] → (P → ∀ x[Φ] ), where x is any individual variable, and Φ is either a Wff or a propositional function of x.

P 5. ∀ x [Φ] → Φ(x_n), where x_n is any specific individual constant, and Φ(x_n) is the result of replacing all free occurrences of x in Φ by x_n. (In the event there are no free occurrences of x in Φ, Φ(x_n) = Φ)

Note: If x_n is any specific individual constant then

x1=x_n ∧ x2=x_n ∧ x3=x_n ∧...

in which case x_n is an arbitrary constant, that is a general constant.

In Rosser's System RS for the propositional calculus, you need only the first three postulates, and one underived rule of inference, namely Modus Ponens.

You prove the rule of replacement as a Metatheorem, and the rule of replacement allows you to replace a a Wff that is part of a larger Wff by any Wff that is materially equivalent to the part being replaced. Thus, you don't need the equality symbol or Hao Wang's axiom of identity to prove any theorem of the propositional calculus. Copi goes to the trouble to prove the propositional calculus is analytic and complete. Analytic means only tautologies are theorems, and complete means all tautologies besides the axioms, are theorems.

In RS_1, for FOL, you need two underived rules of inference:

R1: P, P → Q; therefore Q

R2: Φ(α); therefore ∀x[Φ].

Here α is an arbitrary individual constant that is not a specific individual constant that occurs at all places x occurs free in Φ. If Φ is a Wff then Φ(α) = Φ.

Now I think the reduction is possible through the use of the following definition.

∀x [Φ] = Φ(x1) ∧ Φ(x2) ∧ Φ(x3) ∧...

Where it is understood that every individual has at least one name.

We postulate an unlimited number of individual constants.

x1, x2, x3,...

Now in order to get my idea to work I need the equality symbol '=', and the following substitution principle.

Substitution Principle

x_n = α, Φ(α); therefore Φ(x_n)

Here x_n is any specific individual constant, and α is any arbitrary individual constant.


C is a specific constant iff ∃! x[x=C]

C is an arbitrary constant iff ∀x[x=C] ∨ ∃! x [x=C]

C is a general constant iff ∀x [x=C] ∧ ¬ ∃! x [x=C]

I will derive R2, and leave it an open question as to whether or not you can prove Rosser's postulates 4, and 5.

Derived Rule R2: Φ(α); therefore ∀x[Φ]

  1. Φ(α)
  2. ∀x [x = α] ∧ ¬∃! x [x = α]
  3. ∀x [x = α] [2; simp 1]
  4. x1=α ∧ x2=α ∧ x3=α ∧... [3; Df]
  5. Φ(x1) ∧ Φ(x2) ∧ Φ(x3) ∧... [1,4; substitution]
  6. ∀x [Φ] [5; Df]

Thus R2 is a derived Rule of inference in this system.

I have proved postulates 4 and 5 of RS_1. What I'm really looking for is any problems to be found with this approach to FOL.

If it's ok, then the completeness of FOL follows from the completeness of the propositional calculus. But I'm not sure if it's ok, hence my question.

  • Propositional Sentences need to be finite. How are you expressing ∀x [Φ] = Φ(x1) ∧ Φ(x2) ∧ Φ(x3) ∧..., in the event that there are infinitely many variables/constants in the language? Commented May 19 at 22:30
  • Gödel sentence is an example where the infinite conjunction is provable but the corresponding universally quantified sentence is not, hence the incompleteness. Your 'definition' makes a non-conservative extension of FOL.
    – Conifold
    Commented May 19 at 23:04
  • @Michael, the idea is that conjunctions don't have to be finite. That's in the definition of a universally quantified propositional function. In the language, there are no variables, but there are an unlimited number of individual constants. The infinite conjunction P(x1)&P(x2)&P(x3)... Has property P assigned to every individual that exists because each individual has at least one name.
    – lee pappas
    Commented May 19 at 23:44
  • @conifold, what do you mean by my 'definition' makes a non conservative extension of FOL. I've never heard of that. Copi proves the completeness of RS_1. So I fail to see how the Goedel sentence leads to incompleteness of FOL.
    – lee pappas
    Commented May 20 at 0:04
  • A similar idea was sketched by Wittgentein into the Tractatus (1922); see e.g. Gregory Landini, On the Curious Calculi of Wittgenstein and Spencer Brown (2018). But there is no reason that it easier to understand "the dots" instead of "all". And see Kai Wehmeier, Wittgeisteinian Predicate Logic (2004). Commented May 20 at 5:40


You must log in to answer this question.

Browse other questions tagged .