5
$\begingroup$

Take second order logic, weaken the comprehension axiom schemata to using only FIRST order formulas; that is, $\phi(x_1,..,x_n)$ in the referred article is restricted to be a first order formula. Keep all the other aspects of second order logic.

Now would the resulting system be a kind of a conservative extension of first order logic? That is, a logic that allows quantification over relation and function symbols, yet not having axioms extra to those of first order logic, and so enjoys the merits of first order logic.

Can we always add a first order theory, but write its schemas as SINGLE axioms in that logic? So for example separation schema in Zermelo would be written as a single axiom by quantifying over predicates, as: $$\forall P \forall A \exists X \forall y (y \in X \leftrightarrow y \in A \land P(y))$$

I had asked a similar question on MathStackExchange, and I received no answer?

Improve this question
$\endgroup$
10
  • $\begingroup$ Could you state the list of axioms of your second-order logic? For example, does it contain the axiom of choice $\forall x\exists y R(x,y)\to \exists f \forall x R(x,f(x))$? $\endgroup$
    – Hanul Jeon
    Commented Aug 22, 2020 at 18:09
  • $\begingroup$ @HanulJeon, well I didn't include those choice axioms. The axioms are those of propositional logic and first order logic. however the comprehension axioms of second order logic are weakened as presented above. The language allows quantification over relation and function symbols, all the formation rules of second order logic, distribution, substitution and inference rules are there. No choice axioms. $\endgroup$
    – Zuhair Al-Johar
    Commented Aug 22, 2020 at 20:05
  • 3
    $\begingroup$ Let $\varphi$ be a first-order formula which is proved in your system. Let $M$ be a first-order structure (adapted to the appropriate first-order language). It is enough to show that $M$ satisfies $\varphi$. Add to $M$ all first-order definable relations, obtaining $M^*$. All axioms and rules of your weakened second-order system are valid in $M^*$, so $M^*$ satisfies $\varphi$. Hence $M$ satisfies $\varphi$. $\endgroup$
    – Rodrigo Freire
    Commented Aug 23, 2020 at 14:17
  • 2
    $\begingroup$ I have not understood your last comment, specially the end of it. Your first comment makes reference to axioms and inference rules, therefore I have concluded that you were presenting your second-order logic proof-theoretically. Now you ask if your logic has a proof system. What is your second-order consequence relation? That is not clear. $\endgroup$
    – Rodrigo Freire
    Commented Aug 25, 2020 at 0:40
  • 2
    $\begingroup$ If your system S is an axiomatic Hilbert calculus with the axioms and rules you have mentioned, then my first comment gives a conservativity proof over first-order logic. If it is anything wrong with that proof, if it does not apply to the system S you have in mind, then you should say exactly why it fails. $\endgroup$
    – Rodrigo Freire
    Commented Aug 25, 2020 at 12:39

1 Answer 1

Reset to default
5
$\begingroup$

Preliminary remark: after some clarification in the comments, I am posting my comment as an answer.

Let $\varphi$ be a first-order formula which is proved in your Hilbert style system $S$. Let $M$ be a first-order structure (adapted to the appropriate first-order language). From the completeness of first-order logic, it is enough to show that $M$ satisfies $\varphi$. Add to $M$ all first-order definable relations and functions, obtaining $M^∗$. All axioms and rules of your weakened second-order system $S$ are valid in $M^∗$ (Henkin semantics), so $M^∗$ satisfies $\varphi$ by soundness. Since $M$ is a reduct of $M^*$ and is adapted to the language of $\varphi$, $M$ satisfies $\varphi$.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .