Profile photo for Hunan Rostomyan

Note 1. If it's not explicitly stated, you should assume that it's the least expressive logic required to validate the proof. The three types of logics you mentioned are such that FOL extends PL, and HOL extends FOL. This means that: (i) any theorem of PL is a theorem of FOL, and that (ii) any theorem of FOL is a theorem of HOL. From these follows that: a proof that can be validated in PL can also be validated in logics extending PL (e.g. first- and high-order logics). This is why we want the least expressive logic.

Example a. "p or ~p" is a theorem of PL, but also a theorem of FOL. Since PL is less expressive than FOL, the background logic here is: PL.

Example b. "[math]\forall x (x = x)[/math]" is a theorem of FOL (with identity) and higher-order logics. FOL is the least expressive, so the background logic here is: FOL.

Example c. "[math]\forall x ([\lambda x. x](x) = x)[/math]" is a theorem of HOL. The background logic here is the least expressive HOL required to prove it: some sort of a simple type theory (e.g. combinatory logic, lambda calculus); one that will allow us to eliminate the lambda term from the theorem.

Note 2. Here's a general algorithm for figuring what the background logic of a proof is: (i) figure out the logical constants used in the proof (such as 'or' and 'not' in Example a; '[math]\forall[/math]' and '=' in Example b; and '[math]\lambda[/math]', '[math]\forall[/math]', and '=' in Example c), and (ii) find the least expressive logic that defines that logical vocabulary.

Note 3. It's not true that "FOL statements do not talk about themselves or other FOL statements". First, being mere sequences of symbols, sentences of any logic can be arithmetized (assigned unique numbers). Secondly, descriptive predicates can be defined for an FOL, allowing its sentences to directly "talk about" themselves.

For example, a sentence on line 17 of a paper can say something like: the sentence on line 17 of this paper contains the '=' symbol. Using Godel's method of arithmetization we can even avoid having descriptive predicates by assigning numbers to sentences and having numerical predications inside sentences which in an indirect way can be said to be about the sentences themselves (provided that the numbers being predicated are the Godel numbers of those sentences).

Apologies for the length. I'll try to shorten the answer when I get a chance.

View 2 other answers to this question
About · Careers · Privacy · Terms · Contact · Languages · Your Ad Choices · Press ·
© Quora, Inc. 2025